On the Expressivity and Applicability of Model Representation Formalisms

TL;DR

This paper investigates the limitations and capabilities of various model representation formalisms in automated reasoning, establishing a finite model property for certain classes and proposing an approximation method to handle infinite models.

Contribution

It proves a finite model property for MSLH clause sets and introduces a novel approximation called reflexive relation splitting for satisfiability checking.

Findings

MSLH clause sets cannot represent inherently infinite models.

Translation to tree automata extends the finite model property to other formalisms.

Reflexive relation splitting enables automatic satisfiability detection for certain infinite models.

Abstract

A number of first-order calculi employ an explicit model representation formalism for automated reasoning and for detecting satisfiability. Many of these formalisms can represent infinite Herbrand models. The first-order fragment of monadic, shallow, linear, Horn (MSLH) clauses, is such a formalism used in the approximation refinement calculus. Our first result is a finite model property for MSLH clause sets. Therefore, MSLH clause sets cannot represent models of clause sets with inherently infinite models. Through a translation to tree automata, we further show that this limitation also applies to the linear fragments of implicit generalizations, which is the formalism used in the model-evolution calculus, to atoms with disequality constraints, the formalisms used in the non-redundant clause learning calculus (NRCL), and to atoms with membership constraints, a formalism used for example in decision procedures for algebraic data types. Although these formalisms cannot represent models of clause sets with inherently infinite models, through an additional approximation step they can. This is our second main result. For clause sets including the definition of an equivalence relation with the help of an additional, novel approximation, called reflexive relation splitting, the approximation refinement calculus can automatically show satisfiability through the MSLH clause set formalism.

Equations

$$\begin{array}[]{rcl}N_{C}&:=&\bigcup_{D\prec C}\delta_{D}\\ \delta_{D}&:=&\left\{\begin{array}[]{ll}\{P(t_{1},\ldots,t_{n})\}&\mbox{if}\;D=D^{\prime}\lor P(t_{1},\ldots,t_{n}),P(t_{1},\ldots,t_{n})\;\mbox{strictly maximal,}\\ &\mbox{no literal selected in}\;D\;\mbox{and}\;N_{D}\not\models D\\ \emptyset&\mbox{otherwise}\\ \end{array}\right.\\ N_{\cal I}&:=&\bigcup_{C\in N}\delta_{C}\\ \end{array}$$

$$N:=\{$$

$$\neg P(u)\vee \neg P(u^{\prime })\vee P(f(u,u^{\prime })),\neg Q(v)\vee \neg Q(v^{\prime })\vee Q(f(v,v^{\prime })),$$

$$\neg P(x)\vee R(f(x,y)),\neg P(y)\vee R(f(x,y)),$$

$$\neg Q(x)\vee R(f(x,y)),\neg Q(y)\vee R(f(x,y))\}.$$

$$P^{\mathcal{H}}$$

$$Q^{\mathcal{H}}$$

$$R^{\mathcal{H}}$$

$$\mathcal{A}(\gamma )(g(r_1,\dots ,r_k)$$

$$\displaystyle\stackrel{{\scriptstyle\text{IH}}}{{=}}g^{\mathcal{A}}\bigl{(}\bigl{[}\mathcal{H}(\beta)(r_{1})\bigr{]}_{\sim},\ldots,\bigl{[}\mathcal{H}(\beta)(r_{k})\bigr{]}_{\sim}\bigr{)}$$

$$\displaystyle=\bigl{[}g\bigl{(}\mathcal{H}(\beta)(r_{1}),\ldots,\mathcal{H}(\beta)(r_{k})\bigr{)}\bigr{]}_{\sim}$$

$$\displaystyle=\bigl{[}\mathcal{H}(\beta)\bigl{(}g(r_{1},\ldots,r_{k})\bigr{)}\bigr{]}_{\sim}~{}.\qed$$

$$\begin{array}{rl}& \to R(x,x)\\ R(x,y)& \to R(y,x)\\ R(x,y),R(y,z)& \to R(x,z)\end{array}$$

$$\begin{array}{rl}& \to R_{\text{ref}}(x,x)\\ R_{\text{irr}}(x,y)& \to R_{\text{irr}}(y,x)\\ R_{\text{ref}}(x,x)& \to R_{\text{ref}}(x,x)\\ R_{\text{irr}}(x,y),R_{\text{irr}}(y,z)& \to R_{\text{irr}}(x,z)\\ R_{\text{irr}}(x,y),R_{\text{irr}}(y,x)& \to R_{\text{ref}}(x,x)\\ R_{\text{irr}}(x,y),R_{\text{ref}}(y,y)& \to R_{\text{irr}}(x,y)\\ R_{\text{ref}}(x,x),R_{\text{irr}}(x,z)& \to R_{\text{irr}}(x,z)\\ R_{\text{ref}}(x,x),R_{\text{ref}}(x,x)& \to R_{\text{ref}}(x,x).\end{array}$$

$$\begin{array}{rl}& \to R_{\text{ref}}(x,x)\\ R_{\text{irr}}(x,y)& \to R_{\text{irr}}(y,x)\\ R_{\text{irr}}(x,y),R_{\text{irr}}(y,z)& \to R_{\text{irr}}(x,z)\end{array}$$

$$\begin{array}{rl}R(x,x)& \to \\ & \to R(x,g(x))\\ R(x,y),R(y,z)& \to R(x,z).\end{array}$$

$$\begin{array}{rl}{R}_{\text{ref}}(x,x)& \to \\ & \to R_{\text{irr}}(x,g(x))\\ R_{\text{irr}}(x,y),R_{\text{irr}}(y,z)& \to R_{\text{irr}}(x,z)\\ R_{\text{irr}}(x,y),R_{\text{irr}}(y,x)& \to R_{\text{ref}}(x,x)\end{array}$$

Full text

1 Introduction

Proving satisfiability of a first-order clause set is more difficult than proving unsatisfiability, in general. Still, for many applications the detection of failing refutations by establishing a counter model is more than desirable. In the past, several methods, calculi and systems have been presented that can detect satisfiability of a clause set, in particular, if there is a finite model that is not too large. The approaches can be separated into the following classes:

1. (1)

the model building is integrated into a first-order calculus or a decision procedure forsome fragment, directly operating on the first-order clause set, complete for unsatisfiability, e.g., [7, 3, 18, 22, 1, 5, 6], 2. (2)

the model building is integrated into a first-order calculus that operates on the first-order clause set modulo an approximation, complete for unsatisfiability, e.g., [15, 24, 13], 3. (3)

the model building aims at finding finite models without being complete for unsatisfiability, e.g., [20, 16, 8], 4. (4)

the model building aims at finding finite and infinite models without being complete for unsatisfiability, e.g., [17],

where superposition [2] does not belong to any of the above classes, because the model building is implicit and reached by a finite saturation of the clause set modulo inferences and the elimination of redundant clauses.

The approaches in classes (1) and (2) select inferences with respect to the explicit (partial) model by identifying a false clause (instance). Therefore, the representation of models needs to be effective, e.g., falsity of a clause (instance) with respect to the model needs to be (efficiently) decidable. This is not the case for superposition, where this problem is undecidable. The clause set consisting of $R(\epsilon,\epsilon)$ and clauses $R(x,y)\rightarrow R(t_{i}[x],s_{i}[y])$ where the $t_{i},s_{i}$ are terms build over the monadic functions $g,h$ and variables $x$, $y$, respectively, is saturated with strictly maximal atoms $R(t_{i}[x],s_{i}[y])$ and can encode the words of a PCP [19] $({\tt w}_{1},\ldots,{\tt w}_{n})$, $({\tt v}_{1},\ldots,{\tt v}_{n})$ over letters $g,h$. That means words are represented by nestings of monadic functions. The PCP has a solution iff a ground atom $R(g(t),g(t))$ or $R(h(t),h(t))$ is a consequence of the above clause set. This corresponds to testing whether one of the clauses $R(g(x),g(x))$ or $R(h(x),h(x))$ has a false instance with respect to the model generated by the superposition model operator.

Reasoning with respect to a (partial) model assumption has advantages. The superposition completeness proof shows that an inference with a clause that is false in the current partial model is not redundant [2]. This has meanwhile also been shown for the CDCL [27] and the NRCL [1] calculus. The non-redundant inference property might also hold for other calculi of classes (1) and (2).

Our first contribution is showing that the model representation used in [24], monadic shallow linear Horn clauses (MSLH) has the finite model property, Section 3. This means that if a finite MSLH clause set has a model, it also has a finite model. Hence, MSLH clause sets cannot be used directly to represent models of clause sets with inherently infinite models. A further consequence is that any calculus in class (1), where the model representation can be represented by an MSLH clause set, cannot terminate on clause sets with inherently infinite models. A more detailed discussion of this aspect is contained in Section 4.

The fact that MSLH clause sets have the finite model property does not mean that the approximation refinement (AR) calculus presented in [24] cannot be used for finding infinite models of clause sets with inherently infinite models. The reason is that the MSLH model representation in [24] does not directly relate to the clause set, but via an approximation. For the approximation it is shown in a constructive way that it preserves satisfiability. This is done modulo the minimal Herbrand model of a saturated MSLH clause set. Such Herbrand models become infinite as soon as there are non-constant function symbols. So the question is whether AR can actually terminate on clause sets with inherently infinite models. In Section 5, we show that this is the case for certain classes of such clause sets relying on reflexivity of a binary (equivalence) relation. The technique we propose is an additional approximation called reflexive relation splitting. A similar relationship between a clause set and its approximation was already observed in [17] where an approximation of a first-order clause set into a class of tree automata is used in order to find finite and infinite models.

Our results concerning the MSLH fragment and the reflexive relation splitting modulo the AR calculus can be demonstrated by the following example. Consider the following three clauses defining a reflexive binary relation $R$ (see [7], page 55 for further discussion of this example).

$\{R(x,x),\quad R(g(x),g(y))\rightarrow R(x,y),\quad\neg R(g(x),c)\}$

The clause set has only infinite models. No resolution inference between $R(x,x)$ and $\neg R(g(x),c)$ is possible. Following the AR approach [24], the MSLH clause set

$\{T(f_{R}(x,y)),\quad T(f_{R}(g(x),g(y)))\rightarrow T(f_{R}(x,y)),\quad\neg T(f_{R}(g(x),c))\}$

is generated. We write unit clauses as single literals, and non-unit clauses as implications. The relation $R$ is translated into a binary function $f_{R}$ over a monadic predicate $T$. The approximation is the replacement of $R(x,x)$ by $T(f_{R}(x,y))$, where now the connection between the non-linear occurrences of $x$ is lost. As a consequence, a refutation containing a resolution step between $T(f_{R}(x,y))$ and $\neg T(f_{R}(g(x),c))$ with substitution $\{x\mapsto g(v),y\mapsto c\}$ is possible, which cannot be lifted to the original clause set because $g(v)$ and $c$ are not unifiable. The refinement then excludes this particular instance by generating $R(g(x),g(x))$, however, after approximating this clause, the empty clause can be derived again. This time the derivation also uses the second clause, where the substitution instance of the refutation contains one further nesting of $g$. The approximation refinement approach does not terminate on this example.

Obviously, if in the approximation the inference between $T(f_{R}(x,x))$ and $\neg T(f_{R}(g(x),c))$ can be blocked, saturation will terminate without finding a contradiction. As said, in the original clause set this inference is not possible, because of the non-linear occurrence of $x$. Now the idea is to split the relation $R$ into its reflexive and irreflexive part, denoted by the two predicates $R_{\text{ref}}$ and $R_{\text{irr}}$, respectively. The original clause set is satisfiable if and only if the following clause set is satisfiable

$\{R_{\text{ref}}(x,x),\quad R_{\text{irr}}(g(x),g(y))\rightarrow R_{\text{irr}}(x,y),\quad\neg R_{\text{irr}}(g(x),c)\}$,

details are explained in Section 5. After approximation it becomes

$\{T(f_{R_{\text{ref}}}(x,y))^{*},T(f_{R_{\text{irr}}}(g(x),g(y)))^{+}\rightarrow T(f_{R_{\text{irr}}}(x,y)),\neg T(f_{R_{\text{irr}}}(g(x),c))^{*}\}$ ($\dagger$)

where ∗ highlights maximal and + selected literals of the ordered resolution calculus used to decide MSLH clauses [23, 24]. There are no possible inferences generating further clauses, i.e. the set is already saturated.

The infinite minimal Herbrand model is $\mathcal{I}=\{T(f_{R_{\text{ref}}}(g^{i}(c),g^{j}(c)))\mid i,j\geq 0\}$ which is also a model for the clause set before approximation [23, 24] by simply undoing the shift of $R_{\text{irr}}$, $R_{\text{ref}}$ to the function level: $\mathcal{I}=\{R_{\text{ref}}(g^{i}(c),g^{j}(c)))\mid i,j\geq 0\}$. Nestings of functions in the Herbrand model representing relations, e.g., $f_{R_{\text{ref}}}$, can be prevented by adding further MSLH clauses. We omit these here for simplicity. This model can then be translated, see the proof of Lemma 10, into the Herbrand model $\mathcal{I}=\{R(g^{i}(c),g^{i}(c)))\mid i\geq 0\}$ of the original clause set.

