Symbolic Model Construction for Saturated Constrained Horn Clauses

TL;DR

This paper introduces a method for constructing effective symbolic models for saturated constrained Horn clauses with linear arithmetic constraints, enabling finite-time model construction and evaluation.

Contribution

It presents the first effective symbolic model construction for saturated constrained Horn clauses with linear arithmetic and function-free first-order parts.

Findings

Model construction is finite and efficient.

Non-ground clauses can be effectively evaluated.

Constructed models are the least models.

Abstract

Clause sets saturated by hierarchic ordered resolution do not offer a model representation that can be effectively queried, in general. They only offer the guarantee of the existence of a model. We present an effective symbolic 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 is constructed in finite time, and non-ground clauses can be effectively evaluated with respect to the model. Furthermore, we prove that our model construction produces the least model.