# Symbolic Model Construction for Saturated Constrained Horn Clauses

Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach

► To cite this version:

Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach. Symbolic Model Construction for Saturated Constrained Horn Clauses. Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2023. [hal-04315210](https://hal-04315210)

HAL Id: hal-04315210

https://inria.hal.science/hal-04315210v1

Submitted on 30 Nov 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Symbolic Model Construction for Saturated
Constrained Horn Clauses

Martin Bromberger¹, Lorenz Leutgeb¹,², and Christoph
Weidenbach¹

¹Max Planck Institute for Informatics,
Saarland Informatics Campus, Saarbrücken, Germany,
{mbromber,lorenz,weidenb}@mpi-inf.mpg.de

²Graduate School of Computer Science,
Saarland Informatics Campus, Saarbrücken, Germany

2023-07-18

## 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.

# 1 Introduction

Constrained Horn Clauses (CHCs) combine logical formulas with constraints over various domains, e.g. linear real arithmetic, linear integer arithmetic, equalities of uninterpreted functions [15]. This formalism has gained widespread attention in recent years due to its applications in a variety of fields, including program analysis and verification: safety, liveness, and termination [38, 17], complexity and resource analysis [33], intermediate representation [22], and software testing [35]. Technical controls, so called *Supervisors*, like an electronic engine control unit, or a lane change assistant in a car [9, 8] can be modelled, run, and proven safe. Moreover, there exist many different approaches for reasoning in CHCs and associated first-order logic fragments extended with theories [15, 7, 24, 25, 34, 28, 2, 23, 29, 37, 5, 10]. Thus, CHCs are a powerful tool for reasoning about complex systems that involve logical constraints, and they have been used to solve a wide range of problems.

A failed proof attempt of some conjecture or undesired run points to a bug. In this case investigation of the cause of the unexpected result or behavior is
crucial. Building a model of the situation that can then be effectively queried is an important means towards a repair. However, some algorithms for CHCs, e.g. hierarchic superposition, which boils down to hierarchic ordered resolution in the context of CHCs, do not return a model that can be effectively queried if a proof attempt fails, in general. If so, queries are still restricted to ground clauses [4].

The contribution of our paper can be seen as an extension for these saturation based algorithms that produces models and not just saturated clause sets. In fact, we show how to build symbolic models out of any saturated CHC clause set over linear arithmetic. This fragment is equivalent to Horn clause sets of linear arithmetic combined with the Bernays-Schönfinkel fragment. Recall that although satisfiability in this fragment is undecidable [16, 26], in general, for a finitely saturated set we can construct such a representation in finite time.

Our models fulfill all important properties postulated in the literature for automated model building in first-order logic [20, 13]. First, they can be *effectively constructed*, i.e., each model is represented by one linear arithmetic formula of finite size for each of its predicates and it can be constructed in finite time. Second, they are *unique*, i.e., the model representation specifies exactly one interpretation; in our case the least model. Third, they can be *effectively queried*, i.e., we provide decision procedures that evaluate whether an atom, clause, or formula is entailed/satisfied by the model. Fourth, it is possible to *test* the *equivalence* of two models. The approach we present does not exploit features of linear arithmetic beyond equality, the existence of a well-founded order for the theories' universe, and decidability of the theory. The results may therefore be adapted to other constraint domains. Model representation that can be effectively constructed and queried like ours are also called *effective model representations*. Moreover, our method is the first effective model construction approach for ordered resolution (or its extension to superposition) that is based on saturation, goes beyond ground clauses, and includes theory constraints. In the future, we plan to use this approach as the basis for a more general model construction approach that also works on more expressive fragments of first-order logic modulo theories.

Our model construction is inspired by the model construction operator used in the proof for refutational completeness of hierarchic superposition [30, 6, 3]. The main difference is that the model construction operator from the refutational completeness proof is restricted to ground clauses and executed on the potentially infinite ground instances of the saturated clause set (in addition to an infinite axiomatization of the background theory as ground clauses). As a result, the model construction operator from the refutational completeness proof cannot effectively construct a model because iterating over a potentially infinite set means it may diverge. Moreover, in contrast to our model construction, the original model operator cannot effectively evaluate non-ground atoms, clauses, or formulas. It is, however, sufficient, to show the existence of a model if the clause set is saturated and does not contain the empty clause [30, 6, 3]. In our version of the model construction operator, we managed to lift the restriction to ground clause sets by restricting the input logic to the Horn Bernays-Schönfinkel fragment instead of full first-order logic. This enables us to define a strict propagation/production order for our non-ground clauses instead of just for ground clauses. As a result, we can construct the model one clause at a time.

The paper is organized as follows. In Section 2 we clarify notation and
preliminaries. The main contribution is presented in Section 3. At the end of this section, we also explain how our models satisfy the postulates (see [13, Section 5.1, p. 234]) by Fermüller and Leitsch for automated model building. We conclude in Section 4.

## 2 Preliminaries and Notation

We briefly recall the basic logical formalisms and notations we build upon [9]. Our starting point is a standard first-order language with *variables* (denoted $x, y, z$), *predicates* (denoted $P, Q$) of some fixed *arity*, and *terms* (denoted $t, s$). An *atom* (denoted $A$) is an expression $P(t_1, \dots, t_n)$ for a predicate $P$ of *arity* $n = \text{arity}(P)$. When the terms $t_1, \dots, t_n$ in $P(t_1, \dots, t_n)$ are not relevant in some context, we also write $P(*)$. A *positive literal* is an atom $A$ and a *negative literal* is a negated atom $\neg A$. We define $\text{comp}(A) = \neg A$, $\text{comp}(\neg A) = A$, $|A| = A$ and $|\neg A| = A$. Literals are usually denoted $L, K$. We sometimes write literals as $[\neg]P(*)$, meaning that the sign of the literal is arbitrary, often followed by a case distinction. Formulas are defined in the usual way using quantifiers $\forall, \exists$ and the boolean connectives (in order of decreasing binding strength) $\neg, \forall, \wedge, \rightarrow$, and $\leftrightarrow$. The logic we consider does not feature a first-order equality predicate.

A *clause* (denoted $C, D$) is a universally closed disjunction of literals $A_1 \lor \dots \lor A_n \lor \neg B_1 \lor \dots \lor \neg B_m$. We may equivalently write $B_1 \land \dots \land B_m \rightarrow A_1 \lor \dots \lor A_n$. A clause is *Horn* if it contains at most one positive literal, i.e. $n \le 1$. In Section 3, all clauses considered are Horn clauses. If $Y$ is a term, formula, or a set thereof, $\text{vars}(Y)$ denotes the set of all variables in $Y$, and $Y$ is *ground* if $\text{vars}(Y) = \emptyset$. Analogously, $\Pi(Y)$ is the set of predicate symbols occurring in $Y$.

The *Bernays-Schönfinkel Clause Fragment* (BS) in first-order logic consists of first-order clauses where all terms are either variables or constants. The *Horn Bernays-Schönfinkel Clause Fragment* (HBS) is further restricted to Horn clauses.

A *substitution* $\sigma$ is a function from variables to terms with a finite domain and codomain. We denote substitutions by $\sigma, \tau$. The application of substitutions is often written postfix, as in $x\sigma$, and is homomorphically extended to terms, atoms, literals, clauses, and quantifier-free formulas. A substitution is *ground* if its codomain is ground. Let $Y$ denote some term, literal, clause, or clause set. A substitution $\sigma$ is a *grounding* for $Y$ if $Y\sigma$ is ground, and $Y\sigma$ is a *ground instance* of $Y$ in this case. We denote by $\text{gnd}(Y)$ the set of all ground instances of $Y$. The *most general unifier* $\text{mgu}(Z_1, Z_2)$ of two terms/atoms/literals $Z_1$ and $Z_2$ is defined as usual, and we assume that it does not introduce fresh variables and is idempotent.

### 2.1 Horn Bernays-Schönfinkel with Linear Arithmetic

The class HBS(LRA) is the extension of the Horn Bernays-Schönfinkel fragment with linear real arithmetic (LRA). Analogously, the classes HBS(LQA) and HBS(LIA) are the extensions of the Horn Bernays-Schönfinkel fragment with linear rational arithmetic (LQA) and linear integer arithmetic (LIA), respectively. The only difference between the three classes are the sort LA their variables and terms range over and the universe $\mathcal{U}$ over which their interpretations range. As the names already imply LA = LRA and $\mathcal{U} = \mathbb{R}$ for HBS(LRA),
LA = LQA and $\mathcal{U} = \mathbb{Q}$ for HBS(LQA), and LA = LIA and $\mathcal{U} = \mathbb{Z}$ for HBS(LIA). The results presented in this paper hold for all three classes and by HBS(LA) we denote that we are talking about an arbitrary one of them.

Linear arithmetic terms are constructed from a set $\mathcal{X}$ of variables, the set of constants $c \in \mathbb{Q}$ (if in HBS(LRA) or HBS(LQA)) or $c \in \mathbb{Z}$ (if in HBS(LIA)), and binary function symbols $+$ and $-$ (written infix). Additionally, we allow multiplication $\cdot$ if one of the factors is a constant. Multiplication only serves us as syntactic sugar to abbreviate other arithmetic terms, e.g., $x+x+x$ is abbreviated to $3 \cdot x$. Atoms in HBS(LA) are either first-order atoms (e.g., $P(13, x)$) or (linear) arithmetic atoms (e.g., $x < 42$). Arithmetic atoms are denoted by $\lambda$ and may use the predicates $\leq, <, \approx, \not\approx, >, \geq$, which are written infix and have the expected fixed interpretation. We use $\approx$ instead of $=$ to avoid confusion between equality in LA and equality on the meta level. While we do not permit quantifiers in the syntax of clauses, the notion of symbolic interpretations that we will develop does require this, denoted as usual. By atoms($Y$)/quants($Y$) we denote the linear arithmetic atoms/quantifiers in a formula or set of formulas $Y$. First-order literals and related notation is defined as before. Arithmetic literals coincide with arithmetic atoms, since the arithmetic predicates are closed under negation, e.g., $\neg(x \geq 42)$ is equivalent to $x < 42$.

HBS(LA) clauses are defined as for HBS but using HBS(LA) atoms. We often write clauses in the form $\Lambda \parallel C$ where $C$ is a clause solely built of free first-order literals and $\Lambda$ is a multiset of LA atoms called the constraint of the clause. A clause of the form $\Lambda \parallel C$ is therefore also called a constrained clause. Since the interpretation of linear arithmetic relations is fixed, we set $\Pi(\Lambda \parallel C) := \Pi(C)$.

The fragment we consider in Section 3 is restricted even further to abstracted clauses: For any clause $\Lambda \parallel C$, all terms in $C$ must be variables. Put differently, we disallow any arithmetic function symbols, including numerical constants, in $C$. Variable abstraction, e.g. rewriting $x \geq 3 \parallel P(x, 1)$ to $x \geq 3, y \approx 1 \parallel P(x, y)$, is always possible. Hence, the restriction to abstracted clauses is not a theoretical limitation, but allows us to formulate our model construction operator in a more concise way. We assume abstracted clauses for theory development, but we prefer non-abstracted clauses in examples for readability, e.g., a unit clause $P(3, 5)$ is considered in the development of the theory as the clause $x \approx 3, y \approx 5 \parallel P(x, y)$.

In contrast to other works, e.g. [11], we do not permit first-order constants, and consequently also no variables that range over the induced Herbrand universe. All variables are arithmetic in the sense that they are interpreted by $\mathcal{U}$. Since we only allow equalities in the arithmetic constraint, it is possible to simulate variables over first-order constants, by e.g. numbering them, i.e. defining a bijection between $\mathbb{N}$ and constant symbols. So this again not a theoretical limitation.

The semantics of $\Lambda \parallel C$ is as follows:

$$ \Lambda \parallel C \quad \text{iff} \quad (\bigwedge_{\lambda \in \Lambda} \lambda) \to C \quad \text{iff} \quad (\bigvee_{\lambda \in \Lambda} \neg \lambda) \lor C $$

For example, the clause $x > 1 \lor y \not\approx 5 \lor \neg Q(x) \lor R(x, y)$ is also written $x \leq 1, y \approx 5 \parallel \neg Q(x) \lor R(x, y)$. The negation $\neg(\Lambda \parallel C)$ of a constrained clause $\Lambda \parallel C$ where $C = A_1 \lor \dots \lor A_n \lor \neg B_1 \lor \dots \lor \neg B_m$ is thus equivalent to $(\bigwedge_{\lambda \in \Lambda} \lambda) \land \neg A_1 \land \dots \land \neg A_n \land B_1 \land \dots \land B_m$. Note that since the neutral element of conjunction is $\top$, an empty constraint is thus valid, i.e. equivalent to true. In analogy to the
empty clause in settings without constraints, we write □ to mean any and all clauses $Λ || ⊥$ where $Λ$ is satisfiable, which are all unsatisfiable.

An assignment for a constraint $Λ$ is a substitution (denoted $β$) that maps all variables in vars($Λ$) to values in $U$. An assignment is a solution for a constraint $Λ$ if all atoms $λ ∈ (Λβ)$ evaluate to true. A constraint $Λ$ is satisfiable if there exists a solution for $Λ$. Otherwise it is unsatisfiable.

We assume pure input clause sets because otherwise satisfiability is undecidable for impure HBS(LA) [21]. This means the only constants of our sort LA are concrete rational numbers. Irrational numbers are not allowed by the standard definition of the theory. Fractions are not allowed if LA = LIA. Satisfiability of pure HBS(LA) clause sets is semi-decidable, e.g., using hierarchic superposition [3] or SCL($T$) [10]. Note that pure HBS(LA) clauses correspond to constrained Horn clauses (CHCs) with LA as background theory.

All arithmetic predicates and functions are interpreted in the usual way denoted by the interpretation $A^{LA}$. An interpretation of HBS(LA) coincides with $A^{LA}$ on arithmetic predicates and functions, and freely interprets non-arithmetic predicates. For pure clause sets this is well-defined [3]. Logical satisfaction and entailment is defined as usual, and uses similar notation as for HBS.

**Example 1.** The clause $y ≥ 5$, $x' ≈ x + 1 || S_0(x, y) → S_1(x', 0)$ is part of a timed automaton with two clocks $x$ and $y$ modeled in HBS(LA). It represents a transition from state $S_0$ to state $S_1$ that can be traversed only if clock $y$ is at least 5 and that resets $y$ to 0 and increases $x$ by 1.