In Section 3, we prove a finite model for saturated, satisfiable MSLH clause sets. For the example, see ($\dagger$), the thus constructed model has the domain $\mathsf{A}:=\{\mathsf{a}_{c},\mathsf{a}^{(1)},\mathsf{a}^{(2)},\mathsf{a}^{(3)},\mathsf{b}^{(1)},$ $\mathsf{b}^{(2)},\mathsf{b}^{(3)}\}$. The predicate $T$ is interpreted with the set $\{\mathsf{b}^{(1)},\mathsf{b}^{(2)},\mathsf{b}^{(3)}\}$. For the constant $c$ we use the distinguished element $\mathsf{a}_{c}$. The interpretation of the function $f_{R_{\text{ref}}}$ is given in the following function table:

\begin{array}[]{c@{\hspace{5ex}}r@{\;}c@{\;}c@{\hspace{3ex}}l}\hfil\hskip 21.52771pt&\langle\mathsf{a}_{c},\mathsf{a}_{c}\rangle&\longmapsto&\mathsf{b}^{(1)}\hfil\hskip 12.91663pt\\ \hfil\hskip 21.52771pt&\langle\mathsf{a}^{(i)},\mathsf{a}^{(i)}\rangle&\longmapsto&\mathsf{b}^{(j)}\hfil\hskip 12.91663pt&\text{for every i$and some$j\neq i}\\ \hfil\hskip 21.52771pt&\langle\mathsf{b}^{(i)},\mathsf{b}^{(i)}\rangle&\longmapsto&\mathsf{b}^{(j)}\hfil\hskip 12.91663pt&\text{for every i$and some$j\neq i}\\ \hfil\hskip 21.52771pt&\langle\mathsf{c},\mathsf{d}\rangle&\longmapsto&\mathsf{a}^{(j)}\hfil\hskip 12.91663pt&\text{for any \mathsf{c},\mathsf{d}\in\mathsf{A}$with$\mathsf{c}\neq\mathsf{d}and}\\ \hfil\hskip 21.52771pt&&&\hfil\hskip 12.91663pt&\text{somej$chosen such that for any$i,}\\ \hfil\hskip 21.52771pt&&&\hfil\hskip 12.91663pt&\text{if \mathsf{c}$or$\mathsf{d}$is equal to$\mathsf{a}^{(i)}$or$\mathsf{b}^{(i)}$, then$j\neq i}\end{array}

For the function $f_{R_{\text{irr}}}$ we get a similar function table in which every pair $\langle\mathsf{c},\mathsf{d}\rangle$ is mapped to some $\mathsf{a}^{(j)}$, where $j$ is chosen such that $\mathsf{c},\mathsf{d}\neq\mathsf{a}^{(j)}$. Finally, the interpretation of the function $g$ is given by $g(\mathsf{a}_{c})=\mathsf{a}^{(1)}$, $g(\mathsf{a}^{(i)})=\mathsf{a}^{(j)}$ and $g(\mathsf{b}^{(i)})=\mathsf{a}^{(j)}$ for every $i$ and some $j\neq i$.

The paper is now organized as follows: after fixing some notions and notations, Section 2, the finite model property of MSLH clause sets is shown in Section 3. Consequences of this result for other model representation formalisms are discussed in Section 4. In Section 5 reflexive relation splitting is introduced and its application to AR investigated. The present paper ends with a discussion on the obtained results and future research directions, Section 6.

2 Preliminaries

