We present a sound and complete ordered resolution calculus for rstorder clauses with straight dismatching constraints. The extended clause language is motivated by our rst-order theorem proving approach through approximation and re nement. Using a clause language with straight dismatching constraints, single re nement steps do not result in a worst-case quadratic blowup in the number of clauses anymore. The re nement steps can now be represented by replacing one input clause with two equivalent clauses. We show soundness and completeness of ordered resolution with straight dismatching constraints. All needed operations on straight dismatching constraints take linear or linear logarithmic time in the size of the constraint.
Q(x)
P (g(x; f (x))) Q(f (g(a; a))) Q(f (g(b; b))) Copyright c by the paper's authors. Copying permitted for private and academic purposes. P (g(f (g(a; a); f (f (g(b; b))))
S(y); Q(x)
Q(z) ! ! ! ! !
P (g(x; y)) S(f (z)) Q(f (g(a; a)))
Q(f (g(b; b))) ! ! ! ! !
P (g(f (g(a; a); f (f (g(b; b)))) via linearization of g(x; f (x)) to g(x; f (z)) and then deep variable term extraction of f (z) through the introduction of a fresh predicate S [TW15]. The approximated clause set has a refutation and the corresponding con icting core, a minimal unsatis able set of instances from the above clauses generating this refutation, is S(f (f (g(b; b)))); Q(f (g(a; a))) P (g(f (g(a; a)); f (f (g(b; b)))))
Q(f (g(b; b))) S(f (f (g(b; b))))
Q(f (g(a; a))) Q(f (g(b; b)))
Lifting the con icting core to the original clause set fails, because the resolvent of the rst two con ict clauses, eliminating the introduced S predicate
Q(f (g(b; b))); Q(f (g(a; a))) P (g(f (g(a; a)); f (f (g(b; b)))))
! is not an instance of the original clause Q(x) ! P (g(x; f (x))), modulo duplicate literal elimination. A re nement step replaces Q(x) ! P (g(x; f (x))) by the instance Q(f (g(a; y))) ! P (g(f (g(a; y)); f (f (g(a; y))))), and instances representing Q(x) ! P (g(x; f (x))), where x is not instantiated with f (g(a; y)). The former clause contains the ground instance Q(f (g(a; a))) ! P (g(f (g(a; a)); f (f (g(a; a))))) and the latter clauses include the ground instance Q(f (g(b; b))) ! P (g(f (g(b; b)); f (f (g(b; b))))):
Q(a) ! P (g(a; f (a)))
Q(b) ! P (g(b; f (b))) Q(g(x; y)) ! P (g(g(x; y); f (g(x; y))))
Q(f (a)) ! P (g(f (a); f (f (a))))
Q(f (b)) ! P (g(f (b); f (f (b))))
Q(f (f (x))) ! P (g(f (f (x)); f (f (f (x)))))
Q(f (g(b; y))) ! P (g(f (g(b; y)); f (f (g(b; y)))))
Q(f (g(f (x); y))) ! P (g(f (g(f (x); y)); f (f (g(f (x); y)))))
Q(f (g(g(x; y); z))) ! P (g(f (g(g(x; y); z)); f (f (g(g(x; y); z))))) Then, the approximation of the above nine clauses, via linearization and deep variable term extraction, excludes the previously found refutation. Actually, the re ned approximated clause set yields a nite saturation and therefore shows satis ability of the original clause set.
Clauses with straight dismatching constraints are closed under resolution and factoring. Repeated re nement steps and resolution inferences can add further atomic constraints to a clause, which are interpreted as conjunctions, e.g., (C; x 6= t ^ y 6= s) represents instances of C where neither x is an instance of t nor y is an instance of s. Straight dismatching constraints can be e ciently encoded in amortized constant space once the input constraint terms are stored. Any straight term generated by the calculus is a subterm of an input straight term. Relevant operations (substitution, intersection, solvability and subset tests) take linear time in the size of the constraints, once they are ordered. Ordering can be done as usual in linear logarithmic time. The ordered resolution calculus with straight dismatching constraints is sound and complete, enables an abstract redundancy criterion and follows the saturation principle: if all non-redundant inferences from a clause set are performed and the empty clause is not generated then the resulting saturated clause set has a model computed by a model operator.
Ordered resolution on constraint clauses has already been investigated. Clauses with dismatching constraints are an instance of the constraint clauses introduced in [NR01]. The authors prove soundness and completeness for ordered superposition extended with general syntactic equality and ordering inequality constraints powerful enough to encode uni cation and maximality restrictions. Algorithms for solving these constraints are NP-hard. In our more speci c setting, the operations on the constraints are linear or linear logarithmic. Furthermore, our completeness proof is an extension of the original superposition completeness proof without constraints [BG94], enabling the standard superposition redundancy criterion.
Our constraints are also a restricted version of the dismatching constraints from [AW15]. These constraints are more powerful than straight constraints as they also allow dismatching between variables in a clause. However, solving these constraints is again NP-hard and completeness for the NRCL calculus is only shown for a nite domain rst-order fragment.
The same dismatching constraints are used in DInst-Gen [Kor13] to exclude redundant instances of clauses. Solving constraints can even be done in linear time because of an extended signature with an additional fresh constant ?. All satis able atomic constraints share the solution where all variables are substituted with ?. Solving constraints therefore reduces to the matching problem on the atomic constraints. Our constraint clause language, however, does not rely on an extended signature.
In [CZ92], clauses are constrained by equational systems [CL89]. An equational system is a quanti er free formula over (dis)equations that are syntactically interpreted over a Herbrand domain. The authors show soundness and completeness of an ordered resolution calculus for the extended clauses. They devise a separate calculus for model building. Testing solvability of equational systems is NP-hard. Straight dismatching constraints are a special case of equational systems. They enable more e cient algorithms (Section 4) that are not instances of the general algorithms for systems. Furthermore, our correctness result for ordered resolution (Section 3) includes a notion of redundancy and the concept of saturation, i.e., model building is the result of a saturated clause set.
Our approach to solving constraints is a special case of the solved form construction described in [CL89]. Normalizing straight constraints only requires the Clash (C2), Decomposition (D2) and Universality (U1) rules. For straight terms the Decomposition rule simpli es to f (t1; : : : ; tn) 6= f (y1; : : : ; yi 1; si; yi+1; : : : ; yn) ) ti 6= si. The Explosion (E) rule is re ned to instantiations with shallow instances (De nition 12).
An alternative to using constraints is the explicit representation described in [LM87]. Their algorithm allows computing a nite set of clauses covering the same ground clauses as a clause with constraint. For example, for (Q(x) ! P (g(x; f (x))); x 6= f (g(a; v))) the explicit representation is exactly the nine clauses listed in the example. This always succeeds because by de nition our constraint represents unrestricted counter-examples. While using the explicit representations is equivalent to using constraints, we require quadratically fewer clauses.
The paper is organized as follows. After the preliminaries, we formally de ne straight dismatching constraints in Section 2. Then, Section 3 contains the soundness and completeness proofs for our ordered resolution calculus with constraints. We conclude with discussing the complexity of operations on straight dismatching constraints.
We consider a standard rst-order language without equality. The letters v; w; x; y; z denote variables, f; g; h functions, a; b; c constants, s; t terms, p; q; r positions and Greek letters ; ; ; are used for substitutions. Capital letters S; P; Q; R denote predicates, A; B atoms, E; L literals, C; D clauses.
A rst-order language is constructed over a signature = (F; P), where F and P are non-empty, disjoint, in general in nite sets of function and predicate symbols, respectively. Every function or predicate symbol has a xed arity and nullary functions are called constants. Further, we assume an in nite set X of variable symbols disjoint from . Then, the set of all terms T(F; X) is de ned recursively by: (i) every constant symbol c 2 F is a term, (ii) every variable x 2 X is a term and (iii) whenever t1; : : : ; tn are terms and f 2 F is a function symbol with arity n, then f (t1; : : : ; tn) is a term. If t1; : : : ; tn are terms and P 2 P is a predicate symbol with arity n, then P (t1; : : : ; tn) is an atom and the ti are its arguments. A term is called linear if there are no duplicate variable occurrences. For brevity, we also write ~t instead of t1; : : : ; tn for the argument of functions and predicates. A literal is either an atom or an atom preceded by : and it is then called positive or negative, respectively.
The set of free variables of an atom (term) denoted by vars( ) is de ned as follows: vars(P (t1; : : : ; tn)) = Si vars(ti), vars(f (t1; : : : ; tn)) = Si vars(ti) and vars(x) = fxg. The function naturally extends to literals, clauses and sets thereof.
A multiset over a set A is a function M from A to the natural numbers. For an element e 2 A, M (e) is the number of occurrences of e in M . We say e is an element of M if M (e) > 0. The union, intersection, and di erence of multisets are de ned by M1(x) [ M2(x) = M1(x) + M2(x), M1(x) \ M2(x) = min(M1(x); M2(x)), and M1(x) n M2(x) = max(0; M1(x) M2(x)). We use set-like notation for multisets.
A clause is a multiset of literals which we write as an implication ! where the atoms in the multiset (the succedent ) denote the positive literals and the atoms in the multiset (the antecedent ) the negative literals. We write for the empty clause. If is empty we omit !, e.g., we write P (x) as an alternative of ! P (x) whereas if is empty ! is always shown. We abbreviate disjoint set union with sequencing, for example, we write ; 0 ! ; A instead of [ 0 ! [ fAg. Terms, literals and clauses are called ground if they contain no variables.
A substitution is a mapping from variables V into terms denoted by pairs fx 7! tg where x 6= x holds only for nitely many variables. The update [x 7! t] denotes the substitution where x maps to t and y maps to y for all y 6= x. The composition denotes the substitution (x ) for all variables x. A substitution is a grounding substitution for V if x is ground for every variable x 2 V.
Given two terms (atoms) s; t, a substitution is called a uni er for s and t if s = t . It is called a most general uni er (mgu) if for any other uni er of s and t there exists a substitution with = . s is called an instance of t if there exists a substitution such that t = s.
An atom ordering is a well-founded, total ordering on ground atoms. For the atom ordering , A B is de ned by A B or A = B. An atom A is maximal with respect to a multiset of atoms , if for all B 2 we have A 6 B. Any atom ordering is extended to literals by A :A B if A B. The multiset extension mul of an ordering is de ned by M1 mul M2 i M1 6= M2 and for all m 2 M1 with M1(m) > M2(m) there is an m0 2 M2 with m m0. The multiset extension of the literal ordering induces an ordering on ground clauses. The clause ordering is compatible with the atom ordering: if the maximal atom in C is greater than the maximal atom in D then D C. We use simultaneously to denote an atom ordering and its literal and clause extensions. For a ground clause set N and clause C, the set N C = fD 2 N j D Cg denotes the clauses of N smaller than C. A literal E (A or :A) is (strictly) maximal in a clause ! ; A ( ; A ! ) if there is no literal in ! that is greater (or equal) than E with respect to .
A Herbrand interpretation I is a - possibly in nite - set of ground atoms. A ground atom A is called true in I if A 2 I and false, otherwise. I is said to satisfy a ground clause C = ! , denoted by I C, if \ I 6= ; or 6 I. A non-ground clause C is satis ed by I if I C for every grounding substitution . An interpretation I is called a model of N , I N , if I C for every C 2 N . A model I of N is considered minimal with respect to set inclusion if there is no model I0 with I0 ( I and I0 N . A set of clauses N is satis able, if there exists a model of N . Otherwise, the set is unsatis able. 2.1
In the following, we extend clauses with dismatching constraints x 6= t which restrict the allowed ground instances. An important restriction is that the term t is straight, i.e., it only has a single branch. De nition 1 (Straight Terms). A term f (s1; : : : ; sn) is called straight, if f (s1; : : : ; sn) is linear and all arguments are variables except for at most one straight argument si.
For example, the terms f (x; f (a; y)) and f (x; f (y; z)) are straight, while f (x; f (a; b)) is not. We can identify straight terms visually in their tree form, if there is exactly one branch with function symbols on each node. f f f f f f a a b Note that for two di erent ground terms t1 and t2, there always exists a position in both where they have di erent function symbols. The path from the root to this position in t1 de nes a straight term t that has only t1 as an instance but not t2. Thus, a straight terms are su cient to isolate two ground instances.
De nition 2 (Straight Dismatching Constraint). A straight dismatching constraint is of the form ^ i2I
si 6= ti where I is a nite set of indices, the si are arbitrary terms and the ti are straight terms.
Given a substitution , = Vi2I si 6= ti. lvars( ) = Si2I vars(si) are the left hand variables in constraint . We further extend the set of constraints with the constants > and ? representing the empty and the unsolvable constraint, respectively. An atomic constraint s 6= t occurring in is called a subconstraint of . The length j j is de ned as the number of subconstraints, i.e., jIj. The size, size( ), and depth, d( ), of a constraint = Vi2I si 6= ti are the sum and maximum of the term depths of the ti, respectively. For brevity, we will call straight dismatching constraints just constraints in the following.
De nition 3 (Solutions). Let be a constraint, a signature and V a set of variables with lvars( ) V. A solution of over V is a grounding substitution over V such that for all i 2 I, si is not an instance of ti. DV( ) := f j is a solution of over Vg. A constraint is solvable if it has a solution and unsolvable, otherwise. Two constraints are equivalent if they have the same solutions over all V. In particular, all grounding substitutions are solutions of >, and ? has no solution.
For example, consider the constraint = x 6= b ^ x 6= f (f (u)) ^ x 6= g(v; w) with the signature F = fa=0; b=0; f =1; g=2g. is solvable and DV( ) = ffx 7! ag; fx 7! f (a)g; fx 7! f (b)g; fx 7! f (g(s; t))g j s; t 2 T(F; ;)g is the set of solutions of over fxg.
Note that atomic constraints are not symmetric. For example x 6= a can have a solution while a 6= x is unsolvable. Furthermore, the right-hand variables in a constraint can be arbitrarily renamed while the left-hand variables are xed. For example, the constraints x 6= f (v) and x 6= f (w) are equivalent but x 6= f (v) and y 6= f (v) are not. For an atom P (g(x; y)) and a constraint x 6= f (y), the two y variables are not connected since for = fy 7! tg, P (g(x; y)) = P (g(x; t)) but (x 6= f (y)) = (x 6= f (y)). To avoid confusion, we generally rename right-hand variables to be unique in a given context.
If is a solution of ^ 0, then is a solution of and if is a solution of , then is a solution of . These two properties follow directly from the de nition. We will ignore V if it is clear in a given context. For example, if restricts the clause C, V is always vars(C) [ lvars( ).
and for all si = sj with i 6= j, ti is not an instance of tj . = Vi2I si 6= ti is called normal, if all si are variables De nition 5 (Constraint Normalization). We de ne constraint normalization following transition system over constraints. # as the normal form of the 1 2 3 4 5 ^ s 6= y ^ f (s1; : : : ; sn) 6= f (y1; : : : ; yn) ^ f (s1; : : : ; sn) 6= f (t1; : : : ; tn) ^ f (s1; : : : ; sn) 6= g(t1; : : : ; tm) ^ x 6= t ^ x 6= t ) ? ) ? ) ) ) ^ si 6= ti if ti is complex
if f 6= g ^ x 6= t
# is a normal constraint and equivalent to .
Proof. In the rst and second rule, f (s1; : : : ; sn) is an instance of y and f (y1; : : : ; yn), respectively. Hence, there are no solutions, which is equivalent to the unsatis able constraint ?. In the third rule, a grounding substitution is a solution of f (s1; : : : ; sn) 6= f (t1; : : : ; tn), if and only if at least one sj is not an instance of tj , i.e. f (s1; : : : ; sn) 6= f (t1; : : : ; tn) is equivalent to s1 6= t1 _ : : : _ sn 6= tn. However, since f (t1; : : : ; tn) is straight and the second rule does not apply, there is exactly one complex ti. Thus, each sj is an instance of the respective variable tj for j 6= i and therefore s1 6= t1 _ : : : _ sn 6= tn simpli es to just si 6= ti. In the forth rule, f (s1; : : : ; sn) can never be an instance of g(t1; : : : ; tm) for any grounding substitution. Hence, all solutions of are solutions of ^ f (s1; : : : ; sn) 6= g(t1; : : : ; tm). In the last rule, let be a solution of ^ x 6= t. Then, x is not an instance of t and hence, not an instance of t either. Therefore, is a solution of ^ x 6= t ^ x 6= t . All rules together cover every case where the left-hand side of a subconstraint is not a variable or there are two constraints x 6= t and x 6= s where s is an instance of t. Hence, # is a normal constraint. De nition 8 (Constrained Clause). A pair of a clause and a constraint (C; ) is called a constrained clause. A constrained clause is normal, if is normal and lvars( ) vars(C). For a given signature , the set G((C; )) = fC j 2 DV( ); V = vars(C) [ lvars( )g is called the set of ground instances of (C; ). The notion extends to sets of constrained clauses. Two constrained clauses are equivalent if they have the same ground instances. A Herbrand interpretation I satis es (C; ), if I G((C; )).
Note that in the context of a constrained clause (C; ), a solution of is implicitly over V = vars(C)[lvars( ) such that C 2 G((C; )). We can now also formally de ne the re nement described in the introduction. Lemma 9 (Re nement). Let N [ f(C; )g be a constrained clause set, x 2 vars(C) and t a straight term with vars(t) \ vars(C) = ;. Then N [ f(C; )g and N [ f(C; ^ x 6= t); (C; )fx 7! tgg are equisatis able. Proof. Let C 2 G((C; )). If x is not an instance of t, then is a solution of ^x 6= t and C 2 G((C; ^x 6= t)). Otherwise, = fx 7! tg 0 for some substitution 0. Then, 0 is a solution of fx 7! tg and thus, C = Cfx 7! tg 0 2 G((Cfx 7! tg; fx 7! tg)). Hence, G((C; )) G((C; ^ x 6= t)) [ G((C; )fx 7! tg): Therefore, if I is a model of N [ f(C; ^ x 6= t); (C; )fx 7! tgg, then I is also a model of N [ f(C; )g.
Let D 2 G((C; ^ x 6= t)) [ G((C; )fx 7! tg). If D = C 2 G((C; ^ x 6= t)), then is also a solution of and therefore D 2 G((C; )). If D = Cfx 7! tg 2 G((C; )fx 7! tg), then fx 7! tg is a solution of and therefore D 2 G((C; )). Hence, G((C; ^ x 6= t)) [ G((C; )fx 7! tg) G((C; )): Therefore, if I is a model of N [ f(C; )g, then I is also a model of N [ f(C; ^ x 6= t); (C; )fx 7! tgg.
Consider again the introductory example. Lifting the con icting core of the approximation failed because the so-called lift-con ict D = Q(f (f (b))); Q(f (f (a))) ! P (g(f (f (a)); f (f (b)))) is not an instance of the original clause Q(x) ! P (g(x; f (x))). Speci cally, because x cannot be instantiated with an instance of both f (f (a)) and f (f (b)). Therefore, we re ne the original clause with the instantiation fx 7! f (f (a))g and the opposing constraint x 6= f (f (a)), resulting in C1 = Q(f (f (a))) ! P (g(f (f (a)); f (f (f (a))))) and C2 = (Q(x) ! P (g(x; f (x))) ; x 6= f (f (a))). D di ers from C1 because both occurrences of x are already instantiated with f (f (a)), excluding any approximations, where the second x is instantiated with f (f (b)). Since x 6= f (f (a)) has no solutions where x is instantiated with f (f (a)) and our approximation preserves this fact, D can not be inferred from the approximation of C2. Therefore, the lift-con ict D can not happen again.
normal, x 2= vars(C) [ lvars( ) and Vi2I x 6= ti is solvable.
Proof. Let C 2 G(C; ), where is a solution of over V. Because Vi2I x 6= ti is solvable, there is a solution fx 7! tg over fxg. Then, [x 7! t] is a solution of Vi2I x 6= ti ^ over V [ fxg. Hence, C [x 7! t] 2 G(C; Vi2I x 6= ti ^ ). The reverse direction is trivial. ^ Vi2I x 6= ti) is equivalent to (C; ), if is
Lemmas 7 and 10 show that for any constrained clause there exists an equivalent normal clause. In the following we assume that constrained clauses are normal.
Lastly in this section, we show that solvability of a constraint is decidable. Note that not all unsolvable constraints trivially normalize to ?. A normal constraint can actually be both solvable and unsolvable depending on the signature. For example, x 6= a is a normal constraint that is solvable for signature fa=0; b=0g but unsolvable for signature fa=0g. A discussion of the implementation is deferred to Section 4.
of # that has no solution.
has no solution if and only if #= ? or there exists a subset x = Vi2I x 6= si De nition 12 (Shallow Instances). Let fy1; y2; : : :g be an in nite set of pairwise distinct variables. We de ne the set of shallow instantiations of x under signature as the set of substitutions
x = ffx 7! f (y1; : : : ; yn)g j f 2 Fg:
Note that if the set of function symbols F is in nite, x is also in nite, but then any constraint is trivially solvable if its normal form is di erent from ?. In the context of oredered resolution, the function symbols appearing in the input clause set constitute a nite signature.
Lemma 13. A constraint x = Vi2I x 6= si has no solution under signature for every 2 x . if and only if x has no solution Proof. \)". Assume is a solution of x for some shallow instantiation . Then, is a solution of x, which contradicts the assumption.
\(". Assume is a solution of x. Then, x is ground and hence, x = f (y1; : : : ; yn) for some function f 2 F and substitution . Thus, xfx 7! f (y1; : : : ; yn)g = Vi2I f (y1; : : : ; yn) 6= si has as a solution, which contradicts the assumption.
Proof. If F is not nite, a constraint has no solution if and only if #= ?. Let #= x1 ^ : : : ^ xn with xi 6= xj for i 6= j. Because j xi j is nite, there exists a function symbol f 2 F such that xi 6= f (~t ) 2= xi for all straight terms f (~t ). Thus, for an arbitrary ground term f (~s ), i = fxi 7! f (~s )g is a solution of xi . Then, 1 [ : : : [ n is a solution of .
If F is nite, we use Proposition 11 and Lemma 13 recursively to check solvability of . Using Proposition 11 we pick the constraints of one variable. Then the constraints are instantiated according to Lemma 13. The instantiated constraints are normalized and then the overall procedure is repeated until either ? or > is derived. The procedure terminates because each instantiation strictly decreases the term depths of the respective constraint and the signature is nite. 3
In this section we de ne an ordered resolution calculus with selection and redundancy on constrained clauses. In [NR01] the authors show that superposition without equality, i.e., ordered resolution, is compatible with arbitrary constraint systems. So their completeness results provide completeness for a straightforward combination of straight dismatching constraints with ordered resolution. However, our calculus is by far more re ned. The constraints are already considered in order to determine maximal literals, they are an inherent part of our notion of redundancy and normalization and inheritance is built into the inference rules. Therefore, we provide here a separate proof of completeness that follows the classical superposition completeness recipe without constraints [BG94].
De nition 15 (Orderings with Constraints). Let be an ordering on ground atoms. A literal A is called (strictly) maximal in a clause (C _ A; ) if and only if there exists a solution of such that for all literals B in C, B A (B A ).
De nition 16 (Selection). A selection function assigns to a clause ! clause C and selection function sel, the literals in sel(C) are called selected. a possibly empty subset of . For a De nition 17 (Redundancy). For a given ordering on ground clauses , a constrained clause (C; ) is redundant w.r.t. N if for every D 2 G((C; )), there exist D1; : : : ; Dn 2 G(N ) D with D1; : : : ; Dn D.
Note that a constrained clause (C; ) with a tautology C or an unsolvable constraint is redundant. As usual, our notion of redundancy does not cover cases such as A(x) subsuming A(f (x)). It can be extended to consider such matches by extending the ordering [BG94] or the notion of fairness [NR01]. De nition 18 (Constrained Subsumption). A clause (C; ) subsumes (D; 0) if there is a substitution that C ( D and DV( 0) DV( ).
Lemma 19. If (C; ) subsumes (D; 0), (D; 0) is redundant in N [ f(C; )g.
Proof. Let D 2 G((D; 0)). Then, is a solution of and hence, C 2 G((C; )). Since C C 2 G((C; )) D and C D . Therefore, (D; 0) is redundant in N [ f(C; )g. such D , De nition 20 (Constrained Condensation). A constrained clause (C; ) can be condensed if there exists a substitution such that (C ; ) with duplicate literals removed subsumes (C; ). (C ; ) is then called the condensation of (C; ).
De nition 21 (Constrained Subsumption Resolution). Let (C _ A; ) and (D _ :A0; 0) be two constrained clauses. Let be the matcher A = A0 and let (C; ) subsume (D; 0), then (D; 0) is called a subsumption resolvent of the clauses (C _ A; ) and (D _ :A0; 0).
In the presence of (D; 0) the clause (D_:A0; 0) is redundant. Therefore, in practice, subsumption resolution directly replaces (D _ :A0; 0) with (D; 0).
De nition 22 (Constrained Resolution). Lemma 24 (Soundness). Constrained Resolution and Factoring are sound.
Proof. Let ( 1; 2 ! 1; 2) be a ground instance of (( 1; 2 ! 1; 2) ; ( 1 ^ 2) ). Then, is a solution of ( 1 ^ 2) and is a solution of 1 and 2. Hence, ( 1 ! 1; A) and ( 2; B ! 2) are ground instances of ( 1 ! 1; A; 1) and ( 2; B ! 2; 2), respectively. Because A = B , if ( 1 ! 1; A) and ( 2; B ! 2) are satis ed, then ( 1; 2 ! 1; 2) is also satis ed. Therefore, Constrained Resolution is sound.
Let ( ! ; A) be a ground instance of (( ! ; A) ; ). Then, is a solution of and is a solution of . Hence, ( ! ; A; B) is a ground instance of ( ! ; A; B; ). Because A = B , if ( ! ; A; B) is satis ed, then ( ! ; A) is satis ed. Thus, Constrained Factoring is sound.
De nition 25 (Saturation). A constrained clause set N is called saturated up to redundancy, if for every inference between clauses in N the result (R; ) is either redundant in N or G((R; )) G(N ). De nition 26 (Partial Minimal Model Construction). Given a constrained clause set N , an ordering and a selection function sel, we construct an interpretation IN for N , called a partial model, inductively on the ground instances of clauses from N as follows:
IC := C := IN :=
[ D2G(N) C 8 < fAg : ;
[ C2G(N)
C
D if C = ! ; A A strictly maximal, sel(C) = ; and IC 6 C otherwise A clause C with C 6= ; is called productive. The smallest ground instance C 2 G(N ), where IN 6 C, is called the minimal false clause. If no minimal false clause exists, then IN is a model of N .
Recall that a ground instance of a constraint clause is a standard clause, De nition 8.
Lemma 27 (Completeness). Let N be a constrained clause set saturated up to redundancy by ordered resolution with selection. Then N is unsatis able, if and only if ( ; >) 2 N .
Proof. Assume N is unsatis able, but ( ; >) 2= N . For the partial model IN , there exists a minimal false clause C 2 G((C; )) for some (C; ) 2 N .
C is not productive, because otherwise IN C . Hence, either sel(C) 6= ; or no positive literal in C is strictly maximal. Assume C = 2; B ! 2 with B 2 sel(C) or :B maximal. Then, B 2 IC and there exists a ground instance ( 1 ! 1; A) = D C of some clause (D; 0) 2 N , which produces A = B . Therefore, there exists a = mgu(A; B) and ground substitution such that C = C , D = D . Since = is a solution of and 0, is a solution of ( ^ 0) . Under these conditions, constrained resolution can be applied to ( 1 ! 1; A; 0) and ( 2; B ! 2; ). Their resolvent (R; R) = (( 1; 2 ! 1; 2) ; ( ^ 0) ) is either redundant in N or G((R; R)) G(N ). Its ground instance R is false in IN and R C . If (R; R) is redundant in N , there exist C1; : : : ; Cn in G(N ) R with C1; : : : ; Cn R . Because Ci R C , IN Ci and hence IN R , which contradicts IN 6 R . Otherwise, if G((R; R)) G(N ), then R 2 G(N ), which contradicts C being minimal false.
Now, assume sel(C) = ; and C = ! ; B with B maximal. Then, C = ! 0; A; B with A = B . Therefore, there exists a = mgu(A; B) and ground substitution such that C = C and is a solution of . Hence, is a solution of . Under these conditions, constrained factoring can be applied to ( ! 0; A; B; ). The result (R; R) = (( ! 0; A) ; ) is either redundant in N or G((R; R)) G(N ). Its ground instance R is false in IN and R C . If (R; R) is redundant in N , there exist C1; : : : ; Cn in G(N ) R with C1; : : : ; Cn R . Because Ci R C , IN Ci and hence IN R , which contradicts IN 6 R . Otherwise, if G((R; R)) G(N ), then R 2 G(N ), which contradicts C being minimal false.
Therefore, if ( ; >) 2= N , no minimal false clause exists and N is satis able.
As an example for an application of the calculus we consider the following puzzle [Pel86]: \Someone who lives in Dreadsbury Mansion killed Aunt Agatha. Agatha (a), the butler (b), and Charles (c) live in Dreadsbury Mansion, and are the only people who live therein." "A killer always hates his victim, and is never richer than his victim." ( ! K(a; a); K(b; a); K(c; a) ; >) "Charles hates no one that Aunt Agatha hates. Agatha hates everyone except the butler." The compact representation of this exception results in a non-trivial straight dismatching constraint.
[1 : Inp] [2 : Inp] [3 : Inp] [4 : Inp] [5 : Inp]
(K(x; y) ! H(x; y) ; >) (K(x; y); R(x; y) ! ; >) (H(a; x); H(c; x) ! ; >)
( ! H(a; x) ; x 6= b) [6 : Inp] In this section we consider implementation aspects of constraints including the representation of constraints, the solvability test and operations on constraints.
Looking again at constrained resolution, factoring, and normalization, note that the constraint-terms of the inference are all subterms of the constraints of the parent clauses. This means that throughout a saturation, every straight constraint term is a subterm of the constraints in the input set. Therefore, in an implementation we can store the input constraints separately and represent atomic constraints as just a variable and a pointer to the respective subterm.
Furthermore, by adding for each n-ary function symbol f the unary functions f1; : : : ; fn and a constant symbol f0, we can encode and store any straight term as an array of function symbols terminated by a constant symbol. For example, f (x; f (a; y)) and f (x; f (y; z)) become f2; f1; a0 and f2; f0, respectively.
All of the operations on constraints can be applied on arbitrary constraints, but most of them become signi cantly faster if the constraints are sorted. Given total orderings on X and F, we sort normal atomic constraints ascending the following order: x 6= [l] < y 6= [r]
if x <X y x 6= fi; [l] < x 6= gj ; [r] if f <F g x 6= fi; [l] < x 6= fj ; [r] if x 6= fi; [l] < x 6= fi; [r] if i <N j 0 <N i and x 6= [l] < x 6= [r]
The rst operation that becomes faster after sorting is the fth normalization rule (De nition 5). In a sorted constraint, x 6= t will be immediately followed by any x 6= t 1; : : : ; x 6= t n, because any straight instance of a straight term fi; : : : ; g0 has the form fi; : : : ; gj ; : : : ; h0.
While initially sorting a constraint takes linear-logarithmic time, sorting new constraints created from already sorted constraints is generally faster. Adding a fresh constraint and intersection require only a linear insert and merge operation, respectively.
Substitution and normalization, fx 7! tg#, preserves the sorting if t is linear and variable disjoint from the left-hand variables of . Otherwise, we can rst bucket sort the constraint depending on the left-hand variables without changing the ordering of the subconstraints with the same variables. Then, we merge the individual partially sorted intervals of subconstraints. For example, fx 6= f (t1; z) ^ : : : ^ x 6= f (tn; z) ^ x 6= f (z; s1) ^ : : : ^ x 6= f (z; sm)gfx 7! f (y; y)g normalizes to fy 6= t1 ^ : : : ^ y 6= tn ^ y 6= s1 ^ : : : ^ y 6= smg, where y 6= t1 to y 6= tn and y 6= s1 to y 6= sm are still sorted.
Since clauses with an unsolvable constraint are tautologies, checking constraint solvability is an important tool to avoid unnecessary inferences. Compared to the at least NP-complete solvability tests for general constraints [Com91], solvability of straight dismatching constraints can be tested in linear time.
Considering again Lemma 14, note that for any shallow instantiation 2 x an atomic constraint (x 6= t) normalizes to > except for exactly the one where both x and t have the same top function symbol. In that case, normalization reduces the size of t by removing the top symbol of t. This means that in total every nonvariable position in the straight right-hand terms of the constraint is considered exactly once for each 2 x . Solvability can therefore be decided in O(jFjsize( )).
If the subconstraints are sorted, the solvability check can be computed in-place, because each recursive call on some x and # applies to non-overlapping and consecutive sections in the sorted constraint. Recall that right hand sides of constraints do not share any variables. Now, looking at the overall recursive derivation tree generated along the proof of Lemma 14, the follwing invariant holds: Each subterm of the right hand sides of the inital constraint occurs at most once as a top level term on a right hand side constraint in the overall derivation tree. Solvability of a sorted constraint can therefore be decided independently of the size of F in O(size( )).
Furthermore, we can use intermediate results of the solvability check to simplify the constraint. If xfx 7! tg has no solutions for some straight term t but xfx 7! tg #6= ?, we can add x 6= t to (Corollary 29) which replaces the sub-constraints in xfx 7! tg# by De nition 5.5.
We can further improve the chance to identify unsolvable constraints by using many-sorted signatures. Then, the shallow instantiations x only range over the function symbols in the sort of variable x. In array-theories, for example, data, indices, and arrays are usually modeled to be distinct from each other. A constraint on an index-variable is therefore already unsolvable if just all ground terms of the index-sort are excluded. Without sort information, such a constraint is still solvable.
An algorithm to extract a many-sorted signature with a maximal number of sorts was introduced in [Cla03]. At rst, all function and predicate symbols start with di erent sorts. Then, compute equivalence classes of sorts that should be equal for the problem to be well-sorted: Wherever a function symbol is the argument of another function or predicate, their result and argument sorts are the same and for each variable in each clause, the sorts of its occurrences are also the same. Using union- nd, the whole algorithm has linear complexity.
For rst-order logic without equality, the resulting sorts are always monotone [CLS11], which means that the unsorted and many-sorted versions of the same problem are equisatis able. As a consequence, the resolution calculus can continue to use the unsorted signature while the constraint operations use the corresponding manysorted signature.
Another important advantage of straight constraints is the ability to e ciently check whether the solutions of one constraint are a subset of the solutions of another constraint. The subset check allows common redundancy eliminations such as subsumption, condensation, and subsumption resolution to account for constraints. For example, (P (x); x 6= a) subsumes (P (x); Q(y); x 6= a ^ y 6= b), while (Q(x); x 6= a) does not.
If #= > the subset condition on the solutions is trivially ful lled, but even for general constraints, we can decide the subset relation.
Lemma 28. Let and 0 be solvable normal constraints. Then DV( ) solutions for every subconstraint x 6= t in 0.
DV( 0) if and only if fx 7! tg has no Proof. \)". Assume there exists a subconstraint x 6= t in 0, such that is a solution of fx 7! tg. Then, fx 7! tg is a solution of . Because xfx 7! tg = t is an instance of t, fx 7! tg is not a solution of 0. This contradicts the assumption that DV( ) DV( 0).
\(". Assume DV( ) 6 DV( 0). Let be a solution of , but not of 0. There exists a subconstraint x 6= t of 0 such that x is an instance of t. Hence, there is a substitution such that = fx 7! tg . Then, is a solution of fx 7! tg. This contradicts the assumption that fx 7! tg has no solutions.
is equivalent to
^ x 6= t, if fx 7! tg has no solution.
Proof. DV( ^ x 6= t)
DV( ) holds trivially and DV( )
DV( ^ x 6= t) follows from Lemma 28.
Note that if was fully simpli ed according to Corollary 29, then fx 7! tg has no solutions if and only if fx 7! tg#= ?. This means fx 7! tg is unsolvable if there exists a constraint x 6= s 2 such that t is an instance of s. If both and 0 are also sorted, we can therefore implement the subset check similar to a merge in merge-sort in O(size( ) + size( 0)).
As the name ordered resolution suggests the ordering on atoms holds another key role in the e ciency of the calculus. Just as their unconstrained counterparts, the constrained resolution and factoring rules (De nitions 22 and 23) are only applied if the uni ed literals are (strictly) maximal. This means that we can avoid inferences if we can show that these literals are not maximal.
In general, we can continue to use any traditional ordering by ignoring the constraints. If an atom is not (strictly) maximal in the clausal part, it is not (strictly) maximal for any ground instance including the ones solving the constraint. On the other hand, the constraint could be excluding all ground instances where the atom is (strictly) maximal. For example, the lexicographic path ordering (LPO) can be extended with straight dismatching constraints. Similar extensions are possible for the RPO and KBO.
De nition 30 (LPO with Constraints). Let s; t be terms, a constraint and F nite. We de ne the constrained lexicographic path ordering with the following transition system on pairs (s t; ): (f (t1; : : : ; ti 1; si; : : : ; sn) (f (s~n ) (f (s~n ) (x (s (x (s g(t~m ) ; ) ) g(t~m ) ; ) ) f (t~n ) ; ) ) g(t~m ) ; ) ) x t t ; ) ) ; ) ) ; ?) ) 1 i m
^ (si 1 i n
^ (sj i<j n
> ^ (s 2 x ^ (x 2 x > _ (f (s~n ) ti; )
where g g(t~m ); ) f (t~n ); ) x ; t ; #) #) f g where f ^ (si
ti; ) where x 2 vars(g(t~m )) where x 2 lvars( ) where x 2 lvars( )
Proof. The rst to third rule each decrease the depth of s or t, while the constraint remains the same. The fourth and last rules are trivially terminating. For the fth and sixth rule, size( #) < size( ). Therefore, the constrained lexicographic path ordering terminates.
Note that the rst four rules directly follow the de nition of lpo and therefore (s t; >) is the same as computing s lpo t. The fth and sixth rule reuse the principle idea of the solvability check to instantiate until it normalizes to > or ?. In the latter case, the last rule applies to remove instantiations that are excluded by the constraint. For example, consider (a x ; x 6= a) with precedence a b f g. The only ground case where a 6 lpo x is (a a ; a 6= a), but the constraint a 6= a is unsolvable. Therefore, a lpo x under constraint x 6= a.
Furthermore, note that (a b ; b 6= a) ) > directly implies that also (a f (x) ; f (x) 6= a) ) > and (a g(x; y) ; g(x; y) 6= a) ) >. In general, we need to check only the \minimal" solution with respect to of x lpo in the fth rule. Analogously, the \maximal" solution of x su ces for the sixth rule, if it exists. A solution of x is minimal (maximal) if for every solution 0 of x, x lpo x 0 ( x lpo x 0 ). For example, the constraint x 6= a ^ x 6= f (b) ^ x 6= f (f (u)) has under signature a b f the minimal solution fx 7! bg and maximal solution fx 7! f (a)g, but no maximal solution exists under signature a b f g. If there is no maximal solution, it means that arbitrarily large terms are solutions for x. Then, we can immediately conclude (x t; ) ) ? if x 2= vars(t). Therefore, we can re ne these rules to (s (x x; ) ) (s t ; ) ) (x x ; t ; #) #) where x 2 lvars( ) and where x 2 lvars( ) and is the minimal solution of x is the maximal solution of x
Just like the solvability check, minimal and maximal solutions can be computed in linear time. Unless an earlier case allows an early termination, the previous rules would eventually generate all cases for solutions of x including the minimal and maximal. Generating the cases alone corresponds to the work required to nd the minimal or maximal solution.
Lemma 32. I (s t; ) ) >, then s lpo t for every solution of . s 6 lpo x . Then, x Proof. \)": By induction on the derivation (s t; ) ) >.
The rst four rules follow directly from the de nition of lpo. For example, consider the rst rule. Let (f (s~n ) g(t~m ); ) ) W1 i m(f (s~n ) ti; ) ) >. Then, (f (s~n ) ti; ) ) > for at least one 1 i m. By the inductive hypothesis, f (s~n ) lpo ti for every solution of . Therefore by the de nition of lpo, f (s~n ) lpo g(t~m ) for every solution of .
For the fth rule, let (s x; ) ) V 2 x (s x ; ) ) >. Assume there is a solution of such that = f (y1; : : : ; yn) 0 for some substitution 0 and there is a x . = fx 7! f (y1; : : : ; yn)g 2 Since 0 is a solution of , s 0 6 lpo x 0 contradicts the inductive hypothesis on (s x ; ) ) >. The sixth rule is analogous. The last rule is trivial as ? has no solutions.
\(": Let (s t; ) 6) >, i.e., there is normal form (s t; ) ) F , where F is either ? or a formula consisting of conjunctions and disjunctions of pairs (s t; ) where no rule can be applied. We prove by induction on the derivation (s t; ) ) F , that there is a solution of such that s 6 lpo t .
Again, the rst four rules follow directly from the de nition of lpo. For example, consider the second rule. Let (f (s~n ) g(t~m ); ) ) V1 i n(si g(t~m ); ) 6) >. Then, (f (s~n ) ti; ) 6) > for at least one 1 i n. By the inductive hypothesis, si 6 lpo g(t~m ) for a solution of . Therefore, by the de nition of lpo, f (s~n ) 6 lpo g(t~m ) for the solution of .
For the fth rule, let (s x; ) ) V 2 x (s x ; ) 6) >. Then, (s > for at least one 2 x . By the inductive hypothesis, s 6 lpo x for a solution of 6 lpo x for the solution of . The sixth rule is analogous and the last rule contradicts (s
Constrained LP O extends to atoms and literals in the usual way.
Corollary 33. Let (C _ E; ) be a constrained clause. If (E L; ) ) L in C, then E is not (strictly) maximal in (C _ E; ) under lpo. 5
> ((E
L; ) ) >) for some literal We have presented a sound and complete ordered resolution calculus for rst-order clauses with straight dismatching constraints. This constraint clause language enables a re nement method for our abstraction-re nement calculus [TW15] by replacing an input clause by exactly two constrained clauses instead of a quadratically ((j j 1) d(t), see Section 1) sized explicit representation using standard clauses [LM87]. At the same time, a resolution prover only needs to store the input constraint terms once and can then store atomic constraints in constant space. Aside from sorting constraints, all operations on constraints perform in linear time. This is in contrast to general dismatching constraints where solvability is NP-hard [CL89]. SAT can be encoded as solvability of dismatching constraints with only ground terms on the right-hand side. For example, the SAT clause Ci = x1 _ :x2 _ x3 is encoded by the atomic constraint i = fi(x1; x2; x3) 6= fi(false; true; false). Then a general dismatching constraint 1 ^ ^ n as the result of the encoding of a clause set fC1; : : : ; Cng with signature = ftrue; falseg is solvable i the clause set fC1; : : : ; Cng is satis able. Currently, we are working on the extension of classical decidable clause fragments to clauses with straight dismatching constraints.
The authors would like to acknowledge discussions with and helpful comments by Gabor Alagi. We further thank our reviewers for their helpful and constructive comments. [BG94]
Leo Bachmair and Harald Ganzinger. Rewrite-based equational theorem proving with selection and simpli cation. Journal of Logic and Computation, 4(3):217{247, 1994. Revised version of Max-PlanckInstitut fur Informatik technical report, MPI-I-91-208, 1991.
Hubert Comon and Pierre Lescanne. Equational problems and disuni cation. Journal of Symbolic Computation, 7(3/4):371{425, 1989.
Koen Claessen. New techniques that improve MACE-style nite model nding. In Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications, 2003.