## 2.2 Ordering Literals and Clauses

In order to define redundancy for constrained clauses, we need an order: Let $<_Π$ be a total, well-founded, strict ordering on predicate symbols and let $<_U$ be a total, well-founded, strict ordering on the universe $U$. (Note that $<$ cannot be the standard ordering $<$ because it is not well-founded for $Z$, $Q$, or $R$. In the case of $R$, the existence of such an order is even dependent on whether we assume the axiom of choice [18].) We extend these orders step by step. First, to atoms, i.e., $P(\vec{a}) <_Q Q(\vec{b})$ if $P <_Π Q$ or $P = Q$, $\vec{a}, \vec{b} ∈ U^{||\vec{a}|}$, and $\vec{a} <_{lex} \vec{b}$, where $<_{lex}$ is the lexicographic extension of $<_U$. Next, we extend the order to literals with a strict precedence on the predicate and the polarity, i.e.,

$$P(\vec{t}) <_Q P(\vec{s}) <_Q Q(\vec{u}) \quad \text{if } P <_Q Q$$

independent of the arguments of the literals. Then, take the multiset extension to order clauses. To handle constrained clauses extend the relation such that constraint literals (in our case arithmetic literals) are always smaller than first-order literals. We conflate the notation of all extensions into the symbol $<$ and define $\leq$ as the reflexive closure of $<$. Note that $<$ is only total for ground atoms/literals/clauses, which is sufficient for a hierarchic superposition order [6].

**Definition 2** ($<_{-maximal}$ Literal). A literal $L$ is called $<_{-maximal}$ in a clause $C$ if there exists a grounding substitution $σ$ for $C$, such that there is no different $L' ∈ C$ for which $Lσ <_L L'σ$. The literal $L$ is called strictly $<_{-maximal}$ if there is no different $L' ∈ C$ for which $Lσ \leq L'σ$.
**Proposition 3.** If $\prec$ is a predicate-based ordering, $C$ is a Horn clause, $C$ has a positive literal $L$, and $L$ is $\prec$-maximal in $C$, then $L$ is strictly $\prec$-maximal in $C$.

**Definition 4** ($\prec$-maximal Predicate in Clause). A predicate symbol $P$ is called (strictly) $\prec$-maximal in a clause $C$ if there is a literal $[\neg]P(*) \in C$ that is (strictly) $\prec$-maximal in $C$.

**Definition 5.** Let $N$ be a set of clauses, $\prec$ a clause ordering, $C$ a clause, and $P$ a predicate symbol. Then $N^{\prec C} := \{C' \in N \mid C' \prec C\}$ and $N^{\succeq P} := \{C \in N \mid Q$ is $\prec$-maximal in $C$ and $Q \succeq P\}$.

## 2.3 Hierarchic Superposition, Redundancy and Saturation

For pure HBS(LA) most rules of the (hierarchic) superposition calculus become obsolete or can be simplified. In fact, in the HBS(LA) case (hierarchic) superposition boils down to (hierarchic) ordered resolution. For a full definition of (hierarchic) superposition calculus in the context of linear arithmetic, consider $SUP(LA)[1]$. Here, we will only define its simplified version in the form of the hierarchic resolution rule.

**Definition 6** (Hierarchic $\prec$-Resolution). Let $\prec$ be an order on literals and $\Lambda_1 \parallel L_1 \lor C_1$, $\Lambda_2 \parallel L_2 \lor C_2$ be constrained clauses. The inference rule of hierarchic $\prec$-resolution is:

$$ \frac{\Lambda_1 \parallel L_1 \lor C_1 \qquad \Lambda_2 \parallel L_2 \lor C_2 \qquad \sigma = \text{mgu}(L_1, \text{comp}(L_2)) \\ (\Lambda_1, \Lambda_2 \parallel C_1 \lor C_2)\sigma}{\Lambda_1 \parallel L_1 \lor C_1} $$

where $L_1$ is $\prec$-maximal in $C_1$ and $L_2$ is $\prec$-maximal in $C_2$.

Note that in the resolution rule we do not enforce explicitly that the positive literal is strictly maximal. This is possible because in the Horn case any positive literal is strictly maximal if it is maximal in the clause.

For saturation, we need a termination condition that defines when the calculus under consideration cannot make any further progress. In the case of superposition, this notion is that any new inferences are redundant.

**Definition 7** (Clause Redundancy). A ground clause $\Lambda \parallel C \in N$ is redundant with respect to a set $N$ of ground clauses and order $\prec$ if $N^{\prec \Lambda} \parallel C \models \Lambda \parallel C$. A potentially non-ground clause $\Lambda \parallel C \in N$ is redundant with respect to a potentially non-ground clause set $N$ and order $\prec$ if for all $\Lambda' \parallel C' \in \text{gnd}(\Lambda \parallel C)$ the clause $\Lambda' \parallel C'$ is redundant with respect to $\text{gnd}(N)$.

If a clause $\Lambda \parallel C \in N$ is redundant with respect to a clause set $N$, then it can be removed from $N$ without changing its semantics. If $\Lambda \parallel C$ is newly inferred, then we also call it redundant if $\Lambda \parallel C$ is already part of $N$. The same cannot be said for clauses in $N$ or all clauses in $N$ would be redundant. Determining clause redundancy is an undecidable problem [10, 40]. However, there are special cases of redundant clauses that can be easily checked, e.g., tautologies and subsumed clauses. Redundancy also means that $\mathcal{I} \models N^{\prec \Lambda} \parallel C$ implies $\mathcal{I} \models \Lambda \parallel C$ if $\Lambda \parallel C$ is redundant w.r.t. $N$. We will exploit this fact in the model construction.

**Definition 8** (Saturation). A set of clauses $N$ is saturated up to redundancy with respect to some set of inference rules, if application of any rules to clauses in $N$ yields a clause that is redundant with respect to $N$ or is contained in $N$.
## 2.4 Interpretations

In our context, models are interpretations that satisfy (sets of) clauses. The standard notion of an interpretation is fairly opaque and interprets a predicate $P$ as the potentially infinite set of ground arguments that satisfy $P$.

**Definition 9 (Interpretation).** Let $P$ be a predicate symbol with arity($P$) = $n$. Then, $P^I$ denotes the subset of $U^n$ for which the interpretation $I$ maps the predicate symbol $P$ to true.

Since our model construction approach manipulates interpretations directly, we need a notion of interpretations that always has a finite representation and for which it is possible to decide (in finite time) whether a clause is satisfied by the interpretation. Therefore, we rely on the notion of symbolic interpretations:

**Definition 10 (Symbolic Interpretation).** Let $x_1, x_2, \dots$ be an infinite sequence of distinct variables, i.e. $x_i \neq x_j$ for all $1 \le i < j$. (We assume the same sequence for all symbolic interpretations in order to prevent conflicts when we later combine multiple symbolic interpretations into one.) A symbolic interpretation $S$ is a function that maps every predicate symbol $P$ with $\text{arity}(P) = n$ to a formula denoted $P^S(\vec{x})$ of finite size, constructed using the usual boolean connectives over LA atoms, where the only free variables appear in $\vec{x} = (x_1, \dots, x_n)$. The interpretation $I_S$ corresponding to $S$ is defined by $P^{Is} = \{(\vec{x})\beta \mid \beta \vdash P^S(\vec{x})\}$ and maps the predicate symbol $P$ to true for the subset of $U^n$ which corresponds to the solutions of $P^S(\vec{x})$.

**Example 11.** Let $N$ be a clause set consisting of the clauses $0 \le x \le 2, 0 \le y \le 2 \parallel P(x, y)$ and $x_Q \ge x_P + 1, y_Q \ge y_P + 1 \parallel \neg P(x_P, y_P) \lor Q(x_Q, y_Q)$. An example of a symbolic interpretation $S$ that satisfies $N$, would be the function that maps $P$ to $P^S(x_1, x_2) = 0 \le x_1 \le 2 \land 0 \le x_2 \le 2$ and $Q^S(x_1, x_2) = 1 \le x_1 \le 1 \le x_2$. It corresponds to the interpretation $I_S$ where $P^{Is} = \{(a_1, a_2) \in U \mid 0 \le a_1 \le 2 \land 0 \le a_2 \le 2\}$ and $Q^{Is} = \{(a_1, a_2) \in U \mid 1 \le a_1 \le 1 \le a_2\}$.

The notion of symbolic interpretations is closely related to *A-definable models* [7, Definition 7] and *constrained atomic representations* [13, Definition 5.1, pp. 236-237]. Each symbolic interpretation $S(\vec{x})$ is equivalent to a constrained atomic representation that consists of one constraint atom $[[P(\vec{x}) : P^S(\vec{x})]]$ (written in the notation from [13]) for every predicate $P$. Note that in this context the constraint is not just a quantifier-free conjunction of linear arithmetic atoms, but a linear arithmetic formula potentially containing quantifiers (although those can be eliminated with quantifier elimination techniques).