We consider a standard first-order language without equality where letters $v,w,$ $x,y,z$ denote variables, $f,g,h$ functions, $a,b,c$ constants, $s,t$ terms, and Greek letters $\sigma,\tau,\rho$ are used for substitutions. $S,P,Q,R$ denote predicates, $A,B$ atoms, $E,K,L$ literals, $C,D$ clauses, $N$ clause sets and $\mathcal{V}$ sets of variables. The notation $[\neg]A$ denotes $A$ or its negation. The signature $\Sigma=(\mathcal{F},\mathcal{P})$ consists of two disjoint, non-empty, in general infinite sets of function and predicate symbols $\mathcal{F}$ and $\mathcal{P}$, respectively. The set of all terms over the variables in $\mathcal{V}$ is $\mathcal{T}(\mathcal{F},\mathcal{V})$. If there are no variables, then terms, literals and clauses are called ground, respectively. A substitution $\sigma$ is denoted by pairs $\{x\mapsto t\}$. A substitution $\sigma$ is a grounding substitution for a term, atom, literal, clause if the application of $\sigma$ yields a ground term, ground atom, ground literal, ground clause, respectively.

The set of free variables of an atom $A$ (term $t$, literal $L$, clause $C$) is denoted by $\operatorname{vars}(A)$ ($\operatorname{vars}(t),\operatorname{vars}(L),\operatorname{vars}(C)$). A predicate with exactly one argument is called monadic. A term is complex if it is not a variable and shallow if it is a constant, a variable, or of the form $f(x_{1},\ldots,x_{n})$. A term, atom is called linear if there are no duplicate variable occurrences.

A clause is a multiset of literals which we write as an implication $\Gamma\rightarrow\Delta$ where the atoms in the multiset $\Delta$ (the* succedent*) denote the positive literals and the atoms in the multiset $\Gamma$ (the antecedent) the negative literals. Alternatively, we write a clause also as a disjunction of its literals. We write $\square$ for the empty clause. We abbreviate disjoint set union with sequencing, for example, we write $\Gamma,\Gamma^{\prime}\rightarrow\Delta,L$ instead of $\Gamma\cup\Gamma^{\prime}\rightarrow\Delta\cup\{L\}$. A clause $\Gamma\rightarrow\Delta$ is called an MSLH clause, if (i) $\Delta$ contains at most one atom, i.e., the clause is Horn, (ii) all occurring predicates are monadic, (iii) the argument of any monadic atom in $\Delta$ is shallow and linear. The first-order fragment consisting of finite MSLH clause sets we call MSLH.

An atom ordering $\prec$ is an irreflexive, well-founded, total ordering on ground atoms. It is lifted to literals by defining $A\prec\neg A\prec B$ for any atoms $A$, $B$ with $A\prec B$. It is lifted to clauses by its multiset extension. The ordering is lifted from the ground level through ground instantiation: for two different atoms $A$, $B$ containing variables, $A\prec B$ if $A\sigma\prec B\sigma$ for all grounding substitutions $\sigma$ and the atoms are incomparable otherwise. A literal $L$ is maximal (strictly maximal) in a clause $C\lor L$ if there is no literal $K\in C$ with $L\prec K$ ($L\preceq K$). The clause ordering is compatible with the atom ordering; if the maximal atom in $C$ is greater than the maximal atom in $D$ then $D\prec C$. We use $\prec$ simultaneously to denote an atom ordering and its multiset, literal, and clause extensions. For a ground clause set $N$ and clause $C$, the set $N^{\prec C}=\{D\in N\mid D\prec C\}$ denotes the clauses of $N$ smaller than $C$.

As usual, we interpret atoms, clauses, and clause sets with respect to structures $\mathcal{A}$, also called interpretations, consisting of a nonempty universe $\mathsf{A}$ and interpretations $c^{\mathcal{A}}$, $f^{\mathcal{A}}$, and $P^{\mathcal{A}}$ of all occurring constants, functions, and predicates. We often use a special kind of interpretations, called Herbrand interpretations, whose universe is the set of all ground terms. A Herbrand interpretation $\mathcal{I}$ is represented by a – possibly infinite – set of ground atoms. A ground atom $A$ is true in $\mathcal{I}$ if $A\in\mathcal{I}$ and false, otherwise. $\mathcal{I}$ is said to satisfy a ground clause $C=\Gamma\rightarrow\Delta$, denoted by $\mathcal{I}\vDash C$, if $\Delta\cap\mathcal{I}\neq\emptyset$ or $\Gamma\not\subseteq\mathcal{I}$. A non-ground clause $C$ is satisfied by $\mathcal{I}$ if $\mathcal{I}\vDash C\sigma$ for every grounding substitution $\sigma$. An interpretation $\mathcal{I}$ is called a model of $N$, $\mathcal{I}\vDash N$, if $\mathcal{I}\vDash C$ for every $C\in N$. A Herbrand model $\mathcal{I}$ of $N$ is considered minimal (with respect to set inclusion) if there is no model $\mathcal{I}^{\prime}$ with $\mathcal{I}^{\prime}\subset\mathcal{I}$ and $\mathcal{I}^{\prime}\vDash N$. A set of clauses $N$ is satisfiable, if there exists a model that satisfies $N$. Otherwise, the set is unsatisfiable.

The superpositon calculus [2] restricted to first-order logic without equality results in the ordered resolution calculus together with the superposition redundancy criterion and partial model operator. For ordered resolution, a selection function is assumed that may select negative literals in clauses. Then $(C\lor D)\sigma$ is an ordered resolution inference between a clause $C\lor A$ and a clause $D\lor\neg B$, if (i) $\sigma$ is the mgu between $A$ and $B$, (ii) $A\sigma$ is strictly maximal in $(C\lor A)\sigma$ and nothing is selected in $C\lor A$, (iii) $\neg B\sigma$ is maximal in $(D\lor\neg B)\sigma$ or selected. The clause $(C\lor A)\sigma$ is an ordered factoring inference on a clause $C\lor A\lor A^{\prime}$, if (i) $\sigma$ is the mgu between $A$ and $A^{\prime}$, (ii) $A\sigma$ is maximal in $(C\lor A)\sigma$ and nothing is selected in $C\lor A\lor A^{\prime}$. Selection is stable under instantiation, i.e., if $\neg A$ is selected in $\neg A\lor C$ it is also selected in $(\neg A\lor C)\sigma$, for any substitution $\sigma$. A clause $C$ is redundant with respect to a clause set $N$, if for all ground instances $C\sigma$ there are ground instances $D_{1}\sigma_{1},\ldots,D_{n}\sigma_{n}$, $\{D_{1},\ldots,D_{n}\}\subseteq N$, $D_{i}\sigma_{i}\prec C\sigma$ for all $i$, such that $D_{1}\sigma_{1},\ldots,D_{n}\sigma_{n}\models C\sigma$, i.e., $C\sigma$ is implied by smaller ground instances from clauses in $N$. A clause set $N$ is called saturated if all clauses generated by ordered resolution or ordered factoring from clauses in $N$ are either redundant or contained in $N$. Given a ground clause set $N$ and an ordering $\prec$ we can construct a (partial) Herbrand model $N_{\cal I}$ for $N$ by the superposition partial model operator inductively as follows:

[TABLE]

Clauses $C$ with $\delta_{C}\not=\emptyset$ are called productive. For a non-ground clause set $N$ we define N_{\cal I}:=(\{C\sigma\mid C\in N,\sigma\text{ grounding for C}\})_{\cal I}. The main completeness result of superposition is: for a clause set $N$ let $N^{*}$ be its (possibly infinite) saturation, then either $\square\in N^{*}$ and $N$ is unsatisfiable, or $N^{*}_{\cal I}\models N$ [2].

3 MSLH Model Properties

By definition, Herbrand models for MSLH clause sets with non-constant function symbols have an infinite domain. In what follows we show how to construct non-Herbrand models with finite domains for satisfiable finite MSLH clause sets. The constructed model is a finite representation of the minimal Herbrand model.

Consider a satisfiable finite MSLH clause set $N$. It is known that $N$ can be finitely saturated using superposition (ordered resolution) with an appropriate ordering and selection strategy such that the following property holds for the obtained saturated clause set $N^{*}$ [26]. Every clause $C$ in $N^{*}$ that is productive in the sense of the superposition model operator has the form $C=\;P_{1}(x_{1}),\ldots,P_{n}(x_{n})\rightarrow S(f(y_{1},\ldots,y_{m}))$ where $\{x_{1},\ldots,x_{n}\}\subseteq\{y_{1},\ldots,y_{m}\}$,$f(y_{1},\ldots,y_{m})$ is linear, and $S(f(y_{1},\ldots,y_{m}))$ is strictly maximal in $C$. Such a saturation can, e.g., be obtained by choosing for $\prec$ a Knuth-Bendix-Ordering (KBO) with weight one for all function symbols, variables, and a selection strategy that selects a negative literal $P_{i}(t_{i})$ in any clause $P_{1}(t_{1}),\ldots,$ $P_{n}(t_{n})\rightarrow S(f(y_{1},\ldots,y_{m}))$ if $t_{i}$ is not a variable, if $t_{i}$ is a variable that does not occur in $f(y_{1},\ldots,y_{m})$, or if $t_{i}$ is a variable in a clause $P_{1}(x),\ldots,P_{n}(x)\rightarrow S(x)$ [26, 25].

