SGGS (Semantically-Guided Goal-Sensitive reasoning) is a refutationally complete theoremproving method that ofers first-order conflict-driven reasoning and is model complete in the limit. This paper investigates the behavior of SGGS on Horn clauses, which are widely used in declarative programming, knowledge representation, and verification. We show that SGGS generates the least Herbrand model of a set of definite clauses, and that SGGS terminates on Horn clauses if and only if hyperresolution does, with the advantage that SGGS builds a model. We report on experiments applying the SGGS prototype prover Koala to Horn problems, with promising performances especially on satisfiable inputs.
role of queries. Horn clauses are also an essential language for program verification [
In this paper we analyze the behavior of SGGS on Horn clauses and relate it to that of
hyperresolution [
We assume the basic notions in theorem proving, and we use a, b for constants, P, Q, R, T for predicates, f, g for functions, x, y, z for variables, t, u, v for terms, Var(t) for the set of variables in t, and top(t) for the top symbol of t. We also use L, M, P, Q for literals, at(L) for L’s atom, C, D, E for clauses, Greek lower case letters for substitutions, and I, J for
to literals. A clause is positive if all its literals are positive, negative if all its literals are negative, and mixed otherwise. A clause is Horn if it has at most one positive literal, and definite if it has exactly one positive literal. C+ and C− denote the disjunctions of the positive and negative literals in C.
We refer the readers to [
SGGS is semantically guided by an initial interpretation I. Given a set S of clauses, if I 6|= S, SGGS seeks a model of S, by building candidate partial interpretations diferent from I, and using I as default to complete them. If the empty clause ⊥ is generated, unsatisfiability is reported. If I is I− (I+) SGGS tries to discover which positive (negative) literals need to be true to satisfy S.
SGGS works with a trail of clauses = A1 B C1[L1], . . . , An B Cn[Ln], where Ai B Ci[Li] occurs at index i and the brackets mean that literal Li is selected in Ci. The length of and its prefix of length j are denoted | | and |j . An SGGS trail represents a partial interpretation Ip( ): if is empty, denoted ε, Ip( )=∅; otherwise, Ip( )=Ip( |n−1) ∪ pcgi(An B Ln, ), where pcgi abbreviates proper constrained ground instances. A pcgi of An B Cn[Ln] is a cgi C[L] that is not satisfied by Ip( |n−1) (i.e., Ip( |n−1) ∩ C[L] = ∅) and can be satisfied by adding L as ¬L 6∈ Ip( |n−1). Thus, pcgi’s are productive instances as they produce Ip( ). For the selected literal, pcgi(An B Ln, ) = {L : C[L] ∈ pcgi(An B Cn[Ln], )}. Ip( ) is completed into an interpretation I[ ] by consulting I for the truth value of any literal undefined in Ip( ).
Then, L is said to be I-false if it is uniformly false in I and I-true if it is true 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. I-false literals are preferred for selection to diferentiate I[ ] from I. An I-true literal is selected only in an I-all-true clause.
A clause is a conflict clause if all its literals are uniformly false in I[ ]. SGGS ensures that every I-all-true clause C[L] in is either a conflict clause or the justification of its selected literal L, meaning that all literals of C[L] except L are uniformly false in I[ ], so that L must be true in I[ ] to satisfy C[L]. To this end, SGGS assigns I-true literals to clauses. Given trail = A1 B C1[L1], . . . , An B Cn[Ln], an I-true literal M ∈ Cj [Lj ] is assigned to Ck[Lk] if k<j and the selection of Lk makes M uniformly false in I[ ] (all literals in Gr(Aj B M ) appear negated in pcgi(Ak B Lk, ) and hence in Ip( )). SGGS requires that a non-selected I-true literal is assigned, while a selected I-true literal is assigned if possible. If all the literals of an I-all-true clause C[L] in are assigned, C[L] is a conflict clause, and L is assigned to the largest index (or to the rightmost clause) among all literals in C[L]. If all the literals of C[L] except L are assigned, C[L] is the justification of L, and C[L] is in the disjoint prefix of . The disjoint prefix of , denoted dp( ), is the longest prefix such that pcgi(Aj B Cj [Lj ], ) = Gr(Aj B Cj [Lj ]) for all Aj B Cj [Lj ] in dp( ). Thus, all selected literals in dp( ) are disjoint.
An SGGS-derivation is a series of trails 0 ` 1 ` . . . j ` . . ., where 0 = ε, and ∀j, j > 0, an SGGS-inference generates j from j−1 and S. If ⊥ 6∈ and I[ ] 6|= S, SGGS has two ways to make progress. If = dp( ), the trail is in order, but since I[ ] 6|= S it means that I[ ] 6|= C0 for a C0 ∈ Gr(C) and C ∈ S. Then, SGGS applies SGGS-extension to generate from C and a clause A B E, such that E is an instance of C and C0∈Gr(A B E). If 6= dp( ), the trail needs repair: either there are intersections between selected literals to be removed by SGGS-splitting, or there is a conflict. The SGGS-extension rules specialize the SGGS-extension scheme ([3, Def. 12]) that we instantiate for I = I+ or I = I−: Definition 1. Given input set S and trail , if there is a clause C∈S such that for all its I-true literals L1, . . . , Ln (n≥0) there are clauses B1 B D1[M1], . . . , Bn B Dn[Mn] in dp( ), such that literals M1, . . . , Mn are I-false, and ∀j, 16j6n, Lj α=¬Mj α with simultaneous most general unifier (mgu) α, SGGS-extension adds to the extension clause A B E = (Vjn=1 Bj α) B Cα, assigning L1α, . . . , Lnα to D1, . . . , Dn, respectively. Clause C is the main premise and B1 B D1[M1], . . . , Bn B Dn[Mn] are the side premises. An SGGS-extension is conflicting , if A B E is a conflict clause, and non-conflicting otherwise, that is, if A B E has pcgi’s and therefore extends I[ ]. If A B E is I-all-true then it is a conflict clause. A derivation starts with a non-conflicting SGGS-extension where C is I-all-false, so that α is empty, n = 0, and E = C. All such steps can be done as one and we assume they are.
Example 1. Consider the following set S of definite clauses with I− as initial interpretation:
P(f(a, x)) ¬P(f(y, a)) ∨ P(g(y, a)) (i) (iii)
P(g(b, x)) ¬P(g(z, b)) ∨ P(f(z, b)) (ii) (iv).
I− satisfies clauses (iii) and (iv) because they have negative literals, but not the positive
clauses (i) and (ii). SGGS extends the trail with (i) and (ii), so that I[
SGGS-deletion removes all disposable clauses, where An B Cn[Ln] is disposable if Ip( |n−1) |= An B Cn[Ln]. SGGS-splitting aims at isolating intersections between selected literals, and it is the rule that introduces constraints. A partition of A B C[L] is a set {Ai B Ci[Li]}in=1 such that Gr(A B C) = Sin=1{Gr(Ai B Ci)}, the Li’s are chosen consistently with L, and the Ai B Li’s are pairwise disjoint (cf. [3, Sect. 3.2]). Given trail clauses A B C[L] and B B D[M ], a splitting of C by D, denoted split (C, D), is a partition of A B C[L] such that at(Gr(Aj B Lj )) for some j is the intersection of A B L and B B M , and all other Ai B Li’s are disjoint from B B M . SGGS-splitting replaces A B C[L] with split (C, D). Clause A B C[L] is the split clause, and Aj B Cj [Lj ] is the representative of B B D[M ] in the splitting. Splitting by similar literals (s-splitting) and splitting by dissimilar literals (d-splitting) apply when A B C[L] occurs at a higher index than B B D[M ], with similar and dissimilar referring to whether L and M have the same or opposite sign. After an s-splitting, D’s representative in split (C, D) is disposable (cf. [3, Lem. 3]) and hence removed by SGGS-deletion. After a d-splitting, the intersection between L and M is removed by SGGS-resolution.
If a clause A B C[L] added by SGGS-extension is in conflict with I[ ] and L is I-false, SGGS-resolution explains the conflict by resolving A B C[L] with the justification in dp( ) whose selected literal makes L uniformly false in I[ ].
Definition 2 (SGGS-Resolution). If contains clauses B B D[M ] and A B C[L] such that B B D[M ] is I-all-true, is in dp( ), and occurs at a smaller index than A B C[L], L is I-false, L = ¬M ϑ for some substitution ϑ, and A |= Bϑ, then SGGS-resolution generates the SGGS-resolvent A B R, where R is (C \ {L}) ∪ (D \ {M })ϑ, replaces C by A B R, deletes all clauses with literals assigned to C, and assigns every I-true literal P ϑ in R to the same clause that P in C or D was assigned to (cf. [3, Def. 26]).
In conflict explanation the resolvent is still a conflict clause. As SGGS-extension ensures that all I-false literals of a conflict clause can be resolved away (cf. [ 3, Def. 19]), conflict explanation generates either ⊥ or an I-all-true conflict clause H B E[P ]. Conflict solving moves H B E[P ] to the left of the clause A B C[L] in dp( ) to which P is assigned (SGGS-move): the efect is to flip P from being uniformly false to being an implied literal. Then E resolves with C, so that the simplest conflict explanation and solving sequence has the form resolve∗ move resolve. Prior to the move, if the pcgi’s of L contain more than the complements of the cgi’s of P (i.e., ¬Gr(H B P ) ⊂ pcgi(A B L, )), left splitting replaces A B C[L] by split (C, E) with P assigned to the representative of E in split (C, E). Left splitting enables SGGS-move, which places E to the left of its representative in split (C, E). Thus, the sequence has the form resolve∗ l-split? move resolve, where ? means at most once. If E contains another literal Q that is assigned to clause C and unifies with P with mgu ϑ, E cannot move because Q would have nowhere to be assigned. Then SGGS-factoring replaces E by split (E, Eϑ), where the SGGS-factor Eϑ is its own representative and literal assignments are inherited. As SGGS-factoring may repeat, the full form of the sequence is resolve∗ factor∗ l-split? move resolve.
Fairness of an SGGS-derivation involves several properties: an inference is applied whenever ⊥6∈ and I[ ] 6|= S; no trivial splitting (e.g., splitting a ground clause) occurs; SGGS-deletion and other clause removals are applied eagerly; conflicts are solved before more SGGS-extensions; and inferences applying to shorter prefixes of the trail are not forever neglected in favor of others applying to longer prefixes (cf. [ 3, Defs. 32, 37, and 49]). The limit of a fair derivation 0 ` 1 ` . . . j ` j+1 ` . . . is the longest trail ∞ such that ∀i, i 6 | ∞|, there exists an ni such that ∀j, j > ni, if | j | ≥ i then j |i is equivalent to ∞|i (cf. [3, Def. 50]). In words, all prefixes of the trail stabilize eventually, and dp( ∞) = ∞. Both derivation and ∞ may be infinite, but ∞ is k if the derivation halts at stage k. SGGS is refutationally complete and model complete in the limit: for all inputs S, initial interpretations I, and fair derivations, if S is satisfiable, I[ ∞] |= S, and if S is unsatisfiable, ⊥ ∈ k for some k (cf. [3, Thms. 9 and 11]).
lattice ordered by the subset relation ⊆, with intersection T as the greatest lower bound (glb) operator, union S as the least upper bound (lub) operator, ∅ as bottom, and A as top element. A set of definite clauses admits a least Herbrand model, defined as the intersection of all Herbrand models of S, or, equivalently, as the fixpoint of the functional
P ∨ ¬Q1 ∨ . . . ∨ ¬Qm (m > 0) in S and a ground substitution σ, such that L = P σ and {Q1σ . . . Qmσ} ⊆ J , then L ∈ TS(J ) and vice versa. As TS is continuous (cf. [10, Prop.
so that lfp(TS) = Sk>0 TSk(∅) (cf. [10, Thm. 6.5]).
I− reasons forward or bottom-up. The derivation starts with an SGGS-extension that puts on the trail all the positive unit clauses in S. If this addition of positive literals to Ip( ) falsifies all the negative literals in instances of mixed clauses, SGGS-extensions with mixed clauses follow. Since I−-false (i.e., positive) literals are preferred for selection, and every clause has exactly one, all selected literals are positive, with no choice of selected literal. All extensions are non-conflicting extensions that add pcgi’s to Ip( ), which contains only positive literals and grows monotonically: ∀j, j > 0, Ip( j ) ⊆ Ip( j+1). Since all selected literals are positive, the only splitting inferences are s-splitting steps, followed by deletions of representatives that remove intersections between selected literals, without afecting Ip( ) and its monotonic growth. Since I = I−, for an atom L ∈ A, I[ ∞] |= L if and only if L ∈ Ip( ∞). In other words, I[ ∞] seen as a set of atoms is Ip( ∞). The next theorem shows that Ip( ∞) = lfp(TS).
Theorem 1. Given an input set S of definite clauses, with Herbrand base A and functional TS : P(A) → P(A), for all fair SGGS-derivations with I− as initial interpretation and limit ∞, it is Ip( ∞) = lfp(TS).
Proof: lfp(TS) ⊆ Ip( ∞): since SGGS is model complete in the limit, I[ ∞] |= S, that is, Ip( ∞) |= S, writing Herbrand models as sets of atoms. Thus, lfp(TS) ⊆ Ip( ∞), because lfp(TS) is the least Herbrand model.
the derivation. Since it is still there in ∞, there exists a stage k such that for all stages j, j > k, clause Ai B Ci[Li] is at index i in j and L ∈ Ip( j ). The proof is by induction on the smallest such k.
Base case: k = 1 and L ∈ Ip( 1). Trail 1 is the result of the first SGGS-extension that adds all the I−-all-false input clauses. Since S is a set of definite clauses, the I−-all-false input clauses are the positive unit clauses of S. Thus, L ∈ Ip( 1) means that L = P σ for a ground substitution σ and a positive unit clause P ∈ S with [P ] in 1. By definition of TS, L ∈ TS(∅) and L ∈ lfp(TS).
Induction hypothesis: for all k (k > 1), for all n 6 k, if n is the smallest stage of the
such that for all j, j > k + 1, L ∈ Ip( j). This means that L 6∈ Ip( k). Thus, the step k ` k+1 must be a non-conflicting SGGS-extension with main premise C = P ∨ ¬Q1 ∨ . . . ∨ ¬Qm in S (m>0), mgu α, and extension clause Cα = [P α] ∨ ¬Q1α ∨ . . . ∨ ¬Qmα, such that L ∈ pcgi(P α, k+1). Therefore, there exist a ground substitution σ0 such that L = P ασ0 and hence a substitution σ such that Cσ is ground and L = P σ. Furthermore, ∀i, 1 6 i 6 m, Qiσ ∈ Ip( k), because otherwise I[ k] |= ¬Qiσ (as I− |= ¬Qiσ), and hence [P σ] ∨ ¬Q1σ ∨ . . . ∨ ¬Qmσ would not be in pcgi([P α] ∨ ¬Q1α ∨ . . . ∨ ¬Qmα, k+1) and L would not be in pcgi(P α, k+1). Then, for all i, 1 6 i 6 m, let hi be the smallest stage such that ∀j, j > hi, Qiσ ∈ Ip( j). Since Qiσ ∈ Ip( k), we have hi 6 k for all i, 1 6 i 6 m. Thus, by induction hypothesis, for all i, 1 6 i 6 m, Qiσ ∈ lfp(TS). Since lfp(TS) |= S, we have lfp(TS) |= P ∨ ¬Q1 ∨ . . . ∨ ¬Qm and hence lfp(TS) |= P σ ∨ ¬Q1σ ∨ . . . ∨ ¬Qmσ. Therefore, L = P σ ∈ lfp(TS).
For instance, in Example 1, lfp(TS) is Ip( 3). We describe next the behavior of SGGS when also negative clauses enter the picture, first with I− and then with I+.
model of S is found, the consequence of adding positive ground literals to Ip( ) towards building lfp(TSD ) is that some instance of a negative clause in S becomes an I−-all-true conflict clause, that a conflicting SGGS-extension adds to the trail. Let C be the first conflict clause of this kind and k the first trail where C appears. The fact that C is in conflict with I[ k] means that C is in conflict with Ip( k). By Theorem 1, this means that C is in conflict with a subset of lfp(TSD ) and hence with lfp(TSD ) itself. Since lfp(TSD ) is the intersection of all the Herbrand models of SD, it follows that C is in conflict with all of them. Therefore, the appearance of C on the trail reveals that S is unsatisfiable. By contrast, a set of first-order clauses does not admit a least Herbrand model, and the appearance of a negative conflict clause on a trail k in an SGGS-derivation with I− simply means that I[ k] 6|= S, so that SGGS solves the conflict and searches for another model.
Furthermore, because all the literals in C are assigned, it is possible to predict the number of SGGS-resolutions needed to go from C to ⊥. This number turns out to be equal to the cardinality |dΓ(C)| of the dependence set dΓ(C) of C in . This set is defined inductively as follows: if an I-true literal in C is assigned to clause D then D ∈ dΓ(C); if
else is in dΓ(C).
Lemma 1. Given an input set S of Horn clauses and I− as initial interpretation, for all fair SGGS-derivations, if an SGGS-extension adds to a trail an I−-all-true conflict clause C, the derivation is a refutation, and the number of SGGS-resolution steps after the stage of is |dΓ(C)|.
Base case: |dΓ(C)| = 0 and hence dΓ(C) = ∅. Since C is an I−-all-true conflict clause, all its literals must be assigned. Thus, dΓ(C) = ∅ implies that C is ⊥ and both claims are fulfilled.
Induction hypothesis: if |dΓ(C)| = k for k > 0 then both claims hold.
Inductive case: let |dΓ(C)| = k + 1, literal L be selected in C, and D[M ] be the clause which L is assigned to.
If SGGS-factoring applies to C[L] (one or more times), let Cf [Lf ] and 1 be the final SGGSfactor and trail, or Cf [Lf ] = C[L] and 1 = otherwise. Either way, dΓ1 (Cf ) = dΓ(C), because SGGS-factoring unifies two literals of C that are both assigned to D and SGGSfactors inherit assignments, so that Lf is still assigned to D in 1. Also, dΓ1 (D) = dΓ(D) trivially holds.
If left-splitting applies to Cf [Lf ] and D, let D0[M 0] and 2 be the representative of Cf in split (D, Cf ) and the resulting trail, or D0[M 0] = D[M ] and 2 = 1 otherwise. Either way, Lf is assigned to D0 in 2 and dΓ2 (D0) = dΓ1 (D) = dΓ(D), because the I−-true literals in D0 inherit their assignments from those in D. Thus, dΓ2 (Cf ) = dΓ1 (Cf ) \ {D} ∪ {D0} = dΓ(C) \ {D} ∪ {D0} as the only change is that Lf is assigned to D in 1 and to D0 in 2 (†).
SGGS-move places Cf [Lf ] to the left of D0[M 0] and then SGGS-resolution applies to Cf [Lf ] and D0[M 0] generating the SGGS-resolvent R = (Cf \ {Lf }) ∪ (D0 \ {M 0})ϑ that replaces D0 in the resulting trail 3. Every I−-true literal P ϑ in R is assigned to the same clause that P in Cf or in D0 was assigned to (?). Since Cf is negative and D0 is Horn, R is negative, it is another I−-all-true conflict clause, and all its literals are assigned. We show that dΓ3 (R) = dΓ(C) \ {D}. For every clause E ∈ dΓ3 (R) due to a literal in (Cf \ {Lf })ϑ, it is E ∈ dΓ2 (Cf ) by (?), and E ∈ dΓ1 (Cf ) by (†), and E ∈ dΓ(C) because dΓ1 (Cf ) = dΓ(C). For every clause E ∈ dΓ3 (R) due to a literal in (D0 \ {M 0})ϑ, it is E ∈ dΓ2 (D0) by (?), and E ∈ dΓ(D) as dΓ2 (D0) = dΓ1 (D) = dΓ(D), and hence E ∈ dΓ(C) because the selected literal L of C is assigned to D in . Up to here we have shown that dΓ3 (R) ⊆ dΓ(C). Next, D ∈ dΓ(C), but D 6∈ dΓ3 (R), because Lf was resolved away, and
it is exactly dΓ3 (R) = dΓ(C) \ {D}, because by inspection of the above inferences nothing else has changed. Since |dΓ(C)| = k + 1, we have |dΓ3 (R)| = k. By induction hypothesis the first claim holds, and the number of SGGS-resolutions after the stage of 3 is k, so that the number of SGGS-resolutions after the stage of is k + 1 = |dΓ(C)|.
clauses, SGGS with I+ does not do anything as I+ |= S. If S is a set of Horn clauses, where
the negative clauses are the goal clauses, I+ is goal-sensitive (it satisfies the assumptions,
not the goal clauses), and hence SGGS with I+ is goal-sensitive (all generated clauses are
connected to goal clauses) [
Example 2. Given S = {¬Q(a, x), ¬R(x, y) ∨ ¬R(y, x) ∨ Q(x, y), R(b, a), R(a, b)}, the SGGS-derivation with I+ starts as follows: and continues extending with I+-all-true conflict clause R(a, b) and solving the conflict:
3 : [¬Q(a, x)], [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y) 4 : [¬Q(a, x)], [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y), [R(a, b)] 5 : [¬Q(a, x)], [¬R(a, b)] ∨ ¬R(b, a) ∨ Q(a, b), top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y), [R(a, b)]
6 : [¬Q(a, x)], [R(a, b)], [¬R(a, b)] ∨ ¬R(b, a) ∨ Q(a, b), top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y)
7 : [¬Q(a, x)], [R(a, b)], [¬R(b, a)] ∨ Q(a, b), top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y) ` ` ` ` ` ` ` ` ` ` Then the derivation proceeds extending with I+-all-true conflict clause conflict-solving phase finds a refutation: R(b, a) whose 8 : [¬Q(a, x)], [R(a, b)], [¬R(b, a)] ∨ Q(a, b), top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y), [R(b, a)]
9 : [¬Q(a, x)], [R(a, b)], [R(b, a)], [¬R(b, a)] ∨ Q(a, b), top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y)
10 : [¬Q(a, x)], [R(a, b)], [R(b, a)], [Q(a, b)], top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y)
11 : [¬Q(a, b)], top(x) 6= b B [¬Q(a, x)], [R(a, b)], [R(b, a)], [Q(a, b)], top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y)
12 : [Q(a, b)], [¬Q(a, b)], top(x) 6= b B [¬Q(a, x)], [R(a, b)], [R(b, a)], top(y) 6= b B [¬R(a, y)] ∨ ¬R(y, a) ∨ Q(a, y)
13 : [Q(a, b)], ⊥, . . .
If the second literal is selected in the second clause of 2, the derivation is very similar, extending first with R(b, a) and then with R(a, b). 4. On the Termination of SGGS and Hyperresolution Both SGGS and hyperresolution halt on the clause set of Example 1. We show that this is a general result: given a Horn set, SGGS with I− halts if and only if hyperresolution extend extend extend l-split move resolve extend
move resolve l-split move resolve with subsumption, henceforth HR+S , halts. A derivation by HR+S has the form S0 ` S1 ` . . . Sj ` Sj+1 ` . . ., where S0=S; for all j, j > 0, Sj+1 is obtained from Sj by either a hyperresolution or a subsumption step; and the limit S∞ is the set Si>0 Tj>i Sj of the persistent clauses. In the Horn case, all hyperresolvents are unit clauses identified with their single literal. The next lemma establishes a correspondence between clauses in the respective limits of the two derivations.
Lemma 2. Given a satisfiable set S of Horn clauses, for all fair derivations by SGGS with I− and HR+S , respectively, (i) for all clauses A B C[L] in ∞, there exists a unit clause Q ∈ S∞ such that Gr(A B L) ⊆ Gr(Q), and (ii) for all unit clauses Q ∈ S∞ there exist clauses {Bj B Dj [Mj ]}jn=1 in ∞ such that Gr(Q) ⊆ Sjn=1 Gr(Bj B Mj ). Proof: As S is satisfiable and both methods are sound, neither derivation is a refutation. As described in Sect. 3 and by Lemma 1, the only inferences in the SGGS-derivation are non-conflicting SGGS-extensions, that add non-negative clauses where the single positive literal is selected, s-splitting, or SGGS-deletion steps.
Proof of Claim (i): by induction on the smallest stage k (k > 1) such that A B C[L] is in k.
Base case: k = 1 and C[L] is an I−-all-false (i.e., positive, hence unit) input clause
Q = L ∈ S∞. Otherwise, there exists a Q ∈ S∞ that subsumes L, that is, L = Qσ for some substitution σ, so that Gr(L) ⊆ Gr(Q) holds.
Induction hypothesis: for all j, 0 6 j 6 k, for all clauses A B C[L] for which j is the smallest stage such that A B C[L] is in j , the claim holds.
Inductive case: let A B C[L] be a clause for which k + 1 is the smallest stage such that A B C[L] is in k+1. This means that A B C[L] is placed on the trail by step k ` k+1. If k ` k+1 is an s-splitting step, A B C[L] is a clause in a partition of a split clause B B D[M ] in k. By definition of partition, Gr(A B C[L]) ⊆ Gr(B B D[M ]) and hence Gr(A B L) ⊆ Gr(B B M ). By induction hypothesis, there exists a Q ∈ S∞ such that Gr(B B M ) ⊆ Gr(Q). Thus, Gr(A B L) ⊆ Gr(B B M ) ⊆ Gr(Q) and the claim holds. Otherwise, k ` k+1 is an SGGS-extension. Let C ∈ S be the main premise, B1 B D1[M1], . . . , Bn B Dn[Mn] in dp( k) the side premises, and (Vin=1 Biα) B C[L]α the extension clause, where L is the only positive literal in C, and α is the simultaneous mgu of all the I−-true (i.e., negative) literals ¬L1, . . . , ¬Ln of C with M1, . . . , Mn (i.e., Liα = Miα for all i, 1 6 i 6 n). By induction hypothesis, for all i, 1 6 i 6 n, there exists a Qi ∈ S∞ such that Gr(Bi B Mi) ⊆ Gr(Qi). This implies that for all i, 1 6 i 6 n, there exists a substitution σi (which can be a variable renaming or even empty) such that Mi = Qiσi. The fact that the Mi’s are instances of the Qi’s, together with the fact that the Mi’s do not share variables (∀i ∀j, 1 6 i 6= j 6 n, Var(Mi) ∩ Var(Mj ) = ∅), because they come from distinct clauses, and the existence of the above simultaneous mgu α, imply the existence of a simultaneous mgu τ such that ∀i, 1 6 i 6 n, Liτ = Qiτ . For all i, 1 6 i 6 n, let ri be the stage such that Qi ∈ Tj>ri Sj and let r = max{ri : 1 6 i 6 n}, so that Q1, . . . , Qn ∈ Sr. Therefore, hyperresolution applies to nucleus C ∈ S and satellites
general literals, there exists a substitution σ such that Lα = Lτ σ. If Lτ is persistent, Q = Lτ ∈ S , and from Lα = Lτ σ we get Gr((Vjn=1 Bj α) B Lα) ⊆ Gr(Lα) ⊆ Gr(Q).
∞ If Lτ is subsumed, there exist a Q ∈ S∞ and a substitution δ, such that Lτ = Qδ. Thus, it is Gr((Vjn=1 Bj α) B Lα) ⊆ Gr(Lα) ⊆ Gr(Lτ ) ⊆ Gr(Q).
Base case: k=0 and Q ∈ S0 = S is a positive unit input clause. Thus, the first SGGSextension that adds to the trail all I−-all-false clauses (i.e., all positive unit input clauses) places [Q] on trail 1 at some index i. If [Q] is subject to neither SGGS-deletion nor s-splitting, [Q] is in ∞ and the claim holds. Since SGGS-move never applies, no clause is inserted to the left of [Q] (i.e., at an index smaller than i) at any subsequent stage j (j > 1) of the SGGS-derivation. Thus, the only clauses that can s-split [Q] or make it disposable are other positive unit input clauses that the first SGGS-extension places on the left of [Q]. By fairness, SGGS-deletion is applied before any other inference, and removes all disposable clauses in 1 in one step. If a bunch of positive unit input clauses [Q1], . . . , [Qn] on the left of [Q] in 1 make it disposable, we have Gr(Q) ⊆ Sjn=1 pcgi(Qj , 1) ⊆ Sjn=1 Gr(Qj ). If [Q0] on the left of [Q] splits [Q] into a partition {Bj B [Mj ]}jn=1, the representative of [Q0] is subsequently deleted by SGGS-deletion. Without loss of generality, let the representative of [Q0] be Bn B [Mn]. Then {[Q0]} ∪ {Bj B [Mj ]}jn=−11 is a partition of [Q], that is, Gr(Q) = Gr(Q0) ∪ Sjn=−11 Gr(Bj B Mj ). Since the model-fixing phase between the ifrst and the second SGGS-extension is finite, even if some of these clauses were subject in turn to s-splitting, the reasoning repeats and the process cannot go on forever, so that the claim is satisfied by clauses in ∞.
Induction hypothesis: for all j, 0 6 j 6 k, for all unit clauses Q for which j is the smallest stage such that Q ∈ Sj , the claim holds.
Inductive case: let Q be a unit clause for which k + 1 is the smallest stage such that
Let C = (P ∨ ¬L1 ∨ . . . ∨ ¬Lm) ∈ S ⊆ Sk (m > 0) be the nucleus, Q1, . . . , Qm ∈ Sk the positive unit satellites, and τ the simultaneous mgu for this hyperresolution inference (i.e., ∀i, 1 6 i 6 m, Liτ = Qiτ ), so that Q = P τ . By induction hypothesis, for all i, 1 6 i 6 m, there exist sets of clauses {Bhi B Dhi [Mhi ]}hnii=1 all in ∞ = dp( ∞), such that Gr(Qi) ⊆ Sni
hi=1 Gr(Bhi BMhi ). Let r be the smallest stage of the SGGS-derivation where all these clauses are in dp( r). By Lemma 3, at most im=1ni SGGS-extensions, applying at stages equal to or greater than r, generate extension clauses {Aj B C[P ]αj }jh=1, with h 6 im=1ni, such that Gr(Q) = Gr(P τ ) ⊆ Sjh=1 Gr(Aj B P αj ). By the Lifting Theorem for SGGS [3, Thm. 4], extension clauses are not disposable in the trail to which they are added. Since SGGS-move never applies, it cannot be that these clauses are made disposable by clauses that move to their left at subsequent stages. Thus, the clauses in {Aj B ([P αj ] ∨ ¬L1αj ∨ . . . ∨ ¬Lmαj )}jh=1 are in ∞, unless some of them is subject to s-splitting during the finite model-fixing phases that follow each SGGS-extension. As already shown in the base case, if this happens, each split clause get replaced by clauses in ∞ with the same ground instances, so that the claim holds.
The lemma invoked in the above proof is stated and proved below.
Lemma 3. Given a set S of Horn clauses, assume that hyperresolution generates from nucleus C = (P ∨ ¬L1 ∨ . . . ∨ ¬Lm) ∈ S and satellites Q1, . . . , Qm the unit hyperresolvent Q = P τ , where τ is the simultaneous mgu such that ∀i, 1 6 i 6 m, Liτ = Qiτ . Suppose that for every satellite Qi, SGGS with I− has in dp( ) a set of clauses {Bhi BDhi [Mhi ]}hnii=1 with positive selected literals, such that Gr(Qi) ⊆ Sni hi=1 Gr(Bhi B Mhi ). Then at most im=1ni SGGS-extensions with main premise C apply and generate extension clauses {Aj B C[P ]αj }jh=1 (h 6 im=1ni), such that Gr(Q) = Gr(P τ ) ⊆ Sjh=1 Gr(Aj B P αj ). Proof: We show that Gr(P τ ) ⊆ Sjh=1 Gr(Aj B P αj ). Let L ∈ Gr(P τ ), that is, L = P τ σ for some ground instance Cτ σ of C. By the first part of the hypothesis, for all i, 1 6 i 6 m, Liτ = Qiτ , and hence Liτ σ = Qiτ σ, so that Qiτ σ is a ground instance of Qi. By the second part of the hypothesis, for all i, 1 6 i 6 m, there exists an hi (1 6 hi 6 ni) such that
Qiτ σ ∈ Gr(Bhi B Mhi ). Their positive selected literals Mh1 , . . . , Mhm are simultaneously unifiable with the atoms L1, . . . , Lm, as witnessed by the unifier τ σ. Let α be their most general unifier, and δ the substitution such that τ σ = αδ. Then, SGGS-extension applies with main premise C, side premises Bhi B Mhi , 1 6 i 6 m, and simultaneous mgu α, producing extension clause (Vim=1 Bhi α) B C[P ]α, such that L ∈ Gr((Vim=1 Bhi α) B P α), because L = P τ σ = P αδ. Since an SGGS-extension with main premise C needs m side premises whose positive selected literals unify simultaneously with L1, . . . , Lm, and for each Li, 1 6 i 6 m, there are ni candidates, there are clearly at most im=1ni such extensions.
The main theorem follows.
Theorem 2. Given a set of Horn clauses SGGS with I− halts if and only if HR+S halts. Proof: Since both SGGS and HR+S are refutationally complete, it sufices to prove the claim for a satisfiable input set S of Horn clauses. Let SD ⊆ S be the subset of the definite clauses. (⇒) By way of contradiction, assume that SGGS with I− halts and HR+S does not. SGGS halts at a stage k (k > 0) with finite limit k = B1 BD1[M1], . . . , Bm BDm[Mm] and Ip( k) = Sjm=1 pcgi(Bj B Mj , k) = Sjm=1 Gr(Bj B Mj ), as k = dp( k). By Theorem 1, Ip( k) = lfp(TSD ). The HR+S -derivation is infinite with infinite limit S∞ containing infinitely many persistent positive unit clauses L0, L1, L2, . . .. Also HR+S generates lfp(TSD ), represented by Si>0 Gr(Li). Thus, Sjm=1 Gr(Bj B Mj ) = Si>0 Gr(Li). By
Gr(Qj ). Therefore, Si>0 Gr(Li) = Sjm=1 Gr(Bj B Mj ) ⊆ Sjm=1 Gr(Qj ). Since the Qj ’s are finitely many, this means that all but finitely many clauses in S∞ can be subsumed, contradicting the assumption that S∞ (the limit of a fair derivation) is infinite. (⇐) By way of contradiction, assume that HR+S halts whereas SGGS with I− does not. HR+S halts at some stage k (k > 0) with finite limit Sk. The set {L1, . . . , Lm} of the positive unit clauses in Sk represents lfp(TSD ), in the sense that Sim=1 Gr(Li) = lfp(TSD ). SGGS with I− produces an infinite derivation with infinite limit ∞ = B1 B D1[M1], . . . , Bj B Dj [Mj ], Bj+1 B Dj+1[Mj+1], . . ., where ∀j, j > 0, Mi ∈ D+ i and Ip( ∞) = Sj>1 pcgi(Bj B Mj , ∞) = Sj>1 Gr(Bj B Mj ) as ∞ = dp( ∞). By Theorem 1, Ip( ∞) = lfp(TSD ). Thus, Sj>1 Gr(Bj B Mj ) = Sim=1 Gr(Li). By Claim (ii) in Lemma 2, for all i, 1 6 i 6 m, there exist clausesj>{1BGhirB(BDjBhi [MMjh)i ]}=hniiS=1min ∞ such that Gr(Li) ⊆ Shnii=1 Gr(Bhi B Mhi ). Therefore, S i=1 Gr(Li) ⊆ Sim=1 Shnii=1 Gr(Bhi B Mhi ). Since the Li’s are finitely many, and each of them is covered by finitely many clauses in ∞, this means that all but finitely many clauses in ∞ are disposable, contradicting the assumption that ∞ (the limit of a fair derivation) is infinite. Example 3. Given the following set S of definite clauses
P(x, f(x)) ¬Q(f(x), y) ∨ R(x) ¬R(x) ∨ Q(a, a)
(i) (iii)
(v)
SGGS with I− halts after five extensions:
as I[
Thanks to its model-based character and model representation via selected literals, SGGS can learn from a Horn subproblem of a non-Horn first-order problem a literal selection strategy that is useful for termination on the non-Horn problem. Definition 3. A clause set SH is a Horn subproblem of a clause set S if for every C ∈ S the set SH contains a maximal subclause C0 ⊆ C that is Horn, and SH contains no other clauses.
Let SH be a Horn subproblem of a non-Horn first-order problem S. Note that if J |= SH then J |= S for a Herbrand interpretation J . A Horn subproblem SH defines a literal selection strategy, that can be used when SGGS with I− is applied to S, as follows. Whenever SGGS-extension adds an instance Cα of a clause C ∈ S, such that Cα has multiple positive literals that can be selected,1 the strategy picks the positive 1The SGGS-extension is non-conflicting and Cα has more than one positive literal with pcgi’s, or Cα is a non-I−-all-true conflict clause where any positive literal can be selected. literal Lα such that L appears in the maximal Horn subclause C0 ⊆ C in SH . While S may have more than one Horn subproblem SH , the strategy is uniquely defined once an SH is chosen. The next example portrays a situation where SGGS with I− halts with the literal selection based on SH and diverges otherwise.
Example 4. Let S = {(i) P(x, a), (ii) ¬P(x, y) ∨ R(y) ∨ P(x, f(y)), (iii) ¬R(f(x)) ∨ ¬P(x, f(x))} and SH = {(i), (ii0) ¬P(x, y) ∨ R(y), (iii)}. Given SH , SGGS with I− halts in two steps:
ε ` [P(x, a)] ` [P(x, a)], ¬P(x, a) ∨ [R(a)].
If the literal selection strategy defined by SH is adopted, SGGS with I− halts also on S: ε ` [P(x, a)] ` [P(x, a)], ¬P(x, a) ∨ [R(a)] ∨ P(x, f(a)).
In both derivations Ip( 2) is {P(fk(a), a) : k > 0} ∪ {R(a)} and I[
Hyperresolution also halts on SH , but if given S it generates an infinite series of hyperresolvents where both depth and number of literals increase: R(a) ∨ P(x, f(a)), R(a) ∨ R(f(a)) ∨ P(x, f2(a)), R(a) ∨ R(f(a)) ∨ R(f2(a)) ∨ P(x, f3(a)), . . . . Furthermore, in this example, the nontermination of hyperresolution cannot be cured by an ordering on literals and the restriction to resolve only upon maximal literals in satellites. Indeed, the ifrst satellite (i) is a unit clause, and in the generated hyperresolvents no ground literal can dominate the non-ground literal. For example, R(a) 6 P(x, f(a)) as R(a) and x are incomparable.
The following theorem generalizes the observation that termination of SGGS on a satisfiable Horn subproblem corresponds to termination on the original non-Horn problem. Theorem 3. Given a set S of clauses and I− as initial interpretation, if S has a satisfiable Horn subproblem SH for which there exists a fair, finite SGGS-derivation, then there exists a fair finite SGGS-derivation for S that selects the same literals and hence builds the same model.
Proof: Let and 0 denote SGGS-derivations with initial interpretation I− and input
We show by induction on the length k of 0 that there exists a fair, finite derivation : 0 ` 1 ` · · · ` k of the same length, such that for all stages j (0 6 j 6 k) and indices h (1 6 h 6 | j |) if 0j has at index h clause Ah B Ch0[Lh] then j has at index h a clause Ah B Ch[Lh] with the same selected constrained literal. Since the induced partial interpretation is determined by the selected literals, it follows that for all stages j (0 6 j 6 k) it holds that Ip( j ) = Ip( 0j ) and hence I[ j ] = I[ 0j ].
Base case: k = 0: 00 is empty and so is 0.
Induction hypothesis: the claim holds for length k.
Inductive case: let the length of 0 be k +1. As described in Sect. 3 and by Lemma 1, since
non-conflicting extension or an s-splitting or an SGGS-deletion step. If 0k ` 0k+1 is a nonconflicting extension with main premise C0 ∈ SH and side premises D10[M1], . . . , Dn0[Mn] in dp( 0k), it adds extension clause C0[L]α, where α is the simultaneous mgu of all the
(C0)− = C− because C0 is a maximal Horn subclause. By induction hypothesis, there exist clauses D1[M1], . . . Dn[Mn] in dp( k) with the same selected literals. Therefore, can be extended with a non-conflicting extension k ` k+1 with the same mgu and extension clause C[L]α. If 0k ` 0k+1 is an s-splitting step, it replaces a clause Ah B Ch0[Lh] by split (Ch0, C0 ) for some Ar B Cr0 [Lr] (r < h), where split (C0 , C0 ) is a r h r partition {Bi B Di0[Mi]}in=1 such that Gr(Ah B Ch0) = Sin=1{Gr(Bi B Di0)}. By induction hypothesis, k has constrained clauses Ah B Ch[Lh] and Ar B Cr[Lr] at positions h and r respectively. Since the partition in SGGS-splitting is determined by the selected literals, can be extended with an s-splitting step that replaces Ah B Ch[Lh] by split (Ch, Cr), where split (Ch, Cr) is a respective partition {Bi B Di[Mi]}in=1 such that Gr(Ah B Ch) = Sin=1{Gr(Bi B Di)}. If 0k ` 0k+1 deletes Ah B Ch0[Lh], it means that this clause is disposable, that is, Ip( 0k|h−1) |= Ah B Ch0[Lh]. By induction hypothesis, k has a clause Ah B Ch[Lh] at index h and Ip( k|h−1) = Ip( 0k|h−1). Thus, Ah B Ch[Lh] is disposable in k and can be extended with a deletion step that removes it. Since is made of inferences mirroring those in 0 and 0 is fair, also is fair.
Suppose that S is a first-order problem that is not in an SGGS-decidable fragment [
are made of atoms in B. A fair SGGS-derivation in a finite basis is finite [ 13, Thm. 1]. An SGGS-derivation is ground, if all clauses on the trail during the derivation are ground. The following example shows that a ground derivation may arise also if the input is not ground.
Example 5. Let Sn be the following parametric set of Horn clauses (n > 0):
{(i) P(fn(a)), (ii) ¬P(f(x)) ∨ P(x), (iii) ¬P(x) ∨ ¬P(f(x)) ∨ . . . ∨ ¬P(fn(x))}. These
sets belong to an SGGS-decidable class named restrained where SGGS-derivations are
ground and in a finite basis [
¬P(fn−1(a)) ∨ [P(fn−2(a))] ` . . . ` n+1 : . . . , ¬P(f(a)) ∨ [P(a)] ` n+2 : . . . , [¬P(a)] ∨ . . . ∨ ¬P(fn(a)) ` n+3 : . . . , [¬P(a)] ∨ . . . ∨ ¬P(fn(a)), ¬P(f(a)) ∨ [P(a)] ` n+4 : . . . , [¬P(f(a))] ∨ . . . ∨ ¬P(fn(a)) ` . . . ` 3n+4 : ⊥, . . . extend (i) extend (ii) extend (ii) extend (ii) extend (iii)
move resolve resolve where the derivation length is 3n+4 = n+4+2n as it takes 2 steps (move and resolve) to eliminate each of the n literals in the last clause in n+4. Hyperresolution generates P(fn−1(a)), . . . , P(a) and then ⊥. Unrestricted resolution does not stay in B (e.g., resolving (i) upon ¬P(fn−1(x)) in (iii) gets a clause including ¬P(fn+1(a))), and may generate exponentially many clauses in the worst case (e.g., the 2n+1 subclauses of the instance of (iii) where x ← a).
Theorem 4. Given a set S of Horn clauses, for all fair SGGS-derivations with I− as initial interpretation, if the derivation is ground and in a finite basis B, its length is linear in |B|.
Proof: By [13, Lem. 1], for all stages j (j > 0) of a fair derivation in a finite basis B, | j | 6 |B|+1 and | j | 6 |B| if dp( j ) = j . Let denote a fair ground derivation in B. Since is ground, dp( j ) = j holds at all stages, because ground literals have no intersection. Also, is finite by [ 13, Thm. 1]. Recall the behavior of SGGS with I− from Sect. 3. Since is ground, no SGGS-splitting (and hence no SGGS-deletion) applies, and the model-constructing phase of is made only of SGGS-extensions. If S is satisfiable, no conflict ever arises, itself is made only of SGGS-extensions, and | j | 6 |B| at its final stage j means that the number of SGGS-extensions and hence | | is in O(|B|). If S is unsatisfiable, a conflict with an I−-all-true conflict clause must arise.
By Lemma 1, is a refutation, and the number of SGGS-resolutions after stage i + 1 is equal to the cardinality of the dependence set of the conflict clause, which is bounded by | i|, hence by |B|. Since is ground, SGGS-factoring and left splitting do not apply problem class Horn during the conflict-solving phase. As there is at most one application of SGGS-move for every resolution step, the length of the conflict-solving phase is in O(|B|). Since the length of both model-constructing and conflict-solving phases is in O(|B|), the claim follows.
set of the ground atoms occurring in S. While also hyperresolution behaves linearly, given a set of ground Horn clauses, other resolution-based strategies (e.g., positive or negative resolution, ordered resolution) can still generate an exponential number of clauses [15, Ch. 1].
We focus on Horn problems as Horn logic is the subject of this paper. We wrote a script that considers all 5,000 problems without equality in TPTP 7.4.0, transforms problems into clausal form if needed and detects Horn problems. This resulted in 1,220 Horn problems that we submitted to the SGGS prototype prover Koala,2 with I− or I+ as initial interpretation, E, Vampire, and iProver. All experiments were run single-threaded on a 12-core Intel i7-5930K 3.50GHz machine with 32GB of main memory.
Table 1 reports how many problems were found satisfiable (SAT) or unsatisfiable (UNS) by each tool. Since Koala with I− succeeded on 712 of the 1,220 Horn sets (58% success rate), whereas Koala with I+ succeeded on 633 of them (51% success rate), the results suggest that I− is more efective than I+ on Horn problems. In comparison with the other provers, Koala is ahead on the satisfiable instances but remains behind on the unsatisfiable ones. Indeed, SGGS works by building models, whereas resolution-based strategies are notoriously very good at discovering the unsatisfiability of Horn sets.
Table 2 displays data about the length of the derivations by Koala on Horn problems,
distinguishing between satisfiable and unsatisfiable instances, and among four classes that
are SGGS-decidable because they admit finite bases [
We studied what happens when SGGS with sign-based semantic guidance is applied to Horn clauses. If the input is Horn, SGGS reasons forward (a.k.a. bottom-up) or backward (a.k.a. top-down), depending on whether the guiding interpretation is all-negative (I−) or all-positive (I+). SGGS with I− generates the least fixpoint model of a set of definite clauses, and if the input is unsatisfiable, the first conflict with negative conflict clause announces a refutation: while hyperresolution may get ⊥ in one step, SGGS may get it with a multi-step conflict explanation and solving phase, because SGGS builds a model and has to fix it when a conflict arises.
SGGS with I− and hyperresolution with subsumption have the same termination
behavior on Horn (note that SGGS-deletion and subsumption are not equivalent, because
SGGS-deletion depends on the order of appearance of clauses on the trail, e.g. [3, Ex. 2
and Lem. 1]). Furthermore, SGGS can learn from a Horn subproblem of a non-Horn
problem a literal selection strategy useful for termination on the non-Horn problem. The
model-based character of SGGS pays of on satisfiable inputs, as seen in the experiments
comparing the Koala prototype with mature theorem provers such as Vampire [
Horn problems are not the playground that SGGS was designed for, and hence it is
plausible that they do not exercise all its features, such as its conflict-driven nature and its
similarity to CDCL. This is not surprising, because the approaches to generalize features
of DPLL-CDCL from propositional to first-order logic (e.g., first-order splitting [ 19], the
model evolution calculus [20], SGGS [
A main direction for future work is to endow SGGS with equality reasoning by building the equality axioms in both inference system and model representation. The model-based and conflict-driven style of SGGS also makes it an attractive candidate for integration in frameworks for satisfiability modulo theories such as CDSAT [ 21, 22]. The Koala prototype may be developed in many ways, including preprocessing the input w.r.t. unit resolution, unit-resulting resolution, and subsumption, and devising caching techniques to avoid recomputations.
Acknowledgements This work was done while the first author was visiting the Computer Science Laboratory of SRI International, whose support is greatly appreciated. (Ed.), Proc. CADE-27, volume 11716 of LNAI, Springer, 2019, pp. 495–507. doi:10. 1007/978-3-030-29436-6_29. [18] A. Duarte, K. Korovin, Implementing superposition in iProver, in: N. Peltier, V. Sofronie-Stokkermans (Eds.), Proc. IJCAR-10, volume 12167 of LNAI, Springer, 2020, pp. 388–397. doi:10.1007/978-3-030-51054-1_24. [19] C. Weidenbach, Combining superposition, sorts and splitting, in: J. A. Robinson, A. Voronkov (Eds.), Handbook of Automated Reasoning, volume 2, Elsevier, 2001, pp. 1965–2013. doi:10.1016/b978-044450813-3/50029-1. [20] P. Baumgartner, B. Pelzer, C. Tinelli, Model evolution with equality - revised and implemented, J. Symb. Comput. 47 (2012) 1011–1045. doi:10.1016/j.jsc.2011.12. 031. [21] M. P. Bonacina, S. Graham-Lengrand, N. Shankar, Conflict-driven satisfiability for theory combination: transition system and completeness, J. of Autom. Reason. 64 (2020) 579–609. doi:10.1007/s10817-018-09510-y. [22] M. P. Bonacina, S. Graham-Lengrand, N. Shankar, Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs, J. of Autom. Reason. 66 (2022) 43–91. doi:10.1007/s10817-021-09606-y.