Abstract
The main topic of this article are SGGS decision procedures for fragments of first-order logic without equality. SGGS (Semantically-Guided Goal-Sensitive reasoning) is an attractive basis for decision procedures, because it generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability. As SGGS is both refutationally complete and model-complete in the limit, SGGS decision procedures are model-constructing. We investigate the termination of SGGS with both positive and negative results: for example, SGGS decides Datalog and the stratified fragment (including Effectively PRopositional logic) that are relevant to many applications. Then we discover several new decidable fragments, by showing that SGGS decides them. These fragments have the small model property, as the cardinality of their SGGS-generated models can be upper bounded, and for most of them termination tools can be applied to test a set of clauses for membership. We also present the first implementation of SGGS—the Koala theorem prover—and we report on experiments with Koala.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
1 Introduction
Many applications of automated reasoning require to combine the decidability of satisfiability with an expressive logic. In first-order logic (FOL), validity, or equivalently unsatisfiability, is semidecidable, whereas satisfiability is not even semidecidable. Therefore, the quest for decidable fragments of FOL is key in advancing the field, and many classes of formulae were shown decidable (e.g., [25, 36, 43] for surveys). An approach to prove the decidability of a class is to show that a refutationally complete inference system for first-order theorem proving is guaranteed to terminate on all inputs in that class. It follows that any theorem proving strategy given by that inference system and a fair search plan is a decision procedure for satisfiability in that class.
In this paper we apply this approach to SGGS, or Semantically-Guided Goal-Sensitive reasoning [19, 20]. Similar to semantic resolution [76] and hyperresolution [71], SGGS is semantically guided by a fixed initial interpretation. However, SGGS generates primarily instances of clauses, not resolvents. By this characteristic, SGGS is a descendant of hyperlinking [53] and ordered semantic hyperlinking [67]. Other methods with this characteristic include hypertableaux [8, 11, 13] and Inst-Gen [39, 46]. Nonetheless, the essential features of SGGS set it apart from the theorem-proving methods based on resolution, instance generation, or tableaux.
SGGS is a generalization to FOL of the CDCL (Conflict-Driven Clause Learning) procedure for propositional satisfiability (SAT) [56]. Indeed, SGGS searches for a model of the input set of clauses by building candidate models, represented by selected literals on a trail of clauses. In this sense SGGS is model-based, meaning that the state of an SGGS-derivation is a representation of a candidate model (cf. [22] for a survey of first-order model-based methods). The initial interpretation in SGGS acts as a starting point, as the candidate models are built by selecting preferably literals that are not true in the initial interpretation, but may be needed to get a model of the clauses. In this process, a conflict may arise in the form of a conflict clause. SGGS applies a restricted form of resolution only to explain the conflict, which is then solved by moving the conflict clauses and flipping the sign of its selected literal. In this sense SGGS is also conflict-driven (cf. [15] for a survey of conflict-driven methods).
By these features, SGGS is a first-order search-based satisfiability procedure, similar to the methods that generalize CDCL to satisfiability modulo theories (SMT), such as CDCL(\(\mathcal{T}\)) [63]Footnote 1, CDCL(\(\varGamma \!+\!{{\mathcal {T}}}\)) [21], MCSAT [28], and CDSAT [23, 24]. For CDCL, termination descends from the finitary nature of the SAT problem. The termination of CDCL(\({{\mathcal {T}}}\)) in its original formulation stems from the fact that it does not create new atoms. As CDCL(\(\varGamma \!+\!{{\mathcal {T}}}\)) integrates superposition in CDCL(\({{\mathcal {T}}}\)), the result is a semidecision procedure whose termination is guaranteed only under suitable hypotheses and using speculative inferences [21]. MCSAT, CDSAT, and an extension of CDCL(\(\mathcal{T}\)) [7] create new terms and atoms, and they are proved to be terminating by showing that all new objects come from a finite basis [7, 23, 28].
The termination of SGGS is challenging, because SGGS is refutationally complete for FOL, and especially significant, since SGGS is model complete in the limit: given a satisfiable input, the limit of any fair SGGS-derivation represents a model. Thus, model generation is guaranteed if termination is, and SGGS-based decision procedures are model-constructing, a standard feature for SAT and SMT procedures, but not for first-order theorem-proving methods.
With this motivation, we apply the finite basis approach to SGGS. A finite basis for SGGS is a finite subset of the Herbrand base of the input set of clauses. An SGGS-derivation is in a finite basis if all ground instances of all clauses generated during the derivation are made of atoms coming from the finite basis. Previous work showed that if the length of the trail during a fair SGGS-derivation is upper bounded, the derivation is finite [20, Thm. 6 and Cor. 2]. We show that if a fair SGGS-derivation is in a finite basis, the length of the trail is upper bounded, and hence the derivation is finite. Also, we prove that given a satisfiable input, the cardinality of the SGGS-generated model is upper bounded. These results hold regardless of the initial Herbrand interpretation guiding SGGS. If for all clause sets in a class \({{\mathcal {F}}}\) it is possible to identify a finite basis, \({{\mathcal {F}}}\) is SGGS-decidable and has the small model property.
It follows that SGGS with any guiding interpretation decides all fragments where the Herbrand base itself is finite, including the Datalog language (e.g., [26]), the Bernays–Schönfinkel class [14, 68], whose clausal version is known as EPR for Effectively PRopositional logic [3, 37, 65], and the stratified fragment [1, 47], which is the generalization of EPR to many-sorted logic.Footnote 2 EPR and the stratified fragment find application in verification (e.g., [57, 64]), while Datalog is a fundamental language for deductive databases and knowledge representation, and has been applied also in connection with neural networks [58].
These positive results are balanced by negative ones: we show by counterexamples that SGGS with sign-based semantic guidance (i.e., either all-negative—all negative literals are true—-or all-positive—all positive literals are true) does not decide the Ackermann [2, 35, 44], monadic [2, 38, 44], \(\mathsf{F\!O}^2\) [38, 41], and guarded [4, 29] fragments. Since the sets of clauses in these counterexamples admit finite model, these counterexamples also show that the existence of a finite model does not imply the termination of SGGS with sign-based semantic guidance. However, we also give examples where SGGS terminates and represents with a finite trail an infinite Herbrand model. Thus, the termination of SGGS does not imply the existence of a finite Herbrand model.
A clause is positively/negatively ground-preserving, or range-restricted, if all its variables occur in its negative/positive literals. This property is used in deductive databases [61, 78], as it is also a property of Datalog clauses, in theorem proving [49, 50, 55], model building [25, 34], and decision procedures [9, 21, 25, 34, 52]. The role of sign in the definition of ground-preserving clauses suggests to adopt sign-based semantic guidance for SGGS and compare it with hyperresolution, that is semantic resolution with sign-based semantic guidance. Under the assumption that the input clauses are ground-preserving, we prove two results: first, similar to hyperresolution, SGGS generates only ground clauses; second, SGGS terminates whenever hyperresolution does. It follows that SGGS decides all ground-preserving fragments decided by hyperresolution, such as the positive variable dominated (PVD) [25, 34] and the bounded depth increase (BDI) [52] fragments. However, many theorem-proving problems do not belong to any known decidable class.
Example 1
Problem HWV036-2 from TPTP 7.3.0 [77] specifies a full-adder in 51 clauses, including for instance:
This set is satisfiable, but it does not belong to any known decidable fragments.
In the second part of the paper we apply SGGS to find new decidable fragments. We define the positively/negatively restrained fragments by adding to ground-preservingness an ordering-based restriction. By distinguishing between sorts populated by finitely or infinitely many ground terms, we define the positively/negatively sort-restrained classes, where restrainedness is imposed only to the literals having infinitely many ground instances. These fragments generalize the respective restrained fragments and the stratified fragment, which represents the special case where there are finitely many ground terms for all sorts. The sort-refined-PVD class is defined analogously with the PVD restrictions in place of restrainedness, so that it generalizes the PVD and the stratified fragments. We show that SGGS with sign-based semantic guidance decides all these new classes by the finite basis approach, so that the new classes have the small model property. We prove that sign-based resolution strategies (e.g., hyperresolution and PO-resolution) decide the restrained fragments. However, they do not decide the sort-restrained and sort-refined-PVD classes, because they do not decide the stratified fragment.
The introduction of a new decidable class poses the problem of how to determine that a clause set belongs to the class and whether this test is decidable. We reduce the problem of deciding whether a clause set is restrained or sort-restrained to that of deciding whether rewriting by an associated rewrite system terminates. It follows that membership in these fragments is undecidable in general, but can be tested in practice by termination tools for rewriting such as 
[48] and AProVE [40].
In the experiments, we applied these tools to discover restrained and sort-restrained problems in the TPTP library [77]. The other decidability criteria (e.g., stratification, PVD) can also be tested automatically, resulting in a classification of TPTP problems. This allows us to evaluate empirically the relevance of the new classes and discover problems not previously known to be decidable. For instance, the axiomatization in Example 1 and all the TPTP problems that include it are restrained. Then we describe the Koala theorem prover, which is the first implementation of SGGS. We report on applying Koala to TPTP problems, including both SGGS-decidable and semidecidable problems. We present and analyze these experiments, which show promising performances especially on satisfiable problems.
The paper is organized as follows. After the basic definitions (Sect. 2) we give an overview of SGGS (Sect. 3). Section 4 presents the finite basis approach, and all the results about SGGS and already known decidable fragments. Section 5 introduces the new decidable fragments and contains the results showing that they are SGGS-decidable. Section 6 covers the reduction of membership in the new fragments to the termination of rewriting, the application of the termination tools, the Koala prover, and the experiments. Discussions of related and future work conclude the paper. A short version of this paper appeared [17].
2 Basic Definitions
A signature is given by a set \(\varSigma \) of sorts and a set of constant, function, and predicate symbols. We use \(s, s_1, s_2,\ldots \) for sorts, \(\textsf{a}, \textsf{b}, \textsf{0}, \textsf{1}\) for constants, \(\textsf{P}, \textsf{Q}, \textsf{R}\) for predicates, \(\textsf{f}, \textsf{g}, \textsf{h}, \textsf{s}\) for functions, v, w, x, y, z for variables, t, u for terms, \(\mathcal Var(t)\) for the set of variables in t, \(\mathcal Var_s(t)\) for those of sort s, \( top (t)\) for the top symbol of t. Sorts are nonempty (there is a ground term for every sort), and \(t:s\) says that t has sort s. We use L, M, P, Q for literals, at(L) for L’s atom, \(\alpha , \sigma , \vartheta , \tau \) for substitutions, C, D, E for clauses, that are disjunctions of literals where all variables are implicitly universally quantified, and S for a (finite) set of clauses, understood as the conjunction of its elements.
The \( top \) notation is extended to atoms, \(\mathcal Var\) and \(\mathcal Var_s\) to atoms, literals, and clauses, and at to sets of literals, clauses, and sets of clauses. A clause C is positive if all its literals are positive, negative if all its literals are negative, and mixed otherwise. \(C^+\) and \(C^-\) denote the disjunctions of the positive and negative literals in C. A unit clause has exactly one literal, and a Horn clause has at most one positive literal. A Horn clause is a fact if it is a positive unit, a query if it is negative, and a rule if it is mixed. We use I and J for Herbrand interpretations and \({{\mathcal {I}}}\) for other interpretations. The symbol \(\models \) is overloaded to mean satisfaction of a clause or set of clauses in an interpretation, validity in the sense of satisfaction in all Herbrand interpretations, and logical entailment.
Viewing terms as trees, the depth of a term t is defined as \(\text {depth}(t) = 0\), if t is a constant or a variable, and \(\text {depth}(t) = 1 + max\{\text {depth}(t_i)\mathop {\,:}1\!\leqslant \! i\!\leqslant \! n\}\), if t is a compound term \(\textsf{f}(t_1,\ldots , t_n)\). The depth of a literal L is defined as \(\text {depth}(L) = \text {depth}(at(L)) = 1 + max\{\text {depth}(t_i)\mathop {\,:}1\!\leqslant \! i\!\leqslant \! n\}\) if \(t_1,\ldots , t_n\) are the predicate’s arguments in at(L). By labeling arcs with natural numbers, every subterm has a position defined as the string of natural numbers from the root to the subterm. We use p, q, r, and o for positions. The subterm of t at position p, denoted as \(t \vert _p\), is defined by \(t \vert _\varLambda = t\), where \(\varLambda \) is the top position, and \(f(t_1, \dots , t_n)\vert _{ip} = t_i\vert _p\) for all i, \(1\!\leqslant \! i \!\leqslant \! n\). The notation \(t = c[u]_p\) says that t is equal to a context c where u occurs as subterm at position p. A term t has occurrence depth k in atom L if \(L \vert _p = t\) and k is the length of position p.
An ordering > on terms is well-founded, if it admits no infinite descending chain, stable, if \(t > u\) implies \(t\sigma > u\sigma \) for all substitutions \(\sigma \), monotonic, if \(t > u\) implies \(c[t]_p > c[u]_p\) for all contexts c and positions p, and has the subterm property, if \(c[t]_p > t\) for all contexts c and positions p with \(p \ne \varLambda \). A simplification ordering is stable, monotonic, and has the subterm property. A complete simplification ordering (CSO) is also total on ground terms. A simplification ordering is well-founded [30]. Recursive path orderings (RPO’s) [30], lexicographic (recursive) path orderings (LPO’s), and Knuth-Bendix orderings (KBO’s) [45, 54] employ a precedence, which is a partial ordering \(\succ _p\) on the symbols in the signature. A KBO attributes non-negative weights to terms: all variables have weight \(w_0\), a weight function w attributes a weight to every non-variable symbol, and the weight of a term is the sum of the weights of its symbols. RPO’s, LPO’s, and KBO’s are simplification orderings. If \(\succ _p\) is total, KBO’s and LPO’s are CSO’s (see e.g., [31] for a survey on orderings).
We recapitulate resolution [72], because resolution-based strategies appear in later sections. Binary resolution generates from parents \(\lnot L \vee C\) and \(L^\prime \vee D\) the resolvent \((C \vee D)\sigma \), if \(L\sigma = L^\prime \sigma \) with most general unifier (mgu) \(\sigma \). Factoring generates from parent \(L_1 \vee \ldots \vee L_k \vee C\) the factor \((L_1 \vee C)\sigma \), if \(L_1\sigma \!=\! L_2\sigma \!=\! \ldots \!=\! L_k\sigma \) with mgu \(\sigma \). Many refinements of resolution preserve its refutational completeness. Positive resolution, also known as the P1-strategy [42, 71] or P1-deduction [66], requires that every binary resolution step has a positive parent. Negative resolution, also known as all-negative-resolution [66], requires that every binary resolution step has a negative parent. Semantic resolution [76] generates only resolvents that are false in a fixed guiding interpretation I. Hyperresolution [71] is semantic resolution where I is either the all-negative interpretation \(I^-\) or the all-positive interpretation \(I^+\). Positive hyperresolution resolves a non-positive clause C, called the nucleus, with as many positive clauses, termed satellites, as needed to resolve away with a simultaneous mgu all literals in \(C^-\) and get a positive clause, which is false in \(I^-\). Negative hyperresolution is defined dually. Ordered resolution [42] assumes a CSO > on literals and requires that in every binary resolution step \(\lnot L\sigma \) is >-maximal in \((\lnot L \vee C)\sigma \) and \(L^\prime \sigma \) is >-maximal in \((L^\prime \vee D)\sigma \); and in every factoring step \(L_1\sigma \) is >-maximal in \((L_1 \vee \ldots \vee L_k \vee C)\sigma \). PO-resolution adds the requirement that \(L^\prime \vee D\) is positive and drops the >-maximality constraint on \(\lnot L\sigma \).
3 SGGS: An Overview
SGGS [19, 20] works with constrained clauses, written \(A\rhd C\), where A is a constraint and C is a clause. The atomic constraints are \( true \), \( false \), \( top (t)\, {=}\, f\), and \(t\,{\equiv }\,u\), where \(\equiv \) is identity. For ground terms t and u, \(\models top (t)\, {=}\, f\) if the top symbol of t is f, and \(\models t\,{\equiv }\,u\) if t and u are the same term. The negation, conjunction, and disjunction of constraints is a constraint. Any variable that appears in A and not in C is implicitly existentially quantified. Thus, if A is ground, either \(\models A\) or \(\models \lnot A\), and if A is not ground, \(\models A\) means that the existential closure of A is valid. A constraint is in standard form if it is \( true \), \( false \), or a conjunction of distinct atomic constraints of the form \(x\,{\not \equiv }\,y\) or \( top (x)\, {\ne }\, f\). SGGS keeps constraints in standard form [20, Sect. 7]. Substitutions are sort-preserving (i.e., \(x\sigma \) has the same sort as x) so that instantiation respects sorts. For a constrained clause \(A \rhd C\) the set of its constrained ground instances (cgi’s) is \(Gr(A\rhd C) = \{C\vartheta \mathop {\,:}C\vartheta \text{ is } \text{ ground } \text{ and } \models A\vartheta \}\). Thus, \(Gr( false \rhd C) = \emptyset \), \(Gr( true \rhd C) = Gr(C)\), and \( true \rhd C\) can be written C. Literals \(A \rhd L\) and \(B \rhd M\) intersect if \(at(Gr(A \rhd L)) \cap at(Gr(B \rhd M)) \ne \emptyset \) and are disjoint otherwise. The notation \(Gr\) is extended to sets of atoms. Constraints can be omitted if irrelevant or for brevity.
Example 2
Given a signature with constant symbols \(\textsf{a}:s_1\) and \(\textsf{b}:s_2\), function symbol \(\textsf{f}{:}s_1\, {\rightarrow }\, s_2\), and predicate symbol \(\textsf{P} \subseteq s_2 \times s_2\), the only term of sort \(s_1\) is \(\textsf{a}\), and the only terms of sort \(s_2\) are \(\textsf{b}\) and \(\textsf{f}(\textsf{a})\). Thus, \(Gr(\textsf{P}(x, y)) = \{ \textsf{P}(\textsf{b},\textsf{b}),\ \textsf{P}(\textsf{f}(\textsf{a}),\textsf{b}),\ \textsf{P}(\textsf{b},\textsf{f}(\textsf{a})), \ \textsf{P}(\textsf{f}(\textsf{a}),\textsf{f}(\textsf{a}))\}\). Then, \(top(x) \ne \textsf{a} \rhd \textsf{P}(\textsf{f}(x), y)\) is equivalent to \( false \rhd \textsf{P}(\textsf{f}(x), y)\), while \(top(y) \ne \textsf{a} \rhd \textsf{P}(\textsf{f}(x), y)\) is equivalent to \( true \rhd \textsf{P}(\textsf{f}(x), y)\) with cgi’s \(\textsf{P}(\textsf{f}(\textsf{a}),\textsf{b})\) and \(\textsf{P}(\textsf{f}(\textsf{a}),\textsf{f}(\textsf{a}))\).
SGGS is semantically guided by an initial interpretation I: if \(I\not \models S\), SGGS seeks a Herbrand model of S, by building candidate partial interpretations different from I, and using I as the default to complete them. If the empty clause \(\bot \) arises in the process, unsatisfiability is reported. While I can be any Herbrand interpretation, in this section I is either \(I^-\) or \(I^+\). If I is \(I^-\) (\(I^+\)) SGGS discovers which positive (negative) literals need to be true to satisfy S.
A literal L is uniformly false in an interpretation J if \(J\models \lnot L\), that is, if \(J\models \lnot L^\prime \) for all \(L^\prime \in Gr(L)\). Then, L is said to be I-true if it is true in I, and I-false if it is uniformly false in I. A clause is I-all-true if all its literals are I-true, and I-all-false if all its literals are I-false. If \(I = I^-\) negative literals are I-true, positive literals are I-false, negative clauses are I-all-true, positive clauses are I-all-false, and mixed clauses are neither. If \(I = I^+\) positive literals are I-true, negative literals are I-false, positive clauses are I-all-true, negative clauses are I-all-false, and mixed clauses are neither.
SGGS builds a trail \(\varGamma \) of constrained clauses with selected literals. The selected literals form the partial interpretation represented by the trail. Initially the trail is empty, written \(\varepsilon \). Then SGGS adds clauses forming a sequence \(A_1 \rhd C_1[L_1],\ldots , A_n \rhd C_n[L_n]\) (\(n \ge 1\)). Clause \(A_i \rhd C_i[L_i]\) is the clause at index i in \(\varGamma \). The notation \(C_i[L_i]\) means that \(L_i\) is the literal of \(C_i\) that is selected. SGGS requires that every literal in \(\varGamma \) is either I-true or I-false (trivial if I is \(I^+\) or \(I^-\)). SGGS also requires that if clause \(C_i[L_i]\) has I-false literals, then \(L_i\) is an I-false literal. The selected literal \(L_i\) is I-true only if \(C_i[L_i]\) is an I-all-true clause. I-false literals are preferred for selection because \(I\not \models S\) and hence SGGS tries to change something wrt I towards finding a model of S.
In order to see how the selected literals form a partial interpretation, let the length of a trail \(\varGamma \), written \(\vert \varGamma \vert \), be the number of clauses in \(\varGamma \), and let \(\mathop {\varGamma \vert _{j}}\) denote the prefix of length j of \(\varGamma \). Then, the partial interpretation \(I^p(\varGamma )\) represented by \(\varGamma \) is defined inductively as follows. If \(\varGamma = \varepsilon \), then \(I^p(\varGamma ) = \emptyset \). If \(\varGamma = A_1 \rhd C_1[L_1],\ldots , A_n \rhd C_n[L_n]\), we define \(I^p(\varGamma )\) in terms of \(I^p(\mathop {\varGamma \vert _{n-1}})\). Consider a cgi C[L] of \(A_n \rhd C_n[L_n]\). If \(I^p(\mathop {\varGamma \vert _{n-1}}) \cap C[L] \ne \emptyset \), it means that \(I^p(\mathop {\varGamma \vert _{n-1}})\) already satisfies C[L]. If \(I^p(\mathop {\varGamma \vert _{n-1}}) \cap C[L] = \emptyset \), it means that \(I^p(\mathop {\varGamma \vert _{n-1}})\) does not satisfy C[L]: if \(\lnot L\not \in I^p(\mathop {\varGamma \vert _{n-1}})\), we can satisfy C[L] by adding L to \(I^p(\mathop {\varGamma \vert _{n-1}})\) to form \(I^p(\varGamma )\). Such an instance C[L] is a proper (or productive) constrained ground instance (pcgi) of \(A_n \rhd C_n[L_n]\) and L is a pcgi of \(A_n \rhd L_n\). Then, \(I^p(\varGamma ) = I^p(\mathop {\varGamma \vert _{n-1}}) \cup pcgi(A_n \rhd L_n, \varGamma )\), where \(pcgi(A_n \rhd L_n, \varGamma )\) is the set of all the pcgi’s of \(A_n \rhd L_n\) in \(\varGamma \).
From the partial interpretation \(I^p(\varGamma )\) we get the interpretation \(I[\varGamma ]\) represented by trail \(\varGamma \) as follows: for all ground literals L, if \(I^p(\varGamma )\) determines the truth value of L, then \(I[\varGamma ]\models L\) iff \(I^p(\varGamma )\models L\); otherwise, \(I[\varGamma ]\models L\) iff \(I\models L\). Suppose that all cgi’s of \(A_n \rhd C_n[L_n]\) are pcgi’s: this clause contributes all the ground instances of its selected literal to \(I^p(\varGamma )\). The longest prefix of \(\varGamma \) that is made of clauses with this property is called the disjoint prefix of \(\varGamma \) and is denoted \(dp(\varGamma )\). The name descends from the fact that the selected literals of clauses in \(dp(\varGamma )\) are all disjoint. Suppose that \(I^p(\mathop {\varGamma \vert _{n-1}})\) satisfies all the cgi’s of \(A_n \rhd C_n[L_n]\) and hence \(A_n \rhd C_n[L_n]\) itself. Such a clause is disposable and can be removed by SGGS-deletion (rule \(\textsf{delete}\) in Fig. ). A clause \(A_n \rhd C_n[L_n]\) is a conflict clause, if all the literals of \(C_n\) are uniformly false in \(I[\varGamma ]\).
SGGS rules for model search
An SGGS-derivation (named \(\varTheta \) if needed) is a series of trails \(\varGamma _0\vdash \varGamma _1\vdash \ldots \varGamma _j\vdash \ldots \), where \(\varGamma _0 = \varepsilon \), and \(\forall j\), \(j > 0\), SGGS generates \(\varGamma _j\) from \(\varGamma _{j-1}\) and S by applying either a model-search rule in Fig. 1 or a conflict-solving rule in Fig. . If \(I[\varGamma ]\models S\), a model has been found, and rule \(\textsf{sat}\) in Fig. 1 fires to report the success of the model search. If \(\bot \in \varGamma \), it means that in the attempt to solve a conflict, the conflict-solving rule SGGS-resolution (\(\textsf{resolve}\) in Fig. 2) has generated the empty clause, which signals that the conflict cannot be solved, because S itself is unsatisfiable, so that rule \(\textsf{unsat}\) in Fig. 2 fires to report that a refutation has been found.
Otherwise, SGGS makes progress in two ways. If \(\varGamma \, {=}\, dp(\varGamma )\), the trail is in order, but since \(I[\varGamma ]\not \models S\), there exists some \(C^\prime \, {\in } \, Gr(C)\) for \(C \, {\in } \, S\), such that \(I[\varGamma ] \not \models C^\prime \). Then, SGGS applies SGGS-extension (rule \(\textsf{extend}\) in Fig. 1) to generate from C and \(\varGamma \) a clause \(A \rhd E\), called extension clause, such that E is an instance of C and \(C^\prime \in Gr(A \rhd E)\), in order to extend \(I^p(\varGamma )\) to try to satisfy \(C^\prime \). If \(\varGamma \ne dp(\varGamma )\), the trail needs repair: either there are disposable clauses and SGGS-deletion removes them, or there are intersections between selected literals that can be exposed by SGGS-splitting (rules \(\textsf{s}\text {-}\textsf{split}\) and \(\textsf{d}\text {-}\textsf{split}\) in Fig. 1), or there is a conflict clause to be handled by the conflict-solving rules of Fig. 2. The following example illustrates the model-search rules, demonstrating how SGGS halts on the input set used to show that hyperresolution cannot decide EPR ([36, Ex. 4.8] and [25, Ex. 3.17]).
Example 3
The set S consisting of clauses
defeats hyperresolution, because (iv) is obtained from (ii) by flipping signs, and likewise for (iii) and (i) plus renaming the constant. Positive hyperresolution generates infinitely many clauses of the form \(\textsf{P}(x_1,x_2,\textsf{a}) \vee \textsf{P}(x_2,x_3,\textsf{a}) \vee \dots \vee \textsf{P}(x_{n-1},x_n,\textsf{a})\vee \textsf{P}(x_{n},x_1,\textsf{a})\), for \(n\geqslant 2\), using (ii) as nucleus, (i) as initial satellite, and then each resulting hyperresolvent as next satellite. Negative hyperresolution generates infinitely many clauses of the form \(\lnot \textsf{P}(x_1,x_2,\textsf{b}) \vee \lnot \textsf{P}(x_2,x_3,\textsf{b}) \vee \dots \vee \lnot \textsf{P}(x_{n-1},x_n,\textsf{b})\vee \lnot \textsf{P}(x_{n},x_1,\textsf{b})\), for \(n\geqslant 2\), using (iv) as nucleus, (iii) as initial satellite, and then each resulting hyperresolvent as next satellite. In contrast, SGGS detects that S is satisfiable with either \(I^-\) or \(I^+\). Assume that \(I = I^-\): all input clauses are satisfied except (i). Thus, SGGS-extension puts it on the trail selecting its single literal:
At this point, \(I[\varGamma _1]\) satisfies \(\textsf{P}(x,x,\textsf{a})\), but not the ground instances of clause (ii) where the third literal is an instance of \(\lnot \textsf{P}(x,x,\textsf{a})\). Thus, SGGS-extension unifies the third literal of clause (ii) with \([\textsf{P}(x,x,\textsf{a})]\), and adds to the trail the resulting instance of clause (ii):
An \(I^-\)-false (i.e., positive) literal is selected in the added clause (choosing the other makes no difference). Also, SGGS assigns the literal \(\lnot \textsf{P}(x,x,\textsf{a})\) to \([\textsf{P}(x,x,\textsf{a})]\) to record that \(\lnot \textsf{P}(x,x,\textsf{a})\) (which is true in \(I^-\)) is uniformly false in \(I^p(\varGamma _2)\), and hence in \(I[\varGamma _2]\), due to the selection of \(\textsf{P}(x,x,\textsf{a})\). \(I[\varGamma _2]\) satisfies \(\textsf{P}(y,x, \textsf{a})\) and hence all the ground instances of clause (ii) that had been lost in order to satisfy \(\textsf{P}(x,x,\textsf{a})\). However, the selected literals in \(\varGamma _2\) intersect. Thus, SGGS-splitting partitions the second clause into two clauses:
where both occurrences of \(\lnot \textsf{P}(x,x,\textsf{a})\) are assigned to \([\textsf{P}(x,x,\textsf{a})]\). A partition of a clause \(A \rhd C[L]\) is a set of clauses \(\{A_i \rhd C_i [L_i] \}_{i=1}^n\) that covers the same ground instances (i.e., \(Gr(A \rhd C) = \bigcup _{i=1}^n\{Gr(A_i \rhd C_i)\}\)), but such that the selected literals \(A_i \rhd L_i\) are disjoint (cf. [20, Def. 13]). SGGS-splitting replaces a clause by the partition dictated by another clause: given a clause \(B \rhd D[M]\) at a smaller index on the trail (\([\textsf{P}(x,x,\textsf{a})]\) in \(\varGamma _2\)) and a clause \(A \rhd C[L]\) at a larger index on the trail (\(\textsf{P}(x,y,\textsf{a}) \vee [\textsf{P}(y,x, \textsf{a})] \vee \lnot \textsf{P}(x,x,\textsf{a})\) in \(\varGamma _2\)) such that their selected literals intersect, SGGS-splitting replaces \(A \rhd C[L]\) by a partition \(\{A_i \rhd C_i [L_i] \}_{i=1}^n\) where one of the selected literals \(A_j \rhd L_j\) captures exactly the intersection between \(B \rhd M\) and \(A \rhd L\) (cf. [20, Def. 14]). This partition is called a splitting of \(A \rhd C[L]\) by \(B \rhd D[M]\) and is denoted \( split (C,D)\). Clause \(A \rhd C[L]\) is the split clause. Clause \(A_j \rhd C_j [L_j]\) is the representative of \(B \rhd D[M]\) in \( split (C,D)\). The SGGS-splitting rule applied here is s-splitting (abbreviated \(\textsf{s}\text {-}\textsf{split}\)) for splitting by similar literals, because L and M have the same sign (cf. [20, Def. 23]). Now the second clause in \(\varGamma _3\) is disposable, and SGGS-deletion removes it eliminating the intersection:
This holds in general: after an s-splitting, D’s representative in \( split (C,D)\) is disposable (cf. [20, Lemma 3]). As \(I[\varGamma _4]\models S\), rule \(\textsf{sat}\) reports satisfiable. The derivation with \(I^+\) proceeds dually with (iii) and (iv).
As seen in Example 3, a derivation starts with an SGGS-extension that puts on the trail an I-all-false input clause and selects one of its literals. All such steps can be done as one and we assume they are. In general, SGGS-extension adds to the trail an instance of an input clause C called main premise. SGGS-extension generates this instance by simultaneously unifying the I-true literals \(L_1, \ldots , L_n\) of C with as many I-false selected literals of opposite sign in the side premises \(B_1 \rhd D_1[M_1], \ldots , B_n \rhd D_n[M_n]\) in \(dp(\varGamma )\).
Definition 1
(SGGS-extension scheme) Let S be the input clause set and \(\varGamma \) be the current trail. Let \(C \in S\) be a clause such that \(L_1, \ldots , L_n\) (\(n \ge 0\)) are all its I-true literals, and \(B_1 \rhd D_1[M_1], \ldots , B_n \rhd D_n[M_n]\) be clauses in \(dp(\varGamma )\) such that \(M_1, \ldots , M_n\) are I-false. If \(\forall j\), \(1 \leqslant j \leqslant n\), \(L_j\alpha = \lnot M_j\alpha \) with simultaneous mgu \(\alpha \), then SGGS-extension adds the extension clause \(A \rhd E = (\bigwedge _{j=1}^n B_j\alpha ) \rhd C\alpha \) to \(\varGamma \).
An SGGS-extension is conflicting if the extension clause \(A \rhd E\) is a conflict clause, non-conflicting otherwise, that is, if \(A \rhd E\) has pcgi’s that get added to \(I^p(\varGamma )\). Definition 1 is a simplification of the original [20, Def. 12] under the assumption that \(I = I^-\) or \(I = I^+\), and rule \(\textsf{extend}\) in Fig. 1 abstracts away for simplicity the details of the SGGS-extension rules [20, Defs. 18, 19, 20, and 21] that instantiate the SGGS-extension scheme.
SGGS rules for conflict solving
As seen in Example 3, if the selection of an I-false literal M makes an I-true literal L on the trail uniformly false in \(I^p(\varGamma )\), SGGS assigns L to the clause where M is selected (cf. [20, Defs. 8, 9]). These assignments record why literals that are true in I are uniformly false in \(I[\varGamma ]\). SGGS requires that an I-true literal L on the trail is assigned unless it is selected. Therefore, the SGGS rules establish or preserve assignments. For example, the I-true literals of an extension clause are assigned to the side premises; the I-true literals in the clauses of a partition inherit the assignments from the split clause; and the clauses with literals assigned to a split clause can be deleted after the splitting [20, Def. 36]. This assignment mechanism achieves first-order propagation in SGGS: for all I-all-true clauses C[L] on the trail, either all literals of C[L] are assigned (with L assigned rightmost) and C[L] is a conflict clause, or all literals of C[L] except L are assigned, which means that L is an implied literal, C[L] is its justification, and C[L] is in \(dp(\varGamma )\). First-order propagation applies to I-all-true clauses because it is relative to I.
CDCL [56] uses the two-watched-literals scheme to detect conflict clauses and implied literals without checking the truth value (true, false, or undefined) of every literal in every clause. It suffices to watch two non-false (i.e., either true or undefined) literals per clause: if the clause has zero non-false literals, it is a conflict clause; if it has one, the literal is implied and the clause is its justification. Since the assignment mechanism is built into the SGGS rules, SGGS does not need a first-order analogue of the two-watched-literals scheme to compute propagations ex post. The dependencies among literals that determine the propagations are stored with the clauses.
In SGGS the assignment of I-true literals to clauses also drives the application of the conflict-solving rules in Fig. 2. Suppose that SGGS-extension appends to the trail a conflict clause \(A \rhd C[L]\) with I-false literals. This means that L is I-false. Then SGGS-resolution [20, Def. 26] (rule \(\textsf{resolve}\) in Fig. 2) explains the conflict by resolving upon L in \(A \rhd C[L]\) and M in \(B \rhd D[M]\), where \(B \rhd D[M]\) is the I-all-true clause in \(dp(\varGamma )\) to which L is assigned.
Definition 2
(SGGS-Resolution) Let \(B \rhd D[M]\) and \(A \rhd C[L]\) be clauses in \(\varGamma \) such that \(B \rhd D[M]\) is I-all-true, is in \(dp(\varGamma )\), and occurs at a smaller index than \(A \rhd C[L]\), L is I-false, \(L = \lnot M\vartheta \) for some substitution \(\vartheta \), and \(A\models B\vartheta \). Then SGGS-resolution replaces \(A \rhd C[L]\) by the SGGS-resolvent \( Res (C,D) = A \rhd R\), where R is \((C\setminus \{L\})\cup (D\setminus \{M\})\vartheta \).
The I-true literals in the resolvent inherit their assignments from the I-true literals in the parents. Since M is the implied literal in \(B \rhd D[M]\), the resolvent is still a conflict clause. SGGS-extension ensures that every I-false literal in a conflict clause is assigned to a justification in \(dp(\varGamma )\) (cf. [20, Def. 19]) and therefore can be resolved away. Thus, conflict explanation by one or more SGGS-resolution steps generates either \(\bot \) or an I-all-true conflict clause.
Suppose that SGGS-extension appends to the trail an I-all-true conflict clause \(B \rhd D[M]\), or that \(B \rhd D[M]\) is the result of conflict explanation by SGGS-resolution. Then SGGS-move [20, Def. 25] (rule \(\textsf{move}\) in Fig. 2) moves \(B \rhd D[M]\) to the left of the clause \(A \rhd C[L]\) in \(dp(\varGamma )\) to which M is assigned. The effect is to solve the conflict by flipping the I-true literal M from being uniformly false in \(I[\varGamma ]\) to being an implied literal with justification \(B \rhd D[M]\). This is why the selected literal in an I-all-true conflict clause is the one assigned rightmost: when the clause moves left, all other I-true literals remain assigned. After the move, \(B \rhd D[M]\) resolves with \(A \rhd C[L]\). Prior to the move, \(B \rhd D[M]\) may split \(A \rhd C[L]\) by left-splitting [20, Def. 25] (rule \(\textsf{l}\text {-}\textsf{split}\) in Fig. 2), and then move to the left of its representative in the splitting. If \(B \rhd D[M]\) has another literal Q that is assigned to \(A \rhd C[L]\), has the same sign as M, and unifies with M, SGGS-factoring [20, Def. 27] (rule \(\textsf{factor}\) in Fig. 2) applies to avoid a situation where Q has nowhere to be assigned after the move.
The fairness of an SGGS-derivation involves several properties: an inference is applied whenever \(\bot \not \in \varGamma \) and \(I[\varGamma ]\not \models S\); no splitting is trivial;Footnote 3 SGGS-deletion is applied eagerly; all conflicting SGGS-extensions are followed right away by conflict solving; and inferences applying to shorter prefixes of the trail are never neglected in favor of others applying to longer prefixes (cf. [20, Defs. 32, 37, and 49]). The limit of a fair derivation \(\varGamma _0 \vdash \varGamma _1 \vdash \ldots \varGamma _j \vdash \varGamma _{j+1} \vdash \ldots \) is the longest trail \(\varGamma _\infty \) such that \(\forall i\), \(i \leqslant \vert \varGamma _\infty \vert \), there exists an \(n_i\) such that \(\forall j\), \(j \geqslant n_i\), if \(\vert \varGamma _j \vert \ge i\) then \(\mathop {\varGamma _j\vert _{i}} \approx ^c \mathop {\varGamma _\infty \vert _{i}}\), where \(\approx ^c\) is the equivalence associated to a convergence ordering \(>^c\) on trails ([20, Defs. 46, 50]). In words, all prefixes of the trail stabilize eventually. Both the derivation and its limit \(\varGamma _\infty \) may be infinite, but if the derivation halts at stage k, then \(\varGamma _\infty = \varGamma _k\). The following results are used in this paper:
-
1.
Finiteness of descending chains of length-bounded trails [20, Thm. 6 and Cor. 2]: A chain \(\varGamma _0>^c \varGamma _1>^c \ldots \varGamma _j >^c \varGamma _{j+1} \ldots \) where \(\forall j\), \(j\ge 0\), \(\vert \varGamma _j\vert \leqslant n\), for some \(n\ge 0\), is finite.
-
2.
Descending chain theorem [20, Thm. 8]: A fair SGGS-derivation forms a descending chain \(\varGamma _0>^c \varGamma _1>^c \ldots>^c \varGamma _j >^c \varGamma _{j+1} \ldots \).
-
3.
Completeness [20, Thm. 9 and 11]: For all input clause sets S, initial interpretations I, and fair SGGS-derivations, if S is satisfiable, \(I[\varGamma _\infty ]\models S\) (model completeness in the limit), and if S is unsatisfiable, \(\bot \in \varGamma _k\) for some k (refutational completeness).
Results (1) and (2) above lead to prove termination and decidability by showing that the length of trails in a fair SGGS-derivation is upper bounded.
4 SGGS and Known Decidable Fragments
In this section we use the concept of finite basis to ensure that the length of trails in a fair SGGS-derivation is upper bounded, so that the derivation is guaranteed to halt. If the input is satisfiable, the cardinality of the finite basis offers an upper bound on the cardinality of the generated model. The SGGS-decidability of Datalog and of the stratified fragment is a straightforward consequence. On the other hand, counterexamples show that SGGS with sign-based semantic guidance cannot decide other known decidable fragments. These derivations are useful to understand SGGS. Then we show that if clauses are ground-preserving, SGGS terminates whenever hyperresolution does.
4.1 SGGS-Derivations in a Finite Basis are Finite
Let S be the input set of clauses, \({{\mathcal {H}}}\) its Herbrand universe, and \({{\mathcal {A}}}\) its Herbrand base. A finite subset \(\mathcal{B}\subseteq {{\mathcal {A}}}\) is a finite basis for an SGGS-derivation if all cgi’s of all clauses on the trail during the derivation are made of atoms in \({{\mathcal {B}}}\).
Definition 3
(SGGS-Derivation in a basis) A clause \(A \rhd C\) is in \({{\mathcal {B}}}\) if \(at(Gr(A \rhd C))\subseteq {{\mathcal {B}}}\). A trail is in \({{\mathcal {B}}}\) if all its clauses are. An SGGS-derivation is in \({{\mathcal {B}}}\) if all its trails are.
The next lemma shows that the cardinality of \({{\mathcal {B}}}\) provides an upper bound on the length of the trail during a fair SGGS-derivation.
Lemma 1
If a fair SGGS-derivation \(\varGamma _0 \vdash \varGamma _1 \vdash \ldots \varGamma _j \vdash \varGamma _{j+1} \vdash \ldots \) is in a finite basis \({{\mathcal {B}}}\), then \(\forall j\), \(j\,{\geqslant }\,0\), \(\vert \varGamma _j\vert \leqslant \vert {{\mathcal {B}}}\vert {+}1\), and if \(dp(\varGamma _j) = \varGamma _j\) then \(\vert \varGamma _j\vert \leqslant \vert {{\mathcal {B}}}\vert \).
Proof
SGGS cannot do worse than generating a ground trail where every atom in \({{\mathcal {B}}}\) appears selected with either positive or negative sign: any trail with non-ground clauses cannot be longer, since a non-ground clause covers many (possibly infinitely many) ground instances. By fairness, if the trail contains an intersection given by clauses C[L] and D[L], or C[L] and \(D[\lnot L]\) with \(L\,{\in }\,{\mathcal {B}}\), the clause on the right is either deleted eagerly by SGGS-deletion, or replaced with a resolvent by SGGS-resolution before SGGS-extension applies. Thus, there can be at most one such intersection, and the first claim follows. The second claim holds, because \(dp(\varGamma _j) = \varGamma _j\) implies that there is no such intersection. \(\square \)
By the descending chain theorem and the finiteness of descending chains of length-bounded trails, the following general result follows:
Theorem 1
A fair SGGS-derivation in a finite basis is finite.
If for all sets S of clauses in a fragment \({\mathcal {F}}\) there exists a finite basis \({\mathcal {B}}\), which may depend on S, such that all SGGS-derivations from S are in \({\mathcal {B}}\), all fair SGGS-derivations from problems in \({\mathcal {F}}\) terminate, and SGGS decides \({\mathcal {F}}\). Assuming for simplicity the one-sorted case, where the cardinality of a model is that of its domain, we show that \({\mathcal {F}}\) also has the small model property: every satisfiable clause set in \({\mathcal {F}}\) admits a model whose cardinality is upper bounded. Let \({\mathcal {H}}({{\mathcal {B}}}) = \{ t \mathop {\,:}t \text { is a strict subterm of }L \text { for } L\!\in \! {\mathcal {B}}\}\), where “strict” says that the elements of \({{\mathcal {B}}}\) are not included. Since \({\mathcal {B}}\) is finite, \({\mathcal {H}}({{\mathcal {B}}})\) also is finite.
Theorem 2
If a fair SGGS-derivation from a satisfiable set S of clauses is in a finite basis \({\mathcal {B}}\), then S has a model of cardinality \(\vert {\mathcal {H}}({{\mathcal {B}}})\vert + 1\) that can be extracted from the limit of the derivation.
Proof
Let I be the initial interpretation. By Theorem 1 the derivation halts with some trail \(\varGamma \) which is its limit. Since SGGS is model complete in the limit, \(I[\varGamma ] \models S\). The domain of \(I[\varGamma ]\) is \({{\mathcal {H}}}\), which is infinite in general. However, since the derivation is in \({\mathcal {B}}\), all cgi’s of all clauses in \(\varGamma \) are in \({\mathcal {B}}\), and therefore we can extract from \(I[\varGamma ]\) a model J with domain \(\smash {{\mathcal {H}}({{\mathcal {B}}})} \uplus \{u\}\), where \(u\) is a new constant symbol. For every constant symbol c, let \(c^J = c\) if \(c \in {\mathcal {H}}({{\mathcal {B}}})\), and \(c^J = u\) otherwise; for every n-ary (\(n \geqslant 1\)) function symbol f, let \(\smash {f^J({t_1},\dots ,{t_{n}}) = f(t_1^J, \dots , t_n^J)}\) if \(f({t_1},\dots ,{t_{n}}) \in \smash {{\mathcal {H}}({{\mathcal {B}}})}\), and \(f^J({t_1},\dots ,{t_{n}}) = u\) otherwise; for every predicate symbol P, \(({t_1},\dots ,{t_{n}}) \in P^J\) if and only if \(I[\varGamma ] \models P({t_1},\dots ,{t_{n}})\). Note that J is well-defined because if \(f({t_1},\dots ,{t_{n}}) \in \smash {{\mathcal {H}}({\mathcal B})}\) then \({t_1},\dots ,{t_{n}}\) are also, hence all terms are interpreted in \(\smash {{\mathcal {H}}({{\mathcal {B}}})} \uplus \{u\}\). As J agrees with \(I[\varGamma ]\) on all atoms, \(J \models S\), and its cardinality is \(\vert \smash {{\mathcal {H}}({{\mathcal {B}}})}\vert + 1\) by construction. \(\square \)
In summary, the finite basis approach for SGGS yields termination, decidability, and the small model property.
4.2 SGGS Decides Datalog, EPR, and the Stratified Fragment
A set of Datalog clauses, or Datalog program (e.g., [26]), is a set of Horn clauses where (i) there are no functions, so that all terms are either constants or variables, (ii) every fact is ground, and (iii) every variable that occurs in the positive literal of a rule C also occurs in at least one negative literal of C. Since the Herbrand universe and the Herbrand base \({{\mathcal {A}}}\) of a Datalog program are finite, \({{\mathcal {A}}}\) itself is the finite basis, and Theorem 1, together with the completeness theorems for SGGS, yields the following.
Theorem 3
Given a Datalog program S, every fair SGGS-derivation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
The Bernays–Schönfinkel (BS) class [14, 68] includes the sentences of the form \(\exists ^*\forall ^*\varphi \), where \(\varphi \) is a formula with no occurrences of either quantifiers or functions, while constants are allowed. The reduction of BS formulae to clausal form yields Effectively PRopositional logic [3, 37, 65], abbreviated EPR. The stratified fragment generalizes EPR to many-sorted logic [1, 47, 64].
A signature is stratified [1, 47, 64], if there is a well-founded ordering \(<_s\) on the set \(\varSigma \) of sorts, and for all functions \(f:s_1 \times \dots \times s_n \,{\rightarrow }\, s\), it holds that \(s_i\, {>_s}\, s\) for all i, \(1 \!\leqslant \! i \!\leqslant \! n\). The sort-dependency graph displays dependencies between sorts: it is a directed graph such that the set of vertices is \(\varSigma \) and there is an arc from s to \(s^\prime \) if and only if there is a function symbol \(f:s_1 \times \dots \times s_n \,{\rightarrow }\, s^\prime \) such that \(s_i \!=\! s\) for some i, \(1 \!\leqslant \! i \!\leqslant \! n\). A sort s is cyclic, if there exists a non-trivial path (i.e., a path of length greater or equal than 1) from s to s in the graph, and acyclic otherwise. In a stratified signature all sorts are acyclic. If a sentence over a stratified signature belongs to the \(\exists ^*\forall ^*\) fragment, Skolemization only introduces constants and preserves stratification. If there is only one sort, this fragment reduces to EPR, because stratification over a single sort implies that there are no function symbols. However, also stratified sentences with a prefix other than \(\exists ^*\forall ^*\) can yield stratified clauses [57].
Example 4
Assume the signature from Example 2, which is stratified with ordering \(s_1 >_ss_2\). The Skolemization of \(\forall x \exists y.\, \textsf{P}(\textsf{f}(x),y)\) preserves stratification, as clause \(\textsf{P}(\textsf{f}(x),\textsf{g}(x))\) with Skolem symbol \(\textsf{g}:s_1{\rightarrow } s_2\) is still stratified. On the other hand, the Skolemization of \(\forall x \exists y.\, \textsf{P}(\textsf{f}(y),x)\) yields \(\textsf{P}(\textsf{f}(\textsf{g}(x)),x)\) with Skolem symbol \(\textsf{g}:s_2{\rightarrow } s_1\), so that stratification is lost.
A set of clauses whose signature is stratified is also called stratified. Since stratification prevents building terms of unbounded depth, the Herbrand universe and the Herbrand base are again finite, and we have the next theorem.
Theorem 4
Given a stratified input set S, every fair SGGS-derivation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
However, SGGS-derivations in EPR can be exponentially long, as in the following example with a clause set \(S_k\) that describes a k-digits binary counter. Let \(\textsf{Q}\) be a predicate symbol of arity k, and for all i, \(1\,{\leqslant }\,i\,{\leqslant }\,k\), let \(\overline{\textsf{0}}_i\), \(\overline{\textsf{1}}_i\), and \({\overline{x}}_i\) be i-tuples of \(\textsf{0}\)’s, \(\textsf{1}\)’s, and distinct variables \(x_1,\dots , x_i\), respectively. Then \(S_k\) consists of the following \(k + 2\) clauses, for \(0\leqslant m \leqslant k-1\):
This set was used in the context of an analysis of first-order theorem-proving strategies [66, Def. 2.4.10] to show that resolution can do better than hyperresolution or positive/negative resolution. Indeed, resolution offers a refutation in \(2k{+}1\) steps [66, Thm. 2.4.11], whereas positive resolution and positive hyperresolution simulate the binary counter, and negative resolution and negative hyperresolution do the same counting in reverse, so that all four strategies generate exponentially long derivations [66, Thm. 2.4.12]. As these sign-based refinements of resolution only generate ground clauses from \(S_k\), this set was also used to show that generating ground instances and applying a propositional proof system can do exponentially worse than resolution in EPR [59, Sect. 2.1]. A recent model-based clause-learning decision procedure for EPR named SCL and evolved from NRCL [3] also behaves exponentially on \(S_k\) [37, Sect. 4]. Unlike in Example 3, SGGS behaves like hyperresolution on \(S_k\).
Example 5
Given as input the k-digits binary counter clause set \(S_k\), and \(I^-\) as initial interpretation, SGGS generates a derivation that simulates binary counting with a series of \(2^k{+}1\) SGGS-extension steps, each adding a clause:
At this stage a conflict emerges with \(I^-\)-all-true conflict clause \([\lnot \textsf{Q}(\overline{\textsf{1}}_k)]\). After another \(2^{k+1}\) steps, alternating SGGS-move (abbreviated \(\textsf{move}\)) and SGGS-resolution (abbreviated \(\textsf{resolve}\)), unsatisfiability is detected:
SGGS with \(I^+\) also behaves exponentially operating the counter in reverse.
In essence, this set of clauses appears to defeat simultaneously sign-based semantic guidance, instance generation, and conflict-driven clause learning.
4.3 SGGS Does Not Decide the Ackermann, Monadic, and \(\textsf{FO}^2\) Classes
In this section we show that SGGS with sign-based semantic guidance does not decide the Ackermann, monadic, and \(\textit{FO}^2\) fragments. Let \(\varphi \) be a formula with no occurrences of either quantifiers or functions, while constants are allowed. The Ackermann class comprises the sentences of the form \(\exists ^*\forall \exists ^*\varphi \) [2, 35, 44]. The monadic, or Löwenheim, class contains the sentences where there are no functions and predicates are unary [2, 38, 44]. In the two-variable fragment, denoted \(\mathsf{F\!O}^2\), there are only two variables and no functions [38, 41].
We consider three sets of clauses to illustrate how SGGS works. Two of them are well-known in the literature. As these clause sets admit finite models, the nontermination of SGGS in these examples shows that SGGS is not guaranteed to terminate whenever the input set has a finite model. We conclude the section with an example that shows that it is not the case that whenever SGGS terminates there is a finite Herbrand model. Indeed, a finite SGGS trail can represent an infinite Herbrand model by using non-ground selected literals (SGGS is not restricted to generate ground instances of clauses) and by borrowing infinitely many literals from the initial interpretation.
The first set is \(S_0 = \{\textsf{P}(x) \vee \textsf{P}(\textsf{f}(x)),\ \lnot \textsf{P}(x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\}\) [44, Sect. 5]. Set \(S_0\) is in \(\mathsf{F\!O}^2\), because there are only two variables; and it is in the Ackermann and monadic classes because it is obtained from the Skolemization of the sentence \(\forall x \exists y. (\textsf{P}(x) \vee \textsf{P}(y)) \wedge (\lnot \textsf{P}(x) \vee \lnot \textsf{P}(y))\). \(S_0\) has a finite model \({{\mathcal {I}}}\) with domain \(\{0,1\}\), interpreting \(\textsf{P}\) as \(\textsf{P}^{{\mathcal {I}}} = \{0\}\), and \(\textsf{f}\) as \(\textsf{f}^{{\mathcal {I}}}(0) = 1\) and \(\textsf{f}^{{\mathcal {I}}}(1) = 0\). Adding to the signature a constant \(\textsf{a}\) to form Herbrand universe and Herbrand base, \(S_0\) has two infinite Herbrand models: \(J_1 = \{\textsf{P}(\textsf{f}^{2k}(\textsf{a})), \lnot \textsf{P}(\textsf{f}^{2k+1}(\textsf{a})) \mathop {\,:}k \geqslant 0\}\) and \(J_2 = \{\lnot \textsf{P}(\textsf{f}^{2k}(\textsf{a})), \textsf{P}(\textsf{f}^{2k+1}(\textsf{a})) \mathop {\,:}k \geqslant 0\}\).
The addition of \(\textsf{P} (\textsf{a})\) selects only \(J_1\) as Herbrand model, yielding a simpler problem \(S_1 = \{\textsf{P} (\textsf{a}),\ \textsf{P} (x) \vee \textsf{P}(\textsf{f}(x)), \ \lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\}\). \(S_1\) is in the same classes (membership in the Ackermann and monadic classes stems from the Skolemization of \(\exists w\forall x \exists y. \textsf{P}(w) \wedge (\textsf{P}(x) \vee \textsf{P}(y)) \wedge (\lnot \textsf{P}(x) \vee \lnot \textsf{P}(y))\)), and it is satisfied by finite model \({{\mathcal {I}}}\) extended with \(\textsf{a}^{{\mathcal {I}}} = 0\).
By enriching the signature so that binary clauses are mixed one gets \(S_2 = \{\textsf{P}(\textsf{a}),\ \lnot \textsf{P}(\textsf{b}),\ \lnot \textsf{P} (x) \vee \textsf{P}(\textsf{f}(x)), \ \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{g}(x^\prime ))\}\), which is in the same classes (membership in the Ackermann and monadic classes descends from the Skolemization of \(\exists v \exists w \forall x \exists y \exists z. \textsf{P}(v) \wedge \lnot \textsf{P}(w) \wedge (\lnot \textsf{P}(x) \vee \textsf{P}(y)) \wedge (\textsf{P}(x) \vee \lnot \textsf{P}(z))\)), has only Herbrand model \(J_3 = \{\textsf{P} (\textsf{a}), \lnot \textsf{P}(\textsf{b}), \textsf{P}(\textsf{f}^{k}(\textsf{a})), \lnot \textsf{P}(\textsf{g}^{k}(\textsf{b})) \mathop {\,:}k{\geqslant }0\}\), and finite model \({{\mathcal {I}}}\) extended with \(\textsf{b}^{{\mathcal {I}}} = 1\) and \(\textsf{g}^\mathcal{I} = \textsf{f}^{{\mathcal {I}}}\). Problem \(S_2\) is even simpler, because it is made of Horn clauses, and because with binary mixed clauses every sign-guided hyperinference unifies only one pair of literals.
Resolution, even with subsumption, generates infinitely many clauses from \(S_0\), \(S_1\), and \(S_2\), and so does hyperresolution [44]. From \(S_0\) positive hyperresolution generates \(\{\textsf{P}(x) \vee \textsf{P}(\textsf{f}^{2k+1}(x)) \mathop {\,:}k \geqslant 1\}\) and negative hyperresolution generates \(\{\lnot \textsf{P}(x) \vee \lnot \textsf{P}(\textsf{f}^{2k+1}(x)) \mathop {\,:}k \geqslant 1\}\). From \(S_1\) positive hyperresolution also adds \(\{\textsf{P}(\textsf{f}^{2k}(\textsf{a}) \mathop {\,:}k \geqslant 1\}\), while negative hyperresolution also adds \(\{\lnot \textsf{P}(\textsf{f}^{2k+1}(\textsf{a}) \mathop {\,:}k \geqslant 0\}\). From \(S_2\) positive hyperresolution generates \(\{\textsf{P}(\textsf{f}^k(\textsf{a})) \mathop {\,:}k \geqslant 1\}\) and negative hyperresolution generates \(\{\lnot \textsf{P}(\textsf{g}^k(\textsf{b})) \mathop {\,:}k \geqslant 1\}\). Ordered resolution with an ordering > on literals such that \(\textsf{P}(\textsf{f}(x)) > \textsf{P}(x)\), and \(\textsf{P}(\textsf{g}(x)) > \textsf{P}(x)\) for \(S_2\), plus tautology elimination for \(S_0\) and \(S_1\), terminates right away.
The first example of this section shows how SGGS generates infinite derivations from \(S_2\), working to modify \(I^-\) or \(I^+\) to get model \(J_3\) in the limit. Set \(S_2\) is so simple that derivations made only of SGGS-extensions are possible.
Example 6
Given \(S_2\) and \(I = I^-\), the SGGS-derivation begins by putting on trail \(\varGamma \) the I-all-false (i.e., positive) clause \(\textsf{P}(\textsf{a})\). Thus, \(I[\varGamma ]\models \textsf{P}(\textsf{a})\), but \(I[\varGamma ] \not \models \lnot \textsf{P}(x) \vee \textsf{P}(\textsf{f}(x))\), and an infinite series of instances gets generated:
The derivation lists as selected the positive literals of \(J_3\), while \(I[\varGamma ]\) gets the negative ones from \(I^-\). If the initial interpretation is \(I^+\), SGGS starts by putting \([\lnot \textsf{P}(\textsf{b})]\) on the trail, and then generates the instances of \(\textsf{P}(x^\prime ) \vee \lnot \textsf{P}(\textsf{g}(x^\prime ))\) by an infinite series of SGGS-extensions. The derivation lists as selected the negative literals of \(J_3\), as \(I[\varGamma ]\) imports the positive ones from \(I^+\).
The next example shows how input set \(S_1\) induces SGGS to embark in infinite derivationsFootnote 4 aiming at reaching model \(J_1\) in the limit.
Example 7
Given \(S_1 = \{ \textsf{P} (\textsf{a}),\ \textsf{P} (x) \vee \textsf{P}(\textsf{f}(x)), \ \lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime )) \}\) and \(I = I^-\), the SGGS-derivation starts by placing the I-all-false input clauses on the trail:
where either literal can be selected in the second clause. Selecting \(\textsf{P}(\textsf{f}(x))\) avoids an intersection with \(\textsf{P}(\textsf{a})\), but suppose that \(\textsf{P}(x)\) is selected. Then the first clause splits the second one by s-splitting and SGGS-deletion removes the representative because it is disposable. We abbreviate \(top(x) \ne \textsf{a} \rhd \varphi [x]\) as \(\varphi [\textsf{f}(x)]\) where x is a new variable.
At this point \(I[\varGamma ]\) satisfies no instance of the I-all-true input clause \(\lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\). SGGS-extension fires unifying the two literals of this clause with the two selected literals on the trail (the mgu is \(\alpha = \{ x^\prime \leftarrow \textsf{a},\ x\leftarrow \textsf{a} \}\)):
The added clause is a conflict clause with \(\lnot \textsf{P}(\textsf{a})\) assigned to the first clause, and \(\lnot \textsf{P}(\textsf{f}(\textsf{a}))\) to the second one, so that \(\lnot \textsf{P}(\textsf{f}(\textsf{a}))\) is selected, because the selected literal in an I-all-true clause, if selected, must be assigned rightmost. Since \(\textsf{P}(\textsf{f}(\textsf{a}))\) is less general than \(\textsf{P}(\textsf{f}(x))\) (\(\lnot Gr(\lnot \textsf{P}(\textsf{f}(\textsf{a}))) \subset Pcgi(\textsf{P}(\textsf{f}(x)), \varGamma )\)), the third clause splits the second one by left splitting (abbreviated \(\textsf{l}\text {-}\textsf{split}\)), which enables SGGS-move followed by SGGS-resolution:
The infinite derivation lists as selected the literals \(\textsf{P}(\textsf{a}),\ \lnot \textsf{P}(\textsf{f}(\textsf{a})),\ \textsf{P}(\textsf{f}^2(\textsf{a})),\ldots \) of model \(J_1\), and so do three other infinite derivations, one with \(I = I^-\) and \(\textsf{P}(\textsf{f}(x))\) selected in the second extension clause, one with \(I = I^+\) and \(\textsf{P}(x)\) selected, and one with \(I = I^+\) and \(\textsf{P}(\textsf{f}(x))\) selected.
The following example illustrates how SGGS generates infinite derivations from \(S_0\) to get either model \(J_1\) or model \(J_2\) depending on literal selection.
Example 8
Given \(S_0 = \{\textsf{P}(x) \vee \textsf{P}(\textsf{f}(x)),\ \lnot \textsf{P}(x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\}\), and \(I = I^-\), the first SGGS-extension adds the I-all-false input clause
where either literal can be selected and \(\textsf{P}(x)\) is. If \(\textsf{P}(x)\) is selected, SGGS builds model \(J_1\), and if \(\textsf{P}(\textsf{f}(x))\) is selected, SGGS builds model \(J_2\). SGGS-extension applies next with \(\lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\) as main premise and two variants \([\textsf{P} (x_1)] \vee \textsf{P}(\textsf{f}(x_1))\) and \([\textsf{P} (x_2)] \vee \textsf{P}(\textsf{f}(x_2))\) of the clause in \(\varGamma \) as side premises. There are two mgu’s, hence two possible steps with extension clause \(\lnot \textsf{P} (x) \vee \lnot \textsf{P}(\textsf{f}(x))\): \(\alpha _1 = \{x_1\leftarrow x^\prime , x_2\leftarrow \textsf{f}(x^\prime )\}\) and \(\alpha _2 = \{x_2\leftarrow x^\prime , x_1\leftarrow \textsf{f}(x^\prime )\}\). If \(\alpha _1\) is applied, \(\lnot \textsf{P} (x)\) is assigned to the first variant and \(\lnot \textsf{P}(\textsf{f}(x))\) to the second one, so that \(\lnot \textsf{P}(\textsf{f}(x))\) is selected, because the selected literal in an I-all-true clause, if assigned, must be assigned rightmost. If \(\alpha _2\) is applied, \(\lnot \textsf{P}(\textsf{f}(x))\) is assigned to the first variant and \(\lnot \textsf{P} (x)\) to the second one, so that \(\lnot \textsf{P} (x)\) is selected. Putting both variants on the trail is useless, since SGGS-deletion removes the second one, and both literals of the extension clause can be assigned to the first clause on the trail, but distinguishing the two mgu’s is useful to see which literal gets selected in the extension clause. If \(\alpha _2\) is applied, the result is:
However at this point the derivation is stuck, because neither SGGS-move nor SGGS-factoring nor left splitting apply to the I-all-true conflict clause. SGGS-move does not apply because the second clause has two literals assigned to the first one. SGGS-factoring does not apply because the two literals do not unify. Left splitting does not apply because \(\lnot Gr(\lnot \textsf{P}(x)) = pcgi(\textsf{P}(x), \varGamma )\). Since a stuck derivation is not fair, a stuck state must be avoided by looking ahead or undoing. If \(\alpha _1\) is applied, the derivation proceeds with left splitting:
where \(\lnot \textsf{P}(x) \vee [\lnot \textsf{P}(\textsf{f}(x))]\) is removed, because it has literals assigned to the split clause. SGGS-extension applies again with \(\lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\) as main premise, the two clauses in \(\varGamma \) as side premises, and mgu \(\alpha = \{x^\prime \leftarrow x\}\):
The first and the second literal of the extension clause are assigned to the first and second clause, respectively, so that the second literal is selected. Then left splitting applies:
so that SGGS-move and SGGS-resolution can solve the conflict:
As the selected literals of the third and fourth clauses intersect, s-splitting applies, followed by the deletion of the representative:
Since \(top(x) \ne \textsf{f}\) is satisfied by \(\{x\leftarrow \textsf{a}\}\) in the Herbrand universe, the infinite derivation is listing \(J_1 = \{\textsf{P}(\textsf{a}),\ \lnot \textsf{P}(\textsf{f}(\textsf{a})),\ \textsf{P}(\textsf{f}^2(\textsf{a})),\ldots \}\). If \(\textsf{P} (\textsf{f}(x))\) is selected in the first clause, the same sequence of inference rules is applied:
Unlike in the first derivation, the resolvent is disposable and gets deleted:
The derivation continues with SGGS-extension with \(\lnot \textsf{P} (x^\prime ) \vee \lnot \textsf{P}(\textsf{f}(x^\prime ))\) as main premise, the third and first clauses in \(\varGamma \) as side premises, and mgu \(\alpha = \{x^\prime \leftarrow \textsf{f}^3(y),\ x\leftarrow \textsf{f}(y)\}\), renaming as y the x in the third clause of \(\varGamma \):
The first three selected literals are \(\textsf{P}(\textsf{f}(\textsf{a}))\), \(\lnot \textsf{P}(\textsf{f}^2(\textsf{a}))\), and \(\textsf{P}(\textsf{f}^3(\textsf{a}))\), and since \(I[\varGamma ]\) gets \(\lnot \textsf{P}(\textsf{a})\) from \(I^-\), model \(J_2 = \{\lnot \textsf{P}(\textsf{a}),\ \textsf{P}(\textsf{f}(\textsf{a})),\ \lnot \textsf{P}(\textsf{f}^2(\textsf{a})),\ \textsf{P}(\textsf{f}^3(\textsf{a}))\ldots \}\) emerges. Since \(S_0\) is symmetric with respect to sign, with \(I = I^+\) one gets two derivations identical to those above, except that all signs of all literals on the trail are flipped: the first derivation yields \(J_2\) and the second one yields \(J_1\).
Terminating SGGS-derivations can capture infinite Herbrand models, as a finite SGGS trail can represent an infinite Herbrand model by using non-ground selected literals and by borrowing infinitely many literals from I.
Example 9
Let the input set of clauses be \(S = \{(i)\ \textsf{P}(x, \textsf{a}), \ (ii)\ \lnot \textsf{P}(x,y) \vee \textsf{R}(y) \vee \textsf{P}(x,\textsf{f}(y)), \ (iii)\ \lnot \textsf{R}(\textsf{f}(x)) \vee \lnot \textsf{P}(x,\textsf{f}(x))\}\). SGGS with \(I^+\) halts after putting clause (iii) on the trail. If the first literal is selected, we have
where \(I^p(\varGamma _1) = \{\lnot \textsf{R}(\textsf{f}^k(\textsf{a})) \mathop {\,:}k \geqslant 1\}\) and \(I[\varGamma _1]\) is the infinite Herbrand model given by \(I^p[\varGamma _1]\) plus all the positive literals whose complement is not in \(I^p(\varGamma _1)\). If the second literal is selected,
we have \(I^p(\varGamma _1) = \{\lnot \textsf{P}(\textsf{f}^k(\textsf{a}),\textsf{f}^{k+1}(\textsf{a})) \mathop {\,:}k \geqslant 0\}\) and \(I[\varGamma _1]\) is the infinite Herbrand model given by \(I^p[\varGamma _1]\) plus all the positive literals whose complement is not in \(I^p(\varGamma _1)\). If I is \(I^-\), the termination of SGGS depends on literal selection. The following derivation halts:
with \(I^p(\varGamma _2) = \{\textsf{P}(\textsf{f}^{k}(\textsf{a}), \textsf{a}) \mathop {\,:}k \geqslant 0\} \cup \{ \textsf{R}(\textsf{a})\}\) and \(I[\varGamma _2]\) given by \(I^p(\varGamma _2)\) plus all the negative literals whose atom is not in \(I^p(\varGamma _2)\). If the last literal in the instances of \(\lnot \textsf{P}(x,y) \vee \textsf{R}(y) \vee \textsf{P}(x,\textsf{f}(y))\) is systematically selected, SGGS with \(I^-\) diverges:
Hyperresolution generates infinitely many clauses from this set. For example, using (ii) as nucleus, (i) as initial satellite, and then each resulting hyperresolvent as next satellite, positive hyperresolution produces \(\textsf{R}(\textsf{a}) \vee \textsf{P}(x,\textsf{f}(\textsf{a}))\), \(\textsf{R}(\textsf{a}) \vee \textsf{R}(\textsf{f}(\textsf{a})) \vee \textsf{P}(x,\textsf{f}^2(\textsf{a}))\), \(\textsf{R}(\textsf{a}) \vee \textsf{R}(\textsf{f}(\textsf{a})) \vee \textsf{R}(\textsf{f}^2(\textsf{a})) \vee \textsf{P}(x,\textsf{f}^3(\textsf{a}))\), and so on.
4.4 SGGS Does Not Decide the Guarded Fragment
In this section we show by counterexamples that SGGS with sign-based semantic guidance does not decide the guarded fragment [4, 29]. The guarded fragment admits no function symbols and restricts quantification to the following schemes: \(\forall {\bar{y}}. (R({\bar{x}},{\bar{y}})\supset \psi [{\bar{x}},{\bar{y}}])\) and \(\exists {\bar{y}}. (R({\bar{x}},{\bar{y}})\wedge \psi [{\bar{x}},{\bar{y}}])\), where \(\psi \) is also a guarded formula, and all the variables that occur in \(\psi \) must appear in the atomic guard \(R({\bar{x}},{\bar{y}})\). For the fragments considered in the previous sections, the clausal version of a fragment contains the sets of clauses generated by transforming into clausal form the formulae of the fragment. For the guarded fragment this is not the case: we adopt the existing notion of guarded clauses [29] and we refer to [29] for a discussion of reduction to clausal form in the guarded fragment.
A clause C is guarded, if (i) for all non-ground compound subterms t of C, \(\mathcal Var(t) = \mathcal Var(C)\), and (ii) if \(\mathcal Var(C) \ne \emptyset \), there exists a literal \(L\in C^-\), called a guard, such that \(\mathcal Var(L) = \mathcal Var(C)\) and every compound subterm of L is ground [29]. Although formulæ in the guarded fragment have no function symbols, guarded clauses may contain function symbols introduced by Skolemization. A guarded set is a set of guarded clauses. For example, \(G_0 = \{\textsf{R}(\textsf{f}(\textsf{a})),\ \lnot \textsf{P}(x) \vee \textsf{R}(x) \vee \textsf{Q}(\textsf{f}(x))\}\) is a guarded set. Given \(G_0\), SGGS with \(I^+\) halts right away, and SGGS with \(I^-\) halts after placing \(\textsf{R}(\textsf{f}(\textsf{a}))\) on the trail. However, it is simple to give a guarded set where the termination of SGGS depends on the initial interpretation.
Example 10
Given the guarded set \(G_1 = \{\textsf{P}(\textsf{a}),\ \lnot \textsf{P}(x) \vee \textsf{P}(\textsf{f}(x))\}\), SGGS with \(I^+\) halts right away, but the SGGS-derivation with \(I^-\) is infinite:
In the next example the termination of SGGS depends on both initial interpretation and literal selection.
Example 11
Given the guarded set \(G_2 = \{\lnot \textsf{P}(\textsf{a}),\ \lnot \textsf{Q}(x) \vee \textsf{P}(x) \vee \lnot \textsf{P}(\textsf{f}(x))\}\), SGGS halts right away with \(I^-\), but goes on forever with \(I^+\):
where SGGS-extension is applied at every step. However, it suffices to select \(\lnot \textsf{Q}(\textsf{f}^n(\textsf{a}))\) in place of \(\lnot \textsf{P}(\textsf{f}^{n+1}(\textsf{a}))\), for some \(n \geqslant 0\), that the derivation halts.
In the following example SGGS does not terminate regardless of literal selection and choice between \(I^-\) and \(I^+\).
Example 12
The set \(G_3 = \{\textsf{P}(\textsf{a}),\ \lnot \textsf{P} (x) \vee \textsf{P}(\textsf{f}(\textsf{f}(x))), \ \lnot \textsf{P} (x) \vee \lnot \textsf{P}(\textsf{f}(x))\}\) is guarded and is satisfied by the same finite model \({{\mathcal {I}}}\) and infinite Herbrand model \(J_1\) given for \(S_1\) from the previous section. With \(I^-\) SGGS generates an infinite derivation that lists as selected the positive literals of model \(J_1\):
The SGGS-derivation with \(I^+\) is infinite even if literals of lower depth are preferred for selection, as the literals of model \(J_1\) are listed as selected:
Resolution generates infinitely many clauses from these sets, while hyperresolution behaves similarly to SGGS. From \(G_0\) both positive and negative hyperresolution generate nothing. From \(G_1\) negative hyperresolution does not generate anything, whereas positive hyperresolution yields the infinite series \(\{\textsf{P}(\textsf{f}^k(\textsf{a})) \mathop {\,:}k\geqslant 1\}\). From \(G_2\) positive hyperresolution does not generate anything, whereas negative hyperresolution yields the infinite series \(\{\bigvee _{i=0}^k \lnot \textsf{Q}(\textsf{f}^i(\textsf{a})) \vee \lnot \textsf{P}(\textsf{f}^{k+1}(\textsf{a})) \mathop {\,:}k\geqslant 0\}\). From \(G_3\) positive hyperresolution yields the infinite series \(\{\textsf{P}(\textsf{f}^{2k}(a))\}_{k\geqslant 0}\), while negative hyperresolution generates \(\lnot \textsf{P}(\textsf{f}(\textsf{a}))\) from nucleus \(\textsf{P}(\textsf{a})\) and satellite \(\lnot \textsf{P} (x) \vee \lnot \textsf{P}(\textsf{f}(x))\), and then the infinite series \(\{\lnot \textsf{P}(x) \vee \lnot \textsf{P}(\textsf{f}^{2k+1}(x)) \mathop {\,:}k\geqslant 1\}\) from nucleus \(\lnot \textsf{P} (x) \vee \textsf{P}(\textsf{f}(\textsf{f}(x)))\) using \(\lnot \textsf{P} (x) \vee \lnot \textsf{P}(\textsf{f}(x))\) as initial satellite and then each resulting hyperresolvent as next satellite. Given an ordering > on literals such that \(\textsf{P}(\textsf{f}(x)) > \textsf{P}(x)\) for \(G_1\) and \(G_2\), and such that \(\textsf{P}(\textsf{f}(x)) > \textsf{P}(x)\) and \(\textsf{P}(\textsf{f}^2(x)) > \textsf{P}(x)\) for \(G_3\), ordered resolution halts right away.
4.5 SGGS Decides the Ground-Preserving Sets Decided by Hyperresolution
SGGS with \(I^-\) or \(I^+\) as initial interpretation and hyperresolution share sign-based semantic guidance. We show that if the input clauses are positively ground-preserving, SGGS with \(I^-\) terminates whenever positive hyperresolution does. The result for SGGS with \(I^+\) and negative hyperresolution is dual.
Definition 4
(Ground-Preserving) A clause C is positively ground-preserving if \(\mathcal Var(C)\subseteq \mathcal Var(C^-)\), and negatively ground-preserving if \(\mathcal Var(C)\subseteq \mathcal Var(C^+)\). A set of clauses is positively/negatively ground-preserving if all its clauses are, and ground-preserving if it is one or the other.
For example, \(\lnot \textsf{P}(x,y,z) \vee \textsf{Q}(y) \vee \textsf{Q}(\textsf{f}(z))\) and \(\lnot \textsf{Q}(x) \vee \lnot \textsf{Q}(y)\) are positively ground-preserving. Datalog clauses are positively ground-preserving. The binary counter clauses of Example 5 are both positively and negatively ground-preserving. Guarded clauses are positively ground-preserving, since the guard is negative and contains all variables.
If a set S is positively ground-preserving, the positive clauses in S are ground, hence the initial satellites are ground, and positive hyperresolution generates only ground clauses, as at every step all variables in the nucleus get instantiated with ground terms by the simultaneous mgu with literals in ground satellites. The dual properties hold for the negative variant.
We begin by showing that SGGS also has this property, which implies that SGGS-splitting inferences do not apply and hence SGGS-constraints do not appear. Let I be suitable for a ground-preserving set S if either I is \(I^-\) and S is positively ground-preserving, or I is \(I^+\) and S is negatively ground-preserving.
Lemma 2
If the input set S is ground-preserving, all clauses on the trail of a fair SGGS-derivation with initial interpretation suitable for S are ground.
Proof
Assume that S is positively ground-preserving and I is \(I^-\) (the other case is dual). The proof is by induction on the stage k such that the step \(\varGamma _k \vdash \varGamma _{k+1}\) adds clause C to the trail (i.e., C appears in \(\varGamma _{k+1}\)).
Base case: \(k=0\), and C is one of the \(I^-\)-all-false (i.e., positive) input clauses added by the first SGGS-extension that yields \(\varGamma _1\). (S must contain at least an \(I^-\)-all-false clause, because otherwise it would be satisfied by \(I^-\) and the derivation would not even start.) Since S is ground-preserving, C is ground.
Induction hypothesis: for all j, \(0\le j < k\), all clauses C added by the step \(\varGamma _j \vdash \varGamma _{j+1}\) are ground.
Inductive case: let C be a clause added to the trail by the step \(\varGamma _k \vdash \varGamma _{k+1}\). The only inferences that generate new clauses are SGGS-splitting, SGGS-resolution, and SGGS-extension. \(\varGamma _k \vdash \varGamma _{k+1}\) cannot be a splitting step, because the splitting of a ground clause is trivial, hence excluded by fairness. If \(\varGamma _k \vdash \varGamma _{k+1}\) is an SGGS-resolution step, a resolvent of ground clauses is also ground. If \(\varGamma _k \vdash \varGamma _{k+1}\) is an SGGS-extension step, it adds an instance \(C\alpha \) of a clause \(C\in S\), where \(\alpha \) is the simultaneous mgu of all \(I^-\)-true (i.e., negative) literals \(L_1, \dots , L_n\) in C with as many \(I^-\)-false (i.e., positive) selected literals \(M_1,\ldots , M_n\) in clauses in \(\varGamma \). By induction hypothesis, the clauses containing \(M_1, \ldots , M_n\) are ground. Thus, \(L_1\alpha , \ldots , L_n\alpha \) are also ground. The \(I^-\)-false (i.e., positive) literals of \(C\alpha \) are ground, because C is positively ground-preserving, so that all its variables appear in a negative literal and get grounded by \(\alpha \). Thus, \(C\alpha \) is ground. \(\square \)
Let \(Res^+_{H}(S)\) be the set of positive hyperresolvents generated from S; \(R_{H}^0(S) = S\), \(R_{H}^{k+1}(S) = R_{H}^{k}(S) \cup Res^+_{H}(R_{H}^{k}(S))\), and \(R_{H}^{*}(S) = \bigcup _{k{\geqslant }0} R_{H}^k(S)\). If S is positively ground-preserving, all clauses in \(R_{H}^{*}(S) \setminus S\) are ground.
Lemma 3
If the input set S is positively ground-preserving, for all fair SGGS-derivations with \(I^-\) as initial interpretation, for every clause C on the trail during the derivation, there exists a positive clause \(C^\prime \in R_{H}^{*}(S)\) such that \(C^+ \subseteq C^\prime \).
Proof
By Lemma 2 all clauses C that appear on the trail during the derivation are ground. The proof is by induction on the stage k such that the step \(\varGamma _k \vdash \varGamma _{k+1}\) adds clause C to the trail (i.e., C appears in \(\varGamma _{k+1}\)).
Base case: \(k=0\), and C is one of the \(I^-\)-all-false (i.e., positive) input clauses added by the first SGGS-extension that yields \(\varGamma _1\). Then \(C^+ = C\) and \(C^\prime = C \in S \subseteq R_{H}^{*}(S)\).
Induction hypothesis: for all j, \(0\le j < k\), for all clauses C added by step \(\varGamma _j \vdash \varGamma _{j+1}\) the claim holds.
Inductive case: let C be a clause added to the trail by step \(\varGamma _k \vdash \varGamma _{k+1}\). By fairness, SGGS-splitting does not apply to ground clauses, and we only need to consider SGGS-resolution and SGGS-extension. If \(\varGamma _k \vdash \varGamma _{k+1}\) is an SGGS-resolution step, the added clause is the SGGS-resolvent R generated from (ground) parents \(C_1[L]\) and \(C_2[\lnot L]\), where L is \(I^-\)-false (i.e., positive) and \(C_2[\lnot L]\) is \(I^-\)-all-true (i.e., negative), so that \(R^+ \subseteq {C_1}^+\). By induction hypothesis there exists a positive clause \(C^\prime \in R_{H}^{*}(S)\) such that \({C_1}^+ \subseteq C^\prime \), and hence \(R^+ \subseteq C^\prime \). If \(\varGamma _k \vdash \varGamma _{k+1}\) is an SGGS-extension step with main premise \(C \in S\) and side premises \(D_1[M_1],\ldots , D_n[M_n]\) in \(\varGamma _k\), the added clause is the instance \(C\alpha \), for \(\alpha \) the simultaneous mgu of all \(I^-\)-true (i.e., negative) literals \(L_1, \dots , L_n\) in C with the \(I^-\)-false (i.e., positive) selected literals \(M_1,\ldots , M_n\). By induction hypothesis, for all i, \(1 \leqslant i \leqslant n\), there exists a positive clause \({\widehat{D}}_i \in R_{H}^{*}(S)\) such that \(D_i^+ \subseteq {\widehat{D}}_i\), so that \(M_i\) is a literal of \({\widehat{D}}_i\). Thus, positive hyperresolution applies to nucleus C and satellites \({\widehat{D}}_1, \dots , \widehat{D}_n\) resolving upon all the negative literals \(L_1, \dots , L_n\) in C and the positive literals \(M_i\) in \({\widehat{D}}_i\) (\(1 \leqslant i \leqslant n\)) with simultaneous mgu \(\alpha \). The generated positive hyperresolvent is \(C^\prime = (C^+ \vee {\widehat{D}}_1\setminus \{M_1\} \vee \ldots \vee {\widehat{D}}_n\setminus \{M_n\})\alpha \). Since \(C^+\alpha \subseteq C^\prime \), the claim holds. \(\square \)
Given a set S of clauses, positive hyperresolution is guaranteed to halt if and only if \(R_{H}^{*}(S)\) is finite. The next theorem shows that if positive hyperresolution is guaranteed to halt, so is SGGS.
Theorem 5
If the input set S is positively ground-preserving and \(R_{H}^{*}(S)\) is finite, all fair SGGS-derivations with \(I^-\) as initial interpretation are finite.
Proof
Since S is positively ground-preserving, all clauses in \(R_{H}^{*}(S) \setminus S\) are ground, and all clauses on the trail during an SGGS-derivation are ground. We prove the claim by proving the contrapositive: if there exists an infinite SGGS-derivation \(\varTheta \) with initial interpretation \(I^-\) and input S, then \(R_{H}^{*}(S)\) must be infinite. An SGGS-derivation can be infinite only if there are infinitely many SGGS-extension inferences, because the model fixing and conflict-solving activities of SGGS are inherently finite. Thus, \(\varTheta \) features infinitely many SGGS-extensions, adding ground clauses involving atoms of increasing depth. (If the depth of atoms were upper bounded, \(\varTheta \) would be in a finite basis and would be finite by Theorem 1.) Whenever an SGGS-extension adds a ground instance \(C\alpha \) of a clause \(C\in S\), the substitution \(\alpha \) is the simultaneous mgu of all the negative literals in C with positive selected literals on the trail. Since S is finite, there are finitely many candidates for main premise. Therefore, infinitely many SGGS-extensions can occur only if there are infinitely many distinct sets of side premises in \(\varTheta \) involving atoms of increasing depth. Since the selected literals in the side premises are positive, this means that in the derivation \(\varTheta \) infinitely many distinct \(C^+_j \subseteq C_j\) appear on the trail. By Lemma 3, for all (ground) clauses \(C_j\) on the trail during \(\varTheta \) there exists a positive (ground) clause \(C^\prime \in R_{H}^{*}(S)\) such that \(C^+_j\subseteq C^\prime \). Therefore, \(R_{H}^{*}(S)\) must be infinite. \(\square \)
The dual variants of Lemma 3 and Theorem 5 hold for SGGS-derivations with \(I^+\) and negative hyperresolution. Since the positive variable dominated (PVD) [25, 34] and bounded depth increase (BDI) [52] fragments are positively ground-preserving, and positive hyperresolution decides them, so does SGGS.Footnote 5
Corollary 1
Given a PVD or BDI input set S, every fair SGGS-derivation with \(I^-\) as initial interpretation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
5 SGGS Decides Three New Fragments of First-Order Logic
In this section we introduce three new decidable fragments of first-order logic, by showing that SGGS decides them. The first one is the restrained fragment, which combines ground-preservigness with an ordering-based property. The other two are the sort-restrained fragment, which generalizes the stratified and restrained fragments, and the sort-refined-PVD fragment, which generalizes the stratified and PVD fragments.
5.1 SGGS Decides the Restrained Fragments
The following example gives the intuition for restrained clauses.
Example 13
Consider the set \(S = \{(i)\ \textsf{P}(\textsf{s}^{10}(\textsf{0}), \textsf{s}^9(\textsf{0})),\ (ii)\ \lnot \textsf{P}(\textsf{s}(\textsf{s}(x)),y) \vee \textsf{P}(x,\textsf{s}(y))\}\), which is positively ground-preserving. Let \(I^-\) be the initial interpretation. SGGS-extension puts \(\textsf{P}(\textsf{10}, \textsf{9})\) on the trail, abbreviating \(\textsf{s}^n(\textsf{0})\) as \(\textsf{n}\). This stirs a series of SGGS-extensions aiming at adding to \(I[\varGamma ]\) the positive ground literals needed to satisfy (ii) while satisfying (i). Each SGGS-extension unifies the negative literal in (ii) with a selected positive ground literal in \(\varGamma \), so that new literals in added clauses are positive:
After adding \(\lnot \textsf{P}(\textsf{6,11}) \,\vee \,[\textsf{P}(\textsf{4,12})]\), \(\lnot \textsf{P}(\textsf{4,12})\, \vee \,[\textsf{P}(\textsf{2,13})]\), and \(\lnot \textsf{P}(\textsf{2,13}) \,\vee \, [\textsf{P}(\textsf{0,14})]\), SGGS halts with a model of S. The size of positive literals decreases as the derivation progresses, reflecting the fact that \(\textsf{P}(\textsf{s}(\textsf{s}(x)), y) \succ \textsf{P}(x, \textsf{s}(y))\) in clause (ii), for \(\succ \) any KBO or any LPO with \(\textsf{P} \succ _p \textsf{s}\) in the precedence.
This observation suggests to strengthen ground-preservingness with an ordering-based condition in order to get a finite basis.
Definition 5
(Restraining quasi-ordering) A quasi-ordering \(\succeq \) on terms and atoms is restraining, if (i) it is stable, (ii) the strict ordering \({\succ } = {{\succeq } \setminus {\preceq }}\) is well-founded, and (iii) the equivalence \({\approx } = {{\succeq } \cap {\preceq }}\) has finite equivalence classes.
Condition (i) implies that \(\succ \) and \(\approx \) are also stable. Let \(\succeq \) be a restraining quasi-ordering.
Definition 6
(Restrained) A clause C is (strictly) positively restrained if it is positively ground-preserving, and for all non-ground literals \(L \in C^+\) there exists a literal \(M\in C^-\) such that \(at(M)\succeq at(L)\) (\(at(M) \succ at(L)\)). A set of clauses is positively restrained if all its clauses are.
Negatively restrained clauses and clause sets are defined dually, and a set of clauses is restrained if it is positively or negatively restrained. The set of Example 13 is strictly positively restrained. The next example clarifies why a quasi-ordering is used.
Example 14
Problem PLA030-1 in TPTP is neither stratified, nor monadic, nor guarded. It includes a clause \(\textsf{differ}(x,y) \vee \lnot \textsf{differ}(y,x)\) that cannot be strictly restrained. Let \(\succ _{\textsf{acrpo}}\) be an AC-compatible [73] RPO with \(\textsf{differ}\) as an AC-symbol, where AC abbreviates associative-commutative. The quasi-ordering \(\succeq _{\textsf{acrpo}}\), built from \(\succ _{\textsf{acrpo}}\) and the AC-equivalence \(\approx _{\textsf{AC}}\) that has finite equivalence classes, satisfies \(\textsf{differ}(x,y) \approx _{\textsf{AC}} \textsf{differ}(y,x)\) hence \(\textsf{differ}(x,y) \succeq _{\textsf{acrpo}} \textsf{differ}(y,x)\), so that PLA030-1 is negatively restrained.
Definition 7
(Basis for a restrained set) Given a restrained set S of clauses with Herbrand base \({{\mathcal {A}}}\), let \({\mathcal {A}}_{S}\) be the set of ground atoms occurring in S. Then the basis for S is \({\mathcal {A}}_{S}^{\preceq } = \{L \mathop {\,:}L \in {{\mathcal {A}}},\ \exists M \in {\mathcal {A}}_{S} \text { such that } M \succeq L\}\).
In words, \({\mathcal {A}}_{S}^{\preceq }\) contains all the ground atoms upper bounded by those occurring in clauses in S. By Conditions (ii) and (iii) in Definition 5, \({\mathcal {A}}_{S}^{\preceq }\) is a finite basis. Since restrained sets are ground-preserving, the notion of suitable initial interpretation is the same as for ground-preserving sets.
Lemma 4
If the input set S is restrained, every fair SGGS-derivation with suitable initial interpretation is in the finite basis \({\mathcal {A}}_{S}^\preceq \).
Proof
We consider S positively ground-preserving and \(I^-\) (for the dual case one exchanges the signs). Since the set is restrained hence ground-preserving, the derivation is ground by Lemma 2 (\(\dag \)). The proof is by induction on the length k of the derivation, and it follows the same pattern as that of Lemma 2. Let \(\varGamma \vdash \varGamma ^\prime \) be the \((k{+}1)\)-th step. By induction hypothesis, \(\varGamma \) is in \({\mathcal {A}}_{S}^\preceq \). If \(\varGamma \vdash \varGamma ^\prime \) is an SGGS-resolution step, it is a ground resolution step which does not generate new atoms, and also \(\varGamma ^\prime \) is in \({\mathcal {A}}_{S}^\preceq \). If \(\varGamma \vdash \varGamma ^\prime \) is an SGGS-extension step, it adds an instance \(C\alpha \) of a clause \(C \in S\), where \(\alpha \) is the simultaneous mgu of all \(I^-\)-true (i.e., negative) literals \(\lnot L_1, \dots , \lnot L_n\) in C with as many \(I^-\)-false (i.e., positive) selected literals \(M_1,\ldots , M_n\) in \(\varGamma \). The literals \(M_1, \ldots , M_n\) are ground by (\(\dag \)), and by induction hypothesis they are in \({\mathcal {A}}_{S}^\preceq \). We have to show that \(at(C\alpha )\subseteq {\mathcal {A}}_{S}^\preceq \). For the negative literals \(\lnot L_1\alpha , \dots , \lnot L_n\alpha \) we have \(L_i\alpha = M_i\alpha = M_i \in {\mathcal {A}}_{S}^\preceq \). Let L be a literal in \(C^+\). If L is ground, then \(L\alpha = L\in {\mathcal {A}}_{S} \subseteq {\mathcal {A}}_{S}^\preceq \). If L is not ground, by positive restrainedness there exists a \(\lnot L_i\), \(1\,{\leqslant }\,i\,{\leqslant }\,n\), such that \(L_i \succeq L\). By stability, \(L_i\alpha \succeq L\alpha \). Since for all i, \(1\,{\leqslant }\,i\,{\leqslant }\,n\), \(M_i \in {\mathcal {A}}_{S}^\preceq \) and \(M_i = M_i\alpha = L_i\alpha \succeq L\alpha \), we have \(L\alpha \in {\mathcal {A}}_{S}^\preceq \). \(\square \)
Therefore, Theorems 1 and 2 yield decidability and the small model property.
Theorem 6
Given a restrained input set S, every fair SGGS-derivation with suitable initial interpretation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
Corollary 2
A restrained satisfiable set S of clauses has a model of cardinality \(\vert {\mathcal {H}}({{\mathcal {A}}_{S}^\preceq })\vert + 1\) that can be extracted from the limit of any fair SGGS-derivation with input S and suitable initial interpretation.
Example 15
The clause set of Example 13 is a subset of the following satisfiable clause set S from problem PUZ054-1 in TPTP:
This set, which is neither EPR nor \(\mathsf{F\!O}^2\) nor monadic, can be shown strictly positively restrained by any LPO with \(\textsf{P} \succ _p \textsf{s}\) in the precedence or by any KBO. Let \(\succ \) be a KBO with empty precedence, \(w(\textsf{P}) = 0\), and \(w(\textsf{s}) = w(\textsf{0}) = w_0 = 1\). \({\mathcal {A}}_{S}\) is \(\{ \textsf{P}(\textsf{s}^{10}(\textsf{0}), \textsf{s}^9(\textsf{0})),\ \textsf{P}(\textsf{s}(\textsf{0}), \textsf{0}) \}\) and its largest atom has weight \(w(\textsf{P}(\textsf{s}^{10}(\textsf{0}), \textsf{s}^9(\textsf{0}))) = 21\). \({\mathcal {A}}_{S}^{\preceq }\) cannot contain an atom \(L = \textsf{P}(\textsf{s}^n(\textsf{0}), \textsf{s}^m(\textsf{0}))\), with \(n \geqslant 0\) and \(m \geqslant 0\), if \(n > 19\) or \(m > 19\), because otherwise \(w(L) > w(\textsf{P}(\textsf{s}^{10}(\textsf{0}), \textsf{s}^9(\textsf{0})))\). Therefore, \(\smash {{\mathcal {H}}({{\mathcal {A}}_{S}^\preceq })} = \{\textsf{s}^i(\textsf{0}) \mathop {\,:}0{\leqslant }i{\leqslant }19\}\) and S has a model of cardinality 21 by Corollary 2.
Sign-based semantic guidance makes SGGS well suited for the restrained fragments. We see next that this holds also for sign-based resolution strategies.
5.2 Sign-Based Resolution Strategies Decide the Restrained Fragments
We consider PO-resolution and the positively restrained fragment. The results will then be extended to other positive strategies and to the dual case. Let \(Res^+_>(S)\) be the set of PO-resolvents generated from clauses in S, where > is the CSO on literals assumed by PO-resolution. Then, \(R_{>}^0(S) = S\), \(R_{>}^{k+1}(S) = R_{>}^{k}(S) \cup Res^+_{>}(R_{>}^{k}(S))\), and \(R_{>}^{*}(S) = \bigcup _{k{\geqslant }0} R_{>}^k(S)\).
Lemma 5
If S is positively restrained, then for all \(C \in R_{>}^*(S)\), for all \(L \in C^+\) either \(L \in {\mathcal {A}}_{S}^{\preceq }\) or \(at(M) \succeq at(L)\) for some \(M \in C^-\).
Proof
The proof is by induction on the stage k of the construction of \(R_{>}^*(S)\). For \(k{=}0\), the clauses in \(R_{>}^0(S)=S\) satisfy the claim by Definitions 6 and 7. The induction hypothesis is that all clauses in \(R_{>}^{k}(S)\) satisfy the claim. For the inductive case, let \((C \vee D)\sigma \in Res^+_{>}(R_{>}^{k}(S))\) be a PO-resolvent with mgu \(\sigma \) from parents \(\lnot L \vee C\) and \(L^\prime \vee D\) in \(R_{>}^{k}(S)\), where \(L^\prime \vee D\) is a positive clause. By induction hypothesis \(at(L^\prime \vee D) \subseteq {\mathcal {A}}_{S}^{\preceq }\) (\(\dag \)), which means \(L^\prime \vee D\) is ground, \((L^\prime \vee D)\sigma = L^\prime \vee D\), and \(at(D\sigma )\subseteq {\mathcal {A}}_{S}^{\preceq }\). For the positive literals in \(C\sigma \), let \(Q\sigma \) be one of them, so \(Q \in C^+\). By induction hypothesis, either (i) \(Q \in {\mathcal {A}}_{S}^{\preceq }\), or (ii) \(M \succeq Q\) for some negative literal \(\lnot M\) in \(\lnot L \vee C\). In case (i), Q is ground, \(Q\sigma = Q\), and \(Q\sigma \in {\mathcal {A}}_{S}^{\preceq }\). In case (ii), if \(\lnot M\) is one of the literals in C, then \(\lnot M\sigma \in C\sigma \), and \(M\sigma \succeq Q\sigma \) holds by stability, so that the claim follows. Otherwise, \(\lnot M\) is the resolved-upon literal \(\lnot L\) with \(L\sigma = L^\prime \sigma \). Thus, \(L = M \succeq Q\), which implies \(L\sigma \succeq Q\sigma \) by stability. By (\(\dag \)), \(L^\prime \in {\mathcal {A}}_{S}^{\preceq }\), \(L^\prime \) is ground, and \(L^\prime \sigma = L^\prime \). Since \(L^\prime \in {\mathcal {A}}_{S}^{\preceq }\) and \(L^\prime = L^\prime \sigma = L\sigma \succeq Q\sigma \), it follows that \(Q\sigma \in {\mathcal {A}}_{S}^{\preceq }\) by Definition 7. \(\square \)
Thus, a positive clause \(C \in R_>^*(S)\) is ground, as all its literals are in \({\mathcal {A}}_{S}^{\preceq }\).
Theorem 7
Given a positively restrained input set S, every fair PO-resolution derivation terminates and is a refutation if S is unsatisfiable.
Proof
We prove that if S is positively restrained then \(R_>^*(S)\) is finite, which guarantees termination. The second part of the claim follows by refutational completeness of PO-resolution [42]. Consider any PO-resolvent \((C \vee D)\sigma \in R_>^*(S)\) from parents \(\lnot L \vee C\) and \(L^\prime \vee D\) with mgu \(\sigma \). Since \(L^\prime \vee D\) is positive, \((C \vee D)\sigma \) has strictly fewer negative literals than \(\lnot L \vee C\). By way of contradiction, suppose that \(R_>^*(S)\) is infinite. Since the number of negative literals in PO-resolvents decreases at every resolution step, an infinite \(R_>^*(S)\) must contain infinitely many positive clauses. By Lemma 5, all positive clauses in \(R_>^*(S)\) are ground clauses made of atoms from \({\mathcal {A}}_{S}^{\preceq }\). Since \({\mathcal {A}}_{S}^{\preceq }\) is finite, and repeated literals in ground clauses disappear by merging, only finitely many clauses can be built from \({\mathcal {A}}_{S}^{\preceq }\), which contradicts \(R_{>}^*(S)\) being infinite. \(\square \)
These resultsFootnote 6 extend to positive resolution, since the >-maximality of \(L^\prime \sigma \) in \((L^\prime \vee D)\sigma \) is not used in the proofs, and to positive hyperresolution, for which the proof of Theorem 7 is trivial, since only positive clauses get generated.
Corollary 3
PO-resolution, positive hyperresolution, and positive resolution decide the positively restrained fragment.
Thus, Theorem 6 follows also from Theorem 5 and Corollary 3. Dually, negative resolution and negative hyperresolution decide the negatively restrained fragment. The next example shows that SGGS can be exponentially more efficient than saturation-based resolution strategies because it is model-based.
Example 16
Consider the following parametric clause set \(S_n\) consisting of \(n+1\) clauses, using \(i{+}1\)-ary predicates \(\textsf{P}_i\) and constants \(\textsf{c}_i\), for all i, \(0{\leqslant }i{\leqslant }n\):
The set \(S_n\) is positively restrained by an LPO with precedence \(\textsf{P}_0> \dots> \textsf{P}_n > \textsf{c}_i\) for all i, \(0{\leqslant }i{\leqslant }n\). SGGS with \(I^-\) detects satisfiability after \(n+1\) SGGS-extension steps, selecting for instance the leftmost positive literal in each extension clause, so that the model where \(\textsf{P}_0(\textsf{c}_0), \textsf{P}_1(\textsf{c}_0, \textsf{c}_0), \dots , \textsf{P}_n(\textsf{c}_0, \dots , \textsf{c}_0)\) are true and all other positive literals are false is produced. A saturation by PO-resolution or positive hyperresolution produces exponentially many clauses, because for all i, \(0{\leqslant }i{\leqslant }n\), all n positive literals in \(C_i\) unify with the negative literal in \(C_{i+1}\), generating \(n^{i+1}\) positive clauses, so that the total clause count is given by \(\sum _{i=0}^n n^{i+1}\) or equivalently \(\sum _{k=1}^{n+1} n^k\).
5.3 Sort-Refined Versions of the Restrained and PVD Fragments
As observed for the stratified fragment, where all sorts are acyclic, such sorts are harmless for termination. In this section we consider a signature with both cyclic and acyclic sorts. Since the key point for termination is the existence of a finite basis, we reason in terms of whether there are finitely or infinitely many ground terms of a given sort.
Definition 8
(Infinite domain) A sort has infinite domain if there are infinitely many ground terms of that sort, and it has finite domain otherwise. A variable has infinite domain if its sort does, and finite otherwise.
Clearly, a cyclic sort has infinite domain. For example, if the signature contains a constant \(\textsf{a}:s\) and a function \(\textsf{f}:s \rightarrow s\), sort s has infinite domain, as the infinitely many terms \(\textsf{f}^n(\textsf{a})\), for all \(n \ge 0\), have sort s. If the signature also contains a function \(\textsf{g}:s \rightarrow s^\prime \), also \(s^\prime \) has infinite domain, as the infinitely many terms \(\textsf{g}(f^n(\textsf{a}))\), for all \(n \ge 0\), have sort \(s^\prime \). In general, a sort s has infinite domain if and only if there exists a path from a cyclic sort to s in the sort dependency graph. A term, or atom, or literal has infinitely many ground instances if and only if it contains a variable with infinite domain. The idea is to apply the restrictions of the restrained, or PVD [34], fragments, respectively, only to the variables of infinite domain and the literals where such variables occur. The result will be the sort-restrained and sort-refined-PVD fragments. We begin by making ground-preservingness relative to a sort:
Definition 9
(Ground-preserving for a sort) A clause C is positively ground-preserving for sort s if \(\mathcal Var_s(C)\subseteq \mathcal Var_s(C^-)\), and negatively ground-preserving for sort s if \(\mathcal Var_s(C)\subseteq \mathcal Var_s(C^+)\). A set of clauses is positively/negatively ground-preserving for sort s if all its clauses are.
Both sort-restrained and sort-refined-PVD fragments will require that clauses are ground-preserving for all sorts of infinite domain.
5.3.1 SGGS Decides the Sort-restrained Fragments
The next example gives the intuition for the sort-restrained fragment.
Example 17
Consider the following set S of clauses with sorts \(\{s_1, s_2\}\):
where \(\textsf{a}:s_1\), \(\textsf{b}:s_2\), \(\textsf{f}:s_2 \rightarrow s_2\), \(\textsf{P}\subseteq s_1\times s_2\), and \(\textsf{Q}\subseteq s_1 \times s_1\). This clause set is not restrained because it is not ground-preserving since the positive clause (i) is not ground, and it is not stratified because function symbol \(\textsf{f}\) induces a cycle over sort \(s_2\). However, S is positively ground-preserving for sort \(s_2\): there are no variables of sort \(s_2\) in positive clause (i), and the only variable of sort \(s_2\) in a mixed clause, namely y in (iii), occurs in negative literal \(\lnot \textsf{P}(x, \textsf{f}(y))\). Moreover, \(\textsf{P}(x,y)\) in clause (iii) is dominated by \(\lnot \textsf{P}(x, \textsf{f}(y))\) in the sense of positive restrainedness, since \(\textsf{P}(x, \textsf{f}(y)) \succ \textsf{P}(x,y)\) for \(\succ \) any LPO or KBO. Indeed, SGGS using \(I^-\) terminates on input S:
In the second extension clause either positive literal can be selected with either choice leading to termination.
Let \(\succeq \) be a restraining quasi-ordering with the subterm property.
Definition 10
(Sort-Restrained) A clause C is positively sort-restrained if it is positively ground-preserving for all sorts with infinite domain, and for all literals \(L \in C^+\) such that \(Gr(L)\) is infinite there exists a literal \(M\in C^-\) such that \(at(M)\succeq at(L)\). A set is positively sort-restrained if all its clauses are.
Negatively sort-restrained clauses and clause sets are defined dually, and a set of clauses is sort-restrained if it is positively or negatively sort-restrained. The set of Example 17 is positively sort-restrained.
Let a set of atoms \({\mathcal {L}}\) be (i) closed with respect to instantiation, or instantiation-closed for short, if \(L\sigma \in {\mathcal {L}}\) whenever \(L \in {\mathcal {L}}\); and (ii) closed under \(\preceq \), or \(\preceq \)-closed for short, if \(M\in {\mathcal {L}}\) whenever \(M\preceq L\) for some \(L\in \mathcal L\).
Definition 11
(Basis for a sort-restrained set) Given a sort-restrained set S of clauses with set of sorts \(\varSigma \), let \({\mathcal {L}}_\varSigma ^{\downarrow }\) be the set of all atoms L such that L occurs in a clause of S and \(Gr(L)\) is finite. Let \({\mathcal {L}}^\preceq _{\varSigma }\) be the smallest instantiation-closed and \(\preceq \)-closed superset of \(\mathcal L_\varSigma ^{\downarrow }\). The basis for S is \({\mathcal {A}}_{S,\varSigma }^\preceq = Gr({\mathcal {L}}^\preceq _{\varSigma })\), that is, the set of the ground instances of the atoms in \(\mathcal L^\preceq _{\varSigma }\).
Note that \({\mathcal {A}}_{S,\varSigma }^\preceq \subseteq {\mathcal {L}}^\preceq _{\varSigma }\) because \({\mathcal {L}}^\preceq _{\varSigma }\) is instantiation-closed.
Example 18
For the clause set of Example 17 let \(\succeq \) be the reflexive closure of an LPO with empty precedence. \({\mathcal {L}}_\varSigma ^{\downarrow }\) is \(\{\textsf{P}(x, \textsf{f}(\textsf{b})), \textsf{Q}(x,\textsf{a}), \textsf{Q}(\textsf{a},x), \textsf{Q}(x,x)\}\). \({\mathcal {L}}^\preceq _{\varSigma }\) is the union of four sets: \(\mathcal L_\varSigma ^{\downarrow }\), the singleton set \(\{\textsf{P}(x, \textsf{b})\}\) by \(\preceq \)-closure since \(\textsf{P}(x, \textsf{b}) \prec \textsf{P}(x, \textsf{f}(\textsf{b}))\), the set \(\{\textsf{P}(\textsf{a}, \textsf{f}(\textsf{b})), \textsf{Q}(\textsf{a}, \textsf{a}), \textsf{P}(\textsf{a}, \textsf{b})\}\) by instantiation-closure, and the set of all the variants of these atoms (i.e., all the variants of \(\textsf{P}(x, \textsf{f}(\textsf{b}))\), \(\textsf{Q}(x,\textsf{a})\), \(\textsf{Q}(\textsf{a},x)\), \(\textsf{Q}(x,x)\), and \(\textsf{P}(x, \textsf{b})\)). Then \({\mathcal {A}}_{S,\varSigma }^\preceq \) is the set of the ground instances of the atoms in \({\mathcal {L}}^\preceq _{\varSigma }\), that is, \(\{\textsf{P}(\textsf{a}, \textsf{f}(\textsf{b})),\ \textsf{Q}(\textsf{a}, \textsf{a}),\ \textsf{P}(\textsf{a}, \textsf{b})\}\).
The above definition of closure lets instantiation introduce variables, but this is not a problem for the finiteness of \({\mathcal {A}}_{S,\varSigma }^\preceq \) for the following reason: a substitution replaces a variable with finite domain by a term of the same sort, hence with finite domain, and such a term cannot contain a variable with infinite domain, because a term of a sort with finite domain cannot have a subterm of a sort with infinite domain.
Lemma 6
For all sort-restrained sets S of clauses, the basis \(\smash {{\mathcal {A}}_{S,\varSigma }^\preceq }\) is finite.
Proof
In order to show that \(\smash {{\mathcal {A}}_{S,\varSigma }^\preceq } = Gr({\mathcal {L}}^\preceq _{\varSigma })\) is finite, it suffices to show that all variables occurring in atoms in \(\mathcal L^\preceq _{\varSigma }\) have finite domain. The set \(\smash {\mathcal L_\varSigma ^{\downarrow }}\) satisfies this property by definition. The closure with respect to instantiation introduces no variable with infinite domain by the above observation. The \(\preceq \)-closure does not introduce variables, because \(L\succeq M\) implies \(\mathcal Var(M) \subseteq \mathcal Var(L)\) by the stability and subterm properties of the restraining quasi-ordering. \(\square \)
Similar to the ground-preserving and restrained cases, an initial interpretation I is suitable for a sort-restrained set S if either I is \(I^-\) and S is positively sort-restrained, or I is \(I^+\) and S is negatively sort-restrained.
Lemma 7
Given a sort-restrained input set S, every fair SGGS-derivation with suitable initial interpretation is in \({\mathcal {A}}_{S,\varSigma }^\preceq \).
Proof
We consider S positively sort-restrained and \(I^-\) (for the dual case one flips the signs). We show that the derivation is in \(\smash {{\mathcal {A}}_{S,\varSigma }^\preceq = Gr(\mathcal L^\preceq _{\varSigma })}\) by showing that all atoms of all clauses appearing on the trail during the derivation are in \(\mathcal L^\preceq _{\varSigma }\). The proof is by induction on the length k of \(\varTheta \). The base case (\(k=0\)) is vacuously true. The induction hypothesis is that all atoms of all clauses on a trail \(\varGamma \) produced by a derivation of length k are in \(\mathcal L^\preceq _{\varSigma }\). Let \(\varGamma \vdash \varGamma ^\prime \) be the \((k{+}1)\)-th step. If \(\varGamma \vdash \varGamma ^\prime \) is a splitting step, the atoms in the split clause are in \(\mathcal L^\preceq _{\varSigma }\) by induction hypothesis, and so are those in the instances generated by splitting, since \(\mathcal L^\preceq _{\varSigma }\) is closed with respect to instantiation. If \(\varGamma \vdash \varGamma ^\prime \) is an SGGS-resolution step, the atoms in the parents are in \({\mathcal {L}}^\preceq _{\varSigma }\) by induction hypothesis, and so are those in the SGGS-resolvent, by the closure of \({\mathcal {L}}^\preceq _{\varSigma }\) with respect to instantiation. If \(\varGamma \vdash \varGamma ^\prime \) is an SGGS-extension step, it adds an instance \(C\alpha \) of a clause \(C \in S\), where \(\alpha \) is the simultaneous mgu of all \(I^-\)-true (i.e., negative) literals \(\lnot L_1, \dots , \lnot L_n\) in C with as many \(I^-\)-false (i.e., positive) selected literals \(M_1,\ldots , M_n\) in \(\varGamma \). For all i, \(1\leqslant i\leqslant n\), \(M_i \in {\mathcal {L}}^\preceq _{\varSigma }\) by induction hypothesis, and \(L_i\alpha = M_i\alpha \in \mathcal L^\preceq _{\varSigma }\) by instantiation closure. For an \(L\in C^+\), there are two cases. If \(Gr(L)\) is finite, \(\smash {L\in \mathcal L_\varSigma ^{\downarrow } \subseteq {\mathcal {L}}^\preceq _{\varSigma }}\) by Definition 11, and \(L\alpha \in {\mathcal {L}}^\preceq _{\varSigma }\) by instantiation closure. Otherwise, by positive sort-restrainedness there exists a \(\lnot L_i\), for some i, \(1\,{\leqslant }\,i\,{\leqslant }\,n\), such that \(L \preceq L_i\). By stability of \(\preceq \), \(L\alpha \preceq L_i\alpha \). It follows that \(L\alpha \preceq L_i\alpha = M_i\alpha \in \mathcal L^\preceq _{\varSigma }\) because \(\smash {{\mathcal {L}}^\preceq _{\varSigma }}\) is \(\preceq \)-closed. \(\square \)
Since the basis \({\mathcal {A}}_{S,\varSigma }^\preceq \) is finite, decidability and the small model property follow by Theorems 1 and 2.
Theorem 8
Given a sort-restrained input set S, every fair SGGS-derivation with suitable initial interpretation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
Corollary 4
A sort-restrained satisfiable set S of clauses has a model of cardinality at most \(\vert {\mathcal {H}}({{\mathcal {A}}_{S,\varSigma }^\preceq })\vert + 1\) that can be extracted from the limit of any fair SGGS-derivation with input S and suitable initial interpretation.
While sign-based resolution strategies decide the restrained fragments (cf. Sect. 5.2), they do not decide the sort-restrained ones, because they do not decide the stratified fragment (cf. Example 3), which is contained in each sort-restrained fragment as the special case where all sorts have finite domain.
5.3.2 SGGS Decides the Sort-refined-PVD Class
We recall the PVD property [25, 34] in order to apply it to the variables of infinite domain. For a clause C, let \(\text {depth}_x(C)\) be the maximum occurrence depth in C of a variable \(x\in \mathcal Var(C)\).
Definition 12
(PVD fragment) A set S of clauses is in the PVD fragment if every clause \(C \in S\) is positively ground-preserving and \(\forall x \in \mathcal Var(C^+)\) it holds that \(\text {depth}_x(C^+) \leqslant \text {depth}_x(C^-)\).
The next example captures the intuition for the sort-refined-PVD fragment.
Example 19
Assume a signature with sorts \(\{s_1, s_2, s_3, s_4\}\) and symbols \(\textsf{a}:s_1\), \(\textsf{b}:s_2\), \(\textsf{c}:s_3\), \(\textsf{f}:s_1 \rightarrow s_1\), \(\textsf{g}:s_3 \rightarrow s_2\), \(\textsf{h}:s_1 \times s_2 \rightarrow s_4\), \(\textsf{P}\subseteq s_1\times s_2\), \(\textsf{Q}\subseteq s_4\), and \(\textsf{R}\subseteq s_1 \times s_1\), so that the sort-dependency graph is as follows:
Sort \(s_1\) is cyclic, and both \(s_1\) and \(s_4\) have infinite domain, while \(s_2\) and \(s_3\) have finite domain. Consider the set S made of the following clauses:
This set is neither stratified nor ground-preserving, hence neither restrained nor PVD. Neither it is sort-restrained, because the positive literal \(\textsf{R}(x,y)\) in clause (iv) involves sort \(s_1\), but no negative literal in (iv) can dominate \(\textsf{R}(x,y)\) in a restraining quasi-ordering, since no negative literal in (iv) contains both x and y. However, S is positively ground-preserving for \(s_1\) and \(s_4\), and all variables of sorts with infinite domain that occur in a positive literal also occur in a negative literal of the same clause. Furthermore, such variables occur in the negative literals at greater or equal depth. In other words, S satisfies the PVD property restricted to sorts with infinite domain.
Definition 13
(Sort-refined-PVD) A clause C is sort-refined-PVD if it is positively ground-preserving for all sorts with infinite domain, and for all variables \(x \in \mathcal Var(C^+)\) of infinite domain it holds that \(\text {depth}_x(C^+) \leqslant \text {depth}_x(C^-)\). A set of clauses is sort-refined-PVD if all its clauses are.
The set of Example 19 is sort-refined-PVD. We apply the finite basis approach to show that SGGS decides also this fragment. While the essence of PVD is to control the depth of variable occurrences, for sort-refined-PVD the crux is to exclude variables of infinite domain and to ensure that the occurrence depth of terms whose sort has infinite domain is upper bounded. Let d be the maximum depth of an atom in a set S of clauses, or \(d = max\{\text {depth}(L) \mathop {\,:}L\text { is an atom in clause }C\text { and } C\in S\}\).
Definition 14
(Basis for a sort-refined-PVD set) Given a sort-refined-PVD set S of clauses with set of sorts \(\varSigma \), let \({\mathcal {L}}^d_{S,\varSigma }\) be the set of all atoms where all variables have finite domain and all subterms of a sort with infinite domain have occurrence depth at most d. Then the basis for S is \({{\mathcal {A}}}^d_{S,\varSigma } = Gr(\mathcal L^d_{S,\varSigma })\).
Note that \(\smash {{\mathcal {L}}^d_{S,\varSigma }}\) is instantiation-closed, because instantiation replaces variables with finite domain with terms whose sort has finite domain, so that no subterm whose sort has infinite domain can be introduced. It follows that \(\smash {{\mathcal {A}}_{S,\varSigma }^d \subseteq \mathcal L^d_{S,\varSigma }}\).
Lemma 8
For all sort-refined-PVD sets S of clauses, the basis \(\mathcal{A}^d_{S,\varSigma }\) is finite.
Proof
We show that the depth of any ground atom \(L\sigma \in \mathcal{A}^d_{S,\varSigma }\) for \(L\in \smash {{\mathcal {L}}^d_{S,\varSigma }}\) is upper bounded. The occurrence depth of any subterm of \(L\sigma \) whose sort has finite domain is trivially upper bounded. By Definition 14 the occurrence depth of any subterm of L whose sort has infinite domain is upper bounded by d, and L does not contain variables of infinite domain. Thus, the substitution \(\sigma \) cannot introduce subterms of infinite domain and also the occurrence depth of any subterm of \(L\sigma \) whose sort has infinite domain is upper bounded by d. As there are only finitely many ground atoms of bounded depth, \(\mathcal{A}^d_{S,\varSigma }\) is finite. \(\square \)
Example 20
In Example 19 the maximum depth of an atom in S is \(d=2\). Thus, \({{\mathcal {A}}}^d_{S,\varSigma }\) is the set of all ground atoms where all subterms of sort \(s_1\) or \(s_4\) occur at depth at most 2:
For instance, \(\textsf{Q}(\textsf{h}(\textsf{f}(\textsf{a}), \textsf{b}))\not \in \mathcal{A}^d_{S,\varSigma }\) as the subterm \(\textsf{a}\) occurs at depth 3.
Lemma 9
Given a sort-refined-PVD input set S, every fair SGGS-derivation with \(I^-\) is in the finite basis \({\mathcal {A}}_{S,\varSigma }^d\).
Proof
We show that the derivation is in \({\mathcal {A}}_{S,\varSigma }^d = Gr({\mathcal {L}}^d_{S,\varSigma })\) by showing that all atoms of all clauses appearing on the trail during the derivation are in \({\mathcal {L}}^d_{S,\varSigma }\). As \({\mathcal {L}}^d_{S,\varSigma }\) is instantiation-closed, the proof is the same as that of Lemma 7 except for the case of SGGS-extension. Consider an SGGS-extension step that adds an instance \(C\alpha \) of a clause \(C \in S\), where \(\alpha \) is the simultaneous mgu of all \(I^-\)-true (i.e., negative) literals \(\lnot L_1, \dots , \lnot L_n\) in C with as many \(I^-\)-false (i.e., positive) selected literals \(M_1,\ldots , M_n\) in \(\varGamma \). For all i, \(1\leqslant i\leqslant n\), \(M_i \in {\mathcal {L}}^d_{S,\varSigma }\) by induction hypothesis, and \(L_i\alpha = M_i\alpha \in {\mathcal {L}}^d_{S,\varSigma }\) by instantiation closure. For an \(L\in C^+\), let t be a subterm of \(L\alpha \) at position p (i.e., \(t = L\alpha \vert _p\)) whose sort has infinite domain. We show that for all such terms t, it holds that t is not a variable and that \(\vert p \vert \leqslant d\). We distinguish two cases depending on whether p is a position in L or is introduced by \(\alpha \).
-
If p is a position in L then \(\vert p \vert \leqslant d\) because \(L \in C\) and \(C \in S\). For the other part, by way of contradiction, suppose that t is a variable. Then also \(L\vert _p\) must be a variable x of infinite domain such that \(x\alpha = t\). By Definition 13, x occurs in some \(L_i\), \(1\,{\leqslant }\,i\,{\leqslant }\,n\), so \(x\alpha \) occurs in \(L_i\alpha = M_i\alpha \). This gives a contradiction, because \(\smash {M_i \in {\mathcal {L}}^d_{S,\varSigma }}\), \(\smash {M_i\alpha \in \mathcal L^d_{S,\varSigma }}\), and hence \(x\alpha = t\) cannot be a variable of infinite domain by Definition 14.
-
If p is introduced by \(\alpha \), there must be two positions q and r and a variable y such that \(p = qr\), \(L\vert _q = y\), \(y\alpha \vert _r = t\), and also y must have infinite domain. By Definition 13, variable y occurs in some \(L_i\), \(1\,{\leqslant }\,i\,{\leqslant }\,n\), and \(\text {depth}_y(L) \leqslant \text {depth}_y(L_i)\). Hence there is some position o in \(L_i\) such that \(L_i \vert _o = y\) and \(\vert q \vert \leqslant \vert o \vert \). It follows that \(L_i\alpha \vert _{or} = M_i\alpha \vert _{or} = t\). Since \(\smash {M_i \in {\mathcal {L}}^d_{S,\varSigma }}\) and \(\smash {M_i\alpha \in {\mathcal {L}}^d_{S,\varSigma }}\), term t cannot be a variable. Moreover, by Definition 14 terms of sort with infinite domain occur at depth at most d, so that \(\vert or \vert \leqslant d\). From \(\vert q \vert \leqslant \vert o \vert \) it follows that \(\vert p \vert = \vert qr \vert \leqslant \vert or \vert \leqslant d\), which proves the claim.
\(\square \)
By Lemmas 8 and 9, Theorems 1 and 2 apply yielding the following results.
Theorem 9
Given a sort-refined-PVD input set S, every fair SGGS-derivation with \(I^-\) as initial interpretation halts, is a refutation if S is unsatisfiable, and constructs a model of S if S is satisfiable.
Corollary 5
A sort-refined-PVD satisfiable set S of clauses has a model of cardinality at most \(\vert {\mathcal {H}}({{\mathcal {A}}_{S,\varSigma }^d})\vert + 1\) that can be extracted from the limit of any fair SGGS-derivation with \(I^-\) as initial interpretation and input set S.
Hyperresolution decides the PVD class [25, 34], but it does not decide sort-refined-PVD, because it does not decide the stratified fragment (cf. Example 3), which is contained in sort-refined-PVD as the special case where all sorts have finite domain.
6 Testing for Membership, the Koala Prover, and the Experiments
This section presents first an approach to determine whether a set of clauses is restrained, and then the experiments. We show that a set S of clauses is positively restrained, if an associated rewriting relation terminates and defines a restraining quasi-ordering. The case for negatively restrained sets is dual. Thanks to this reduction, one can have a tool that extracts candidate rewrite systems from a set of clauses and invokes a termination tool to test whether the rewriting relation terminates. Our tool tries both 
[48] and AProVE [40] to find restrained and sort-restrained problems, and it also detects whether a problem belongs to any of the other decidable classes considered in this article.
In the experiments, we applied this tool to classify the problems in the TPTP library [77]. This allows us to assess the relevance of the new decidable classes and the power of SGGS as a decision procedure: it turns out that SGGS can decide 65% of the decidable problems without interpreted symbols (e.g., equality)Footnote 7 in TPTP 7.4.0. Then, we present Koala, the first SGGS-based theorem prover. We tested Koala on all the problems without interpreted symbols in TPTP 7.4.0. We analyze these experiments, report statistics, and compare Koala with several state-of-the-art reasoners.
6.1 Discovering Restrained Sets
In order to show that a clause set S is positively restrained, one needs to find a restraining quasi-ordering (cf. Definitions 5 and 6). Since the strict part of a restraining quasi-ordering is a well-founded ordering, the first intuition is to extract from S a rewrite system \({\mathcal {R}}_S\) on atoms such that the rewrite relation \(\rightarrow _{{\mathcal {R}}_S}\) is terminating, so that its transitive closure \(\rightarrow _{{\mathcal {R}}_S}^+\) is a well-founded ordering. Then the transitive and reflexive closure \(\rightarrow _{{\mathcal {R}}_S}^*\) is a restraining quasi-ordering whose equivalence relation is identity.
If the problem requires a quasi-ordering whose equivalence is not identity as in Example 14, one needs to extract from S a pair \(({\mathcal {R}}_S, {\mathcal {E}}_S)\), where \({\mathcal {R}}_S\) is a rewrite system and \({\mathcal {E}}_S\) is a set of equations. Then the rewrite relation is the rewriting modulo relation \(\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}\), which is defined by \(\leftrightarrow _{{\mathcal {E}}_S}^{*}\circ \rightarrow _{{\mathcal {R}}_S} \circ \leftrightarrow _{{\mathcal {E}}_S}^{*}\). The crucial point is that \(\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}\) is terminating, so that its transitive and reflexive closure \(\smash {\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}^*}\) is a restraining quasi-ordering.
Definition 15
(Restraining system) Given a set S of clauses, a system \(({\mathcal {R}}_S, {\mathcal {E}}_S)\) is positively restraining for S if for all clauses \(C\,{\in }\,S\), for all non-ground literals \(L\in C^+\), there exists a literal \(\lnot M\in C^-\) such that \((M \rightarrow L)\in {\mathcal {R}}_S\) or \((M \simeq L)\in {\mathcal {E}}_S\).
Often \({\mathcal {E}}_S\) contains permutative equations, such as \(\textsf{differ}(x,y) \simeq \textsf{differ}(y,x)\) in Example 14. For Example 15, a possible choice is \({\mathcal {R}}_S = \{\textsf{P}(\textsf{s}(\textsf{s}(x)),y) \rightarrow \textsf{P}(x,\textsf{s}(y)), \textsf{P}(x, \textsf{s}(\textsf{s}(y))) \rightarrow \textsf{P}(x,\textsf{s}(y)), \textsf{P}(\textsf{s}(x), \textsf{s}(y)) \rightarrow \textsf{P}(\textsf{s}(x),y)\}\) and \({\mathcal {E}}_S=\emptyset \).
Theorem 10
Given a set S of clauses, if there exists a positively restraining system \(({\mathcal {R}}_S, {\mathcal {E}}_S)\) for S such that (i) \(\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}\) is terminating, (ii) for all \(t\simeq u\) in \({\mathcal {E}}_S\), \(\mathcal Var(t) = \mathcal Var(u)\), and (iii) \(\leftrightarrow _{{\mathcal {E}}_S}^*\) has finite equivalence classes, then S is positively restrained, and S is strictly positively restrained if \({\mathcal {E}}_S = \emptyset \).
Proof
We show that S is positively ground-preserving, that is, for all clauses \(C\in S\), it holds that \(\mathcal Var(C)\subseteq \mathcal Var(C^-)\). Suppose that C has a non-ground literal \(L\in C^+\). By Definition 15, there exists a rule \(t\rightarrow u\) in \({\mathcal {R}}_S\) or an equation \(t \simeq u\) in \({\mathcal {E}}_S\) where \(t = M\) and \(u = L\) for some literal \(\lnot M\in C^-\). In the first case, \(\mathcal Var(u)\subseteq \mathcal Var(t)\) by hypothesis (i), since otherwise \(\rightarrow _{{\mathcal {R}}_S}\), and hence \(\smash {\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}}\), would not be terminating. In the second case, \(\mathcal Var(u) = \mathcal Var(t)\) by hypothesis (ii). It follows that \(\mathcal Var(C^+)\subseteq \mathcal Var(C^-)\) and hence \(\mathcal Var(C)\subseteq \mathcal Var(C^-)\). To complete the proof, it suffices to check that \(\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}^*\) is a restraining quasi-ordering. Indeed, \(\smash {\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}^*}\) is stable, its strict part \(\smash {\rightarrow _{{\mathcal {R}}_S/{\mathcal {E}}_S}^+}\) is well-founded by hypothesis (i), and the equivalence classes of \(\leftrightarrow _{{\mathcal {E}}_S}^*\) are finite by hypothesis (iii). If \({\mathcal {E}}_S = \emptyset \), the restraining quasi-ordering is \(\rightarrow _{{\mathcal {R}}_S}^*\). Indeed, \(\rightarrow _{{\mathcal {R}}_S}^*\) is stable, its strict part \(\rightarrow _{{\mathcal {R}}_S}^+\) is well-founded by hypothesis (i), and the equivalence classes of 
are finite, because 
is identity. \(\square \)
6.2 Classifying Decidable Problems for the Experiments
The TPTP 7.4.0 library has over 17,000 first-order problems, 4005 of which do not have interpreted symbols (e.g., equality, arithmetic). If a problem is not in clausal form, our testing tool transforms it into clausal form. Given a set of clauses, the tool extracts all the candidates for restraining rewrite systems. Then the tool invokes 
and AProVE to determine whether at least a candidate is a restraining rewrite systems satisfying the termination conditions for a restrained set. For instance, problem HWV036-2 (cf. Example 1) is a set of axioms which is combined with sets of ground clauses in several other TPTP problems (e.g., HWV008-2.002 adds 23 ground clauses). We found a terminating positively restraining rewrite system for HWV008-2.002, so that both this problem and HWV036-2 are strictly positively restrained.
Both the number of candidate rewrite systems and their size grow exponentially with the number of literals in the clause set. Thus, 555 problems had to be excluded, because they have more than 500 clauses and the candidate rewrite systems turned out to be too large to handle. Also, for each clause set, 
and AProVE were applied to at most 100 rewrite systems, with a timeout of 10 sec each. Membership in the already known decidable classes can also be determined automatically. For example, stratified input problems are recognized by computing the sort dependency graph and testing it for acyclicity [47]. This test is applied also to identify sort-restrained and sort-refined-PVD problems.
Table shows how many of the remaining 3450 problems belong to the various (non-disjoint) decidable classes. Initially, 377 problems were found restrained. For those still undetermined, we tested whether it is sufficient to flip the sign of all literals with a certain predicate to get a restrained problem, which succeeded in 36 cases, for a total of 413 restrained problems. Overall, 2137 of the 3450 problems are decidable according to at least one of the criteria, and 1399 belong to at least one of the SGGS-decidable classes (i.e., ground, EPR, stratified, PVD, restrained, sort-restrained, and sort-refined-PVD), so that SGGS can decide 65% of the available decidable problems.
We analyze next how many new decidable problems are discovered thanks to the classes introduced in this paper. Of the 413 restrained problems in Table 1, 332 are positively restrained, 202 negatively restrained, and 121 are both; 74 are ground, 266 are EPR, 277 are stratified, 89 are Ackermann, 169 are monadic, 204 are \(\textsf{FO}^2\), 209 are guarded, and 232 are PVD, but 77 problems fall in no other decidable class, and therefore, to the best of our knowledge, they are found to be decidable for the first time.
Of the 1398 sort-restrained problems in Table 1, 82 are ground, 1059 are EPR, 1260 are stratified, 93 are Ackermann, 406 are monadic, 534 are \(\textsf{FO}^2\), 569 are guarded, 346 are PVD, 413 are restrained, and 20 belong to no other decidable class. Adding these 20 to the above 77 gives 97 new decidable problems. The existence of problems that are sort-restrained, but neither stratified nor restrained, shows that the generalization conquers more problems.
Of the 1304 sort-refined-PVD problems in Table 1, 82 are ground, 1059 are EPR, 1260 are stratified, 93 are Ackermann, 404 are monadic, 515 are \(\textsf{FO}^2\), 569 are guarded, and 347 are PVD. Since 26 sort-refined-PVD problems are neither stratified nor PVD, also this generalization is useful. However, the sort-refined-PVD class did not unveil previously unknown decidable problems.
The average TPTP rating of the problems in the new decidable classes is low,Footnote 8 which means that most provers can solve them. Nonetheless, the group of restrained problems includes hard ones such as instances of the binary counter problem in Example 5 (MSC015-1.n), and Rubik’s cube problems (e.g., PUZ052-1). For example, MSC015-1.030 is restrained and has rating 1.00, that is, no theorem prover could solve it so far in the time allotted in competitions.
6.3 The Koala Prover and the Experiments
Koala is a new prototype theorem prover written in OCaml and it is the first implementation of SGGS.Footnote 9 In Koala, the trail is implemented as a list, with constraints maintained in standard form, and selected literals stored in a discrimination tree to compute substitutions efficiently. Koala computes the sort dependency graph, because it facilitates testing sorted constraints for satisfiability. Thus, Koala can detect stratified problems on its own. The search plans in Koala are fair, so that all derivations are fair.
In the experiments,Footnote 10 the initial interpretation was \(I^-\) by default and \(I^+\) for positively ground-preserving problems. The time-out was 300 sec of wall-clock time. All experiments were run single-threaded on a 12-core Intel i7-5930K 3.50GHz machine with 32GB of main memory. Table reports how many problems Koala showed satisfiable or unsatisfiable along with statistics and the average running time. Considering all problems whose satisfiability status is known, Koala succeeded on 64% of the satisfiable problems, and on 38% of the unsatisfiable problems, with an overall success rate of 43%. Considering the problems in SGGS-decidable fragments, Koala found 360 satisfiable sets and 726 unsatisfiable sets, solving 1086 problems out of 1399 (78% success rate). Koala solved 87 of the 97 problems that were discovered decidable for the first time (90% success rate). Specifically, it solved 69 of the 77 restrained problems, finding 61 unsatisfiable sets and 8 satisfiable sets, and 18 of the 20 sort-restrained problems, finding 16 unsatisfiable sets and 2 satisfiable sets.
In Table 2, the columns labeled #steps, #ext, and #confl report the average derivation length, average number of SGGS-extensions, and average number of conflicts, respectively. The latter two give some intuition about the time spent in model building and conflict solving, respectively, where the number of conflicts may measure the difficulty of the search. The columns labeled #gen, #del, and max \(|\varGamma |\) report space-related statistics: average number of generated clauses, average number of deleted clauses, and average maximum trail length during the derivation. Deleted clauses include disposable clauses and clauses deleted because they have literals assigned to either a split clause or the parent that gets deleted in an SGGS-resolution step. Across all problem classes, SGGS-extensions represent between one third and one half of all inferences, and about half of the generated clauses are extension clauses. The number of deletions is in a similar magnitude as the number of extensions, though somewhat smaller. The number of conflicts equals about one third of the number of inference steps. A comparison of the columns labeled #steps and max \(|\varGamma |\) shows that the maximum trail length is much smaller than the derivation length on average. The SGGS trail grows when SGGS-extension expands the model and shrinks when the other rules fix it.
We compared Koala with E 2.4 [74], Vampire 4.4 [51], iProver 3.5 [33], CVC5 1.0.0 [6], and Darwin 1.4.4 [12]. E and Vampire are saturation-based theorem provers, and hence feature ordered resolution, which decides the Ackermann, monadic, \(\textsf{FO}^2\), and guarded fragments [29, 36, 44].Footnote 11 iProver implements both saturation and a model-driven instance-based engine that generates instances of clauses by the Inst-Gen method [39, 46], grounds them, and submits them to a SAT-solver: if a ground set is found unsatisfiable, so is the input; otherwise, the next round of instance generation gets instances that are false in the model. Darwin implements the model evolution calculus (MEC) [10], which lifts to FOL the DPLL procedure for propositional satisfiability [27]. Inst-Gen and MEC decide the stratified [47] but not the restrained fragments: if Inst-Gen picks an unfortunate literal selection for Example 15, it does not halt, and MEC may not halt on satisfiable negatively restrained sets (e.g., Example 14), as it starts with \(I^+\) as candidate model. CVC5 is a CDCL(\({{\mathcal {T}}}\))-based SMT solver with instance generation to handle unversally quantified variables; it also features superposition. We included the finite model (-fm) versions of CVC5 and Darwin that search for a finite model by iterative deepening on the model’s cardinality, generating all the ground instances of the clauses for a given cardinality, and giving them to a SAT solver.
Table reports how many problems each prover found unsatisfiable in each class, and Table does the same for the problems found satisfiable. The column #sets gives for each category the number of problems that have status unsatisfiable (in Table 3) or satisfiable (in Table 4) in TPTP 7.4.0 (these data are not necessarily current, hence the tools may find more). The best performance is highlighted in boldface. On unsatisfiable problems, Koala trails behind most systems on most or all classes, except for Darwin -fm. Finite model search pays the price of the exponential growth of the search space by iterative deepening, and is less suitable for unsatisfiable instances. However, CVC5 -fm does better, possibly due to a different underlying CDCL-based SAT solver. On satisfiable problems, Koala solves more problems than E, CVC5, and even Vampire in most classes, but remains behind CVC5 -fm, both versions of Darwin, and iProver, which emerges as the strongest system in both tables.
7 Related Work
Several methods decide Datalog (e.g., positive hyperresolution) or the EPR or stratified fragments (e.g., [3, 37, 47, 65]) that are popular for applications [1, 57, 64]. The other SGGS-decidable fragments in this article involve ground-preserving clauses. Positively ground-preserving clauses are also termed range-restricted [9, 25, 55, 61]. Manthey and Bry introduced “range-restricted” for positively ground-preserving clauses [55]. At the same conference Kounalis and Rusinowitch introduced “ground-preserving” for negatively ground-preserving clauses [49, 50]. Ground-preserving was used for positively ground-preserving in [21] and for either positively or negatively ground-preserving in [17]. Ground-preserving captures exactly the property we are interested in, namely that only ground clauses get generated. Since the two names are equally old and ground-preserving is more expressive for our purposes, we chose to use it.
Ground-preserving clauses were introduced in Horn logic [49, 50, 55]. When reasoning forward or bottom-up, that is, from the facts (e.g., by positive hyperresolution) variables that appear in the positive but not in the negative literals of a rule were deemed problematic, because they get introduced in the forward chaining process. In other words, even if we start from ground facts we get non-ground facts. The restriction to positively ground-preserving clauses was introduced to prevent this phenomenon [55].
When reasoning backward or top-down, that is, from a query (e.g., by negative hyperresolution) variables that appear in the negative but not in the positive literals of a rule get introduced in the backward chaining process. Even if we start from a ground query we get non-ground queries. The restriction to negatively ground-preserving clauses was introduced to prevent this phenomenon in Horn theories with equality [49, 50]. The purpose was to obtain linear input proofs where all center clauses are ground and decreasing in the CSO used in ordered resolution and superposition (see also [16, Sect. 5.2]). Thus, positively ground-preserving clauses are convenient for positive strategies that reason forward or bottom-up, and negatively ground-preserving clauses are convenient for negative strategies that reason backward or top-down. SGGS with \(I^-\) is another forward-reasoning or bottom-up method and SGGS with \(I^+\) is another backward-reasoning or top-down method.
CDCL(\(\varGamma \!+\!{{\mathcal {T}}}\)), where \(\varGamma \) is an inference system including hyperresolution, superposition with negative selection, and simplification, decides essentially finite theories with positively ground-preserving axiomatizations [21]. Essentially finite means only one monadic function f with finite range. This decidability result rests on adding speculative axioms of the form \(f^j(x)\,{\simeq }\,f^k(x)\) (\(j > k\)) for increasing values of j and k. Simplification applies the speculative axioms to limit the depth of generated terms.
Example 21
The clause set \(\{\textsf{P}(\textsf{a}),\ \lnot \textsf{P} (x) \vee \textsf{P}(\textsf{f}(\textsf{f}(x))),\ \lnot \textsf{P} (x) \vee \lnot \textsf{P}(\textsf{f}(x))\}\) from Example 12 is essentially finite (the range of \(\textsf{f}\) is finite, because the set admits a finite model). CDCL(\(\varGamma \!+\!{{\mathcal {T}}})\) tries \(\textsf{f}(x)\simeq x\), detects a conflict, backtracks, tries \(\textsf{f}^2(x)\simeq x\), and halts reporting satisfiability. Without speculative axioms and simplification, it is not surprising that SGGS does not halt.
Baumgartner and Schmidt offered a comprehensive treatment of bottom-up model-generation (BUMG) methods, with an emphasis on positive hyperresolution enhanced with first-order splitting [9]. First-order splitting [70, 80] generalizes to first-order clauses the splitting of disjunctions of DPLL, at the expense of introducing backtracking in saturation. The model generation and decidability results in [9] involve range-restriction transformations and a technique called blocking. A range-restriction transformation transforms a set of clauses into an equisatisfiable set of range-restricted clauses. Blocking allows the BUMG method to guess an equality on a splitting branch and its negation on another. If a guess causes a conflict it can be undone by backtracking. Thus, these guesses are speculative inferences in the sense of [21]. Since positive hyperresolution with these enhancements decides the Bernays–Schönfinkel class with equality [9], one can conjecture that a generalization to the many-sorted case could enable it to decide the sort-restrained and sort-refined-PVD classes.
8 Future Work
A key open issue in automated reasoning is whether it is better to bring conflict-driven reasoning to the first-order level (e.g., SGGS) or keep it at the propositional level, as done by the instance-based approaches that perform instance generation on top of a CDCL-based SAT solver. Some of the systems that we compared with Koala include in various ways the second approach. We do not regard our experimental comparison as conclusive, because Koala is only a prototype. This fundamental problem is open also in SMT, where it is still unknown whether it is better to stick to the CDCL(\({{\mathcal {T}}}\)) paradigm (conflict-driven reasoning only at the propositional level) [21, 63] or move to the MCSAT/CDSAT paradigm (conflict-driven reasoning in the theories) [23, 24, 28]. An answer based on experiments is premature, as not enough engineering has been invested in first-order conflict-driven systems. Furthermore, comparing implementations is necessary, but it is a comparison of tools, not methods [18]. This is all the more true given that contemporary reasoners implement multiple paradigms. This is a welcome development to get more powerful and flexible provers, but it may make it harder to know to which features a certain empirical behavior should be attributed.
In addition to this broad issue, there are several directions for future work on SGGS. A main one is to add equality reasoning by building the equality axioms in both model representation and rules. A natural candidate would be an SGGS-superposition rule, focused on generating clauses needed to explain equality conflicts. For the ground case, one may integrate in SGGS a congruence closure algorithm (e.g., [5, 32, 60, 62]). Congruence closure and blocking [9] were used to import some equational reasoning in tableaux-based methods [79]. SGGS could be enhanced with blocking or other speculative inferences. Speculative inferences that cause conflicts are undone by backtracking [9, 21, 79]. SGGS does not have backtracking in the sense of undoing inferences. Since the model in SGGS is read off the trail in left-to-right order, it suffices to move a clause by the SGGS-move inference rule to flip the truth value of a selected literal in the candidate model. One would have then to fit speculative inferences in the SGGS approach to represent and fix models.
Methods that integrate first-order theorem proving and SMT solving have gained traction (e.g., [21, 69]). One can envision composing SGGS with theory modules in CDSAT [23, 24], viewing SGGS as a CDSAT module for FOL. Such a composition would lead to study how to bridge Herbrand interpretations and models represented by assignments, including first-order (i.e., non-Boolean) assignments. It would also be a context where to consider SGGS with initial interpretations that are not based on sign, since SGGS could assume as initial interpretation some completion of a partial interpretation built by CDSAT.
An initial interpretation is goal-sensitive, if it satisfies all the input clauses except the goal clauses, that is, those in the clausal form of the negation of the conjecture. If the initial interpretation is goal-sensitive, SGGS is goal-sensitive, meaning that it generates only clauses connected to goal clauses [20]. It is open whether goal-sensitivity is useful to reason in large knowledge bases.
The experiments with Koala allow us to identify critical issues for the performance of an SGGS prover. For example, instance generation by SGGS-extension may be a bottleneck for problems with many input clauses, and forms of caching should be considered to avoid repeating computations.
Notes
The name of the procedure in [63] is DPLL(\({{\mathcal {T}}}\)), but the recent literature calls it CDCL(\({{\mathcal {T}}}\)), since the DPLL (Davis-Putnam-Logemann-Loveland) [27] and CDCL procedures have been recognized as distinct. The same remark applies to DPLL(\(\varGamma \!+\!{{\mathcal {T}}}\)) [21].
An SGGS-splitting is trivial if it produces a singleton partition, such as when trying to split a ground clause or trying to split a clause by a more general one.
The SGGS-derivation with \(I^-\) given for this set in [17, Ex. 11] is incorrect.
For PVD also the finite basis approach applies implying the small model property [17].
SGGS and Koala do not have a built-in treatment of equality.
The average TPTP ratings of the discovered restrained, sort-restrained, and sort-refined-PVD problems are 0.06, 0.08, and 0.08, respectively.
Koala is available at https://github.com/bytekid/koala.
The experimental data are posted at http://cl-informatik.uibk.ac.at/users/swinkler/koala/, http://profs.sci.univr.it/~bonacina/sggs.html or https://github.com/bytekid/koala.
References
Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2), 153–172 (2010). https://doi.org/10.1016/j.jsc.2009.03.003
Ackermann, W.: Solvable Cases of the Decision Problem. North Holland, Amsterdam (1954). https://doi.org/10.1007/BFb0022557
Alagi, G., Weidenbach, C.: NRCL – a model building approach to the Bernays-Schönfinkel fragment. In: C. Lutz, S. Ranise (eds.) Proceedings of FroCoS-10, Lecture Notes in Artificial Intelligence, vol. 9322, pp. 69–84. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-24246-0_5
Andréka, H., van Benthem, J., Nemeti, I.: Modal logics and bounded fragments of predicate logic. J. Phil. Log. 27(3), 217–274 (1998). https://doi.org/10.1023/A:1004275029985
Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reason. 31(2), 129–168 (2003). https://doi.org/10.1023/B:JARS.0000009518.26415.49
Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: CVC5: A versatile and industrial-strength SMT solver. In: D. Fisman, G. Rosu (eds.) Proceedings of TACAS-28, Lecture Notes in Computer Science, vol. 13243, pp. 415–442. Springer, Berlin (2022). https://doi.org/10.1007/978-3-030-99524-9_24
Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: M. Hermann, A. Voronkov (eds.) Proceedings of LPAR-13, Lecture Notes in Artificial Intelligence, vol. 4246, pp. 512–526. Springer, Berlin (2006). https://doi.org/10.1007/11916277_35
Baumgartner, P.: Hyper tableaux – the next generation. In: H. de Swart (ed.) Proceedings of TABLEAUX-7, Lecture Notes in Artificial Intelligence, vol. 1397, pp. 60–76. Springer, Berlin (1998)
Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-up model generation methods. J. Autom. Reason. 64, 197–251 (2020). https://doi.org/10.1007/s10817-019-09515-1
Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4–5), 591–632 (2008). https://doi.org/10.1016/j.artint.2007.09.005
Baumgartner, P., Furbach, U., Niemelä, I.: Hyper tableaux. In: J.J. Alferes, L.M. Pereira, E. Orłowska (eds.) Proceedings of JELIA-5, Lecture Notes in Artificial Intelligence, vol. 1126, pp. 1–17. Springer, Berlin (1996)
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21–52 (2006). https://doi.org/10.1142/S0218213006002552
Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. J. Log. Comput. 20(1), 77–109 (2008)
Bernays, P., Schönfinkel, M.: Zum Entscheidungsproblem der mathematischen Logik. Math. Ann. 99, 342–372 (1928). https://doi.org/10.1007/BF01459101
Bonacina, M.P.: On conflict-driven reasoning. In: N. Shankar, B. Dutertre (eds.) Proceedings of the 6th Workshop on Automated Formal Methods (AFM) May 2017, Kalpa Publications, vol. 5, pp. 31–49. EasyChair (2018). https://doi.org/10.29007/spwm
Bonacina, M.P., Dershowitz, N.: Canonical ground Horn theories. In: A. Voronkov, C. Weidenbach (eds.) Programming Logics: Essays in Memory of H. Ganzinger, Lecture Notes in Computer Science, vol. 7797, pp. 35–71. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-37651-1_3
Bonacina, M.P., Winkler, S.: SGGS decision procedures. In: N. Peltier, V. Sofronie-Stokkermans (eds.) Proceedings of IJCAR-10, Lecture Notes in Artificial Intelligence, vol. 12166, pp. 356–374. Springer, Berlin (2020). https://doi.org/10.1007/978-3-030-51074-9_20
Bonacina, M.P., Hsiang, J.: On the modelling of search in theorem proving - towards a theory of strategy analysis. Inf. Comput. 147, 171–208 (1998). https://doi.org/10.1006/inco.1998.2739
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reason. 56(2), 113–141 (2016). https://doi.org/10.1007/s10817-015-9334-4
Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: inference system and completeness. J. Autom. Reason. 59(2), 165–218 (2017). https://doi.org/10.1007/s10817-016-9384-2
Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161–189 (2011). https://doi.org/10.1007/s10817-010-9213-y
Bonacina, M.P., Furbach, U., Sofronie-Stokkermans, V.: On first-order model-based reasoning. In: N. Martí-Oliet, P. Olveczky, C. Talcott (eds.) Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer, Lecture Notes in Computer Science, vol. 9200, pp. 181–204. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-23165-5_8
Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reason. 64(3), 579–609 (2020). https://doi.org/10.1007/s10817-018-09510-y
Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. J. Autom. Reason. 66(1), 43–91 (2022). https://doi.org/10.1007/s10817-021-09606-y
Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Kluwer Academic Publishers, Oxford (2004). https://doi.org/10.1007/978-1-4020-2653-9
Ceri, S., Gottlob, G., Tanca, L.: What you always wanted to know about Datalog (and never dared to ask). IEEE Trans. Knowl. Data Eng. 1(1), 146–166 (1989). https://doi.org/10.1109/69.43410
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. C. ACM 5(7), 394–397 (1962). https://doi.org/10.1145/368273.368557
de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: R. Giacobazzi, J. Berdine, I. Mastroeni (eds.) Proceedings of VMCAI-14, Lecture Notes in Computer Science, vol. 7737, pp. 1–12. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-35873-9_1
de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. J. Symb. Comput. 35(1), 21–58 (2003). https://doi.org/10.1016/S0747-7171(02)00092-5
Dershowitz, N.: Orderings for term-rewriting systems. Theoret. Comput. Sci. 17(3), 279–301 (1982). https://doi.org/10.1016/0304-3975(82)90026-3
Dershowitz, N., Plaisted, D.A.: Rewriting. In: J.A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. 1, chap. 9, pp. 535–610. Elsevier (2001). https://doi.org/10.1016/b978-044450813-3/50011-4
Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980). https://doi.org/10.1145/322217.322228
Duarte, A., Korovin, K.: Implementing superposition in iProver (system description). In: N. Peltier, V. Sofronie-Stokkermans (eds.) Proceedings of IJCAR-10, Lecture Notes in Computer Science, vol. 12167, pp. 388–397. Springer, Berlin (2020). https://doi.org/10.1007/978-3-030-51054-1_24
Fermüller, C.G., Leitsch, A.: Model building by resolution. In: E. Börger, G. Jäger, H. Kleine Büning, S. Martini (eds.) Proceedings of CSL-6, Lecture Notes in Computer Science, vol. 702, pp. 134–148. Springer, Berlin (1993). https://doi.org/10.1007/3-540-56992-8_10
Fermüller, C.G., Salzer, G.: Ordered paramodulation and resolution as decision procedure. In: A. Voronkov (ed.) Proceedings of LPAR-4, Lecture Notes in Artificial Intelligence, vol. 698, pp. 122–133. Springer, Berlin (1993). https://doi.org/10.1007/3-540-56944-8_47
Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Handbook of Automated Reasoning, pp. 1791–1849. Elsevier and MIT Press, Amsterdam and Cambridge (2001). https://doi.org/10.1016/b978-044450813-3/50027-8
Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: P. Fontaine (ed.) Proceedings of CADE-27, Lecture Notes in Artificial Intelligence, vol. 11716, pp. 233–249. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-29436-6_14
Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: S. Ghilardi, R. Sebastiani (eds.) Proceedings of FroCoS-7, Lecture Notes in Artificial Intelligence, vol. 5749, pp. 263–278. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-04222-5_16
Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of LICS-18, pp. 55–64. IEEE (2003)
Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reason. 58(1), 3–31 (2017). https://doi.org/10.1007/s10817-016-9388-y
Grädel, E., Kolaitis, P.G., Vardi, M.Y.: On the decision problem for two-variable first-order logic. Bull. Symb. Log. 3, 53–69 (1997). https://doi.org/10.2307/421196
Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559–587 (1991). https://doi.org/10.1145/116825.116833
Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. J. of Relational Methods in Computer Science 1, 251–276 (2004). https://doi.org/10.1007/978-3-642-37651-1_15
Joyner, W.H., Jr.: Resolution strategies as decision procedures. J. ACM 23(3), 398–417 (1976). https://doi.org/10.1145/321958.321960
Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: J. Leech (ed.) Proceedings of the Conference on Computational Problems in Abstract Algebras, pp. 263–298. Pergamon Press (1970). https://doi.org/10.1016/B978-0-08-012975-4
Korovin, K.: Inst-Gen – a modular approach to instantiation-based automated reasoning. In: A. Voronkov, C. Weidenbach (eds.) Programming Logics: Essays in Memory of H. Ganzinger, Lecture Notes in Computer Science, vol. 7797, pp. 239–270. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-37651-1_10
Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: P. Fontaine, C. Ringeissen, R.A. Schmidt (eds.) Proceedings of FroCoS-9, Lecture Notes in Artificial Intelligence, vol. 8152, pp. 214–228. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-40885-4_15
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: R. Treinen (ed.) Proceedings of RTA-20, Lecture Notes in Computer Science, vol. 5595, pp. 295–304. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-02348-4_21
Kounalis, E., Rusinowitch, M.: On word problems in Horn theories. In: E. Lusk, R. Overbeek (eds.) Proceedings of CADE-9, Lecture Notes in Computer Science, vol. 310, pp. 527–537. Springer, Berlin (1988). https://doi.org/10.1007/BFb0012854
Kounalis, E., Rusinowitch, M.: On word problems in Horn theories. J. Symb. Comput. 11(1–2), 113–128 (1991). https://doi.org/10.1016/S0747-7171(08)80134-4
Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: N. Sharygina, H. Veith (eds.) Proceedings of CAV-25, Lecture Notes in Computer Science, vol. 8044, pp. 1–35. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-39799-8_1
Lamotte-Schubert, M., Weidenbach, C.: BDI: a new decidable clause class. J. Log. Comput. 27(2), 441–468 (2017). https://doi.org/10.1093/logcom/exu074
Lee, S.J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reason. 9, 25–42 (1992)
Ludwig, M., Waldmann, U.: An extension of the Knuth-Bendix ordering with LPO-like properties. In: N. Dershowitz, A. Voronkov (eds.) Proceedings of LPAR-14, Lecture Notes in Artificial Intelligence, vol. 4790, pp. 348–362. Springer, Berlin (2007). https://doi.org/10.1007/978-3-540-75560-9_26
Manthey, R., Bry, F.: SATCHMO: a theorem prover implemented in Prolog. In: E. Lusk, R. Overbeek (eds.) Proceedings of CADE-9, Lecture Notes in Computer Science, vol. 310, pp. 415–434. Springer, Berlin (1988). https://doi.org/10.1007/BFb0012847
Marques Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: A. Biere, M. Heule, H. Van Maaren, T. Walsh (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 131–153. IOS Press (2009). https://doi.org/10.3233/978-1-58603-929-5-131
McMillan, K.L.: Developing distributed protocols with Ivy. Slides from http://vmcaischool19.tecnico.ulisboa.pt/ (2019)
Mei, H., Qin, G., Xu, M., Esiner, J.: Neural Datalog through time: informed temporal modeling via logical specification. In: H. Daumé III, A. Singh (eds.) Proceedings of ICML-37, Proceedings of Machine Learning Research, vol. 119, pp. 6808–6819 (2020)
Navarro, J.A., Voronkov, A.: Proof systems for effectively propositional logic. In: A. Armando, P. Baumgartner, G. Dowek (eds.) Proceedings of IJCAR-4, Lecture Notes in Artificial Intelligence, vol. 5195, pp. 426–440. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-71070-7_36
Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356–364 (1980). https://doi.org/10.1145/322186.322198
Nicolas, J.M.: Logic for improving integrity checking in relational databases. Acta Infor. 18(3), 227–253 (1982). https://doi.org/10.1145/322186.322198
Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557–580 (2007). https://doi.org/10.1016/j.ic.2006.08.009
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)
Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: Safety verification by interactive generalization. SIGPLAN Notices 51(6), 614–630 (2016). https://doi.org/10.1145/2980983.2908118
Piskac, R., de Moura, L., Bjørner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reason. 44(4), 401–424 (2010). https://doi.org/10.1007/978-3-540-71070-7_35
Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedr. Vieweg & Sohn, Berlin (1997)
Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reason. 25, 167–217 (2000)
Ramsey, F.P.: On a problem in formal logic. Proc. Lond. Math. Soc. 30, 264–286 (1930). https://doi.org/10.1112/plms/s2-30.1.264
Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: A.P. Felty, A. Middeldorp (eds.) Proceedings of CADE-25, Lecture Notes in Artificial Intelligence, vol. 9195, pp. 399–415. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-21401-6_28
Riazanov, A.: Implementing an efficient theorem prover. Ph.D. thesis, Department of Computer Science, The University of Manchester (2003)
Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. of Computer Mathematics 1, 227–234 (1965). https://doi.org/10.2307/2272384
Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965). https://doi.org/10.1145/321250.321253
Rubio, A.: A fully syntactic AC-RPO. Inf. Comput. 178(2), 515–533 (2002). https://doi.org/10.1006/inco.2002.3158
Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3. In: P. Fontaine (ed.) Proceedings of CADE-27, Lecture Notes in Computer Science, vol. 11716, pp. 495–507. Springer, Berlin (2019). https://doi.org/10.1007/978-3-030-29436-6_29
Scott, D.: A decision method for validity of sentences in two variables. J. Symb. Log. 27, 377–377 (1962)
Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687–697 (1967). https://doi.org/10.1145/321420.321428
Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017). https://doi.org/10.1007/s10817-009-9143-8
van Gelder, A., Topor, R.W.: Safety and translation of relational calculus queries. ACM Trans. Database Syst. 16(2), 235–278 (1991). https://doi.org/10.1145/114325.103712
Waldmann, U., Schmidt, R.A.: Modal tableau systems with blocking and congruence closure. In: H. de Nivelle (ed.) Proceedings of TABLEAUX-24, Lecture Notes in Artificial Intelligence, vol. 9323, pp. 38–53. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-24312-2_4
Weidenbach, C.: Combining superposition, sorts and splitting. In: A. Robinson, A. Voronkov (eds.) Handbook of Automated Reasoning, vol. 2, pp. 1965–2012. Elsevier, Amsterdam (2001). https://doi.org/10.1016/b978-044450813-3/50029-1
Acknowledgements
We thank Konstantin Korovin for the iProver (v2.8) code for basic data structures, term indexing, and type inference, imported in Koala. Parts of this work were done while the first author was visiting the Simons Institute for the Theory of Computing, the Leibniz Zentrum für Informatik at Schloss Dagstuhl, and the Computer Science Laboratory of SRI International, whose support is greatly appreciated.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This research was funded in part by grant “Ricerca di base 2017” of the Università degli Studi di Verona. Authors are listed alphabetically.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Bonacina, M.P., Winkler, S. Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover. J Autom Reasoning 67, 6 (2023). https://doi.org/10.1007/s10817-022-09656-w
Received:
Accepted:
Published:
DOI: https://doi.org/10.1007/s10817-022-09656-w