Proposition 1** (Entailed by Lemma 4 from [26]).**

Consider a satisfiable finite MSLH clause set $N$. There is a finite MSLH clause set $N^{*}$ such that $N\subseteq N^{*}$ and $N\models N^{*}$ and there is a (minimal) Herbrand model $\mathcal{H}\models N^{*}$ such that for every ground atom $A$ of the form S\bigl{(}f(s_{1},\ldots,s_{m})\bigr{)} we have $\mathcal{H}\models A$ only if there is some clause $C$ in $N^{*}$ and a variable assignment $\beta$ with the following properties:

1. (a)

$C$ has the form P_{1}(x_{1}),\ldots,P_{n}(x_{n})\rightarrow S\bigl{(}f(y_{1},\ldots,y_{m})\bigr{)} where $\{x_{1},\ldots,x_{n}\}\subseteq\{y_{1},\ldots,y_{m}\}$, the $y_{1},\ldots,y_{m}$ are pairwise distinct, and $m,n\geq 0$; 2. (b)

we have $\beta(y_{i})=s_{i}$ for every $i$, $1\leq i\leq m$; and 3. (c)

we have $\mathcal{H},\beta\models P_{j}(x_{j})$ for every $j$, $1\leq j\leq n$.

Since $N^{*}$ is satisfiable and all its clauses are Horn, it possesses a unique minimal Herbrand model $\mathcal{H}$ (cf. [11], Chapter XI, Theorem 3.8). The property described in Proposition 1 provides the key to construct a finite model for $N$ and $N^{*}$ from $\mathcal{H}$. The following example is intended to illustrate the ideas underlying the construction in a simplified form.

Example 2**.**

Consider the following set of MSLH clauses with constants $a$ and $b$:

[TABLE]

The set $N$ is satisfied by the minimal Herbrand interpretation $\mathcal{H}$ with

[TABLE]

The interpretation $\mathcal{H}$, together with $N^{*}:=N$, satisfies the conditions of Proposition 1: for every term $f(s,t)$ that belongs to $R^{\mathcal{H}}$ we have that one of the clauses $\neg P(x)\vee R(f(x,y))$ or $\neg P(y)\vee R(f(x,y))$ or $\neg Q(x)\vee R(f(x,y))$ or $\neg Q(y)\vee R(f(x,y))$ enforces $\mathcal{H}\models R(f(s,t))$ because of $\mathcal{H}\models P(s)$ or $\mathcal{H}\models P(t)$ or $\mathcal{H}\models Q(s)$ or $\mathcal{H}\models Q(t)$, respectively. Similarly, the presence of any term $f(\ldots)$ in $P^{\mathcal{H}}$ or $Q^{\mathcal{H}}$ is enforced by one of the clauses $\neg P(u)\vee\neg P(u^{\prime})\vee P(f(u,u^{\prime}))$ or $\neg Q(v)\vee\neg Q(v^{\prime})\vee Q(f(v,v^{\prime}))$.

These requirements towards the minimality of $\mathcal{H}$ provide us with a certain knowledge about distinct terms $f(s,t)$ and $f(s^{\prime},t^{\prime})$. Suppose the terms $s$ and $s^{\prime}$ are indistinguishable with respect to their membership in $P^{\mathcal{H}},Q^{\mathcal{H}},R^{\mathcal{H}}$. Further suppose that the same holds for the terms $t$ and $t^{\prime}$. Then, $f(s,t)$ and $f(s^{\prime},t^{\prime})$ are also indistinguishable with respect to their belonging to $P^{\mathcal{H}},Q^{\mathcal{H}}$, and $R^{\mathcal{H}}$, because the arguments $s,t$ and $s^{\prime},t^{\prime}$ trigger the same productive clauses. A formal statement of this property is given in Lemma 3.

Based on this observation, we use $\mathcal{H}$ as a blueprint for a finite model $\mathcal{A}$, which is depicted in Figure 1. The domain of $\mathcal{A}$ shall be $\mathsf{A}:=\{\mathsf{a},\mathsf{b},\mathsf{c},\mathsf{d},\mathsf{e}\}$, and we set $a^{\mathcal{A}}:=\mathsf{a}$ and $b^{\mathcal{A}}:=\mathsf{b}$. The predicate symbols are interpreted by $P^{\mathcal{A}}:=\{\mathsf{a},\mathsf{c}\},Q^{\mathcal{A}}:=\{\mathsf{b},\mathsf{d}\},R^{\mathcal{A}}:=\{\mathsf{c},\mathsf{d},\mathsf{e}\}$. Moreover, we define

\begin{array}[]{l@{\hspace{5ex}}l@{\hspace{5ex}}l@{\hspace{5ex}}l}f^{\mathcal{A}}(\mathsf{a},\mathsf{a}):=\mathsf{c}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{a},\mathsf{c}):=\mathsf{c}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{c},\mathsf{a}):=\mathsf{c}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{c},\mathsf{c}):=\mathsf{c}\\ f^{\mathcal{A}}(\mathsf{b},\mathsf{b}):=\mathsf{d}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{b},\mathsf{d}):=\mathsf{d}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{d},\mathsf{b}):=\mathsf{d}\hfil\hskip 21.52771pt&f^{\mathcal{A}}(\mathsf{d},\mathsf{d}):=\mathsf{d}.\end{array}

For all other inputs, $f^{\mathcal{A}}$ shall yield $\mathsf{e}$ as output. Every domain element in $\mathsf{A}$ represents one equivalence class of the terms in $\mathcal{H}$’s Herbrand domain with respect to membership in the sets $P^{\mathcal{H}}$, $Q^{\mathcal{H}}$, and $R^{\mathcal{H}}$. The domain element $\mathsf{a}$ represents the class $[a]:=\{a\}$ of terms that belong to $P^{\mathcal{H}}$ and to no other set. Similarly, $\mathsf{b}$ represents $[b]:=\{b\}$ of terms that belong to $Q^{\mathcal{H}}$ and to no other set. The element $\mathsf{c}$ represents the class of all terms belonging to $P^{\mathcal{H}}\cap R^{\mathcal{H}}$, i.e. to the class containing $f(a,a),f(a,f(a,a))$ and so on. The class of terms belonging to $Q^{\mathcal{H}}\cap R^{\mathcal{H}}$ is represented by $\mathsf{d}$. Finally, $\mathsf{e}$ corresponds to the class of all terms that are member of $R^{\mathcal{H}}$ but of none of the other predicates, e.g. $f(a,b),f(a,f(b,a))$.

Next, we describe formally how to construct a finite model for the given satisfiable and finite MSLH clause set $N$. Let $N^{*}$ and $\mathcal{H}$ be the objects described in Proposition 1. Then, we have $\mathcal{H}\models N^{*}$ and $\mathcal{H}\models N$. Let $\mathsf{H}$ be the domain of $\mathcal{H}$, i.e. $\mathsf{H}$ is the set of all ground terms over the vocabulary underlying $N$. We aim at constructing a finite model $\mathcal{A}\models N$ starting from $\mathcal{H}$.

Let $\Pi$ denote the set of all predicates occurring in $N$, and recall that $\Pi$ contains only unary predicate symbols. Let $\sim$ be the equivalence relation on $\mathsf{H}$ such that $s\sim t$ holds if and only if we have for every $P\in\Pi$ that $\mathcal{H}\models P(s)$ if and only if $\mathcal{H}\models P(t)$.

Lemma 3**.**

For every non-constant function symbol $f$ in $N$ of arity $m$ and all tuples $\langle s_{1},\ldots,s_{m}\rangle,$ $\langle t_{1},\ldots,t_{m}\rangle\in\mathsf{H}^{m}$ for which $s_{i}\sim t_{i}$ holds for every $i$ we have $f(s_{1},\ldots,s_{m})\sim f(t_{1},\ldots,t_{m})$.

Proof.