Due to the fact that each symbolic interpretation consists of a finite set of formulas of finite size, symbolic interpretations can be considered as finite representations. In contrast, the standard representation of an interpretation as a potentially infinite set of ground atoms is not a finite representation. However, this also means that there are some interpretations for which no corresponding symbolic interpretation exists, for instance the set of prime numbers is a satisfying interpretation for $y \approx 2 \parallel P(y)$, but not expressible as a symbolic interpretation (in LA). As we will later see, at least any saturated set of HBS(LA) clauses either is unsatisfiable or has a symbolic interpretation that satisfies it (Theorem 29).
The top interpretation, denoted $\mathcal{I}_{\top}$, is defined as $P^{\mathcal{I}_{\top}} := \mathcal{U}^n$ for all predicate symbols $P$ with arity($P$) = $n$ and corresponds to the top symbolic interpretation, denoted $\mathcal{S}_{\top}$, defined as $P^{\mathcal{S}_{\top}} := \top$ for all predicate symbols $P$. The bottom interpretation (or empty interpretation), denoted $\mathcal{I}_{\bot}$, and the bottom symbolic interpretation (or empty symbolic interpretation), denoted $\mathcal{S}_{\bot}$, are defined analogously. The interpretation of $P$ under $\mathcal{I} \cup \mathcal{J}$ is defined as $P^{\mathcal{I} \cup \mathcal{J}} := P^{\mathcal{I}} \cup P^{\mathcal{J}}$ for every predicate $P$. In the symbolic case, $\mathcal{S} \cup \mathcal{R}$ is defined as $P^{\mathcal{S} \cup \mathcal{R}}(\vec{x}) := P^{\mathcal{S}}(\vec{x}) \lor P^{\mathcal{R}}(\vec{x})$ for every predicate $P$. We write $\mathcal{I} \subseteq \mathcal{J}$ or $\mathcal{I}$ is included in $\mathcal{J}$ (resp. $\mathcal{I} \subset \mathcal{J}$ or $\mathcal{I}$ is strictly included in $\mathcal{J}$) if $P^{\mathcal{I}} \subseteq P^{\mathcal{J}}$ (resp. $P^{\mathcal{I}} \subset P^{\mathcal{J}}$) for all predicate symbols $P$.

**Definition 12** (Entailment of Literal). Let $\mathcal{I}$ be an interpretation. Given a ground literal $P(a_1, \dots, a_n)$, where $a_i \in \mathcal{U}$, we write $\mathcal{I} \models P(a_1, \dots, a_n)$ if $(a_1, \dots, a_n) \in P^{\mathcal{I}}$. Conversely, we write $\mathcal{I} \not\models P(a_1, \dots, a_n)$ if $(a_1, \dots, a_n) \not\in P^{\mathcal{I}}$. For a non-ground literal $L$, we write $\mathcal{I} \models L$ if for all grounding substitutions $\sigma$ for $L$, we have $\mathcal{I} \models L\sigma$. Conversely, we write $\mathcal{I} \not\models L$, if there exists a grounding substitution $\sigma$ for $L$, such that $\mathcal{I} \not\models L\sigma$.

We overload $\models$ for symbolic interpretations, i.e. we write $\mathcal{S} \models L$ and mean $\mathcal{I}_{\mathcal{S}} \models L$. The following function encodes a clause as an LA formula for evaluation under a given symbolic interpretation.

**Definition 13** (Clause Evaluation Function). Let $\Lambda \parallel C$ be a constrained clause where $C = L_1 \lor \dots \lor L_m$, $L_i = [-]P_i(y_{i,1}, \dots, y_{i,n_i})$ and let $\mathcal{S}$ be a symbolic interpretation. Then the clause evaluation function $(\Lambda \parallel C)^{\mathcal{S}}$ is defined as follows based on the definitions for $\sigma_i$ and $\phi_i$ (for $1 \le i \le m$):

$$ \sigma_i := \{x_j \mapsto y_{i,j} \mid 1 \le j \le n_i\} \qquad \phi_i := \begin{cases} P_i^{\mathcal{S}} & L_i \text{ is positive} \\ \neg P_i^{\mathcal{S}} & L_i \text{ is negative (otherwise)} \end{cases} $$

$$ (\Lambda \parallel C)^{\mathcal{S}} := (\bigwedge_{\lambda \in \Lambda} \lambda) \rightarrow (\bigvee_{i=1}^{m} \phi_i \sigma_i) $$

Note that the free variables of $(\Lambda \parallel C)^{\mathcal{S}}$ are exactly the free variables of $(\Lambda \parallel C)$. Moreover, the substitutions $\sigma_i$ are necessary in the above definition in order to map the variables in the symbolic interpretation for the predicates $P_i^{\mathcal{S}}$ to the variables that appear as arguments in the literals $P_i(y_{1,1}, \dots, y_{1,n_i})$.

**Proposition 14.** Given a constrained clause $\Lambda \parallel C$ with grounding $\beta$, we have

$$ \models (\Lambda \parallel C)^{\mathcal{S}} \beta \quad \text{if and only if} \quad \mathcal{S} \models (\Lambda \parallel C)\beta $$

As a corollary of the previous proposition, the entailment $\mathcal{S} \models \Lambda \parallel C$ holds if and only if the universal closure of the formula $(\Lambda \parallel C)^{\mathcal{S}}$ is valid. This means that for a symbolic interpretation $\mathcal{S}$ it is always computable whether a clause is entailed by $\mathcal{S}$ because there are decision procedures for quantified LRA, LQA, and LIA formulas of finite size.

We require two functions that manipulate LA-formulas directly to express our model construction (cf. Definition 17), i.e. to map solutions for a clause defined by a formula vars($\phi$) to one atom inside the clause. This requires from us to project away all variables in $\phi$ that appear in the clause but not in the atom.
**Definition 15 (Projection).** Let $V$ be a set of variables and $\phi$ be an LA-formula. The projection function $\pi$ is defined as follows:

$$ \pi(V, \phi) := \exists x_1 \dots \exists x_n \phi \quad \text{where } \{x_1, \dots, x_n\} = \text{vars}(\phi) \setminus V $$

$\pi(V, \phi)$ is a standard projection function that binds a subset $V$ of the variables in the formula $\phi$ with existential quantifiers. Note that we also know that $\pi(V, \phi)$ is equivalent to a quantifier-free LA formula just over the variables $x_1, \dots, x_n$ because there exist quantifier elimination algorithms for LRA, LQA, and LIA [32, 14].

A further function $\Upsilon$ is needed when we encounter literals of the form $P(x, x, \dots)$, i.e., where one variable is shared among two arguments. In this case, we use $\Upsilon$ to express in our symbolic interpretation that the equivalent argument positions must also be equivalent in our interpretation.

**Definition 16 (Sharing).** Let $(y_1, \dots, y_n)$ and $(x_1, \dots, x_n)$ be tuples of variables with the same length. The sharing function $\Upsilon$, which encodes variable sharing across different argument positions, is defined as follows:

$$ \Upsilon((y_1, \dots, y_n), (x_1, \dots, x_n)) := \bigwedge_{1 \le i < j \le n, y_i = y_j} x_i \approx x_j $$

## 2.5 Consequence and Least Model

The notion of a least model is common in logic programming. Horn logic programs admit a least model, which is the intersection of all models of the program (see [31, § 6, p. 36]). In our context, the least model of a set of clauses $N$ is the intersection of all models of $N$. An alternative characterization of the least model of $N$ is through the least fixed point of the one-step consequence operator, which we define as $T_N$ for the context of LA constraints analogously to [27, Section 4]. The one-step consequence operator $T_N$ takes a set of clauses $N$ and an interpretation $\mathcal{I}$ as input and returns an interpretation:

$$ P^{T_N(\mathcal{I})} := \left\{ (\vec{y})\beta \mid \begin{array}{l} \Lambda \parallel \neg P_1(\vec{y}_1) \vee \dots \vee \neg P_n(\vec{y}_n) \vee P(\vec{y}) \in N, \\ \qquad \models \Lambda\beta, \text{ and } \mathcal{I} \models P_i(\vec{y}_i)\beta \text{ for } 1 \le i \le n \end{array} \right\} $$

The least fixed point of this operator exists by Tarski's Fixed Point Theorem [39]: Interpretations form a complete lattice under inclusion (supremum given by union, infimum given by intersection), and $T_N$ is monotone.

## 3 Model Construction

In this section we address construction of models for HBS(LA). Throughout this section, we consider a set of constrained Horn clauses $N$ and an order $\prec$ to be given. Our aim is to define an interpretation $\mathcal{I}_N$, such that

$$ \mathcal{I}_N \models N \quad \text{if } N \text{ is saturated and } \square \notin N $$

