Explicit Model Construction for Saturated Constrained Horn Clauses

05/08/2023

∙

by   Martin Bromberger, et al.

∙

0

∙

share

Clause sets saturated by hierarchic superposition do not offer an explicit model representation, rather the guarantee that all non-redundant inferences have been performed without deriving a contradiction. We present an approach to explicit model construction for saturated constrained Horn clauses. Constraints are in linear arithmetic, the first-order part is restricted to a function-free language. The model construction is effective and clauses can be evaluated with respect to the model. Furthermore, we prove that our model construction produces the least model.