By Definition of $\mathcal{H}$, \mathcal{H}\models S\bigl{(}f(s_{1},\ldots,s_{m})\bigr{)} entails that there is a clause $C$ of the form \neg P_{1}(x_{1})\vee\ldots\vee\neg P_{n}(x_{n})\vee S\bigl{(}f(y_{1},\ldots,y_{m})\bigr{)} in $N^{*}$ and a variable assignment $\beta$ that satisfy Properties (a) to (c) from Proposition 1. Let $\gamma$ be a variable assignment for which we have $\gamma(y_{i}):=t_{i}$ for every $i$. Notice that such a $\gamma$ with \bigl{\langle}\gamma(y_{1}),\ldots,\gamma(y_{m})\bigr{\rangle}=\langle t_{1},\ldots,t_{m}\rangle always exists because the $y_{1},\ldots,y_{m}$ are pairwise distinct. Since we assume $s_{i}\sim t_{i}$ for every $i$ and because of $\{x_{1},\ldots,x_{n}\}\subseteq\{y_{1},\ldots,y_{m}\}$, Conditions (b) and (c) of Proposition 1 stipulate for every $j$ that $\beta(x_{j})\in P_{j}^{\mathcal{H}}$ and, hence, we also have $\gamma(x_{j})\in P_{j}^{\mathcal{H}}$. Since $\mathcal{H}$ is a model of $N^{*}$, we have $\mathcal{H},\gamma\models C$. This together with $\mathcal{H},\gamma\models P_{j}(x_{j})$, for every $j$, entails $\mathcal{H},\gamma\models S(f(y_{1},\ldots,y_{m}))$. Put differently, we have \mathcal{H}\models S\bigl{(}f(t_{1},\ldots,t_{m})\bigr{)}.

Consequently, for every $S$ we observe that \mathcal{H}\models S\bigl{(}f(s_{1},\ldots,s_{m})\bigr{)} entails \mathcal{H}\models S\bigl{(}f(t_{1},\ldots,t_{m})\bigr{)}. The converse direction can be shown by a symmetric argument. ∎

We now construct the finite structure $\mathcal{A}$. The universe of $\mathcal{A}$ shall be \mathsf{A}:=\mathsf{H}/_{\sim}:=\bigl{\{}[s]_{\sim}\mid s\in\mathsf{H}\bigr{\}}, where $[s]_{\sim}$ denotes the (unique) equivalence class with respect to $\sim$ which contains the term $s$. For every function symbol $f$ (including constants) we set f^{\mathcal{A}}\bigl{(}[s_{1}]_{\sim},\ldots,[s_{m}]_{\sim}\bigr{)}:=\bigl{[}f(s_{1},\ldots,s_{m})\bigr{]}_{\sim} for all ground terms $s_{1},\ldots,s_{m}$. Finally, we define each predicate $P$ under $\mathcal{A}$ by P^{\mathcal{A}}:=\bigl{\{}[s]_{\sim}\mid\mathcal{H}\models P(s)\bigr{\}}.

Lemma 4**.**

Let $\gamma$ be any variable assignment over $\mathcal{A}$’s domain. Let $\beta$ be some variable assignment over $\mathcal{H}$’s domain defined such that for every $x$ we have \gamma(x)=\bigl{[}\beta(x)\bigr{]}_{\sim}. By definition of $\mathcal{H}$, such a $\beta$ must exist. Then, for every term $t$ in $N$ and every predicate $P$ we have $\mathcal{A},\gamma\models P(t)$ if and only if $\mathcal{H},\beta\models P(t)$.

Proof.

We proceed by case distinction regarding the structure of the term $t$. If $t=x$ is a variable, then we have $\mathcal{A},\gamma\models P(x)$ if and only if \gamma(x)=\bigl{[}\beta(x)\bigr{]}_{\sim}\in P^{\mathcal{A}} if and only if $\beta(x)\in P^{\mathcal{H}}$ if and only if $\mathcal{H},\beta\models P(x)$. If $t=c$ is a constant, then we have $\mathcal{A},\gamma\models P(c)$ if and only if $c^{\mathcal{A}}=[c]_{\sim}\in P^{\mathcal{A}}$ if and only if $c\in P^{\mathcal{H}}$ if and only if $\mathcal{H},\beta\models P(c)$. Suppose $t=f(s_{1},\ldots,s_{m})$ for some function $f$ of arity $m\geq 1$ and terms $s_{1},\ldots,s_{m}$. Let $t_{1},\ldots,t_{m}$ be ground terms such that $\mathcal{A}(\gamma)(s_{i})=[t_{i}]_{\sim}$. Such terms exist by definition of $\mathcal{H}$. Then, we have \mathcal{A},\gamma\models P\bigl{(}f(s_{1},\ldots,s_{m})\bigr{)} if and only if f^{\mathcal{A}}\bigl{(}[t_{1}]_{\sim},\ldots,[t_{m}]_{\sim}\bigr{)}=\bigl{[}f(t_{1},\ldots,t_{m})\bigr{]}_{\sim}\in P^{\mathcal{A}} if and only if \mathcal{H}\models P\bigl{(}f(t_{1},\ldots,t_{m})\bigr{)}. A straightforward induction on the structure of the terms $s_{i}$ yields $t_{i}\sim\mathcal{H}(\beta)(s_{i})$ for every $i$ (see below). Then, by Lemma 3, we have \mathcal{H}\models P\bigl{(}f(t_{1},\ldots,t_{m})\bigr{)} if and only if \mathcal{H}\models P\bigl{(}f\bigl{(}\mathcal{H}(\beta)(s_{1}),\ldots,\mathcal{H}(\beta)(s_{m})\bigr{)}\bigr{)} if and only if \mathcal{H},\beta\models P\bigl{(}f(s_{1},\ldots,s_{m})\bigr{)}.

It remains to prove $t_{i}\sim\mathcal{H}(\beta)(s_{i})$ for any $i$ or, equivalently, A(\gamma)(s_{i})=\bigl{[}\mathcal{H}(\beta)(s_{i})\bigr{]}_{\sim}. We show the latter by induction on the structure of $s_{i}$. If $s_{i}=y$, we have \mathcal{A}(\gamma)(y)=\gamma(y)=[\beta(y)]_{\sim}=\bigl{[}\mathcal{H}(\beta)(y)\bigr{]}_{\sim}. If $s_{i}=c$, we have \mathcal{A}(\gamma)(c)=c^{\mathcal{A}}=[c]_{\sim}=\bigl{[}\mathcal{H}(\beta)(c)\bigr{]}_{\sim}. Let $s_{i}=g(r_{1},\ldots,r_{k})$. Then, we have

[TABLE]

For the special case of ground terms, there is a simpler form of Lemma 4:

Corollary 5**.**

For every ground term $t$ and every predicate symbol $P$ we have $\mathcal{A}\models P(t)$ if and only if $\mathcal{H}\models P(t)$.

Using Lemma 4, it is easy to show that $N$ is satisfied by the finite structure $\mathcal{A}$.

Lemma 6**.**

$\mathcal{A}$ is a model of $N$.

Proof.

Let $C$ be any clause in $N$. Since $N$ is satisfiable, $C$ cannot be the empty clause. Suppose there is some variable assignment $\gamma$ over $\mathcal{A}$’s domain such that $\mathcal{A},\gamma\not\models C$. Let $\beta$ be some variable assignment over $\mathcal{H}$’s domain defined such that $\gamma(x)=[\beta(x)]_{\sim}$ for every $x$. Such a $\beta$ must exist. Consider any atom $P(t)$ in $C$. By Lemma 4, we have $\mathcal{A},\gamma\models P(t)$ if and only if $\mathcal{H},\beta\models P(t)$. But then, $\mathcal{A},\gamma\not\models C$ entails $\mathcal{H},\beta\not\models C$. This contradicts our assumption that $\mathcal{H}$ is a model of $N$. Hence, we must have $\mathcal{A}\models C$. ∎

Theorem 7** (Finite Model Property for MSLH).**

Every satisfiable finite MSLH clause set $N$ has a finite model whose domain contains at most $2^{p}$ elements, where $p$ is the number of predicates in $N$.

4 Model Representation Formalisms

Many known explicit first-order model representation formalisms are build on sequences of literals, often enhanced with constraints, eventually representing Herbrand models, e.g., [3, 18, 5, 1, 6], so called constraints atomic representations (CARMs) [7]. A thorough discussion of all known CARM model representation formalisms is beyond the scope of this paper. We concentrate on three basic building blocks of known model representation formalisms: atoms with disequality constraints [7, 10] (ADCs), implicit generalizations [12] (IGs) and atoms with membership constraints [7, 9] (AMCs). They form the basis for a number of concrete model representation formalisms that actually appear in the above mentioned calculi. For this section we consider a fixed, finite signature $\Sigma=(\mathcal{F},\mathcal{P})$, e.g., the function and predicate symbols occurring in some finite clause set $N$. The results in this section for all three model representations will be the same: if terms, literals are linear, the models represented by the respective approaches have the finite model property. We will prove this as follows: (i) we provide an effective linear time translation of atoms with disequality constraints to implicit generalizations; (ii) we provide a linear time translation of implicit generalizations to intersections of tree automata [9] or complements thereof; (iii) we represent an atom with membership constraints by a tree automaton. Then, because tree automata are closed under intersection and complement, potentially causing an exponential blow up in size [9], the atoms generated by ADCs and IGs can also be represented by the accepted language of a single tree automaton. The accepted language of a tree automaton can be represented by a finite MSLH clause set, e.g., see [14]. Thus, by Theorem 7, linear ADCs, linear IGs, and linear AMCs have all the finite model property, i.e., they cannot represent models for clause sets with inherently infinite models.