Towards that goal, we define the operator $\delta(S, \Lambda \parallel C' \vee P(\vec{y}))$. It takes a symbolic interpretation $S$, and a Horn clause with maximal literal $P(\vec{y})$. It results in a symbolic interpretation that accounts for $\Lambda \parallel C' \vee P(\vec{y})$.

**Definition 17 (Production Operator).** Let $\Lambda \parallel C$ be a constrained Horn clause, where $C = C' \vee P(\vec{y})$, $P(\vec{y}) \succ C'$, and $C' = \neg P_1(y_{1,1}, \dots, y_{1,n_1}) \vee \dots \vee$
$\neg P_m(y_{m,1}, \dots, y_{m,n_m})$. Let $S$ be a symbolic interpretation, where the free variables of $P^S$ are $\vec{x}$ and the free variables of $P_i^S$ are $\vec{x}_i$ (for $1 \le i \le m$). Note that $n = |\vec{y}| = |\vec{x}| = \text{arity}(P)$.

The production operator $\delta(S, \Lambda \parallel C)$ results in a new symbolic interpretation

$$P^{\delta(S, \Lambda \parallel C)}(\vec{x}) := \left( \pi(\{y_1, \dots, y_n\}, \bigwedge_{\lambda \in \Lambda} \lambda \wedge \bigwedge_{i=1}^{m} (P_i^S)\sigma_i) \right) \sigma \wedge \Upsilon(\vec{y}, \vec{x})$$

$$Q^{\delta(S, \Lambda \parallel C)}(\vec{z}) := \perp \quad \text{for all } Q \neq P \text{ where } |\vec{z}| = \text{arity}(Q)$$

where, to map variables from literal arguments to the variables appearing in the symbolic interpretation $S$ and back, we have the substitutions

$$\sigma := \{y' \mapsto x_j \mid y' \in \{y_1, \dots, y_n\} \text{ and } j \text{ is the smallest index s.t. } y_j = y'\}$$

$$\sigma_i := \{x_{i,j} \mapsto y_{i,j} \mid 1 \le j \le n_i\} \quad \text{for } 1 \le i \le m$$

The goal of the operator $\delta(S, \Lambda \parallel C)$ is to define an extension of the symbolic interpretation $S$ such that $S \cup \delta(S, \Lambda \parallel C)$ satisfies $\Lambda \parallel C$. Note that $\delta$ only extends the interpretation over the strictly maximal predicate $P$. Moreover, due to our predicate order, it only needs to consider the interpretation $S$ for predicates $Q$ with $Q \prec P$. $\delta$ also satisfies the following two symmetrical properties: On the one hand, every grounding $\tau$ of $\Lambda \parallel C' \lor P(\vec{y})$ that is not yet satisfied by $S$ must correspond to solution $\beta$ of $P^{\delta(S, \Lambda \parallel C' \lor P(\vec{y}))}$ that satisfies $P(\vec{y})\tau$. On the other hand, every solution $\beta$ of $P^{\delta(S, \Lambda \parallel C' \lor P(\vec{y}))}$ must correspond to a grounding of $\Lambda \parallel C' \lor P(\vec{y})$ that is not yet satisfied by $S$. The first property is needed so $S \cup \delta(S, \Lambda \parallel C' \lor P(\vec{y}))$ satisfies $\Lambda \parallel C' \lor P(\vec{y})$. The second property is needed so we do not accidentally extend our interpretation by any solutions not needed to satisfy $\Lambda \parallel C' \lor P(\vec{y})$.

Note that in the above statements $\beta$ and $\tau$ are generally not the same because the variables $\vec{x}$ used to define $P^S$ are not necessarily the same as the variables appearing in the clause $\Lambda \parallel C$ and literal $P(\vec{y})$. There are three reasons for this that are handled by three different methods in our model construction:

1. The variables in $S$ and $\Lambda \parallel C$ simply do not match, e.g. in $P^S := x_1 \approx 0$ and $\Lambda \parallel C := y_1 > 0 \parallel P(y_1)$. This is handled by the substitution $\sigma$ in $\delta$ that maps all variables in $P(\vec{y})$ to their appropriate variables in $P^S$, e.g. in the previous example $\sigma = \{y_1 \mapsto x_1\}$ and $P^{\delta(S, \Lambda \parallel C)} = (y_1 > 0)\sigma = x_1 > 0$.

2. Not all variables in $\Lambda \parallel C$ also appear in $P(\vec{y})$, e.g. in $P^S := x_1 \approx 0$ and $\Lambda \parallel C := x_1 \approx y_1 + 1 \land y_1 \approx 0 \parallel P(x_1)$. This is handled in $\delta$ by the projection operator $\pi$ (Definition 15) that binds all variables that appear in $\Lambda \parallel C$ but not in $P(\vec{y})$, e.g. in the previous example $P^{\delta(S, \Lambda \parallel C)} := \pi(\{y_1\}, x_1 \approx y_1 + 1 \land y_1 \approx 0)$, where $\pi(\{y_1\}, x_1 \approx y_1 + 1 \land y_1 \approx 0) = \exists y_1. x_1 \approx y_1 + 1 \land y_1 \approx 0$, which is equivalent to $x_1 \approx 1$.

3. Some variables might occur in multiple argument positions, e.g. in $\Lambda \parallel C := \top \parallel P(y_1, y_1)$. This case is covered in $\delta$ by the sharing function $\Upsilon$ (c.f. Definition 16) that expresses which variables in $P^{\delta(S, \Lambda \parallel C)}$ must map to the same value. Continuing the example, $\Upsilon((y_1, y_1), (x_1, x_2)) = x_1 \approx x_2$ and $P^{\delta(S, \Lambda \parallel C)}(x_1, x_2) = \Upsilon((y_1, y_1), (x_1, x_2))$.

The parts of $P^{\delta(S, \Lambda \parallel C)}$ that we have not yet discussed are based on the fact that any constrained Horn clause $\Lambda \parallel C' \lor P(\vec{y})$ can also be written as an
implication of the form $\phi \rightarrow P(\vec{y})$, where $\phi := \Lambda \wedge P_1(y_{1,1}, \dots, y_{1,n_1}) \wedge \dots \wedge P_m(y_{m,1}, \dots, y_{m,n_m})$ and $S \not\models \Lambda \parallel C'\tau$ if and only if $S \models \phi\tau$. This means the groundings $\tau$ of $\Lambda \parallel C'$ not satisfied by $S$ are also the groundings of $\phi$ satisfied by $S$. It is straightforward to express these groundings with a conjunctive formula based on $\Lambda$ and the $P_i^S$. The only challenge is the reverse problem from before, i.e. mapping the variables of $P_i^S$ to the variables in the literals $P_i(y_{1,1}, \dots, y_{1,n_i})$. This mapping is done in $\delta$ by the substitution $\sigma_i$.

Now, based on the production operator $\delta$ for one clause, we can use an inductive definition over the order $\prec$ to define an interpretation $S_N$ for all clauses in $N$. We distinguish the following auxiliary symbolic interpretations: $S_{\prec P}$ which captures progress up to but excluding the predicate $P$, $\Delta_P$ which captures how $P$ should be interpreted considering $S_{\prec P}$, and $S_{\succeq P}$ which captures progress up to and including the predicate $P$. The symbolic interpretation $\Delta_P^\Lambda \parallel C$ is the extension of $S_{\prec P}$ w.r.t. the single clause $\Lambda \parallel C$.

**Definition 18 (Model Construction).** Let $N$ be a finite set of constrained Horn clauses. We define symbolic interpretations $S_{\prec P}$, $S_{\succeq P}$ and $\Delta_P$ for all predicates $P \in \Pi(N)$ by mutual induction over $\prec$:

$$S_{\prec P} := S_{\prec P} \cup \Delta_P \qquad S_{\prec P} := \bigcup_{Q \prec P} \Delta_Q \qquad \Delta_P := \bigcup_{\Lambda \parallel C' \lor P(*) \in N} \Delta_P^\Lambda \parallel C' \lor P(*)$$

$$\Delta_P^\Lambda \parallel C := \begin{cases} \delta(S_{\prec P}, \Lambda \parallel C) & \text{if } P(\vec{y}) \text{ maximal in } C, \text{ and } S_{\prec P} \not\models \Lambda \parallel C \\ S_\perp & \text{otherwise} \end{cases}$$

Finally, based on the above inductive definition of $S_{\prec P}$ for every predicate symbol $P \in \Pi(N)$, we arrive at an overall interpretation for $N$.

**Definition 19 (Candidate Interpretation).** The candidate interpretation for $N$ (w.r.t $\prec$), denoted $\mathcal{I}_N$, is the interpretation associated with the symbolic interpretation $S_N = \bigcup_{P \in \Pi(N)} \Delta_P$ where $P$ ranges over all predicate symbols occurring in $N$.

Note that $S_N = S_{\prec P}$ where $P$ is $\prec$-maximal in $\Pi(N)$. Obviously, we intend that $S_N \models N$ if $\tilde{N}$ is saturated (Theorem 29). Otherwise, i.e. $S_N \not\models N$, we can use our construction to find a non-redundant inference (Corollary 30). Consider the following two examples, demonstrating how $\delta$ sits at the core of the aforementioned inductive definitions of symbolic interpretations.

**Example 20 (Dependent Interpretation).** Assume $P \prec Q$ and consider the following set of clauses:

$$N := \left\{ \begin{array}{llll} 0 \le y_1 \le 2, 0 \le y_2 \le 2 & || & \frac{P(y_1, y_2)}{P(y_1, y_2)} \rightarrow (C_1), & (C_1), \\ y_3 \ge y_1 + 1, y_4 \ge y_2 + 1 & || & \frac{P(y_1, y_2)}{P(y_1, y_2)} \rightarrow \underline{Q(y_3, y_4)} & (C_2) \end{array} \right\}$$

Maximal literals are underlined. Since the maximal literals of $C_1$ and $C_2$ are both positive, ordered resolution cannot be applied. The set is saturated. Since $P$ is the $\prec$-smallest predicate we have $S_{\prec P} = S_\perp$. Applying the $\delta$ operator yields the following interpretation for $P$:

$$P^{S_{\prec P}} = P^{\delta(S_{\prec P}, C_1)}(x_1, x_2) = 0 \le x_1 \le 2 \land 0 \le x_2 \le 2$$

Then, $Q$ is interpreted relative to $P$. Consider the clause $C_2$: For all solutions of its constraint $y_3 \ge y_1 + 1, y_4 \ge y_2 + 1$ our model must also satisfy its logical
part $P(y_1, y_2) \to Q(y_3, y_4)$. The intuition that $Q$ depends on $P$ arises from the implication in the logical part. Whenever the constraint of $C_2$ and $P(y_1, y_2)$ are satisfied, $Q(y_3, y_4)$ must be satisfied. These are exactly the points defined through $\delta(S_{\prec Q}, C_2)$, based on $S_{\prec Q} = S_{\preceq P} = \delta(S_{\prec P}, C_1)$:

$$Q^{\delta(S_{\prec Q}, C_2)}(x_1, x_2) = \exists z_1, z_2. \begin{array}{l} x_1 \ge z_1 + 1 \land x_2 \ge z_2 + 1 \land 0 \le z_1 \le 2 \land 0 \le z_2 \le 2 \\ = x_1 \ge 1 \land x_2 \ge 1 \end{array}$$

Whenever the conjuncts $0 \le y_1 \le 2$ and $0 \le y_2 \le 2$ are satisfied, the premise of the implication is true, thus there must be a solution to the interpretation of $Q$, additionally abiding the constraint of the clause. Since $Q$ is $\prec$-maximal in $N$, we arrive at $S_N = S_{\prec Q} = S_{\prec P} \cup \delta(S_{\prec Q}, C_2) = \delta(S_{\prec}, C_1) \cup \delta(S_{\preceq}, C_2)$. See Figure 1a for a visual representation of $S_N$.

**Example 21 (Unsaturated Clause Set).** Assume $P \prec Q$ and consider the following set of clauses:

$$N := \left\{ \begin{array}{ll} y_1 < 0 & \| P(y_1) & (C_1), & y_1 < 1 & \| Q(y_1) & (C_3), \\ y_1 > 0 & \| \overline{P(y_1)} & (C_2), & y_1 \le 0 & \| \overline{Q(y_1)} & \to P(y_1) & (C_4) \end{array} \right\}$$

Maximal literals are underlined. Note that a resolution inference is possible, since the maximal literals of $C_3$ and $C_4$ have opposite polarity, use the same predicate symbol, and are trivially unifiable. Thus, in this example we consider the effect of applying our model construction to a clause set that is not saturated. Since $P$ is $\prec$-minimal, we start with the following steps:

$$\begin{array}{ll} S_{\prec P} = S_{\prec} & P^{\delta(S_{\prec P}, C_1)}(x_1) = x_1 < 0 \\ & P^{\delta(S_{\prec P}, C_2)}(x_1) = x_1 > 0 \quad P^{S_{\prec P}}(x_1) = x_1 < 0 \lor x_1 > 0 \end{array}$$

Next, we obtain the following results for $Q$:

$$\begin{array}{ll} S_{\prec Q} = S_{\prec P} & Q^{\delta(S_{\prec Q}, C_3)}(x_1) = x_1 < 1 \\ & Q^{\delta(S_{\prec Q}, C_4)}(x_1) = \perp \quad Q^{S_{\prec Q}}(x_1) = x_1 < 1 \lor \perp = x_1 < 1 \end{array}$$

See Figure 1b for a visual representation of $S_N = S_{\prec Q}$. Note that $S_N \not\models C_4$, since we have $S_N \models Q(0)$ but $S_N \not\models P(0)$. Thus, by using the constructed model, we can pinpoint clauses that contradict that $N$ is saturated. Applying resolution to $C_3$ and $C_4$ leads to the clause $y_1 \le 0 \| P(y_1)$ labelled $C_5$. If we then add $C_5$ to $N$, we instead get $P^{S_{\prec P}}(x_1) = x_1 < 0 \lor x_1 > 0 \lor x_1 \le 0 = \top$.

In the following, we clarify some properties of the construction. We provide an upper bound for the number of LA atoms and quantifiers in the symbolic model for LRA and LQA. Although we do not state it explicitly, the estimate for LIA works in a similar way, but due to the higher complexity of LIA quantifier elimination, the size of the symbolic model grows triple exponentially [36].

**Proposition 22.** If $N$ is a finite set of LRA/LQA constrained Horn clauses, and $S'_N$ the result of applying quantifier elimination to $S_N$ then, for every predicate symbol $P \in \Pi(N)$, the number of LA atoms in $P^{S'_N}$ is in $O(m^{2 \cdot q^{p-1}} \cdot n^{2 \cdot q^{p-1}} \cdot (l + a^2)^{q^p})$ where $n$ is the max. number of clauses with the same max. predicate, $m$ is the max. number of non-arithmetic literals in a clause, $l$ is the max. number of arithmetic literals in a clause, $a$ is the max. arity of any predicate, $p = |\Pi(N)|$, $q$ is the max. difference of variables in any clause and its positive maximal literal.
<figure><img src="image_2.png" /><figcaption>Figure 1: Visual representation of the models resulting from Examples 20 and 21.</figcaption></figure>

*Proof.* We proceed in two steps:

1. We argue that, for $P \in \Pi(N)$, $|\text{atoms}(P^{S_N})|$ is in $O(n^p \cdot m^{p-1} \cdot (l+a^2))$ and that $|\text{quants}(P^{S_N})|$ is in $O(n^{p-1} \cdot m^{p-1} \cdot q)$: Induct over the predicates $P_1 \prec \dots \prec P_p \in \Pi(N)$, along the order $\prec$, following Definition 18.

1.1. Base. Since $P_1$ is $\prec$-minimal, we have $S_{\prec P_1} = S_{\perp}$. Thus, by definition of $S_{\prec P_1}$ and union of symbolic interpretations, we have $P_1^{S_{\prec P_1}} = \perp \vee \Delta_{P_1}$. Thus, atoms($P_1^{S_{\prec P_1}}$) = atoms($\Delta_{P_1}$). Next, unfolding the definition of $\Delta_{P_1}$, observe that it is defined as a union of symbolic interpretations, and the operands correspond to some clause $\Lambda \parallel C$ where $C = P_1(*) \vee C'$, i.e., clauses where $P_1$ occurs positively. Consider the definition of $\Delta_{P_1}^{\Lambda \parallel C}$. If $P_1(*)$ is not maximal in $C$, then $P_1^{\Delta_{P_1}^{\Lambda \parallel C}} = \perp$, which contains no atoms. Otherwise, i.e., $P_1(*)$ is maximal, then $P_1^{\Delta_{P_1}^{\Lambda \parallel C}} = \delta(S_{\prec P_1}, \Lambda \parallel C)$. Since the number of clauses where $P_1(*)$ is maximal is in $O(n)$, $|\text{atoms}(\Delta_{P_1})|$ is in $O(n \cdot |\text{atoms}(\delta(S_{\prec P_1}, \Lambda \parallel C))|)$, because $\Delta_{P_1}$ is just a disjunction over these formulas (and possibly multiple other disjuncts that are $\perp$) according to the definition of union for symbolic interpretatons. Next, we argue the number of atoms and quantifiers for each of these $n$ disjuncts of the form $\delta(S_{\prec P_1}, \Lambda \parallel C)$ separately:

1.1.1. $|\text{atoms}(\delta(S_{\prec P_1}, \Lambda \parallel C))|$ is bounded by $l + a^2$: Consider the definition of $\delta$. For the interpretation of $P_1$, it results in a conjunction. The first $l$ elements of the conjunction directly correspond to the elements of $\Lambda$, and since the number of atoms in $\Lambda$ is bounded by $l$, this gives the first summand. Note that the second block of conjuncts, arising from conjunctively combining $P_i^{S_{\prec P_1}}$ are all empty, since $S_{\prec P_1} = S_{\perp}$. To see that the number of conjuncts generated by $\Upsilon$ is bounded by $a^2$, assume that $P_1$ is of the maximal arity $a$, and all arguments of the literal $P_1(*)$ are the same. Then, $\Upsilon$ will generate $a^2$ equality atoms among these $a$ variables.

1.1.2. $|\text{quants}(\delta(S_{\prec P_1}, \Lambda \parallel C))|$ is bound by $q$: Consider the definition of $\pi$. Given a formula over the variables $\text{vars}(\Lambda \parallel C)$, it generates $|\text{vars}(\Lambda \parallel C) \setminus \text{vars}(P_1(*))|$ quantifiers. This number is at most $q$.
Hence, $|\text{atoms}(P_1^{S_{\leq P_1}})|$ is in $O(n \cdot (l+a^2))$ and $|\text{quants}(P_1^{S_{\leq P_1}})|$ is in $O(n \cdot q)$.

1.2. Step. For the same reason as in Case 1.1., $P_{i+1}^{S_{\leq P_{i+1}}}$ is a disjunction over at most $n$ subformulas, one for each clause with maximal predicate $P_{i+1}$. We argue the number of atoms and quantifiers for each of these $n$ disjuncts of the form $\delta(S_{\leq P_{i+1}}, \Lambda \parallel C)$ separately:

1.2.1. $|\text{atoms}(\delta(S_{\leq P_{i+1}}, \Lambda \parallel C))|$ is bound by $l+a^2+m \cdot \max_{k \leq i} |\text{atoms}(P_k^{S_{\leq P_{i+1}}})|$:

The summands $l$ and $a^2$ are justified like in the base. The additional summand is motivated by fact that, in contrast to the base, now $S_{\leq P_{i+1}} = S_{\leq P_i} \neq S_{\perp}$. By the (strong) induction hypothesis, $|\text{atoms}(P_i^{S_{\leq P_i}})|$ is in $O(n^i \cdot m^{i-1} \cdot (l+a^2))$ for all $1 \leq i$. We substitute using the hypothesis to get $|\text{atoms}(P_{i+1}^{S_{\leq P_{i+1}}})|$ in $O(n \cdot (l+a^2+m \cdot (n^i \cdot m^{i-1} \cdot (l+a^2))))$. We expand to $O(n^{i+1} m^i \cdot a^2 + n^{i+1} m^i \cdot l + \mathcal{N}a^2 + \mathcal{N})$, drop the non-exponential summands and factor, which yields $|\text{atoms}(P_{i+1}^{S_{\leq P_{i+1}}})|$ in $O(n^{i+1} m^i (a^2 + l))$.

1.2.2. $|\text{quants}(\delta(S_{\leq P_{i+1}}, \Lambda \parallel C))|$ is bound by $q+m \cdot \max_{k \leq i} |\text{quants}(P_k^{S_{P_i}})|$:

The summand $q$ is justified like in the base case. Like in the previous case, the additional summand $m \cdot \max_{k \leq i} |\text{quants}(P_k^{S_{P_i}})|$ motivated by the fact that, in contrast to the base case, now $S_{\leq P_{i+1}} = S_{\leq P_i} \neq S_{\perp}$. For each of the literals in $C$ that refer to a predicate symbol $P_j$ with $j \leq i$, as many quantifiers as there are in $P_j^{S_{\leq P_{i+1}}}$ are generated by $\delta$. By the (strong) induction hypothesis, $|\text{quants}(P_i^{S_{\leq P_i}})|$ is in $O(n^i \cdot m^{i-1} \cdot q)$ for all $1 \leq i$. We substitute using the hypothesis to get $|\text{quants}(P_{i+1}^{S_{\leq P_{i+1}}})|$ in $O(n \cdot (q \cdot m \cdot (n^i \cdot m^{i-1} \cdot q)))$. After expansion and simplification, this yields that $|\text{quants} P_{i+1}^{\leq P_{i+1}}|$ is in $O(n^{i+1} m^i q)$.

Note that $|\text{atoms}(P_i^{S_{\leq P_i}})| = |\text{atoms}(P_i^{S_N})|$ (and the same is true for the number of quantifiers), which can be seen by Proposition 32.

2. We argue that by applying quantifier elimination to all $P^{S_N}$ for $P \in \Pi(N)$, we obtain an $S'_N$ from $S_N$, which represents an equivalent interpretation, and we arrive at the conclusion. Let $e(q, n) := n^q$ denote the number of atoms after eliminating $q$ quantifiers from the top of a formula with $n$ atoms (see [32, 14]). The inductive argument is very similar to Step 1, just note that we eliminate quantifiers at the level of the disjuncts that form $\Delta$.

2.1. Base. For $P_1$ we have max. $q$ quantifiers for each of the (at most) $n$ clauses with $P_1$ as maximal predicate. Thus, $O(|\text{atoms}(P_1^{S_{\leq P_1}})|) = O(n \cdot e(q, l + a^2)) = O(n \cdot (l + a^2)^q)$.

2.2. Step. By the induction hypothesis:

$$ 
\begin{align*}
O(|\text{atoms}(P_i^{S_{\leq P_i}})|) &= O(n^{q^{i-1}+q^{i-2}+\cdots+1} \cdot m^{q^{i-1}+q^{i-2}+\cdots+q} \cdot (l+a^2)^{q^i}) \\
&= O(n^{2 \cdot q^{i-1}} \cdot m^{2 \cdot q^{i-1}} \cdot (l+a^2)^{q^i})
\end{align*}
$$

For $P_{i+1}$ we still have max. $q$ quantifiers for each of the $n$ clauses with $P_{i+1}$
as maximal predicate.

$$
\begin{align*}
& O(|\text{atoms}(P_{i+1}^{S_{\leq P_i+1}})|) \\
&= n \cdot e(q, (l+a^2 + m \cdot O(|\text{atoms}(P_i^{S_{\leq P_i}})|))) \\
&= O(n \cdot (l+a^2 + m \cdot n^{q^{i-1}+q^{i-2}+\cdots+1} \cdot m^{q^{i-1}+q^{i-2}+\cdots+q} \cdot (l+a^2)^{q^i})^q)
\end{align*}
$$

(We drop non-dominating summands $l + a^2$.)

$$
\begin{align*}
&= O(n \cdot m^q \cdot n^{q^i+q^{i-1}+\cdots+q} \cdot m^{q^i+q^{i-1}+\cdots+q^2} \cdot (l+a^2)^{q^{i+1}}) \\
&= O(n^{q^i+q^{i-1}+\cdots+q+1} \cdot m^{q^i+q^{i-1}+\cdots+q^2+q} \cdot (l+a^2)^{q^{i+1}}) \\
&= O(n^{2 \cdot q^i} \cdot m^{2 \cdot q^i} \cdot (l+a^2)^{q^{i+1}})
\end{align*}
$$

□

**Corollary 23 (Effective Construction).** If $N$ is a finite set of constrained Horn clauses then for every predicate $P \in \Pi(N)$, $P^{SN}$ is a linear arithmetic formula of finite size, and can be computed in a finite number of steps.

*Proof.* Corollary of Proposition 22. The construction terminates, since it computes $S_N$ from $N$ (which are both finite) by a simple recursion (cf. Definition 18). □

We show that all points in $P_N^I$ are necessary and justified in some sense, that $I_N$ is indeed a model of $N$, and that $I_N$ is also the least model of $N$ if $N$ is saturated. The notion of whether a clause is productive captures whether it contributes something to the symbolic interpretation.

**Definition 24 (Productive Clause).** Let $P$ be a predicate symbol with arity($P$) = $n$. We say that $\Lambda \parallel C$ produces $P(a_1, \dots, a_n)$ if $(a_1, \dots, a_n) \in P^{\Delta_P^\Lambda \parallel C}$.

Next, we want to formally express that every element of the resulting interpretation is justified. Firstly, we express that the operator $\delta$ will produce points such that every clause is satisfied whenever necessary, i.e. whenever the maximal literal of the clause is $P(*)$ and the maximal literal not satisfied by $S_{\leq P}$.

**Proposition 25.** Let $\Lambda_C \parallel C$ where $C = C' \lor P(\vec{y})$ and $C' \prec P(\vec{y})$. Let $\tau$ be a grounding substitution for $\Lambda_C \parallel C$. If $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$, then $\models \Lambda_C \tau$ and $S_{\leq P} \models P(\vec{y})\tau$, thus $S_{\leq P} \models (\Lambda_C \parallel C)\tau$.

*Proof.* Let $\Lambda_C \parallel C$ where $C = C' \lor P(\vec{y})$ and $C' \prec P(\vec{y})$. Let $\tau$ be a grounding substitution for $\Lambda_C \parallel C$. Assume $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$. This implies $S_{\leq P} \not\models \Lambda_C \parallel C$, thus $\Delta_P^{\Lambda_C \parallel C} = \delta(S_{\prec P}, \Lambda_C \parallel C)$. Let $\beta_\tau := \{x_i \mapsto y_i\tau \mid 1 \le i \le n\}$ and $\phi = \bigwedge_{\lambda \in \Lambda_C} \lambda \wedge \bigwedge_{i=1}^m (P_i^{S_{\prec P}})\sigma_i$. It remains to show that $\Delta_P \models P(\vec{y})\tau$, i.e. $(\vec{y})\tau \in P^{\delta(S_{\prec P}, \Lambda_C \parallel C)}$, i.e. $\models ((\pi(\{\vec{y}\}, \phi))\sigma \wedge \Upsilon(\vec{y}, \vec{x}))\beta_\tau$. We proceed in two steps, one per conjunct:

1. To see $\models (\Upsilon(\vec{y}, \vec{x}))\beta_\tau$: Let $1 \le i < j \le n = |\vec{y}| = |\vec{x}|$. By definition of $\Upsilon$, for each conjunct $x_i \approx x_j$ in $\Upsilon(\vec{y}, \vec{x})$, there are two variables $y_i = y_j$ from $\vec{y}$. The conjunct $x_i \approx x_j$ is satisfied by $\beta_\tau$, since $\beta_\tau$ and $\tau$ are functions, therefore $(x_i)\beta_\tau = (x_j)\beta_\tau$.
2. To see $\vdash (\pi(\{\vec{y}\}, \phi))\sigma\beta_\tau$: From $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$, we know $\vdash \Lambda_C\tau$, thus $\vdash \lambda\tau$ for all $\lambda \in \Lambda_C$, and that $S_{\prec P} \not\models (L_i)\tau$ for all literals $L_i$ from $C'$. Given that $P_i^{S_{\prec P}}$ encodes $S_{\prec P} \not\models L_i$ it follows that $\vdash P_i^{S_{\prec P}}\sigma_i\tau$ for all $1 \le i \le m$.

Thus, we may construct a potential witness for all existential quantifiers introduced by the application of $\pi$ based on $\tau$: $\gamma_\tau := \{z_i \mapsto z_i\tau \mid z_i \in \text{vars}(\Lambda_C \parallel C) \setminus \{\vec{y}\})\}$.

By definition of $\sigma$ and $\beta_\tau$, we have $(y_i)\sigma\beta_\tau = (y_i)\tau$ for all $y_i$ in $\vec{y}$. Thus $(\phi)\gamma_\tau\sigma\beta_\tau$ is equivalent to $(\phi)\tau$. Again, reasoning from $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$ we arrive at $\vdash (\phi)\tau$, thus $\vdash (\pi(\{\vec{y}\}, \phi))\sigma\beta_\tau$ with witness $\gamma_\tau$.

Hence $\vdash ((\pi(\{\vec{y}\}, \phi))\sigma \wedge \gamma(\vec{y}, \vec{x}))\beta_\tau$, thus $\Delta_P^{\Lambda_C \parallel C} \vdash \Lambda_C \parallel C$, and by definition of $S_{\prec P}$, also $S_{\prec P} \vdash \Lambda_C \parallel C$. $\square$

Secondly, we express that for every point in $P_N^I$, it is justified in the sense that there is a clause that produced the point, i.e. this clause would otherwise not be satisfied by the resulting interpretation.

**Proposition 26.** If $S_{\prec P} \vdash P(\vec{a})$, then there exists a clause $\Lambda_C \parallel C$ where $C = C' \lor P(\vec{y})$ and $C' \prec P(\vec{y})$, and there exists a grounding $\tau$ for $\Lambda_C \parallel C$, such that $P(\vec{a}) = P(\vec{y})\tau$ and $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$.

*Proof.* Assume $S_{\prec P} \vdash P(\vec{a})$.

Firstly, we argue that $\vec{a} \in P^{\Delta_P}$: For the construction of $S_{\prec P}$ only predicates $Q$ s.t. $Q \prec P$ are considered, thus $P^{S_{\prec P}} = \emptyset$. By definition of $S_{\prec P}$ as $S_{\prec P}$ as the union of $S_{\prec P}$ and $\Delta_P$ and thus $P^{S_{\prec P}} = P^{S_{\prec P}} \cup P^{\Delta_P}$. Together with $P^{S_{\prec P}} = \emptyset$ we have $P^{S_{\prec P}} = P^{\Delta_P}$, hence $\vec{a} \in P^{\Delta_P}$.

Secondly, we argue for the existence of $\Lambda_C \parallel C$: $\Delta_P$ is defined as the union of $\Delta_P^{\Lambda \parallel D' \lor P(*)}$ where $\Lambda \parallel D' \lor P(*) \in N$. Thus there must be at least one $\delta(S_{\prec P}, \Lambda \parallel D' \lor L)$ with $L = P(\vec{y})$, $D' \prec L$, $S_{\prec P} \not\models \Lambda \parallel D' \lor L$, s.t. $\vec{a} \in P^{\delta(S_{\prec P}, \Lambda \parallel D' \lor L)}$. We identify $\Lambda \parallel D' \lor L$ with $\Lambda_C \parallel C$.

Thirdly, we construct $\tau$, and show $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$ by unfolding the interpretation of $P$ by $S_{\prec P}$: Let $\beta_x = \{x_1 \mapsto a_1, \dots, x_n \mapsto a_n\}$. From $\vec{a} \in \Delta_P^{\Lambda_C \parallel C}$ we know that $\beta_x$ is a solution for $(\pi(\{\vec{y}\}), \bigwedge_{\lambda \in \Lambda_C} \lambda \wedge \bigwedge_{i=1}^m (P_i^{S_{\prec P}}\sigma_i))\sigma \wedge \gamma(\vec{y}, \vec{x})$. Thus, $\sigma\beta_x$ is a solution for $\pi(\{\vec{y}\}, \bigwedge_{\lambda \in \Lambda_C} \lambda \wedge \bigwedge_{i=1}^m (P_i^{S_{\prec P}}\sigma_i))$. Let

$$ \gamma := \{z \mapsto c_z \mid z \in \text{vars}(C) \setminus \text{vars}(L)\} $$

be a witness for the existential quantifiers introduced by $\pi$, i.e. $\vdash (\bigwedge_{\lambda \in \Lambda_C} \lambda \wedge \bigwedge_{i=1}^m (P_i^S\sigma_i)\gamma\sigma\beta_x)$. The composition $\tau := \gamma\sigma\beta_x$ then maps all variables from $C$ and is a solution for $\bigwedge_{\lambda \in \Lambda_C} \lambda \wedge \bigwedge_{i=1}^m (P_i^S\sigma_i)$. Consequently, $\tau$ is a solution for all conjuncts:

* $\vdash \lambda\tau$ for all $\lambda \in \Lambda_C$ immediately gives $\vdash \Lambda_C\tau$.

* $\vdash (P_i^S\sigma_i)\tau$ for all $1 \le i \le m$ witnesses $S_{\prec P} \not\models L_i\tau$, because the polarity of $P_i^{S_{\prec P}}$ is opposite of the polarity of $L_i$ by definition of $\delta$.

We have $P^{S_{\prec P}} = \emptyset$, and that $L$ is positive, thus $S_{\prec P} \not\models L$. Together with the two above facts we arrive at $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$.

To see that $P(\vec{y})\tau = P(\vec{a})$, consider that $(y_i)\sigma = x_i$, $(x_i)\beta_x = a_i$, and $\gamma$ has no effect on $\vec{y}$ by definition. Thus $(y_i)\sigma\beta_x = (y_i)\tau = a_i$. In case there are two (or more, analogously) variables $y_i$, $y_j$ in $\vec{y}$ where $y_i = y_j$ and $i < j$, $a_i = a_j$
is guaranteed: $(y_i)\tau = (x)\beta_x = a_i$ directly by definition of $\sigma$ and $\beta_x$. $y_j$ is not in the domain of $\sigma$, however the equalities generated by $\Upsilon(\vec{y}, \vec{x})$ ensure that $(x_i)\beta_x = (x_j)\beta_x$. $\square$

Also, observe that once the maximal predicate $P$ of a given clause is interpreted by $S_{\leq P}$, the interpretation of the clause does not change for $S_{\leq Q}$ where $Q \succ P$.

**Corollary 27.** Let $P \prec Q \preceq R$, and $P$ be maximal in clause $C$. If $S_{\leq P} \models \Lambda_C \parallel C$ or $S_{\leq Q} \models \Lambda_C \parallel C$, then $S_{\leq R} \models \Lambda_C \parallel C$ and $S_{\leq R} \models \Lambda_C \parallel C$.

*Proof.* Corollary of Proposition 32. $\square$

As a result, we know that the full model satisfies $N$, i.e., $\mathcal{I}_N \models N$ if every clause is satisfied at the point of the construction, where the interpretation of its maximal predicate $P$ stays fixed.

**Proposition 28.** For every clause $\Lambda_C \parallel C \in N$ with maximal predicate $P$, if $S_{\leq P} \models \Lambda_C \parallel C$, then $\mathcal{I}_N \models N$.

*Proof.* Follows from Corollary 27 and the fact that $\mathcal{I}_N = S_{\leq Q}$ where $Q$ is the $\prec$-maximal predicate symbol in $N$. $\square$

Some auxiliary lemmas follow.

**Proposition 32.** Let $P, Q$, and $R$ be predicate symbols. If $P \prec Q$ and $Q \preceq R$, then $P^{S_{\leq P}} = Q^{S_{\leq Q}} = R^{S_{\leq R}}$.

*Proof.* Generally, for a predicate symbol $S$, we have $P_S^\Delta = \emptyset$ unless $S = P$ by definition of $\Delta_S$. $S_{\leq Q}$ is defined as the union of all $\Delta_S$ for $S \prec Q$, thus $P^{\Delta_P} = Q^{S_{\leq P}} = R^{S_{\leq R}}$. $S_{\leq Q}$ is defined as the union of $S_{\leq Q}$ and $\Delta_Q$. By definition of $\Delta_Q$, the only predicate that $\Delta_Q$ may interpret as non-empty is $Q$. In particular, i.e. since $P \prec Q$, we have $P^{\Delta_Q} = \emptyset$ thus $Q^{S_{\leq Q}} = R^{S_{\leq R}}$. To see that $P^{S_{\leq Q}} = Q^{S_{\leq R}} = R^{S_{\leq R}}$, the same reasoning applies, i.e. $P^{\Delta_R} = \emptyset$ unless $P = R$. $\square$

**Corollary 33.** Let $P, Q$, and $R$ be predicate symbols. If

1. $P \prec Q$, and

2. $Q \preceq R$, and

3. $S_{\leq P} \models [\neg]P(\vec{x})\sigma$ or $S_{\leq Q} \models [\neg]P(\vec{x})\sigma$,

then $I_{\leq R} \models [\neg]P(\vec{x})\sigma$ and $I_{\leq R} \models [\neg]P(\vec{x})\sigma$.

*Proof.* Corollary of Proposition 32. $\square$

**Proposition 34.** Let $\Lambda_D \parallel D$ be a constrained Horn clause with $D = D' \lor P(\vec{y})$. If $\Lambda_D \parallel D$ produces $P(\vec{y})\tau$, then for all grounding substitutions $\sigma$, such that $S_{\leq P} \not\models (\Lambda_D \parallel D')\sigma$, for all $Q$ such that $P \preceq Q$, we have $S_{\leq Q} \not\models (\Lambda_D \parallel D')\sigma$.
*Proof.* Since $\Lambda_D \| D$ produces $P(\vec{y})\tau$, all literals in $D'$ are strictly $\prec$-smaller than $P(\vec{y})$, and $S_{\prec P} \not\models \Lambda_D \| D$.

Let $\sigma$ be a grounding substitution such that $S_{\prec P} \not\models (\Lambda_D \| D')\sigma$.

Assume, towards a contradiction, that the proposition does not hold, i.e. $P \preceq Q$ and $S_{\preceq Q} \models (\Lambda_D \| D')\sigma$. Then we have $\models \Lambda_D \sigma$ and $S_{\preceq Q} \models ([\neg]R(*)\sigma)$ for some literal $[\neg]R(*)$ in $D'$.

However, by assumption, all literals in $D'$ are strictly $\prec$-smaller than $P(\vec{y})$, i.e. $R \prec P$. Thus their respective interpretation is contained in $S_{\prec P}$ by construction, i.e. $R^{S_{\prec P}} = R^{S_{\preceq P}} = R^{S_{\preceq Q}}$. This contradicts $S_{\prec P} \models (\Lambda_D \| D')\sigma$. $\square$

**Proposition 35.** Let $\prec$ be a clause ordering and $N$ be a finite set of constrained Horn clauses. If (1.) $N$ is saturated w.r.t. $\prec$-resolution, and (2.) there is no $\Lambda \| \perp \in N$ where $\Lambda$ is satisfiable, then for every clause $\Lambda_C \| C \in N$, $\models \Lambda_C \| C$ or $P$ is maximal in $C$ and $S_{\prec P} \models \Lambda_C \| C$.

*Proof.* Assume Premises 1 and 2. Let $\Lambda_C \| C \in N$. We distinguish two cases:

1. $C = \perp$. By Premise 2, $\Lambda_C$ is unsatisfiable, thus $\models \Lambda_C \| C$.

2. $C = C' \lor L$ where $L$ is maximal in $C$, and $P$ is the predicate symbol associated with $L$, i.e. $P$ is maximal in $C$. In case $\Lambda_C$ is unsatisfiable, $\models \Lambda_C \| C$. In the following, we thus consider $\Lambda_C$ satisfiable. We distinguish two cases:

2.1. $L = P(\vec{y})$. We distinguish two cases:

2.1.1. $S_{\prec P} \models \Lambda_C \| C$. Corollary 33 applies.

2.1.2. $S_{\prec P} \not\models \Lambda_C \| C$. Proposition 25 applies.

2.2. $L = \neg P(\vec{z})$. Assume, towards a contradiction, that the proposition does not hold, i.e. $S_{\prec P} \not\models \Lambda_C \| C$. Let $\sigma$ be a grounding substitution such that $S_{\prec P} \not\models (\Lambda_C \| C)\sigma$. It follows that $S_{\prec P} \not\models (C')\sigma$ and $S_{\prec P} \not\models L\sigma$, thus $S_{\prec P} \models (P(\vec{z}))\sigma$. Assume, without loss of generality:

* *minimality of P:* There is no predicate symbol $Q \prec P$ such that there is a clause $\Lambda_D \| D \in N$ with maximal predicate $Q$ and $S_{\prec Q} \not\models \Lambda_D \| D$, i.e. for all $Q \prec P$, $S_{\prec Q} \models \{\Lambda_D \| D \in N \mid Q \text{ maximal in } D\}$,

* *minimality of $(\Lambda_C \| C)\sigma$:* There is no clause $\Lambda_D \| D \in N$ with maximal predicate $P$ and grounding $\sigma_D$, s.t. $(\Lambda_D \| D)\sigma_D \prec (\Lambda_C \| C)\sigma$ and $S_{\prec P} \not\models (\Lambda_D \| D)\sigma_D$, i.e. $S_{\prec P} \models \text{gnd}(\{\Lambda_D \| D \in N \mid P \text{ maximal in } C\})^{<(\Lambda_C \| C)\sigma}$,

* *maximality of $L\sigma$:* there is no literal $L'$ in $C'\sigma$ s.t. $\neg P(\vec{z})\sigma \prec L'$.

By Proposition 26 there is a clause $\Lambda_D \| D \in N$ where $D = D' \lor P(\vec{y})$, $D' \prec P(\vec{y})$, and $\Lambda_D$ is satisfiable, that produces $P(\vec{z})\sigma$. Assume, without loss of generality, that the sets of variables occuring in $\Lambda_C \| C$ and $\Lambda_D \| D$ are disjoint, i.e. vars($\Lambda_C \| C$) $\cap$ vars($\Lambda_D \| D$) = $\emptyset$. Let $\tau$ be the substitution that maps $P(\vec{y})$ to $P(\vec{z})\sigma$. Since $P(\vec{y})\tau = P(\vec{z})\sigma$, there exists a most general unifier between $P(\vec{y})$ and $P(\vec{z})$, which we call $\sigma'$. Then, since $\sigma'$ is most general, there is a substitution $\tau'$ such that the substitution $\sigma'\tau'$ is equivalent to $\sigma$ when restricted to vars($\Lambda_C \| C$) and equivalent to $\tau$ when restricted to vars($\Lambda_D \| D$). We have $P(\vec{y})\sigma'\tau' = P(\vec{y})\tau = P(\vec{z})\sigma$. Consider the following $\prec$-resolution inference:

$$ \frac{\Lambda_C \| C' \lor \neg P(\vec{z}) \quad \Lambda_D \| D' \lor P(\vec{y}) \quad \sigma' = \text{mgu}(\neg P(\vec{z}), \text{comp}(P(\vec{y})))}{(\Lambda_C, \Lambda_D \| C' \lor D')\sigma'} $$
Let $(\Lambda_C, \Lambda_D \parallel C' \lor D')\sigma' = \Lambda_R \parallel R$. Since $\vdash \Lambda_C\sigma$ and $\vdash \Lambda_D\tau$ (by Proposition 26), we have $\vdash \Lambda_R\tau'$. Since $\Lambda_D \parallel D$ produces $P$, we have $S_{\prec P} \not\vdash (\Lambda_D \parallel D')\tau$. By Proposition 34, we have that, $S_{\prec P} \not\vdash (\Lambda_D \parallel D')\tau$ and $S_{\prec P} \not\vdash (\Lambda_D \parallel D')\sigma'\tau'$. Thus $S_{\prec P} \not\vdash \Lambda_R \parallel R\tau'$ and $S_{\prec P} \not\vdash \Lambda_R \parallel R$.
We distinguish two cases:

2.2.1. $R = \perp$. We distinguish two cases:

2.2.1.1. $\Lambda_R \parallel \perp \in N$. Contradicts Premise 2.

2.2.1.2. $\Lambda_R \parallel \perp \notin N$. Then, by Premise 1, we have that $\Lambda_R \parallel \perp$ is redundant, i.e. $N^{<\Lambda_R} \parallel \perp \vdash \Lambda_R \parallel \perp$. However, since there is no clause that is $\prec$-smaller than $\Lambda_R \parallel \perp$, we have $N^{<\Lambda_R} \parallel \perp = \emptyset$, which contradicts Premise 1.

2.2.2. $R \neq \perp$. $\neg P(\tilde{z})\sigma$ occurs less often in $R\tau'$ than it occurs in $C\sigma$. The reason being that the number of occurences in $C'\sigma'$ is one less than the number of occurences in $C\sigma'$, while there are no occurences in $D'\sigma'$ since we know that $D'\sigma' \prec P(\tilde{y})\sigma'$ and $D\sigma' \leq P(\tilde{y})\sigma'$, and $P(\tilde{y})\sigma' \prec \neg P(\tilde{z})\sigma'$. By maximality of $\neg P(\tilde{z})\sigma$, also $\neg P(\tilde{y})\tau' \leq R\tau'$. Therefore we have $\Lambda_R \parallel R \prec \Lambda_C \parallel C$. By minimality of $(\Lambda_C \parallel C)\sigma$, Case 2.1., and Corollary 27, we have $S_{\prec P} \vdash \text{gnd}(N)^{<(\Lambda_C \parallel C)\sigma}$. We distinguish two cases:

2.2.2.1. $\Lambda_R \parallel R \in N$. Contradicts minimality of $(\Lambda_C \parallel C)\sigma$. Contradicts $S_{\prec P} \vdash \text{gnd}(N)^{<(\Lambda_C \parallel C)\sigma}$ since $(\Lambda_R \parallel R)\tau' \prec (\Lambda_C \parallel C)\sigma$.

2.2.2.2. $\Lambda_R \parallel R \notin N$. By assumption of Premise 1, $\Lambda_R \parallel R$ is redundant w.r.t. $N$ and $\prec$, i.e. $N^{<\Lambda_R} \parallel R \vdash \Lambda_R \parallel R$. $S_{\prec P} \vdash \text{gnd}(N)^{<(\Lambda_C \parallel C)\sigma}$ contradicts $\text{gnd}(N)^{<(\Lambda_R \parallel R)\tau'} \vdash (\Lambda_R \parallel R)\tau'$ and $N^{<\Lambda_R} \parallel R \vdash \Lambda_R \parallel R$. Therefore $\Lambda_R \parallel R$ is not redundant, which contradicts Premise 1.

□

With the above propositions we show that indeed $\mathcal{I}_N \vdash N$ if $N$ is saturated and does not contain the empty clause.

**Theorem 29.** Let $\prec$ be a clause ordering and $N$ be a set of constrained Horn clauses. If (1.) $N$ is saturated w.r.t. $\prec$-resolution, and (2.) $\square \notin N$, then $\mathcal{I}_N \vdash N$.

*Proof.* By Proposition 35 and Proposition 28. □

For clauses with positive maximal literal, the fact that they are satisfied by $\mathcal{I}_N$ follows from Proposition 25. For clauses with maximal literal $\neg P(\ast)$, we prove this theorem by contradiction: If there is a minimal clause $\Lambda_C \parallel C$ such that $S_N \not\vdash \Lambda_C \parallel C$. We can then exploit Proposition 26 to find the smallest clause $\Lambda_D \parallel D$ that produced the respective instance $P(\vec{a})$. Applying hierarchic $\prec$-resolution to $\Lambda_C \parallel C$ and $\Lambda_D \parallel D$ then yields a non-redundant clause. This idea then leads to the following theorem.

**Corollary 30.** Let $\prec$ be a clause ordering and $N$ be a set of constrained Horn clauses. If (1.) $\mathcal{I}_N \not\vdash N$, and (2.) $\square \notin N$, then there exist two clauses $\Lambda_C \parallel C$, $\Lambda_D \parallel D \in N$ such that: (1.) $\Lambda_C \parallel C$ is the smallest clause not satisfied by $\mathcal{I}_N$, i.e. there exists a grounding $\tau$ such that $\mathcal{I}_N \not\vdash (\Lambda_C \parallel C)\tau$, but there does not exist a clause $\Lambda_{C'} \parallel C' \in N$ with grounding $\tau'$, such that $\mathcal{I}_N \not\vdash (\Lambda_{C'} \parallel C')\tau'$ and $(\Lambda_{C'} \parallel C')\tau' \prec (\Lambda_C \parallel C)\tau$, (2.) $\neg P(\vec{a})$ is the maximal literal of $(\Lambda_C \parallel C)\tau$, (3.) $\Lambda_D \parallel D$ is the minimal clause that produces $P(\vec{a})$, (4.) $\prec$-resolution is applicable to $\Lambda_C \parallel C$ and $\Lambda_D \parallel D$, and (5.) the resolvent of $\Lambda_C \parallel C$ and $\Lambda_D \parallel D$ is not redundant w.r.t. $N$.
*Proof.* Similar to Case 2.2. in the proof of Proposition 35. □

Additionally, we show that $\mathcal{I}_N$ is the least model of $N$, establishing a connection between our approach and the literature on constrained Horn clauses (see [27, Section 4] and [15, Section 2.4.1]) and logic programming (see [31, § 6, p. 37]).

**Theorem 31.** *$\mathcal{I}_N$ is the least model of $N$.*

*Proof.* Assume, towards a contradiction, that $\mathcal{I}_N$ is not the least model of $N$, i.e. there exists an interpretation $\mathcal{I}$ such that $\mathcal{I} \subset \mathcal{I}_N$ and $\mathcal{I} \models N$. Since $\mathcal{I} \subset \mathcal{I}_N$, there is a predicate symbol $P$ and a point $\vec{a}$ such that $\vec{a} \in P^{\mathcal{I}_N}$, i.e. $\mathcal{I}_N \models P(\vec{a})$ but $\vec{a} \notin P^{\mathcal{I}}$, i.e. $\mathcal{I} \not\models P(\vec{a})$. Assume, w.l.o.g., that $P$ is minimal, i.e. $Q^{\mathcal{I}_N} = Q^{\mathcal{I}}$ for all $Q \prec P$. By Proposition 26 from $\mathcal{I}_N \models P(\vec{a})$ it follows that there is a clause $\Lambda_C \parallel C \in N$ such that $C = C' \lor P(\vec{y})$, $C'' \prec P(\vec{y})$, $\tau$ is a grounding for $\Lambda_C \parallel C$, $P(\vec{a}) = P(\vec{y})\tau$, and $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$. From $S_{\prec P} \not\models (\Lambda_C \parallel C)\tau$ we know that $S_{\prec P} \not\models (\Lambda_C \parallel C')\tau$ and by Proposition 32 we have $\mathcal{I}_N \not\models (\Lambda_C \parallel C')\tau$. Since $C' \prec P(\vec{y})$ and by minimality of $P$, we know that $\mathcal{I}_N$ and $\mathcal{I}$ agree on $\Lambda_C \parallel C'$, i.e. $\mathcal{I} \not\models (\Lambda \parallel C')\tau$. However, $\mathcal{I} \models N$, which implies $\mathcal{I} \models (\Lambda_C \parallel C)\tau$, requires $\mathcal{I} \models P(a)$ which contradicts the assumption $\mathcal{I} \not\models P(\vec{a})$. □

Fermüller and Leitsch define four postulates (see [19] as cited in [13, Section 5.1, p. 234]) regarding *automated model building*. In the following, we instantiate the postulates for our setting. By $\mathfrak{S}(N)$ we denote the set of all symbolic interpretations of the set of constrained Horn clauses $N$. We argue how our approach satisfies all postulates, one by one:

**Uniqueness** Each element of $\mathfrak{S}(N)$ specifies a single interpretation of $N$.

We have shown (cf. Theorem 31) that $\mathcal{I}_N$, the model represented by $S_N$, is the least model of $N$, which is unique.

**Atom Test** There exists a fast procedure to evaluate arbitrary ground atoms over $\Pi(N)$ in the interpretation defined by a $S$ in $\mathfrak{S}(N)$.

This is a special case of clause evaluation (cf. Proposition 14): A ground atom $P(\vec{t})$ is true in $S$ if and only if $\models P^S(\vec{x})\{x_i \mapsto t_i \mid 1 \le i \le |\vec{x}| = |\vec{t}|\}$. Fulfillment of this property thus hinges on the meaning of “fast”. We consider methods for evaluating formulas of LA against points to be fast.

**Formula Evaluation** There exists an algorithm deciding the truth values of arbitrary formulas in interpretations defined by $S \in \mathfrak{S}(N)$.

Proposition 14 states that evaluating a constrained clause $\Lambda \parallel C$ is achieved by evaluating the universal closure of $(\Lambda \parallel C)^S$, which is decided by quantifier elimination algorithms for LRA, LQA, and LIA [32, 14]. For sets of clauses, evaluate each clause individually and combine the results con-junctively.

**Equivalence Test** There exists an algorithm which decides whether two representations $S_1$ and $S_2$ in $\mathfrak{S}(N)$ describe the same interpretation.

$S_1$ and $S_2$ describe the same interpretation if and only if for each predicate $P \in \Pi(N)$ of arity $n$, we have $\forall x_1 \dots \forall x_n. P^{S_1}(\vec{x}) \leftrightarrow P^{S_2}(\vec{x})$.
# 4 Conclusion

We have presented the first model construction approach to Horn clauses with linear arithmetic constraints based on hierarchic ordered resolution, (cf. Definition 19). The linear arithmetic constraints may range over the reals, rationals, or integers. The computed model is the canonical least model of the saturated Horn clause set (cf. Theorem 31). Clauses can be effectively evaluated with respect to the model (cf. Proposition 14). This offers a way to explore the properties of a saturated clause set, e.g., if the set represents a failed refutation attempt.

**Future Work** It is straightforward to see that any symbolic LQA model is also a symbolic LRA model. (This holds due to convexity of conjunctions of ground LQA atoms.) So even if the axiom of choice is not assumed, there is an alternative way to obtain a model for a HBS(LRA) clause set: Simply treat it as an HBS(LQA) clause set, saturate it and construct its model based on HBS(LQA).

In this work, we restrict ourselves to only one sort LA per set of clauses. An extension to a many-sorted setup, e.g. including first-order variables with sort $\mathcal{F}$ is possible. This can even be simulated, by encoding first-order constants as concrete natural numbers via a bijection to $\mathbb{N}$, since $\mathbb{N} \subset \mathcal{U}$. By not placing any arithmetic constraints on the variables used for the encoding, it can be read off and mapped back from the resulting model.

One obvious challenge is relaxation of the restriction to Horn clauses. With respect to ordered resolution saturation there is typically no difference in the sense that if a Horn fragment can always be finitely saturated, so can the non-Horn fragment be. However, our proposed ordering for the model construction at the granularity of predicate symbols will not suffice in this general case, and the key to overcome this challenge seems to be the appropriate treatment of clauses with maximal literals of the same predicate. Backtracking on the selection of literals might also be sufficient.

The approach we presented does not exploit features of linear arithmetic beyond equality and the existence of a well-founded order for the underlying universe $\mathcal{U}$. The results may therefore be adapted to other constraint domains such as non-linear arithmetic.

**Acknowledgements** We thank our reviewers for their constructive comments.
References

[1] Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: FroCoS 2009. LNCS, vol. 5749, pp. 84–99. Springer (2009). doi:10.1007/978-3-642-04222-5_5

[2] Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC’93, Brno, Czech Republic, August 24-27, 1993, Proceedings. LNCS, vol. 713, pp. 83–96. Springer (1993). doi:10.1007/BFb0022557

[3] Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. AAECC 5, 193–212 (1994). doi:10.1007/BF01190829

[4] Basin, D.A., Ganzinger, H.: Automated complexity analysis based on ordered resolution. JACM 48(1), 70–109 (2001). doi:10.1145/363647.363681

[5] Baumgartner, P., Fuchs, A., Tinelli, C.: (LIA) - model evolution with linear integer arithmetic constraints. In: LPAR 2008. LNCS, vol. 5330, pp. 258–273. Springer (2008). doi:10.1007/978-3-540-89439-1_19

[6] Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday. LNCS, vol. 11560, pp. 15–56. Springer (2019). doi:10.1007/978-3-030-22102-7_2

[7] Bjørner, N.S., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. LNCS, vol. 9300, pp. 24–51. Springer (2015). doi:10.1007/978-3-319-23534-9_2

[8] Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., González, L., Krötzsch, M., Marx, M., Murali, H.K., Weidenbach, C.: A sorted catalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: TACAS 2022 as part of ETAPS 2022. LNCS, vol. 13243, pp. 480–501. Springer (2022). doi:10.1007/978-3-030-99524-9_27

[9] Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Krötzsch, M., Weidenbach, C.: A catalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: FroCoS 2021. LNCS, vol. 12941, pp. 3–24. Springer (2021). doi:10.1007/978-3-030-86205-3_1

[10] Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the bernays-schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: VMCAI 2021. LNCS, vol. 12597, pp. 511–533. Springer (2021). doi:10.1007/978-3-030-67067-2_23

[11] Bromberger, M., Leutgeb, L., Weidenbach, C.: An efficient subsumption test pipeline for BS(LRA) clauses. In: IJCAR 2022. LNCS, vol. 13385, pp. 147–168. Springer (2022). doi:10.1007/978-3-031-10769-6_10
[12] Bromberger, M., Leutgeb, L., Weidenbach, C.: Symbolic model construction for saturated constrained horn clauses. arXiv (2023). doi:10.48550/arXiv.2305.05064

[13] Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building, APLS, vol. 31. Springer (2004). doi:10.1007/978-1-4020-2653-9

[14] Cooper, D.C.: Theorem proving in arithmetic without multiplication. Machine Intelligence **7**, 91–99 (1972)

[15] De Angelis, E., Fioravanti, F., Gallagher, J.P., Hermenegildo, M.V., Pettorossi, A., Proietti, M.: Analysis and transformation of constrained horn clauses for program verification. TPLP **22**(6), 974–1042 (2022). doi:10.1017/S1471068421000211

[16] Downey, P.J.: Undecidability of presburger arithmetic with a single monadic predicate letter. Tech. rep., Center for Research in Computer Technology, Harvard University (1972)

[17] Fedyukovich, G., Zhang, Y., Gupta, A.: Syntax-guided termination analysis. In: CAV 2018. LNCS, vol. 10981, pp. 124–143. Springer (2018). doi:10.1007/978-3-319-96145-3_7

[18] Feferman, S.: Some applications of the notions of forcing and generic sets. Fundamenta Mathematicae **56**(3), 325–345 (1964), http://eudml.org/doc/213821

[19] Fermüller, C.G., Leitsch, A.: Hyperresolution and automated model building. LOGCOM **6**(2), 173–203 (1996). doi:10.1093/logcom/6.2.173

[20] Fermüller, C.G., Leitsch, A.: Decision procedures and model building in equational clause logic. IGPL **6**(1), 17–41 (1998). doi:10.1093/jigpal/6.1.17

[21] Fiori, A., Weidenbach, C.: SCL with theory constraints. arXiv (2020), https://arxiv.org/abs/2003.04627

[22] Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Horn clauses as an intermediate representation for program analysis and transformation. TPLP **15**(4-5), 526–542 (2015). doi:10.1017/S1471068415000204

[23] Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th LICS, 1999. pp. 295–303. IEEE Computer Society (1999). doi:10.1109/LICS.1999.782624

[24] Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: PLDI. pp. 405–416. ACM (2012). doi:10.1145/2254064.2254112

[25] Hoder, K., Bjørner, N.S.: Generalized property directed reachability. In: SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer (2012). doi:10.1007/978-3-642-31612-8_13
[26] Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable. arXiv (2017), http://arxiv.org/abs/1703.01212

[27] Jaffar, J., Maher, M.J.: Constraint logic programming: A survey. JLP 19/20, 503–581 (1994). doi:10.1016/0743-1066(94)90033-7

[28] Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. In: CAV 2014 as part of VSL 2014. LNCS, vol. 8559, pp. 17–34. Springer (2014). doi:10.1007/978-3-319-08867-9_2

[29] Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: CSL 2007. LNCS, vol. 4646, pp. 223–237. Springer (2007). doi:10.1007/978-3-540-74915-8_19

[30] Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Saarland University (2013), http://scidok.sulb.uni-saarland.de/volltexte/2013/5559/

[31] Lloyd, J.W.: Foundations of Logic Programming, 2nd Edition. Springer (1987). doi:10.1007/978-3-642-83189-8

[32] Loos, R., Weispfenning, V.: Applying linear quantifier elimination. The Computer Journal 36(5), 450–462 (1993). doi:10.1093/comjnl/36.5.450

[33] López-García, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F., Hermenegildo, M.V.: Interval-based resource usage verification by translation into horn clauses and an application to energy consumption. TPLP 18(2), 167–223 (2018). doi:10.1017/S1471068418000042

[34] McMillan, K.L.: Lazy annotation revisited. In: CAV 2014 as part of VSL 2014. LNCS, vol. 8559, pp. 243–259. Springer (2014). doi:10.1007/978-3-319-08867-9_16

[35] Mesnard, F., Payet, É., Vidal, G.: Concolic testing in CLP. TPLP 20(5), 671–686 (2020). doi:10.1017/S1471068420000216

[36] Oppen, D.C.: A 2^2^2^pn upper bound on the complexity of presburger arithmetic. JCSS 16(3), 323–332 (1978). doi:10.1016/0022-0000(78)90021-1

[37] Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: LPAR 2008. LNCS, vol. 5330, pp. 274–289. Springer (2008). doi:10.1007/978-3-540-89439-1_20

[38] Spoto, F., Mesnard, F., Payet, É.: A termination analyzer for java bytecode based on path-length. TOPLAS 32(3), 8:1–8:70 (2010). doi:10.1145/1709093.1709095

[39] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285 – 309 (1955). doi:pjm/1103044538
[40] Weidenbach, C.: Automated reasoning building blocks. In: Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. LNCS, vol. 9360, pp. 172–188. Springer (2015).
doi:10.1007/978-3-319-23506-6_12