A linear ADC has the form $(A\colon x_{1}\neq t_{1},\ldots,x_{n}\neq t_{n})$ where the $x_{i}$ are all different and occur in $A$, the $x_{i}$ do not occur in any $t_{j}$, the variables of the $t_{j}$ do not occur in $A$ and $A$ as well as all $t_{j}$ are linear. The ground atoms generated by such an ADC are all ground atoms $A\sigma$ such that there is no $\delta$ with $x_{i}\sigma=t_{i}\delta$ for some $i$. A linear IG is an expression $A/\{B_{1},\ldots,B_{n}\}$ where $A$ and the $B_{i}$ are linear atoms. Every ground instance of $A$ that is not an instance of any $B_{i}$ is generated by the IG $A/\{B_{1},\ldots,B_{n}\}$. The ground atoms generated by an ADC are exactly the ground atoms generated by the respective linear IG $A/\{A\{x_{1}\mapsto t_{1}\},\ldots,A\{x_{n}\mapsto t_{n}\}\}$.

A tree automaton consists of a finite set ${\cal Q}$ of states, a finite set ${\cal O}$ of operators, a subset of accepting states ${\cal Q}_{A}\subseteq{\cal Q}$, and a finite set of rules $f(q_{1}\ldots,q_{n})\mapsto q$ where $q,q_{i}\in{\cal Q}$, $f\in{\cal O}$. The accepted language of a tree automaton is inductively defined by $f(t_{1},\ldots,t_{n})\in q^{\cal A}$ if there is a rule $f(q_{1}\ldots,q_{n})\mapsto q$ and $t_{i}\in q_{i}^{\cal A}$ for all $i$. The overall accepted language is then $\bigcup\;\{q^{\cal A}\mid q\in{\cal Q}_{A}\}$.

For example, the ground instances of the linear atom $R(x,g(a,y))$ over signature $\Sigma=(\{g,a,b\},\{R\})$ is the accepted language of the tree automaton ${\cal O}=\{R,g,a,b\}$ with rules $a\mapsto q_{1}$, $b\mapsto q_{1}$, $g(q_{1},q_{1})\mapsto q_{1}$, hence state $q_{1}$ accepts all ground terms, $a\mapsto q_{2}$, $g(q_{2},q_{1})\mapsto q_{3}$, and $R(q_{1},q_{3})\mapsto q_{4}$ where $q_{4}$ is the only accepting state recognizing all ground instances of $R(x,g(a,y))$.

If $\operatorname{ta}$ is a function mapping linear atoms to a tree automata accepting the respective ground instances, then the ground atoms generated by an IG $A/\{B_{1},\ldots,$ $B_{n}\}$ are accepted by the tree automaton $\operatorname{ta}(A)\cap\neg\operatorname{ta}(B_{1})\cap\ldots\cap\neg\operatorname{ta}(B_{n})$. Recall that tree automata are closed under intersection ($\cap$) and complement ($\neg$), however the above tree automaton may be exponentially larger in size compared to the size of $\operatorname{ta}(A)$ and the $\operatorname{ta}(B_{i})$.

A linear atom with membership constraint $A\colon x\in S$ is the pair of a linear atom $A$ and a constraint $x\in S$ where $x$ occurs in $A$ and $S$ is represented by a tree automaton. It generates all ground instances $A\sigma$ where $x\sigma$ is accepted by the tree automaton representing $S$. There is a function $\operatorname{ta}(A\colon x\in S)$ that computes in linear time a tree automaton accepting exactly the generated ground instances of $A\colon x\in S$. Basically, the state(s) representing the instances of $x$ in $A$ in $\operatorname{ta}(A)$ have to be replaced by the accepting states of the tree automaton representing $S$.

Finally, tree automata can be straight forwardly represented via MSLH clause sets. For example, the tree automaton representing the ground instances of $R(x,g(a,y))$ shown before, can be translated into the MSLH clause set $\rightarrow Q_{1}(a)$, $\rightarrow Q_{1}(b)$, $Q_{1}(x),Q_{1}(y)\rightarrow Q_{1}(g(x,y))$, $\rightarrow Q_{2}(a)$, $Q_{2}(x),Q_{1}(y)\rightarrow Q_{3}(g(x,y))$, and $Q_{1}(x),Q_{3}(y)\rightarrow Q_{f}(f_{R}(x,y))$. This, together with Theorem 7, eventually proves the following theorem.

Theorem 8**.**

Linear disequality constraints (ADCs), linear implicit generalizations (IGs) and linear atoms with membership constraints (AMCs) have the finite model property.

This result can be easily generalized to any “Boolean combination” of linear ADCs, IGs, and AMCs, because tree automata are closed under Boolean operations. Our restriction on linearity does not imply that non-linear ADCs, IGs, and AMCs do not have the finite model property. This is an open problem. Non-linear MSLH clause sets do not have the finite model property, because they are as expressive as full first-order logic.

5 Model Finding by Approximation Refinement

The approximation refinement approach [24] cannot show satisfiability of the simple clause set with the two unit clauses

$R(x,x),\quad\neg R(y,g(y))$.

The approximated clause set consisting of the three clauses

$T(f_{R}(x,y)),\quad\neg S(z)\lor\neg T(f_{R}(y,z)),\quad S(g(y))$

immediately yields a refutation. The problem is that $R(x,x)$ cannot be refined in such a way that all instances of the conflict clause $\neg R(y,g(y))$ are excluded. The refinement loop instead ends up enumerating all $R(g^{i}(x),g^{i}(x))$ but $R(g^{i+1}(y),g^{i+2}(y))$ will always remain as a conflict clause.

The non-termination can be resolved, if the resolution inference in the abstracted clause set can be blocked. Our suggestion in case of reflexive relations is reflexive relation splitting, i.e., we split a reflexive relation into its reflexive part $R_{\text{ref}}$ and irreflexive part $R_{\text{irr}}$. For the example, this yields

$R_{\text{ref}}(x,x),\quad\neg R_{\text{irr}}(y,g(y))$

and after approximation

$T(f_{R_{\text{ref}}}(x,y)),\quad\neg S(z)\lor\neg T(f_{R_{\text{irr}}}(y,z)),\quad S(g(y))$.

Now the approximation is saturated. The operation preserves satisfiability because the two $R$ literals could not be resolved anyway.

In general, for each predicate $R$ with a reflexivity axiom, all occurrences of atoms $R(s,t)$ are replaced with $R_{\text{ref}}(s,t)$ and/or $R_{\text{irr}}(s,t)$. If $s$ and $t$ are not unifiable, $R(s,t)$ is replaced with $R_{\text{irr}}(s,t)$. If there is an mgu $\sigma$ of $s$ and $t$, $R(s,t)$ is replaced with both $R_{\text{ref}}(s\sigma,t\sigma)$ and $R_{\text{irr}}(s,t)$. More precisely, any clause $C\vee[\neg]R(s,t)$ is replaced by two clauses: $C\vee[\neg]R_{\text{irr}}(s,t)$ and $C\sigma\vee[\neg]R_{\text{ref}}(s\sigma,t\sigma)$. The process is repeated until all atom occurrences with $R$ have been replaced. In the final result, any clause that contains an atom of the form $R_{\text{irr}}(s,s)$ can be deleted.

More formally, the following transition system replaces a reflexive $R$ by the two new predicates.

Irreflexive

$N\uplus\{[\neg]R(s,t)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{irr}}(s,t)\lor C\}$

provided $s$ and $t$ are not unifiable

Reflexive

$N\uplus\{[\neg]R(s,t)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{irr}}(s,t)\lor C,[\neg]R_{\text{ref}}(s\sigma,t\sigma)\lor C\sigma\}$

provided $s$ and $t$ are unifiable by an mgu $\sigma$

Delete

$N\uplus\{[\neg]R_{\text{irr}}(s,s)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N$

Lemma 9**.**

$\Rightarrow_{\text{RRS}}$ is terminating and confluent.

Proof sketch.

Termination is easy to prove. Each application of the rules Irreflexive or Reflexive reduces the multiset of the numbers of $R$-occurrences in all clauses, and no new occurrences of $R$ are ever introduced when Delete is applied. Each application of the rule Delete reduces the number of occurrences of $R_{\text{irr}}$. Combining these two properties into a well-founded multi-set-based ordering completes the proof of termination. For local confluence, the non-obvious case is a clause $[\neg]R(s,t)\lor[\neg]R(s^{\prime},t^{\prime})\lor C$ where $R(s,t)$ and $R(s^{\prime},t^{\prime})$ share variables, and without loss of generality, $s$ and $t$ are unifiable by the mgu $\sigma$. Applying first the reflexive transformation to the first literal yields the two clauses $[\neg]R_{\text{ref}}(s\sigma,t\sigma)\lor[\neg]R(s^{\prime}\sigma,t^{\prime}\sigma)\lor C\sigma$ and $[\neg]R_{\text{irr}}(s,t)\lor[\neg]R(s^{\prime},t^{\prime})\lor C$. Now the interesting case is where $s^{\prime}$, $t^{\prime}$ are unifiable but $s^{\prime}\sigma$ and $t^{\prime}\sigma$ are not. Then we get with the mgu $\tau$ of $s^{\prime},t^{\prime}$: $[\neg]R_{\text{ref}}(s\sigma,t\sigma)\lor[\neg]R_{\text{irr}}(s^{\prime}\sigma,t^{\prime}\sigma)\lor C\sigma$, $[\neg]R_{\text{irr}}(s,t)\lor[\neg]R_{\text{irr}}(s^{\prime},t^{\prime})\lor C$, and $[\neg]R_{\text{irr}}(s\tau,t\tau)\lor[\neg]R_{\text{ref}}(s^{\prime}\tau,t^{\prime}\tau)\lor C\tau$. This is also exactly the result we get when starting with a translation of $[\neg]R(s^{\prime},t^{\prime})$: if $s^{\prime}\sigma,t^{\prime}\sigma$ are not unifiable, then $s\tau,t\tau$ are not unifiable as well. For otherwise, $s\tau\tau^{\prime},t\tau\tau^{\prime}$ for unifier $\tau^{\prime}$ is an instance of $s\sigma,t\sigma$, so $s^{\prime}\sigma,t^{\prime}\sigma$ must be unifiable as well, a contradiction to the above assumption. All other cases are similar to this case. By Newman’s Lemma, termination plus local confluence implies confluence. ∎

Given any finite clause set $N$, we write $\operatorname{rrs}(N)$ to address the normal form of $N$ after exhaustively applying $\Rightarrow_{\text{RRS}}$. Notice that any clause $D\in\operatorname{rrs}(N)$ is an instance of a clause in $N$ with respect to the renaming of $R_{\text{ref}}$, $R_{\text{irr}}$ with $R$. Moreover, we use $\operatorname{rrs}(C)$ as shorthand for $\operatorname{rrs}(\{C\})$ for any clause $C$.

Lemma 10** (Reflexive Relation Splitting).**

Let $N$ be a finite clause set that does not contain the predicates $R_{\text{ref}}$ and $R_{\text{irr}}$. $N$ is satisfiable if and only if $\operatorname{rrs}(N)$ is satisfiable.

Proof.

Since $\Rightarrow_{\text{RRS}}$ is confluent, we may assume that $\operatorname{rrs}(N)$ has been derived from $N$ by $\Rightarrow_{\text{RRS}}$ using a strategy that applies the rule Delete with priority. In other words, whenever there is some clause that may be deleted by Delete, we delete it at once. For the rest of the proof, we incorporate this strategy into the rewrite system. Hence, we pretend that $\Rightarrow_{\text{RRS}}$ comprises the following modified rules:

Irreflexive

$N\uplus\{[\neg]R(s,t)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{irr}}(s,t)\lor C\}$

provided $s$ and $t$ are not unifiable

Reflexive1

$N\uplus\{[\neg]R(s,t)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{irr}}(s,t)\lor C,[\neg]R_{\text{ref}}(s\sigma,t\sigma)\lor C\sigma\}$

provided $s$ and $t$ are distinct but unifiable by mgu $\sigma$ and $C\sigma$ does not contain any atom $R_{\text{irr}}(s^{\prime},s^{\prime})$

Reflexive2

$N\uplus\{[\neg]R(s,t)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{irr}}(s,t)\lor C\}$

provided $s$ and $t$ are distinct but unifiable by mgu $\sigma$ and $C\sigma$ contains some atom $R_{\text{irr}}(s^{\prime},s^{\prime})$

Reflexive3

$N\uplus\{[\neg]R(s,s)\lor C\}$ $\;\Rightarrow_{\operatorname{RRS}}\;$ $N\uplus\{[\neg]R_{\text{ref}}(s,s)\lor C\}$

We now prove the following auxiliary result:

Claim I: Let $N_{1},N_{2}$ be clause sets such that $N_{1}\Rightarrow_{\text{RRS}}N_{2}$. Moreover, let $\mathcal{I}$ be any Herbrand interpretation such that

(1) for every ground term $s$ we have $R_{\text{ref}}(s,s)\in\mathcal{I}$ if and only if $R(s,s)\in\mathcal{I}$,

(2) for all ground terms $s,t$ and all $R_{\text{ref}}(s,t)\in\mathcal{I}$ we have $s=t$,

(3) for all ground terms $s,t$ we have $R_{\text{irr}}(s,t)\in\mathcal{I}$ if and only if $R(s,t)\in\mathcal{I}$. Then, $\mathcal{I}\models N_{1}$ if and only if $\mathcal{I}\models N_{2}$.

Proof of Claim I: We distinguish three cases concerning the derivation step from $N_{1}$ to $N_{2}$, where the terms $s,t$ may be non-ground:

1. (a)

$N_{1}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R(s,t)\}$ and $N_{2}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R_{\text{irr}}(s,t)\}$, 2. (b)

$N_{1}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R(s,t)\}$ where $s,t$ are distinct but unifiable by the mgu $\sigma$ and $N_{2}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R_{\text{irr}}(s,t),\;C^{\prime}\sigma\vee[\neg]R_{\text{ref}}(s\sigma,t\sigma)\}$, 3. (c)

$N_{1}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R(s,s)\}$ and $N_{2}=N^{\prime}\uplus\{C^{\prime}\vee[\neg]R_{\text{ref}}(s,s)\}$.

We first consider the “only if” direction. Hence, we assume $\mathcal{I}\models N_{1}$ and, in particular, $\mathcal{I}\models C^{\prime}\vee[\neg]R(s,t)$ in cases (a), (b) and (c) and $\mathcal{I}\models C^{\prime}\vee[\neg]R(s,t)$ in case (d).

Ad (a). Suppose $\mathcal{I}\not\models N_{2}$. Then, we must have $\mathcal{I}\not\models C^{\prime}\rho\vee[\neg]R_{\text{irr}}(s,t)\rho$ for some grounding substitution $\rho$. This entails $\mathcal{I}\not\models C^{\prime}\rho$. The latter, because of $\mathcal{I}\models C^{\prime}\rho\vee[\neg]R(s,t)\rho$, leads to $\mathcal{I}\models[\neg]R(s,t)\rho$. Moreover, by definition of $\mathcal{I}$ , we have $R(s,t)\rho\in\mathcal{I}$ if and only if $R_{\text{irr}}(s,t)\rho\in\mathcal{I}$. But this contradicts $\mathcal{I}\not\models[\neg]R_{\text{irr}}(s,t)\rho$.

Ad (b). Suppose $\mathcal{I}\not\models N_{2}$. Then, we either have $\mathcal{I}\not\models C^{\prime}\rho\vee[\neg]R_{\text{irr}}(s,t)\rho$ for some grounding substitution $\rho$, or $\mathcal{I}\not\models C^{\prime}\sigma\rho\vee[\neg]R_{\text{ref}}(s\sigma,t\sigma)\rho$ for the mgu $\sigma$ of $s,t$ and for some grounding substitution $\rho$. Consider the former case. In analogy to (a), we derive $\mathcal{I}\not\models[\neg]R_{\text{irr}}(s,t)\rho$ and $\mathcal{I}\models[\neg]R(s,t)\rho$. By definition of $\mathcal{I}$, we have $R(s,t)\rho\in\mathcal{I}$ if and only if $R_{\text{irr}}(s,t)\rho\in\mathcal{I}$ – a contradiction. Consider the latter case. In analogy to (a), we derive $\mathcal{I}\not\models[\neg]R_{\text{ref}}(s\sigma,t\sigma)\rho$ and $\mathcal{I}\models[\neg]R(s\sigma,t\sigma)\rho$. Since $\sigma$ unifies $s$ and $t$, we get $s\sigma\rho=t\sigma\rho$. By definition of $\mathcal{I}$, this entails $R(s\sigma,t\sigma)\rho\in\mathcal{I}$ if and only if $R_{\text{ref}}(s\sigma,t\sigma)\rho\in\mathcal{I}$. Again, this constitutes a contradiction.

Ad (c). Suppose $\mathcal{I}\not\models N_{2}$. Then, we have $\mathcal{I}\not\models C^{\prime}\rho\vee[\neg]R_{\text{ref}}(s,t)\rho$ for some grounding substitution $\rho$. In analogy to (a), we derive $\mathcal{I}\not\models[\neg]R_{\text{ref}}(s,s)\rho$ and $\mathcal{I}\models[\neg]R(s,s)\rho$. By definition of $\mathcal{I}$, this entails $R(s,s)\rho\in\mathcal{I}$ if and only if $R_{\text{ref}}(s,s)\rho\in\mathcal{I}$. Again, this constitutes a contradiction.

Next, we consider the “if” direction, i.e. we assume $\mathcal{I}\models N_{2}$.

Ad (a). We have $\mathcal{I}\models C^{\prime}\vee[\neg]R_{\text{irr}}(s,t)$. Suppose $\mathcal{I}\not\models N_{1}$. Then, there must be some grounding substitution $\rho$ for which $\mathcal{I}\not\models C^{\prime}\rho\vee[\neg]R(s,t)\rho$. This entails $\mathcal{I}\not\models C^{\prime}\rho$, which, because of $\mathcal{I}\models C^{\prime}\rho\vee[\neg]R_{\text{irr}}(s,t)\rho$, leads to $\mathcal{I}\models[\neg]R_{\text{irr}}(s,t)\rho$. By definition of $\mathcal{I}$, we then have $R_{\text{irr}}(s,t)\rho\in\mathcal{I}$ if and only if $R(s,t)\rho\in\mathcal{I}$. This yields a contradiction, as we have $\mathcal{I}\not\models[\neg]R(s,t)\rho$.

Ad (b). We have $\mathcal{I}\models C^{\prime}\vee[\neg]R_{\text{irr}}(s,t)$ and $\mathcal{I}\models C^{\prime}\sigma\vee[\neg]R_{\text{ref}}(s\sigma,t\sigma)$. Suppose $\mathcal{I}\not\models N_{1}$. Again, we get $\mathcal{I}\not\models C^{\prime}\rho\vee[\neg]R(s,t)\rho$ for some grounding $\rho$. This entails $\mathcal{I}\not\models C^{\prime}\rho$, which leads to $\mathcal{I}\models[\neg]R_{\text{irr}}(s,t)\rho$. By Assumption (3), we get $R(s,t)\rho\in\mathcal{I}$ if and only if $R_{\text{irr}}(s,t)\rho\in\mathcal{I}$. But then, $\mathcal{I}\not\models[\neg]R(s,t)\rho$ contradicts $\mathcal{I}\models[\neg]R_{\text{irr}}(s,t)\rho$.

Ad (c). We have $\mathcal{I}\models C^{\prime}\vee[\neg]R_{\text{ref}}(s,s)$. Suppose $\mathcal{I}\not\models N_{1}$. Then, we get $\mathcal{I}\not\models[\neg]R(s,s)\rho$ for some grounding substitution $\rho$. But this contradicts Assumption (1), which entails that $R_{\text{ref}}(s\rho,s\rho)\in\mathcal{I}$ if and only if $R(s\rho,s\rho)\in\mathcal{I}$.

This finishes the proof of Claim I. $\Diamond$

Consider the derivation $N\Rightarrow_{\text{RRS}}N_{1}\Rightarrow_{\text{RRS}}\ldots\Rightarrow_{\text{RRS}}\operatorname{rrs}(N)$ based on the modified rewrite system with integrated, prioritized Delete. Let $\mathcal{I}$ be a Herbrand model of $N$. Since $N$ does not contain the predicates $R_{\text{ref}}$ and $R_{\text{irr}}$, we can bring $\mathcal{I}$ into the shape that meets the conditions of Claim I and still ensure that $\mathcal{I}\models N$. It then follows that $\mathcal{I}\models N$, $\mathcal{I}\models N_{1},\ldots,\mathcal{I}\models\operatorname{rrs}(N)$. Symmetrically, let $\mathcal{I}$ be a Herbrand model of $\operatorname{rrs}(N)$. Since $\operatorname{rrs}(N)$ does not contain the predicate $R$, we can reshape $\mathcal{I}$ so that Claim I is applicable and $\mathcal{I}$ is still a model of $\operatorname{rrs}(N)$. Then, we get $\mathcal{I}\models\operatorname{rrs}(N),\ldots,\mathcal{I}\models N$. Consequently, $N$ is satisfiable if and only if $\operatorname{rrs}(N)$ is. ∎

Notice that the above lemma holds independently of the fact whether there is a reflexivity clause in $N$ or not. Such a clause would, of course, also be transformed by $\Rightarrow_{\text{RRS}}$.

Let us take a look at an example that is a little bit more involved. Consider an equivalence relation $R$ with the respective axiom clauses.

[TABLE]

Applying $\Rightarrow_{\text{RRS}}$ exhaustively results in the clause set

[TABLE]

After removing redundant clauses, we are conveniently left with just

[TABLE]

which are no longer trivialized by the linear approximation $T(f_{R}(x,y))$ of the reflexivity axiom. See also the example in the introduction, Section 1, for another application of reflexive relation splitting.

The rule Reflexive replaces a clause by two clauses and can, therefore, cause an exponential blow up in the number of generated clauses. However, this is only the case for a clause with several occurrences $R(s_{i},t_{i})$ such that the respective term pairs are all simultaneously unifiable. This situation can be detected and then reflexive relation splitting may not be efficiently applicable. However, the above example on the equivalence relation $R$ shows that in the case of variable chains as they occur in the transitivity axiom, all of the eventually generated clauses become redundant, except one: $R_{\text{irr}}(x,y),R_{\text{irr}}(y,z)\rightarrow R_{\text{irr}}(x,z)$. We have integrated reflexive relation splitting into Spass-AR [24] and have run it on the overall TPTP [21]. There is no example in TPTP v.7.2.0 showing the exponential blow up and the set of problems solved by Spass-AR with reflexive relation splitting is strictly larger than without.

Nevertheless, reflexive relation splitting is, of course, not sufficient to transform all problems with inherently infinite models based on a (ir)reflexive relation into clause sets that can eventually be decided by AR via MSLH clause sets. Consider a strict partial ordering without endpoints:

[TABLE]

Reflexive relation splitting yields

[TABLE]

but after approximation, the abstraction refinement does not terminate on the example. The reason is the approximation of the clause $R_{\text{irr}}(x,g(x))$ into the two clauses $S(g(x))$ and $S(y)\rightarrow T(f_{R_{\text{irr}}}(x,y))$ where the property is lost that in any ground instance of $R_{\text{irr}}(x,g(x))$ the first argument has one occurrence of $g$ less than the second. This was resolved in [17] by the use of tuple tree automata.

6 Discussion

We have shown that the MSLH clause fragment has the finite model property and can therefore not represent models of clause sets with inherently infinite models. This applies to the model representation building blocks atoms with disequality constraints, implicit generalizations, and atoms with membership constraints as well, if atoms and terms are linear. For non-linear terms, our finite model property proof breaks, and, in fact, the example from the introduction shows already that non-linear atoms can represent models for clause sets with inherently infinite models.

Unsatisfiability of monadic shallow Horn clause sets is undecidable. One occurrence of a clause $\Gamma\rightarrow S(f(x,x))$ suffices to this end. This can be seen by a respective monadic reformulation of the PCP encoding from the introduction. On the other hand, models represented by ground instances of finite sets of (linear or non-linear) atoms are also restricted in expressivity, because they cannot express any recursive structure. For example, MSLH clause sets and extensions thereof have been successfully used for the analysis of security protocols [26, 4] where (counter-) models cannot be expressed by ground instances of finite sets of atoms. In summary, and not surprisingly, there is currently no unique superior model representation formalism.

If models are eventually constructed through the reversal of an approximation, the used representation may have the finite model property and can still show satisfiability of clause sets with inherently infinite models. We obtained this result via reflexive relation splitting. This insight is already a consequence of [17]. There, an approximation into a theory of tuple tree automata is described and it is even complete with respect to models generated out of these automata. We can currently not provide such a completeness result although this would be highly desirable. On the other hand, our techniques are embedded into a refutationally complete procedure, whereas the approach in [17] can only show satisfiability.