# prime_implicate_generation_in_equational_logic__80d60a5d.pdf

Journal of Artiﬁcial Intelligence Research 60 (2017) 827-880 Submitted 02/17; published 12/17

Prime Implicate Generation in Equational Logic

Mnacho Echenim mnacho.echenim@univ-grenoble-alpes.fr Nicolas Peltier nicolas.peltier@univ-grenoble-alpes.fr Univ. Grenoble Alpes, CNRS, Grenoble INP, LIG, F-38000 Grenoble France

Sophie Tourret sophie.tourret@mpi-inf.mpg.de Max-Planck-Institut f ur Informatik, Saarland Informatics Campus, Campus E1 4, 66123 Saarbr ucken, Germany

We present an algorithm for the generation of prime implicates in equational logic, that is, of the most general consequences of formulæ containing equations and disequations between ﬁrst-order terms. This algorithm is deﬁned by a calculus that is proved to be correct and complete. We then focus on the case where the considered clause set is ground, i.e., contains no variables, and devise a specialized tree data structure that is designed to eﬃciently detect and delete redundant implicates. The corresponding algorithms are presented along with their termination and correctness proofs. Finally, an experimental evaluation of this prime implicate generation method is conducted in the ground case, including a comparison with state-of-the-art propositional and ﬁrst-order prime implicate generation tools.

1. Introduction

We tackle the problem of generating the prime implicates of an equational formula. Formally, an implicate of a formula (or set of clauses) φ is a clause C that is a logical consequence of φ, written φ |= C. This implicate is prime if for all implicates D such that D |= C, we have C |= D. In other words, prime implicates are the most general clausal consequences of a formula and in particular, 2 is an implicate of φ if and only if φ is unsatisﬁable. Prime implicate generation is a more diﬃcult problem than satisﬁability checking, and has many natural applications in artiﬁcial intelligence and system veriﬁcation, such as diagnosis (De Kleer, 1992), debugging (Echenim & Peltier, 2012) or knowledge representation (Darwiche & Marquis, 2002). In propositional logic, the computation of prime implicates plays a central role in the minimization of boolean functions (Quine, 1955). Such a relation does not exist in more expressive logics, but prime implicate computation also has numerous applications related to abductive reasoning. Indeed, the negation of an implicate I of a formula φ can be viewed as a suﬃcient condition ensuring that φ is false. If φ = KB Conc, where KB is a knowledge base and Conc is a conclusion to be proven, then I can be seen as a suﬃcient condition ensuring that Conc holds, or as a set of missing hypotheses that can be used to derive Conc from the axioms in KB. In particular, abductive reasoning can be very useful for debugging veriﬁcation problems. Indeed, mistakes frequently arise when writing logical speciﬁcations, ranging from obvious (but annoying) typing errors, to forgot-

c 2017 AI Access Foundation. All rights reserved.

Echenim, Peltier & Tourret

ten cases or more fundamental issues. The eﬀect of these errors is usually that the prover fails to ﬁnd a proof, leaving to the user the burden of understanding where the problem comes from. In some cases, counter-examples can be automatically computed, and these counter-examples can then be analyzed to locate the source of the error. However, when dealing with very expressive logics, such counter-examples may not be very informative, because they are too complex and not focused enough on the relevant part of the problem. In some cases, they can even be impossible to ﬁnd, for instance if the considered knowledge base has no ﬁnite models. On the other hand, pointing out missing hypotheses may allow the user to quickly grasp where the problem comes from, and may even suggest hints to correct the speciﬁcation.

1.1 Roadmap

The rest of the paper is structured in the following way. In Section 2, usual deﬁnitions in ﬁrst-order equational logic are brieﬂy reviewed. In Section 3, a representation of ground1

equational clauses up to equivalence modulo equality is deﬁned and techniques are devised for testing logical entailment eﬃciently (by duality, the results also apply to sets of unit ground equational clauses). In Section 4, a calculus is presented to generate implicates of equational clauses. For the sake of generality, this calculus is deﬁned for non-ground clauses, although the following sections focus on ground clauses. The deﬁned calculus is an extension of the Superposition calculus (Bachmair & Ganzinger, 1994), which is the most advanced and successful proof procedure for ﬁrst-order logic with equality. The underlying idea behind this calculus is based on so-called Assertion rules that add new hypotheses into the considered set on demand, in a controlled way. These hypotheses are collected and attached to the clauses as constraints; if the empty clause is generated, then its constraint corresponds to the negation of an implicate of the original formula. The use of constraints also permits to control the class of implicates that are generated: for example, it is possible to use this calculus to generate implicates up to a ﬁxed size, or to generate only the positive implicates. This is a crucial feature in practice since the number of prime implicates is usually huge. In Section 5, data structures are deﬁned to store sets of ground constrained clauses eﬃciently. We devise algorithms based on the results of Section 3 for detecting redundant constrained clauses, i.e., for checking whether a newly generated clause is redundant and to remove all the previously generated clauses it entails, and we prove that these algorithms are sound and complete. In Section 6, experimental comparisons with all available systems for generating implicates in propositional and ﬁrst-order logic are provided, showing evidence of the relevance of our approach. Finally, in Section 7, potential applications and relevant related work are discussed, and lines of future work are suggested. The present paper is a thoroughly expanded version of a conference paper (Echenim, Peltier, & Tourret, 2015). The procedure and the completeness proof have been revised and extended in order to handle arbitrary ﬁrst-order clauses, whereas only ground clauses were considered in the conference paper. Furthermore, the procedure is now parameterized by a set of constraints, denoting abducible hypotheses, and deductive completeness is directly established w.r.t. this set of constraints. Finally, detailed proofs of the correction of the redundancy detection algorithms are now provided. Note that, while the calculus and the

1. I.e., without variables.

Prime Implicate Generation in Equational Logic

theoretical results handle arbitrary ﬁrst-order clauses as input, the data-structures and algorithms for eﬃcient redundancy detection are deﬁned only for ground clauses and the experimental evaluation is performed only for such clauses.

2. Clausal First-Order Logic with Equality

This section contains deﬁnitions and notations related to ﬁrst-order logic with equality.

2.1 Equational Clausal Logic

We introduce the standard syntax and semantics of equational clausal logic used in the paper.

2.1.1 Syntax

In this section, we brieﬂy review usual deﬁnitions on equational clausal logic. The deﬁnitions are identical or very similar to those used in standard textbooks (see, e.g., Baader & Nipkow, 1998; Nieuwenhuis & Rubio, 2001). We consider ﬁrst-order logic with equality, in which formulæ admit equality (denoted by ) as a unique predicate2. For n 0, Σn denotes a signature of function symbols of arity

n, and we let Σ def = S

n=0 Σn. The elements of Σ0 are constant symbols. Function symbols

of arity strictly greater than 0 are usually denoted by f or g and constant symbols by a, b, c or d. Let V be a set of variables, usually denoted by x, y or z, disjoint from Σ. The notation TV(Σ) stands for the set of terms over Σ, deﬁned inductively as follows:

V Σ0 TV(Σ);

if t1, . . . , tn TV(Σ), f Σn and n > 0 then f(t1, . . . , tn) TV(Σ).

Terms are usually denoted by s, t, u, v, w. A position is a (possibly empty) ﬁnite sequence of natural numbers. The empty position is denoted by ε and the concatenation of two positions p and q is denoted by p.q. For any term t TV(Σ), Pos(t) is the set of all positions in t, inductively deﬁned as follows: ε Pos(t), and if p Pos(ti) then i.p Pos(f(t1, . . . , tn)). The subterm occurring at position p in a term t is denoted by t|p. It is deﬁned inductively by: t|ε def = t and f(t1, . . . , tn)|i.p def = ti|p. We denote by t[s]p the term obtained from t by replacing the term occurring at position p by s, inductively deﬁned as follows: t[s]ε def = s and f(t1, . . . , tn)[s]i.p def = f(t1, . . . , ti 1, ti[s]p, ti+1, . . . , tn).

Example 2.1 Let Σ0 = {a, b}, Σ1 = {f}, Σ2 = {g}. The set of terms includes a, b, f(a), f(f(b)), g(f(a), f(b)), etc. The set of positions in g(f(a), f(b)) is {ε, 1, 2, 1.1, 2.1}. The term at position 1.1 in g(f(a), f(b) is a.

An atom is an expression of the form s t, where s, t TV(Σ). Atoms are considered modulo commutativity of , i.e. s t and t s are viewed as identical. A literal, usually denoted by l or m, is either an atom s t (a positive literal, or a literal of positive polarity)

2. As usual non-equational predicates p(t1, . . . , tn) are encoded as equations p(t1, . . . , tn) .

Echenim, Peltier & Tourret

or the negation of an atom s t (a negative literal, or a literal of negative polarity). A literal l will sometimes be written s t, where the symbol stands for or . The literal lc denotes the complement of l, i.e., lc is s t (resp. s t) when l is s t (resp. s t). A clause is a ﬁnite multiset of literals, usually written as a disjunction. The symbol 2 denotes the empty clause. For every clause C, we deﬁne C+ def = {l C | l is positive} and C def = {l C | l is negative}. A clause C is positive when C = C+, and it is negative when C = C . We denote by C\D the multiset diﬀerence of C and D, deﬁned as usual, and we may write C\l instead of C\ {l}. We denote by |C| the length of clause C, i.e. the number of literals it contains. A clause is unit if |C| = 1. If C = Wn i=1 li then C def = Vn i=1 lc i. We often identify sets of unit clauses with conjunctions; for example, given a set of clauses S, we may write S Vn i=1 li instead of S {li | i [1, n]}, and instead of {l1, . . . , ln} {l 1, . . . , l m}, we may write Vn i=1 li Vm i=1 l i. An expression (term, atom, literal or clause) E is ground if it contains no variable. The notation T(Σ) denotes the set of ground terms and V(E) denotes the set of variables occurring in E.

Example 2.2 Consider the clauses C = f(a) g(f(a), f(b)) a b and D = g(x, y) g(y, x) f(x) f(y). Observe that C is ground but D is not (a, b are constant symbols and x, y are variables). We have: C+ = f(a) g(f(a), f(b)), C = a b, D+ = D and D = 2.

A substitution is a function mapping variables to terms. The image of a variable x by a substitution σ is denoted by xσ. Substitutions can be extended to any term, atom, literal, or clause by induction: aσ def = a if a Σ0, f(t1, . . . , tn)σ def = f(t1σ, . . . , tnσ), (s t)σ def = (sσ tσ), (Wn i=1 li)σ def = Wn i=1 liσ. The domain of a substitution σ is the set of variables x such that xσ = x. A substitution σ is ground if xσ is ground for every x in the domain of σ. An expression (term, atom, literal or clause) E is an instance of an expression E if there exists a substitution σ such that E σ = E. A substitution σ is more general than a substitution θ if there exists a substitution η such that xση = xθ, for any variable x. A substitution σ is a uniﬁer of two terms t and s if tσ = sσ, in which case t and s are uniﬁable. It is well-known (see for instance Jouannaud & Kirchner, 1991) that any uniﬁable pair of terms possesses a (unique up to a renaming of variables) most general uniﬁer, denoted by mgu(t, s).

Example 2.3 Let t = f(g(x), g(b)) and s = f(g(a), g(y)). The substitution σ : {x 7 a, y 7 b} is the (unique) uniﬁer of t and s.

We consider a ground-total strict reduction order (see, e.g., Baader & Nipkow, 1998) on terms. Such an order satisﬁes the following properties: is total on ground terms, i.e., if t and s are distinct terms in T(Σ) then either t s or s t; is well-founded, i.e., there is no inﬁnite decreasing sequence t1 t2 tn . . . ; is closed under substitution, i.e., if t s then tσ sσ; and is closed under contextual embedding, i.e., if t s then u[t]p u[s]p, for any term u. The order is extended to literals and clauses using the Dershowitz-Manna multiset extension (Dershowitz & Manna, 1979). To this purpose, a negative literal t s is associated with the multiset {{t, s}} and a positive literal t s with {{t} , {s}}. Examples of reduction orders include Knuth-Bendix orderings or path orderings (see, e.g., Dershowitz, 1979).

Prime Implicate Generation in Equational Logic

Example 2.4 Let C = f(a) a a b and D = g(f(a), f(b)) a. Since is well-founded and closed under contextual embedding we necessarily have g(f(a), f(b)) f(a) a and g(f(a), f(b)) b; thus D C.

We now recall some basic notions about rewrite systems (Baader & Nipkow, 1998). A ground rewrite rule is a pair written t s, where t and s are ground terms. A ground rewrite system is a set of ground rewrite rules. If R is a ground rewrite system, and u and v are ground terms, we write u R v if there exists a position p such that u|p = t, v = u[s]p, and t s R. The relation R denotes the reﬂexive and transitive closure of R. A term s is a normal form of t if t R s and there is no term s such that s R s . A rewrite system is orthogonal if there are no rules t s and t s and no position p such that t|p = t . It is terminating if R is well-founded, and convergent if every term t admits a unique normal form. A proof of the following result has been presented by Baader and Nipkow (1998).

Proposition 2.5 Every orthogonal and terminating rewrite system is convergent.

2.1.2 Semantics

An interpretation is a congruence relation on T(Σ). The notation s =I t is used as a shorthand for (s, t) I. An interpretation I validates:

a ground literal t s if is and s =I t, or is and s =I t;

a ground clause C if I validates at least one literal in C;

a non-ground clause C if I validates all ground instances of C;

a clause set S if I validates all clauses in S.

We write I |= E and say that I is a model of E if the expression (literal, clause or clause set) E is validated by I. For all expressions E, E , we write E |= E if every model of E is a model of E . A tautology is a clause of which all interpretations are models and a contradiction is a clause that has no model.

2.2 Prime Implicates

We introduce the central notion of a prime implicate, adapted from the corresponding notion in propositional logic (see, e.g., Ngair, 1993).

Deﬁnition 2.6 A ground clause C is an implicate of a set of clauses S if S |= C; it is a prime implicate of S if, moreover, C is not a tautology, and for every clause D such that S |= D, we have either D |= C or C |= D.

Intuitively, the implicates of S are the clausal consequences of S. They are prime if they are minimal w.r.t. logical entailment and not valid. From a practical point of view, it is clear that implicates that are either valid or not minimal are redundant, hence we are interested only in computing prime implicates.

Echenim, Peltier & Tourret

Example 2.7 Consider the clause set S:

1 a b d a 2 a c 3 f(c) f(b) 4 c e d e

The clause d a is an implicate of S, since Clauses 2 and 3 together entail f(a) f(b), which in turn entails a b, which together with Clause 1 entail d a. The clause a e d e can be deduced from Clauses 4 and 2 and thus is also an implicate. But it is not prime, since d a |= a e d e (it is clear that d a, a e |= d e, by transitivity), but a e d e |= d a.

The following proposition restates the deﬁnition of unsatisﬁability in terms of implicates.

Proposition 2.8 A clause set S is unsatisﬁable iﬀ2 is an implicate of S.

Proof. If S is unsatisﬁable then it has no model, thus every clause is an implicate of S. Conversely, if I |= S, and 2 is an implicate of S then I |= 2, which is impossible, since by deﬁnition 2 is false in all interpretations.

Generating all prime implicates is unfeasible in general, since there are inﬁnitely many such clauses. For instance the clause set {f(a) a, f(b) b, a b} has an inﬁnite number of prime implicates, of the form fn(a) fn(b), for every n N, and none of them are prime (since fn+1(a) fn+1(b) |= fn(a) fn(n). In practice, additional restrictions have to be added to control the form of the generated implicates (for instance to limit the length and depth of the clauses). This yields the following deﬁnition:

Deﬁnition 2.9 A ground clause C is a prime implicate of a clause set S w.r.t. a class of ground clauses C if C is an implicate of S, C is not a tautology, and for every clause D C such that S |= D, we have either D |= C or C |= D.

Due to Proposition 2.8, since the satisﬁability problem is undecidable in ﬁrst-order logic, checking whether a given ground clause is an implicate of a set of non-ground clauses S is undecidable. If S is ground, then the problem is co-NP-complete, since it can be polynomialy translated into a propositional entailment problem by ﬂattening the terms and adding all the relevant ground instances of the equality axioms. Similarly, checking whether a set of ground clauses S has an implicate deﬁned over a given set of ground terms is ΣP 2 -complete, since it can be reduced to a -QBF propositional formula (see Eiter & Gottlob, 1995, for more details about the complexity of the abduction problem in propositional logic). In particular, it follows from the results by Eiter and Gottlob (1995) that checking whether a given ground clause is a prime implicate of a set of ground clauses is DP-hard. The following proposition shows that focusing on the computation of ground implicates is actually not restrictive.

Proposition 2.10 Let S be a set of clauses, C be a clause. Let σ be a substitution mapping all variables in C to pairwise distinct constant symbols not occurring in S or C. Then S |= C holds iﬀCσ is an implicate of S.

Prime Implicate Generation in Equational Logic

Proof. The direct implication is trivial: if S |= C, then necessarily S |= Cσ (by deﬁnition of the semantics of universal quantiﬁers), thus Cσ is an implicate of S, by deﬁnition of the notion of an implicate. For the other direction, assume that S |= Cσ and S |= C. This entails that there exist an interpretation I and a ground substitution θ of domain V(C) such that I |= S and I |= Cθ. For every ground expression E (e.g., a literal, a clause. . . ), we denote by E the expression obtained from E by replacing all occurrences of the constant symbols xσ (with x V(C)) by xθ. E is well deﬁned since by hypothesis σ is injective on V(C). Let J be the relation deﬁned as follows: (t, s) J iﬀ(t , s ) I. It is easy to check that J is a congruence, and that, for every clause D, J |= D iﬀI |= D . Since C contains no constant symbol of the form xσ, we have (Cσ) = Cθ; thus J |= Cσ I |= Cθ. Therefore J |= Cσ. Since S |= Cσ, this entails that J |= S, hence that there exist a substitution η and a clause D S such that J |= Dη, i.e., such that I |= (Dη) . Since S (hence D) contains no constant symbol of the form xσ, we have (Dη) = Dη , where xη def = (xη) , for every x V(D). This entails that I |= Dη , which contradicts the fact that I |= S.

Thanks to Proposition 2.10, non-ground implicates can be computed from ground implicates, simply by replacing all constant symbols not occurring in the original clause set by fresh variables3 (see also Remark 4.16).

3. Handling Ground Clauses Modulo Equality

In this section we focus on ground clauses and provide syntactic characterizations of equivalence and logical entailment between clauses in equational logic. Various notions of redundancy are used in diﬀerent contexts. For instance complexity results about the computation of minimal representations of CNF formulæ are presented by Liberatore (2005). In the Superposition calculus (Bachmair & Ganzinger, 1994), a clause is considered to be redundant if it is entailed by smaller clauses (w.r.t. the ordering ), and it is possible to show that such clauses can safely be discarded without threatening refutational completeness. In our case, since we are interested in computing all prime implicates of a formula, an implicate is considered redundant iﬀit is not prime, i.e., if it is a logical consequence of another implicate. In propositional logic, detecting clauses that are entailed by other clauses is an easy task, because a clause C is a logical consequence of D iﬀeither C is a tautology or every literal in D also occurs in C. It is clear that this can be checked in polynomial time w.r.t. the size of C and D. Furthermore, the only tautologies are the clauses containing complementary literals, which is straightforward to test, and two non-tautological clauses are equivalent iﬀ they are identical (up to AC). In equational logic, these properties do not hold anymore: for example, a b f(a) f(b) is a tautology, and e b b c f(a) f(b) is entailed by e c a c. Moreover, a clause may admit several (sometimes exponentially many) equivalent forms, for example, Wn i=1 ai bi f(a1, . . . , an) c is equivalent to any clause of the form Wn i=1 ai bi f(d1, . . . , dn) c, where for all i = 1 . . . , n, di {ai, bi}. In this section, we devise a new criterion that generalizes subsumption to test logical entailment, as well as a way to normalize clauses up to equivalence.

3. This requires that terms containing such constants must be allowed as implicates, which of course increases the search space.

Echenim, Peltier & Tourret

3.1 Testing Logical Entailment Between Ground Equational Clauses

We associate each clause C with an equivalence relation C on terms. Intuitively, two terms t and s are in relation in C iﬀthe equation t s is a logical consequence of the negation of C. The C-representative of a term t is then the smallest (according to the ordering ) term that is equivalent to t. This notion extends to equations and clauses. Formally:

Deﬁnition 3.1 Given a ground clause C, we deﬁne the relation C on terms as follows: for all terms s, t T(Σ), s C t iﬀ C |= s t. It is clear that C is a congruence relation; for any term s T(Σ), the C-equivalence class of s is called the C-congruence class of s and denoted by [s]C. The C-representatives of a term s, literal l and clause l1 ln are respectively deﬁned by:

s C def = min ([s]C),

def = s C t C,

def = l1 C ln C.

Example 3.2 Let C = a b b c. We have C = a b b c, thus by transitivity C |= a c. Consequently, a C b C c. The terms a, b, c are in the same equivalence class. Assuming that c b a, we deduce that a C = b C = c C = c.

Example 3.3 Let C = a b f(c) d f(b) f(c). Since C |= a b, we also have C |= f(a) f(b). Moreover C |= f(c) d. Given the order d c b a f(c) f(b) f(a), we have a C = b C = b, f(a) C = f(b) C = f(b) and f(c) C = d C = d. Thus (f(b) f(c)) C = f(b) d.

The following propositions are straightforward consequences of the previous deﬁnition.

Proposition 3.4 We have (s C t) iﬀ(s t |= C) iﬀ( C |= s t).

Proof. By deﬁnition of C, s C t holds iﬀ C |= s t. By contrapositive this is equivalent to s t |= C.

Proposition 3.5 Let s be a term, l be a literal and C and D be two clauses, then:

C |= s s C, C |= l l C, and C |= D D C.

Proof. By deﬁnition of the notion of a C-representative, we have s C [s]C, hence s C s C. By deﬁnition of C, this means that C |= s s C. The literal l is of the form s t with { , }, and by deﬁnition l C = (s C t C). By the previous relation, we have C |= s s C and C |= t t C, thus, C |= (s t) (s C t C), i.e., C |= l l C. The clause D is of the form l1 ln, where l1, . . . , ln are literals. By deﬁnition, D C = Wn i=1 li C. By the previous relation, C |= li li C for all i, and C |= D D C.

Prime Implicate Generation in Equational Logic

The next proposition states that it is possible to check that a positive ground clause C is a logical consequence of a set of unit clauses S by testing every equation in C independently. This property does not hold if the clause is not positive, for instance the empty clause set entails the tautology (a b a b) but entails neither a b nor a b.

Proposition 3.6 Let S = {ui vi | i {1 . . . k}} be a set of unit positive clauses. If S |= Wn i=1(ti si) where t1, . . . , tn, s1, . . . , sn are ground terms, then there exists j {1 . . . n} such that S |= tj sj.

Proof. Assume that S |= Wn i=1(ti si). Let I be the interpretation such that t =I s iﬀ t =I s holds for every model I of S. Note that I is a congruence, as it is an intersection of congruences. By deﬁnition we have I |= ui vi for every i {1 . . . n}, thus I |= S |= Wn i=1(ti si), and there exists j {1 . . . n} such that I |= tj sj. This entails that I |= tj sj for every model I of S, thus S |= tj sj.

The next lemma shows that, unless C is a tautology, the relation C depends only on the negative literals in C (if C is a tautology then C is unsatisﬁable hence t C s holds for all terms t and s).

Lemma 3.7 Let C and D be two non-tautological ground clauses. The following properties hold:

1. If C = D then C and D are identical; hence E C = E D holds for every expression E. In particular, C and C are identical.

2. If C = 2 then C is the identity relation, thus E C = E for every expression E.

3. The inclusion D C holds iﬀevery negative literal in D C is a contradiction.

Proof. We prove that if C is not a tautology then C and C are identical. Note that C |= C thus C C, we now show that C C . Let t and s be two terms such that t C s. Then C |= t s, thus C C+ |= t s, i.e., C |= C+ t s. By Proposition 3.6 we have either C |= C+ or C |= t s. In the former case C is a tautology which contradicts our hypothesis. We deduce that C |= t s and t C s. Item 1 follows immediately from the previous property. If C = 2 then C= 2 and by deﬁnition 2 is the identity relation. If D C then for every negative literal t s D, we have t D s hence t C s and t C = s C. Conversely, assume that for every negative literal t s D, we have t C = s C. Then C |= t s holds for all t s D, thus C |= D , and D C.

We now deﬁne an adapted notion of subsumption for equational clauses.

Deﬁnition 3.8 Let C, D be two non-tautological ground clauses. The clause D e-subsumes C, written D e C, iﬀthe two following conditions hold:

2. for every positive literal l D, there exists a positive literal m C such that m C lc is a tautology.

Echenim, Peltier & Tourret

If S, S are sets of clauses, we write S e C if there is a clause D S such that D e C, and we write S e S if C S , S e C.

Intuitively, testing whether D |= C is performed by verifying that C |= D. To this purpose, we ﬁrst check that all equations in D are entailed by C, which can be done by verifying that D C holds. Then, we consider the negative literals t s in D. We should have C |= t s, i.e., C t s |= C+, which is equivalent by Proposition 3.6 to C t s |= m for some m C+; and this is the case iﬀm C lc where l = t s is a tautology. We provide an example illustrating both conditions.

Example 3.9 Let C = a b b c f(c) f(d), D = a c c d, and assume d c b a. By deﬁnition, we have a C b C c, hence D C. Consider the literal l = c d in D and let m = f(c) f(d). We have C lc = a b b c c d, hence a, b, c, d are all equivalent w.r.t. C lc. Thus m C lc = f(d) f(d) is a tautology, and D e-subsumes C.

Theorem 3.10 Let C and D be two non-tautological ground clauses. We have D |= C iﬀ D e C.

Proof. First assume that D |= C. Consider a negative literal l = s t in D. We have C |= D |= lc, thus t C = s C by Proposition 3.4, and l C is a contradiction. By Lemma 3.7 (3), we deduce that D C. Now consider a positive literal l D. By hypothesis C |= lc, thus C C+ |= lc and C l |= C+. By Proposition 3.6 we deduce that there exists m C+ such that C l |= m, i.e., by Deﬁnition 3.1, m C lc is a tautology. For the converse implication, we prove that every literal in D entails C. If s t D, then since s D t, we deduce that s C t and by Proposition 3.4, s t |= C. If s t D, then by hypothesis there is a literal u v C such that u C s t = v C s t. It follows that (C s t) |= u v, hence s t |= (C u v) |= C.

Example 3.11 Given the order a b c e f(a) f(b) on terms, let C = e b b c f(a) f(b), D = e c a c, and let l = e c and m = a c be the literals of D. We have l C = b b because [b]C = {b, c, e} and min ([b]C) = b. Moreover the literal f(a) f(b) C is such that (f(a) f(b)) C mc = f(a) f(a), which, by Theorem 3.10, proves that D |= C.

3.2 A Normal Form for Ground Equational Clauses

The following deﬁnition introduces the notion of a normalized clause, which in particular permits to eﬃciently test whether a clause is tautological and whether two clauses are equivalent. The intuition underlying this deﬁnition is that the relation C can be deﬁned in a canonical way by stating that each term t is mapped to its normal form t C, which is expressed by the negative literal t t C when t = t C. Afterwards, each positive literal can be replaced by its normal form, and the literals that are redundant w.r.t. substitutivity can be removed. For example, the literal a b is redundant in f(a) f(b) a b because f(a) f(b) a b f(a) f(b).

Deﬁnition 3.12 A ground clause C is normalized if:

Prime Implicate Generation in Equational Logic

1. every literal l in C is such that l C\l = l;

2. there are no two distinct positive literals l, m in C such that m lc C is a tautology;

3. C contains no literal of the form t t.

Example 3.13 Using the ordering a b c e f(a) f(b) on terms, the clause C = c b e b f(b) f(a) is normalized.

Proposition 3.14 If C is a normalized clause, then each literal in C occur exactly once in C.

Proof. This follows immediately from Item 1 of Deﬁnition 3.12 for negative literals and Item 2 for positive literals.

Proposition 3.15 A normalized clause C is a tautology iﬀC contains a tautological literal.

Proof. If C is a tautology, then C |= C+, hence by Proposition 3.6 there exists a literal l of the form s t in C+ such that C |= l. By Proposition 3.4 we have s C = t C, and since C is normalized, we deduce that l C = l C\l = l, and that the latter is a tautological literal.

The proof that non-tautological normalized clauses that are equivalent are identical relies on a ground rewriting system that is associated with normalizing clauses.

Deﬁnition 3.16 Let C be a normalized clause. The rewriting system RC associated with C is deﬁned by:

RC def = {t s | t s C s t} .

The rules in RC are ordered according to the lexicographic extension of .

By construction, since C is normalized, RC is orthogonal. Furthermore, if t RC s then t s, which entails that RC is terminating, hence convergent by Proposition 2.5. We denote by t RC the RC-normal form of t; note that t RC = t C.

Proposition 3.17 Let C be a normalized clause and t be a term in T(Σ). The term t RC is obtained from t by using only rules of RC that have a left-hand side smaller or equal to t.

Proof. To compute t RC, rewriting rules can only be applied on t or its subterms. All the subterms of t are smaller than t by and by deﬁnition of RC, a rewriting step always replaces a term by a smaller one.

Theorem 3.18 Two non-tautological equivalent and normalized clauses are identical. Furthermore, for any non-tautological ground clause C, there exists a normalized clause equivalent to C, and this clause is the smallest ground clause equivalent to C.

Echenim, Peltier & Tourret

Proof. Consider two non-tautological, equivalent and normalized clauses C1 and C2. Since C1 and C2 are equivalent, C1 and C2 are identical. We ﬁrst show that C1 = C2 . We denote by R1 and R2 the rewriting systems associated with C1 and C2 respectively. If C1 = C2 , then R1 = R2. We consider the smallest rule t s that does not appear in both rewriting systems; w.l.o.g. we assume that t s R1 and t s R2, hence that t s C1. Since C1 and C2 are equivalent and t R1 = s, we also have t R2 = s. By Proposition 3.17, the left-hand sides of the rules used to rewrite t are smaller or equal to t, and since t is eventually rewritten into s in R2, there must be at least one rule u v in R2 that can be applied to t; t is thus of the form t[u]. If u is a strict subterm of t, then u v is smaller than t s and by hypothesis, u v occurs in R1, so that u v C1. But in this case, (t s) C1\t s and t s are distinct, which contradicts Point 1 of Deﬁnition 3.12. Otherwise, we must have u = t and t v s. But then t R2 = v = s, a contradiction. We now show that C1+ = C2+. By Theorem 3.10 we have C1 e C2 and C2 e C1. Let l1 be a positive literal in C1. Since C1 e C2, there exists a literal l2 in C2 such that l2 l1c C2 is a tautology, i.e., l1 C2 |= l2; hence l1 |= C2 l2. Similarly, since C2 e C1 and l2 C2, there is a positive literal m1 in C1 such that m1 l2c C1 is a tautology, so that l2 |= C1 m1. We deduce that

l1 |= C2 l2 |= C2 C1 m1 C1 m1,

and therefore, C1 l1 |= m1 and m1 C1 l1c is a tautology. By Point 2 of Deﬁnition 3.12, we must have m1 = l1. From l1 |= C2 l2 and l2 |= C1 l1, we deduce that l1 C1 |= l2 C1 and l2 C2 |= l1 C2, i.e., l1 C1 l2 C2 (because C1 = C2 ) and so either l1 C1 and l2 C2 are both tautological or l1 C1 = l2 C2. But C1 and C2 are non-tautological, thus necessarily l1 = l2. We conclude that C1+ = C2+. Now, consider a non-tautological ground clause C that is not normalized. We show that there exists a ground clause equivalent to C and strictly smaller than C (then the proof follows by an immediate induction).

If C contains two positive literals l and m such that mlc C is a tautology, then removing the literal l yields a smaller equivalent clause.

If C contains a literal l such that l C\l = l then replacing this literal with l C\l yields a smaller equivalent clause.

Removing literals of the form t t yields a smaller equivalent clause.

Deﬁnition 3.19 For every non tautological ground clause, we denote by C the (unique) normalized clause equivalent to C.

Example 3.20 The clause C = c b e b f(b) f(a) is normalized and equivalent to the clauses c b e b f(c) f(a), c b e b f(e) f(a), c e e b f(b) f(a), etc.

Prime Implicate Generation in Equational Logic

4. An Abductive Superposition Calculus

We now present the calculus for generating implicates, named c SP. This calculus is based on the Superposition Calculus SP (see Bachmair & Ganzinger, 1994), which is the most eﬃcient proof procedure for ﬁrst-order logic with equality (see for instance Nieuwenhuis & Rubio, 2001, or http://www.cs.miami.edu/~tptp/CASC/) and forms the basis of the most powerful theorem provers currently available (Mc Cune, 2010; Schulz, 2013; Voronkov, 1995; Weidenbach, Afshordel, Brahm, Cohrs, Engel, Keen, Theobalt, & Topic, 2001). The calculus can be seen as a reﬁnement of the well-known Resolution calculus (Robinson, 1965), tuned to handle equations eﬃciently. The key inference rule is the Superposition rule, which replaces equals by equals, and for eﬃciency, equations are oriented in such a way that a term may be replaced only by smaller terms. The principle underlying c SP is to apply the inference rules of SP to the set of clauses under consideration along with ground unit clauses that are added during proof search and that act as hypotheses. The hypotheses that permit the generation of the empty clause are extracted: they represent the negation of an implicate. In order to keep track of the hypotheses that were used to derive the empty clause, they are attached to standard clauses as constraints. Thus, c SP is an adaptation of SP to so-called constrained clauses, along with inference rules that permit to generate additional hypotheses. Before introducing the formal deﬁnition of c SP, we provide an example that should give an intuitive understanding of this calculus.

Example 4.1 Consider the clause set: S = {f(a) c, f(b) d, c d}. It easy to check that a b is an implicate of S. Indeed, by contradiction, for every interpretation I such that I |= S and I |= a b, we have f(a) =I f(b), thus by the ﬁrst two clauses we deduce that c =I d, which contradicts the third clause. Consequently, S |= a b. We now show how this clause can be derived from S using the principles underlying c SP, assuming d c b a. We ﬁrst remark that, since b a, a can be rewritten to b in the clause f(a) c, provided the equation a b is added as a new hypothesis. This is asserted by deriving the constrained clause [f(b) c | a b], which is interpreted as an implication: a b f(b) c. Afterwards, the clause [d c | a b] can be derived by replacing f(b) by d, using the second clause in S. We may use the equality d c to replace c by d in the third clause in S, yielding [d d|a b]. Note that the constraint a b is propagated from the premise to the conclusion of the rule. Finally, the contradictory literal d d can be deleted, yielding the constrained clause [2|a b]. This clause means that the empty clause is derivable from S if a b is added as an hypothesis. By soundness, this implies that S {a b} is unsatisﬁable, hence that a b is an implicate of S.

All the rules applied in the previous example are the usual inference rules of SP (adapted to constrained clauses), except the ﬁrst one which was used to assert a new hypothesis in the constraint part of the clause the corresponding rule is called Assertion. In this case, the asserted hypothesis was positive: an equation a b was added as a hypothesis so that a could be rewritten into b. We provide another example, showing that the assertion rule may be applied also on negative literals.

Example 4.2 Consider the clause set: S = {a b, f(b) c}. It is clear that f(a) c is an implicate of S (it suﬃces to replace b by a in the second clause). However, assuming that

Echenim, Peltier & Tourret

c b a, this clause cannot be derived by the rules of the Superposition calculus because a is strictly greater than b. The implicate is generated as follows. By adding the hypothesis f(a) c to the clause a b, we may derive [f(b) c|f(a) c], meaning that f(b) c can be derived from f(a) c and S. Note that this time, the replacement is compatible with the ordering on terms. Afterwards, the term f(b) can be replaced by c by using the second clause in S, yielding a contradiction. We thus obtain the constrained clause [2|f(a) c], meaning that f(a) c is indeed an implicate of S.

4.1 Constrained Clauses

We begin by deﬁning the syntax and semantics of constrained clauses.

Deﬁnition 4.3 A constraint is a set of ground literals, sometimes written as a conjunction. The empty constraint is denoted by . If X = {l1, . . . , ln} then X c denotes the clause Wn i=1 lc i. We denote by X the constraint (X c ), and we say that X is normalized if X = X. A constrained clause (or c-clause) is a pair [C | X] where C is a clause and X is a constraint. The c-clause [C | ] is simply represented as C, and referred to as a standard clause.

Example 4.4 The expression [f(a) b|a b, b c] is a constrained clause. If c b a then (a b b c) = a c b c, hence {a b, b c} = {a c, b c}.

From a semantic point of view, a constrained clause [C | X] is equivalent to the standard clause X c C. More speciﬁcally, the intended meaning of a c-clause [C | X] is that the clause C can be inferred provided the literals in X are added as axioms to the considered clause set.

Remark 4.5 Note that, as stated in Deﬁnition 4.3, the constraint part of a c-clause is always ground. This is suﬃcient in our context: since implicates are universally quantiﬁed formulæ, their negation is necessarily ground (after Skolemization). See also Proposition 2.10 and the following example.

Example 4.6 Consider the clause set: S = {p(x, y), p(x, y) q(x, y)}. It is clear that the (non-ground) clause q(x, y) is an implicate of S. The negation of C is x, y q(x, y) x, y q(x, y) (since variables are implicitly universally quantiﬁed in clauses), and its Skolemized normal form is q(a, b), where a, b are new Skolem constants. The calculus c SP generates the constrained clause [2 | q(a, b)], which can be transformed afterwards into the implicate q(a, b) or, because a, b do not occur in S, x, y q(x, y).

4.2 Inference Rules

The calculus c SP is deﬁned by a set of inference rules that are represented in Figure 1. The calculus is parameterized by the ordering on terms and by a selection function sel mapping every clause C to a subset of C, where sel(C) contains either all maximal literals in C or at least one negative literal. A literal is selected in C if it occurs in sel(C). The calculus is also parameterized by a set of constraints X satisfying the following conditions:

Prime Implicate Generation in Equational Logic

1. X is not empty.

2. X is -closed, i.e., for every X X and constraint Y, if Y X then Y X.

3. Every constraint in X is normalized.

Note that Conditions 1 and 2 together imply that X. Condition 3 is not restrictive since any constraint is equivalent to a normalized constraint. Moreover, if X is normalized then any subset of X is also normalized. Intuitively, the set X allows a user to control the form of the candidate implicates. For instance the user may be interested only in positive implicates, or in implicates of small size (i.e., of a size up to some ﬁxed k N). Instead of ﬁltering the implicates a posteriori, it is more eﬃcient to block the generation of clauses with constraints that do not fulﬁll the required property. The condition on the implicates can also be of a semantic nature, for example, the user may want to obtain all implicates that entail some formula (then X is the set of constraints that are logical consequences of the negation of the considered formula). All these conditions fulﬁll the above restrictions. It is also clear that ﬁlters can be freely combined, i.e., if X1 and X2 fulﬁll Conditions 1-3 above, then so do X1 X2 and X1 X2. The c-Superposition, c-Factoring and c-Reﬂection rules are straightforward adaptations of the usual rules of SP to c-clauses: the constraints of the premises are added to the conclusion. The Positive and Negative Assertion rules are the ones that permit the addition of new hypotheses as constraints to c-clauses. The standard Superposition calculus SP can be recovered from c SP by setting X to { }, in which case the Assertion rules never apply and all constraints are . We provide examples of applications of each rule.

Example 4.7 Consider the c-clauses:

1 [f(a, x) c|a b] 2 [f(y, b) d|a b] 3 [f(y, b) d|b c] 4 [f(a, x) f(y, b) x b|a b] 5 [f(a, x) b f(y, b) b| ]

We assume that d c b a, that sel(C) is the set of maximal literals in C and that X is the entire set of normalized constraints. The c-Superposition rule applies on c-clauses 1 and 2, with uniﬁer σ = {x 7 b, y 7 a} (since we have f(a, b) a, b, c, d) and the c-clause [d c|a b] is derived. In contrast, the rule does not apply on c-clauses 1 and 3. Indeed, the constraint {a b, b c} obtained by taking the union of the constraints of 1 and 3 is not normalized hence does not occur in X. The c-Reﬂection rule applies on c-clause 4, yielding: [b b | a b]. Afterwards the rule may be applied again on the literal b b, yielding [2 | a b]. Note that the rule does not apply on the literal x b of the initial clause 4 because it is not maximal (since f(a, x) x, b). The c-Factorization rule applies on c-clause 5, yielding: [f(a, b) b b b| ]. The Positive Assertion rule applies on c-clause 1. Taking u = f(a, x), t = t = a and s = b, we get [f(b, x) c|a b]. Note that we cannot apply the rule with a term s distinct

Echenim, Peltier & Tourret

from b because the obtained constraint {a b, a s} would not be normalized. For the same reason the rule cannot be applied on the term f(a, x). It cannot be applied on x because this term is a variable, or on c because the term is not maximal. The Positive Assertion rule applies in several ways on c-clause 5, for instance, taking u = f(a, x), t = t = a and t = c, we get: [f(c, x) b f(y, b) b|a c]. The Negative Assertion rule also applies on c-clause 5. For instance, taking u = g(f(a, b)), v = d, t = f(a, x), t = f(a, b), and s = b, we obtain [g(b) d f(y, b) b | g(f(a, b)) d].

Remark 4.8 The term s in the Positive Assertion and the term u in the Negative Assertion rules are arbitrary. There are inﬁnitely many terms that can be used with these inference rules. Let us consider for example the c-clause [b a | X], deﬁned over a signature containing the unary function symbol f. In this case, any term of the form fn(b) for n N can all be introduced in the Negative Assertion rule. This is why in practice it is critical to limit the amout of usable terms by imposing restictions on the set X

4.3 Redundancy Criterion

An important feature of the Superposition calculus is the availability of a general criterion for detecting redundant clauses. In this context, clauses are considered to be redundant if they can be safely discarded without threatening refutational completeness. In the present section, we adapt this criterion to c SP. The deﬁnition is similar to that by Bachmair and Ganzinger (1994), except that the constraints must be taken into account. In SP, a clause is redundant if it is entailed by smaller clauses. In c SP, it is also required that the constraints of the entailing clauses are included in the constraint of the considered clause. Furthermore, the literals occurring in this constraint can also be used in the entailment test, provided they are smaller than the considered clause. Formally:

Deﬁnition 4.9 If X is a constraint and C is a clause, we denote by X| C the set of literals in X that are smaller than or equal to C. A c-clause [C | X] is redundant w.r.t. a set of c-clauses S if either X is unsatisﬁable or for every ground substitution σ of the variables in C, there exist c-clauses [Di | Yi] S (1 i n) and ground substitutions θi (1 i n) such that:

i {1 . . . n}, Cσ Diθi and Yi X,

X| Cσ, D1θ1, . . . , Dnθn |= Cσ.

Example 4.10 Assume that d c b a. The c-clause [f(a, b) c a b a c | c d a b] is redundant w.r.t. S = {[a b b c | c d]}. Indeed, it is clear that we have a b b c |= f(a, b) c a b a c, a b b c f(a, b) c a b a c, and {c d} {c d, a b}. However, the c-clause [a c b c|c d] is not redundant w.r.t. S, although a b b c |= a c b c, because a b b c a c b c. Similarly, [a b b c| ] is not redundant w.r.t. S, because {c d} . The c-clause [a b | a c b c] is redundant w.r.t. {[a d | a c], [b d | b c]}, because a d, b d |= a b; a d, b d a b and {a c} {b c} {a c, b c}. The c-clause [f(a) f(b)|a b] is redundant w.r.t. the empty c-clause [2| ], because a b| f(a) f(b) = (a b) |= (f(a) f(b)).

Prime Implicate Generation in Equational Logic

c-Superposition [t s C |X] [u[t ] v D|Y]

[u[s] v C D|X Y]σ (i), (ii), (iii),

c-Factoring [t u t v C |X]

[t u u v C |X]σ (iv), (ix)

c-Reﬂection [t t C |X]

[C |X]σ (v), (ix)

Positive Assertion [u[t] v C |X]

[u[s] v C |X t s]σ (vi), (vii)

Negative Assertion [t s C |X]

[u[s] v C |X u[t ] v]σ (ii), (viii), (x)

where the following conditions hold:

For all rules: σ = mgu(t, t );

(i): (u[t ] v)σ sel((u[t ] v D)σ) and vσ u[t ]σ;

(ii): (t s)σ sel((t s C)σ) and sσ tσ;

(iii): X Y X;

(iv): (t u)σ sel((C t u t v)σ);

(v): (t t )σ sel((t t C)σ);

(vi): s t , vσ u[t]σ and (u[t] v)σ sel((u[t] v C)σ);

(vii): X t s X;

(viii): v u[t ];

(x): X u[t ] v X.

Figure 1: Inference Rules for c SP.

Remark 4.11 Note that constraints are compared using set inclusion and not logical entailment. For instance the c-clause [a b|f(c) f(d)] is not redundant w.r.t. the set {[a b| c d]}, although c d |= f(c) f(d). Using logical entailment instead of set inclusion would make the redundancy criterion more general (in the sense that more c-clauses would be detected as redundant), unfortunately it would also make the calculus incomplete. More precisely, this relaxed notion of redundancy is not compatible with the assumption that the constraints in X are normalized. Experiments show that this assumption makes the calculus more eﬃcient, even with a more restrictive version of the redundancy elimination rule.

Echenim, Peltier & Tourret

Proposition 4.12 Let C be a ground clause. If C is redundant w.r.t. S, then C is redundant w.r.t. S.

Proof. This follows immediately from the fact that C C and C |= C.

4.4 Soundness and Completeness of c SP

In this section, we establish the soundness and completeness of c SP. More precisely, we prove that a clause C is a prime implicate of S iﬀthe c-clause [2| C] can be derived from S using the rules in c SP. The redundancy criterion of Section 4.3 is taken into account. We thus introduce the notion of a saturated set, and we show that saturated sets obtained from S necessarily contain all prime implicates of S.

Deﬁnition 4.13 A set of c-clauses S is c SP-saturated if every c-clause deducible by the rules of c SP (in one step) is redundant w.r.t. S. A c SP-saturation of a set of c-clauses S is a set of c-clauses S such that: (i) every c-clause in S is redundant w.r.t. S , (ii) every c-clause in S is obtained from those in S by a ﬁnite number of applications of the rules in c SP, (iii) S is c SP-saturated.

Lemma 4.14 Let [C |X] be a c-clause derived (in one step) from premises [Di |Yi], where i {1 . . . n}. Then Yi X for all i {1 . . . n}, X X and {D1, . . . , Dn, X} |= C.

Proof. It is easy to verify that this property holds for each inference rule (using the fact that, by the application conditions (iii), (vii), (ix), (x), in Figure 1, an inference is allowed only if the constraint of the conclusion is in X).

Lemma 4.14 permits to deduce the following soundness result:

Lemma 4.15 Let S be a set of standard clauses and let S be a c SP-saturation of S. For every c-clause [C |X] S , we have S X |= C and X X. In particular, if C = 2, then S |= X, i.e., X is an implicate of S.

Proof. The proof is a straightforward induction on the length of the derivation.

Remark 4.16 Recall that if C is an implicate of S, then, as shown in Proposition 2.10, the non-ground clause D obtained from C by replacing each constant not occurring in S by a new variable is also an implicate of S. This remark means that it is possible to use c SP to compute non-ground implicates: it is suﬃcient for X to contain the Skolemized form of the corresponding candidates (i.e., X should contain constraints with constants not occurring in S).

We now prove that c SP is deductive-complete, i.e., that it permits to generate every prime implicate of a given set of clauses. The proof relies on the following deﬁnition and proposition.

Deﬁnition 4.17 For every set of c-clauses S and for every constraint X, we denote by S|X the set of standard clauses D such that [D|Y] S and Y X.

Prime Implicate Generation in Equational Logic

Proposition 4.18 Let S be a set of c-clauses and X be a satisﬁable constraint. If a c-clause [C |Y] is redundant w.r.t. S and Y X, then C is redundant w.r.t. S|X X.

Proof. By deﬁnition of c-clause redundancy (Deﬁnition 4.9), there are two cases to consider.

If Y is unsatisﬁable, then since Y is a conjunction of literals and Y X, the constraint X is also unsatisﬁable which contradicts the hypothesis of the lemma.

Otherwise, for every ground substitution σ, there exist c-clauses [Di | Yi] S (1 i n) and ground substitutions θi (1 i n) such that i {1 . . . n}, Diθi Cσ, Y1, . . . , Yn Y, and Y| Cσ, D1θ1, . . . , Dnθn |= Cσ. Since Y X, we deduce that i {1 . . . n} , Yi X, hence Di S|X . Thus, Y| Cσ, D1θ1, . . . , Dnθn |= Cσ, Y| Cσ, D1θ1, . . . , Dnθn Cσ and Y| Cσ {D1, . . . , Dn} S|X X; we conclude that C is redundant w.r.t. S|X X.

Theorem 4.19 Let X be a satisﬁable constraint in X and let S be a set of standard clauses such that S |= X c. If S is a c SP-saturation of S, then there exists a constraint Y X such that [2|Y] S .

Proof. Let S = S |X X. We remark that S is unsatisﬁable: indeed, S | |= S since all the standard clauses in S must be redundant w.r.t. S | ; furthermore, S | S |X , so that S |= S | X |= S X |= {X c} X. We now prove that S is saturated w.r.t. SP (assuming that the ordering is the same for both calculi and that if l is selected in [C |X] for c SP, then l is selected in C for SP). We only consider the case where the Superposition rule is applied, the proof for the other inference rules is similar. Let C1 = t r P1 and C2 = u v P2 be two clauses occurring in S , where t = u|p, σ = mgu(t, t ), rσ tσ, vσ uσ and (t r)σ and (u v)σ are selected in C1σ and C2σ respectively. Let D def = (u[r] v P1 P2)σ be the clause generated by a Superposition inference from C1 and C2. We distinguish several cases.

If both C1 and C2 occur in S |X , then S contains a c-clause of the form [t r P1 | X1] and another of the form [u v P2 | X2], where X1, X2 X. It is clear that the c-Superposition rule applies on these c-clauses, yielding [(u[r] v P1 P2)σ | X1 X2]. Since S is a c SP-saturation of S by hypothesis, this c-clause is redundant w.r.t. S , and we deduce by Proposition 4.18 that D is redundant w.r.t. S .

If C1 occurs in S |X and C2 occurs in X, then C2 = u v and S contains a c-clause of the form [C1 | X1] where X1 X. Then the Negative Assertion rule generates [(u[r] v P1) | X1 u v]σ, and since S is a c SP-saturation of S, this clause is redundant w.r.t. S . Since X1 u v X, by Proposition 4.18, we deduce that (u[r] v P1)σ is redundant w.r.t. S .

If C1 occurs in X and C2 occurs in S |X , then the proof is similar to the previous case, this time using the Positive Assertion rule.

If both C1 and C2 occur in X, then X cannot be a normalized constraint, since by Deﬁnition 3.1, (u v)c X c\(u v)c (u[r] v)c (u v)c, which contradicts Point 1 of Deﬁnition 3.12.

Echenim, Peltier & Tourret

Since S is unsatisﬁable and saturated, this set necessarily contains 2 by refutational completeness of SP, which entails that 2 S |X , hence the result.

The following theorem states the soundness and deductive completeness of c SP, w.r.t. the set of implicates with a Skolemized negated form in X.

Theorem 4.20 Let S be a set of standard clauses and S be a c SP-saturation of S. For every X X, X c is an implicate of S iﬀS contains a c-clause of the form [2 | X ] with X X.

Proof. If X c is an implicate of S then S |= X c and Theorem 4.19 gives the required result. Conversely, if S contains a c-clause [2 | X ] where X X then the result is obtained by using Lemma 4.15.

Remark 4.21 Note that the fact that every constraint in X is assumed to be normalized strongly restricts the search space. For instance, when a b c d e, no rule will apply on [a b | c d] and [a b | c e] because the obtained constraint c d c e is not normalized.

Example 4.22 The following example shows how to derive the implicate D = a d f(c) f(b) from {c d, f(a) f(b)}, given the term ordering d c b a f(d) f(c) f(b) f(a).

1 [f(a) f(b)| ] (hyp) 2 [f(d) f(b)|a d] (Pos. AR, 1) 3 [f(d) f(c)|a d f(c) f(b)] (Neg. AR, 2) 4 [c d| ] (hyp) 5 [f(d) f(d)|a d f(c) f(b)] (Sup. 3, 4) 6 [2|a d f(c) f(b)] (Ref. 5)

The negation of the constraint of the last c-clause a d f(c) f(b) is the implicate D.

5. Practical Algorithms for Redundancy Detection

In Section 4.3, an abstract criterion was introduced to characterize c-clauses that are redundant in c SP, i.e., that are useless for deriving implicates. While such a criterion is useful from a theoretical point of view, it does not provide any eﬃcient way for storing the derived sets of c-clauses and for detecting redundant c-clauses. In the present section, we focus on ground clauses and we provide data-structures and algorithms for performing these tasks. It is important to notice that these algorithms may be used for diﬀerent purposes, associated with slightly diﬀerent (albeit strongly related) notions of redundancy.

First, they can be used to store the generated implicates. Here, the stored objects are clauses (without constraints) and redundant clauses are exactly those clauses that are not prime or not normalized. A clause C is stored when the c-clause with empty clausal part [2| C] is derived.

Prime Implicate Generation in Equational Logic

Second, they can be used to store constrained clauses generated during proof search. A c-clause is then considered redundant if it satisﬁes the conditions of Deﬁnition 5.2 below. In particular, both the clause part and constraint must be stored and the ordering restrictions must be taken into account.

In the remainder of the section, all the considered terms, clauses etc. are ground, unless speciﬁed otherwise.

Remark 5.1 The well-known Herbrand theorem states that a set of ﬁrst-order clauses S is unsatisﬁable if and only if there exists a ﬁnite set Sg of ground instances of clauses in S that is unsatisﬁable. There exist many algorithms to compute such a set Sg eﬃciently, eﬀectively reducing ﬁrst-order satisﬁability to ground satisﬁability4. These algorithms range from heuristic approaches (De Moura & Bjorner, 2007), used by SMT solvers with great practical success, to refutationally complete procedures (see, e.g., Ganzinger & Korovin, 2003; Ge & Moura, 2009), possibly for speciﬁc theories (Echenim & Peltier, 2012). Since Sg is a logical consequence of S, every implicate of Sg is also an implicate of S, and these procedures can be used also to generate implicates, at the cost of losing deductive-completeness (generating complete sets of implicates is infeasible in ﬁrst-order logic anyway, as explained in Section 2).

5.1 Constrained Clausal Trees

Instead of using the general notion of redundancy of Deﬁnition 4.9, which is hard to test eﬃciently in practice, we employ a one-to-one redundancy criterion which can be seen as a generalization of subsumption:

Deﬁnition 5.2 A c-clause [C |X] c-subsumes a c-clause [D|Y], written [C |X] c [D|Y], if C e D, C D and X Y.5

Proposition 5.3 If [C |X] c [D|Y] then [D|Y] is redundant with respect to {[C |X]}.

Proof. Since C e D, by Theorem 3.10 we have C |= D; hence the result.

Note that, again, both parts of the c-clauses are handled in diﬀerent ways: the inclusion relation used to compare constraints is clearly stronger than the e-subsumption relation e used for clauses, even enriched with an ordering constraint. For instance, assuming that d c b a, we have [d c c a | ] c [d b c b b a | ], but [2 | d c c a] c [2 | d b c b b a]. As explained in Remark 4.11, comparing constraints using logical entailment would make the calculus incomplete. Since all considered clauses are ground, they can systematically be replaced by the equivalent, normalized clauses; i.e., each c-clause [C |X] can be replaced by [C |X]. This is justiﬁed by the fact that C is equivalent to and smaller than C, thus [C |X] c-subsumes [C | X]. We therefore assume that all the considered c-clauses are normalized and devise data-structures and algorithms for storing and retrieving them eﬃciently.

Deﬁnition 5.4 We deﬁne a total ordering <π on literals as follows:

4. Due to usual theoretical limitations, the generated set of clauses is inﬁnite in general. 5. See Deﬁnition 4.9 for the abstract redundancy criterion and Deﬁnition 3.8 for the deﬁnition of e.

Echenim, Peltier & Tourret

positive literals are all greater than negative ones;

if l1 and l2 are literals with the same polarity then l1 <π l2 iﬀl1 l2.

Sets of constraints are stored in a trie data structure (Fredkin, 1960), formally deﬁned as follows.

Deﬁnition 5.5 A constraint tree is inductively deﬁned as follows:

is a constraint tree.

A given set of pairs {(li, Ti) | i {1 . . . n}}, such that l1, . . . , ln are pairwise distinct ground literals and T1, . . . , Tn are constraint trees, is a constraint tree if, for every i = 1, . . . , n, each time Ti contains a pair (l , T ), we have li <π l .

The set of constraints represented by a constraint tree T is denoted by C(T) and deﬁned inductively as follows:

C(T) def = { } if T = , {l D | (l, T ) T D C(T )} otherwise.

Remark 5.6 Employing the ordering <π to constrain the order in which literals occur along the branches of the trees has two uses:

it limits the number of repetitions of the same literal,

it simpliﬁes the application of the redundancy elimination algorithms presented in Section 5.2.

The ﬁrst point can be enforced by using any total ordering on literals, but to ensure the second point, the use of <π is a necessity.

Note that by deﬁnition C( ) = . As implied by the deﬁnition, leaves of constraint trees can be either or , but in practice if a leaf is then the corresponding branch is irrelevant, because by deﬁnition two constraint trees that only diﬀer by branches with leaves that are represent the same sets of constraints. In other words, a pair (l, ) can be deleted from the tree T without aﬀecting C(T). The only exception is the empty tree, for which the root is labeled with . The storage of constrained clauses is also based on a trie data-structure. It is similar to that of constraints, except that at each leaf of the tree storing the clauses, a constraint tree is appended to store the corresponding constraints.

Deﬁnition 5.7 A constrained clausal tree or c-tree is inductively deﬁned as follows:

If T is a constraint tree then the set {( , T)} is a c-tree.

If l is a literal and T is a c-tree then the set {(l, T)} is a c-tree when for all (l , T ) T, l <π l .

If T1, T2 are c-trees such that every time (l, T 1) T1 (resp. ( , T 1) T1) and (l, T 2) T2 (resp. ( , T 2) T2) we have T 1 = T 2, then T1 T2 is a c-tree.

Prime Implicate Generation in Equational Logic

The set of c-clauses represented by a c-tree T is denoted by Cc(T) and deﬁned inductively as follows:

if T = [2|X] | X C(T ) if T = ( , T ) [l C |X] | [C |X] Cc(T ) if T = (l, T )

Cc(T1) Cc(T2) if T = T1 T2, T1 = and T2 = .

A c-tree T is normalized if all the c-clauses in C(T) are normalized and non-tautological.

Example 5.8 The structure T in Figure 2 is a c-tree with the term order a b c g(c) g(e) f(c) f(d). For readability, the labels are associated with the nodes rather than with the edges leading to them. Dotted lines denote the edges of the constraint trees occurring inside the c-tree.

The clauses in Cc(T) are:

[g(b) a f(a) c| ] [g(b) a|f(d) f(c) c a] [g(b) a|f(d) f(c) g(e) c] [b a|f(a) c]

Figure 2: A Constrained Clausal Tree

Deﬁnition 5.9 Let T be a c-tree or a constraint tree.

size(T) def =

0 if T = ( , T ) or T = { }, X

(l,T ) T 1 + size(T ) otherwise.

Deﬁnition 5.10 Let T be a c-tree and let C be a clause. Assume that l <π l holds for all literals l and l occurring in C and T respectively. Then C.T is deﬁned inductively as follows: 2.T def = T and (l C).T def = {(l, (C.T))} if l = min<π(l C).

5.2 Constrained Clausal Tree Operations

There are three main operations to perform on c-trees. The ﬁrst one, called forward csubsumption, consists in checking whether a new c-clause is c-subsumed by a c-clause already stored in a c-tree. The second one, called backward c-subsumption, removes from a c-tree all c-clauses that are c-subsumed by a given c-clause. The last one is the insertion of a new c-clause into a c-tree. This last operation is straightforward and thus will not be described here.

Echenim, Peltier & Tourret

5.2.1 Forward c-Subsumption

The forward c-subsumption algorithm is called is Entailed (see Algorithm 2). The new c-clause is [C | X], the c-tree is T and the input clause N (initially empty) contains the literals occurring in the parent nodes in the recursive calls. It is also necessary to keep track of the negative literals of C in recursive calls after having used them a ﬁrst time to rewrite literals in the c-tree. They are stored in the input clause M, which is also initially empty. During the traversal of the c-tree T, each branch (l, T ) is dealt with diﬀerently depending on the relation between l and the considered c-clause C.

If it is clear that l |= M C, then the exploration of the branch continues on T . This entailment condition is tested by checking that l M is a contradiction (if l is negative) or that C M lc contains a tautological literal (if l is positive). Such branches are respectively stored into the sets T1 and T3 at Lines 4 and 16.

If the relation between l and M C is not currently determined (because l is <πgreater than the literal currently considered in C and thus may entail literals that remain to be examined), then the minimal literal of C is added to M before restarting the exploration of the branch. Such branches are grouped in T2 at Line 13.

Lastly, if it is clear that l |= C, which is the case e.g. when l is π-smaller than all the literals in C, then the exploration of the branch is halted.

Note that the -test is reduced to a simple comparison between standard clauses (since the corresponding tree branch has already been explored), hence we do not detail the corresponding algorithm. In contrast, the -test requires going through the constraint tree associated with the clausal branch that has just been explored. This test is performed by the is Included routine, which is detailed in Algorithm 1. This algorithm is a lot simpler than is Entailed but its principle is the same, a depth-ﬁrst traversal of the tree with recursive calls deleting the literals one after the other until the inclusion becomes obvious (or obviously false). In this algorithm, the branches (l, T ) T are grouped and dealt with in accordance with their relationship to m1 = min <π {m X}. If l = m1 then only the

inclusion of a branch of T in X \ {m1} is tested at Line 9. Otherwise if l <π m1 then clearly no branch of l.T is included in X, and if m1 <π l, then it is possible that one of these branches is included in X \ {m1}, which is tested at Line 13.

Example 5.11 To illustrate the functioning of these two algorithms, let us consider the c-tree T of Figure 2 and the two c-clauses [C1 | X1] = [f(b) f(a) | a d f(a) c] and [C2 | X2] = [g(b) a | c a]. To test whether there are clauses in T that subsume [C1 | X1] and/or [C2 | X2], we call is Entailed([C1 | X1], T, 2, 2) and is Entailed([C2 | X2], T, 2, 2) which return true and false respectively. The inner workings of these two calls are described in Table 1 and 2 respectively (each line represents a recursive call).

The correctness and termination of is Included are stated in the following proposition.

Proposition 5.12 Let X be a constraint and let T be a constraint tree. The call to is Included(X, T) terminates and is Included(X, T) = true iﬀthere exists a constraint Y C(T) such that Y X.

Prime Implicate Generation in Equational Logic

Call Assignments & tests Next call(s) is Entailed([C1 |X1], T, 2, 2) T1 line 17 (1) m1 f(b) f(a) T3 {(b a, Tβ)} is Entailed([C1 |X1], Tβ, 2, b a) ( , T β) Tβ Line 1 b a f(b) f(a) is Included(X1, T β) m1 a d Line 13 (2) T1 T2 T β is Included(f(a) c, T β) m1 f(a) c Line 9 T1 T β is Included( , ) returns true (3) (Line 2) Comments (1) The left child of T is not used in recursive calls since g(b) a does not entail C1 (line 16). Tβ is the subtree of T below b a. (2) Since T1 is empty, there is no recursive call line 9. T β is the only child of Tβ. (3) This value is propagated up to the initial call, that also returns true.

Table 1: Running of the Call is Entailed([C1 |X1], T, 2, 2)

Algorithm 1 is Included(X, T)

Require: T is a constraint tree, X is a constraint. Ensure: is Included(X, T) = true iﬀ Y C(T), Y X.

1: if T = then

2: return true

4: if X = then

5: return false

7: m1 min <π {m X}

8: T1 {(l, T ) T | l = m1}

(l,T ) T1 is Included(X \ {m1} , T ) then

10: return true

12: T2 {(l, T ) T | m1 <π l}

13: return W

(l,T ) T2 is Included(X \ {m1} , l.T )

Proof. The termination of is Included(X, T) is due to the fact that |X| decreases at each recursive call. To prove the equivalence property, we show each implication by induction on |X|.

Echenim, Peltier & Tourret

Call Assignments & tests Next call(s) is Entailed([C2 |X2], T, 2, 2) T1 Line 14 ( 2) (1) m1 g(b) a T2 T is Entailed([2|X2], {(g(b) a, Tα)} , T1 {(g(b) a, Tα)} Line 5 (2) g(b) a, ) is Entailed([2|X2], Tα, g(b) a, ( , T α) Tα Line 1 (3) g(b) a) g(b) a g(b) a is Included(X2, T α) m1 c a returns false (4) T1 (Line 13) T2 (continued) T1 returns false (5) (Line 9) (continued) returns false (6) (Line 9) is Entailed([2|X2], {(b a, Tβ)} , T1 returns false (7) g(b) a, ) (Line 9) Comments (1) Since T has two children, there are two recursive calls performed line 14. (2) Tα is the subtree of T below g(b) a. (3) T α is the child of Tα below . (4) This value is propagated up to the previous call. (5) Since the call Line 1 returned false, Line 8 is triggered next. This value is propagated up to the previous call. (6) This value is propagated up to the main call. (7) Tβ is the subtree of T below b a. The result is propagated up to the main call.

Table 2: Running of the Call is Entailed([C2 |X2], T, 2, 2)

Assume that is Included(X, T) = true. If T = then C(T) = { } and X. Otherwise X cannot be empty or the instruction at Line 5 would be triggered. Let m1 = min <π {m X}. If the call terminates at Line 10 then there exists a pair (l, T ) T1 such

that is Included(X \ {m1} , T ) returns true. By deﬁnition of T1, we must have l = m1, and by the induction hypothesis there exists Y C(T ) such that Y X \ {m1}, hence Y m1 X. If the call terminates at Line 13, then there exists a pair (l, T ) T2 T such that is Included(X \ {m1} , l.T ) returns true. By the induction hypothesis, there exists a constraint Y C(l.T ) such that Y X \ {m1}, hence Y C(T) and Y X.

For the converse implication, let us assume that T and X are such that there exists a constraint Y C(T), where Y X. If X = then necessarily Y = . By deﬁnition of a constraint tree we must have T = , and true is returned at Line 2. Otherwise X is not empty and we let m1 = min <π {m X}. If T = , then the return statement at Line 2 is

triggered again and we have the result. Otherwise, we deﬁne l1 = min <π {l Y}. Given the

Prime Implicate Generation in Equational Logic

ordering constraints imposed on constraint trees, there necessarily exists a pair (l1, T ) T such that Y \ {l1} C(T ). We distinguish several cases.

If l1 = m1 then (l1, T ) T1 and Y \ {l1} X \ {m1}. Hence by the induction hypothesis is Included(X \ {m1} , T ) returns true, the test at Line 9 succeeds and is Included(X, T) also returns true.

If l1 <π m1 then we cannot have Y X, and this contradicts the initial hypothesis.

If m1 <π l1 then (l1, T ) T2 and we must have Y X \ {m1}. By the induction hypothesis is Included(X \{m1} , l1.T ) returns true, and therefore, is Included(X, T) returns true at Line 13.

Algorithm 2 is Entailed([C |X], T, M, N)

Require: T is a c-tree, M is negative, M C is a normalized non-tautological clause and N |= M C Ensure: is Entailed([C | X], T, M, N) = true iﬀthere exists [D | Y] Cc(T) such that [D N |Y] c [M C |X]

1: if ( , T ) T (N (M C)) is Included(X, T ) then

2: return true

4: T1 {(l, T ) T | l M is a contradiction}

(l,T ) T1 is Entailed([C |X], T , M, N l) then

6: return true

8: if C = 2 then

9: return false

11: m1 min <π {m C}

12: if m1 is of the form u v, with u v then

13: T2 {(l, T ) T | l M <π m1 and w, (l M = u w, with u w v)}

14: return W

(l,T ) T2 is Entailed([C \ {m1}|X], l.T , M m1, N)

16: T3 {(l, T ) T | C M lc contains a tautological literal}

17: return W

(l,T ) T3 is Entailed([C |X], T , M, N l)

The correctness of is Entailed is stated in Theorem 5.16. The next propositions are steps of this proof. Proposition 5.14 shows that all the candidate branches starting with a negative literal are necessarily in T1 T2, and for T2, Proposition 5.15 justiﬁes the restriction imposed on the form of the ﬁrst literal of the selected branches. Both propositions are based on the following result:

Echenim, Peltier & Tourret

Proposition 5.13 If C and D are clauses such that C D is normalized, then C is also normalized.

Proof. This is due to the fact that since C C D, if l C then l = l C D\l l C\l = l, and if l and m are such that m lc C is a tautology then necessarily m lc C D is also a tautology, which is impossible by deﬁnition.

Proposition 5.14 Let C be a non-empty clause such that M C is normalized. Let l be a literal such that l M |= M C, and let m1 = min <π {m C}. If l is a negative literal, then

either l M is a contradiction or l M <π m1.

Proof. Assume that l M is of the form u v and that l M <π m1. Since l M |= M C, by Theorem 3.10, l M e M C, so that u M C v and u M C = v M C.

If m1 is of the form u v where v u, then u M C = v because M C is normalized, hence we also have v M C = v , so that v v. We deduce that m1 l M, which contradicts the assumption that l M <π m1.

Otherwise, m1 is either a positive literal, or of the form s t, where s u and s t. Thus in both cases u C = u and v C = v (because the smallest term to be potentially rewritten by the ground rewriting system associated6 with C, namely s, is greater than u, see Proposition 3.17), thus u = u M = u M C = v M C = v M = v.

Proposition 5.15 Let M C be a normalized clause where M is negative, and assume that m1 = min <π {m C} is a negative literal u v with u v. Let l be a literal such that

l M <π m1 and l M |= M C. The literal l M cannot be of the form u w with u w v

Proof. Assume that l M is of the form u w with u w v. Then because M C is normalized, u M C = v. In addition, by Theorem 3.10, since l M |= M C, we have w C M = u C M, thus w M C = v. Now by Proposition 3.17, since w u and all the maximal terms in the literals of C are strictly greater than w, the latter cannot be rewritten by the rewriting system associated with C. We deduce that w C M = w M = w; hence w = v, which contradicts the hypothesis that w v.

Theorem 5.16 Given a c-clause [C | X] and a c-tree T, let M and N be clauses such that M is negative, M C is normalized and N |= M C. The call is Entailed([C | X], T, M, N) terminates. Furthermore, is Entailed([C | X], T, M, N) = true iﬀthere exists [D|Y] Cc(T) such that [D N |Y] c [M C |X].

Proof. The termination proof is trivial, because at all recursive calls, the positive value |C| + size(T) strictly decreases. The correction proof requires two inductions, one for each implication. For the left-toright direction, the proof consists in going through the diﬀerent cases enumerated by the algorithm to verify that the requirements of the recursive calls are indeed met and that it is possible to derive the required property from its inductive children. In the other direction the diﬀerent cases that validate the right-hand side of the equivalence are considered and matched with the diﬀerent cases of the algorithm.

6. See Deﬁnition 3.16.

Prime Implicate Generation in Equational Logic

Left-to-Right Direction. If is Entailed([C | X], T, M, N) is true, then one of the return statements is triggered and returns true. We consider each of them in their order of appearance.

1. Line 2, ( , T ) T, N M C and is Included(X, T ) returns true. Since is Included is correct by Proposition 5.12, we deduce that Y C(T ) such that Y X. In this case [2 | Y] Cc(T), and since N |= M C by hypothesis, the property [N |Y] c [M C |X] is veriﬁed.

2. Line 5, T1 is set to {(l, T ) T | l M is a contradiction} and true is returned by the disjunction W

(l,T ) T1 is Entailed([C | X], T , M, N l). Thus there exists a pair

(l, T ) T1 such that is Entailed([C | X], T , M, N l) returns true and l M is a contradiction. By Theorem 3.10, l |= M, thus l |= M C. Moreover by hypothesis N |= M C, hence these two properties ensure that the preconditions of the corresponding recursive call are met. By induction there exists [D | Y] Cc(T ) such that [D l N |Y] c [M C |X]. Since [l D|Y] Cc(T), the result holds.

3. Line 14, C = 2 and W

(l,T ) T2 is Entailed([C \ m1 | X], l.T , M m1, N) returns

true, where m1 = min <π {m C} is of the form u v with u v and T2 is the

set {(l, T ) T | l M <π m1 and w, (l M = u w, with u w)} . Thus there is a pair (l, T ) T such that l M <π m1 and l M is not of the form u w with u w, for which is Entailed([C \ m1 |X], l.T , M m1, N) returns true. By hypothesis N |= M C; furthermore, M C = M m1 (C \ m1) and M m1 is negative. Therefore the preconditions of this recursive call are satisﬁed. By induction, its returning true entails that there exists [D | Y] Cc(l.T ) such that D N c M m1 C \ m1. Since Cc(l.T ) Cc(T), the c-clause [D|Y] also belongs to Cc(T), whence the result.

4. Line 17, m1 = min <π {m C} is of the form u v, l is positive and the disjunc-

(l,T ) T3 is Entailed([C | X], T , M, N l) returns true, with T3 equal to the set

{(l, T ) T | C M lc contains a tautological literal}. In this case there exist (l, T ) T and m2 C such that m2 M lc is a tautology, thus, by Theorem 3.10, l |= M m2 and l |= M C. Since N |= M C, the preconditions of the corresponding recursive call are met. Thus by the induction hypothesis [D l N | Y] c [M C | X] and [D|Y] Cc(T ). Since [l D|Y] Cc(T), we have the result.

Right-to-Left Direction. Assume that there exists a c-clause [D|Y] in Cc(T) such that [D N | Y] c [M C | X], where C, T, M and N respect the preconditions of the algorithm. We consider several cases.

If D = 2 then ( , T ) T and Line 2 is reached. Since [D N |Y] c [M C |X] we deduce that Y X and N M C. Consequently, the tests N M C is true and is Included(X, T ) is true by Proposition 5.12, thus is Entailed([C | X], T, M, N) returns true.

Otherwise D is of the form l D , with (l, T ) T and [D |Y] Cc(T ).

Echenim, Peltier & Tourret

If C = 2, then since [l D N |Y] c [M |X], in particular l D N |= M. Theorem 3.10 guarantees that D M, and since M is negative, D cannot contain any positive literal by Condition 2 of Deﬁnition 3.8. This means that l M must be a contradiction, and thus (l, T ) T1. It is straightforward to verify that the preconditions of is Entailed(C, T , M, N l) at Line 5 are met, thus by the induction hypothesis, this call returns true, and is Entailed([C | X], T, M, N) also returns true at Line 6.

If C is of the form m1 C with m1 = min <π {m C} and l is a negative literal,

then since l |= M C and l M C l M by Proposition 3.5, we deduce that l M |= M C. By Proposition 5.14, either 1) l M is a contradiction, or 2) l M <π m1.

1. If l M is a contradiction then (l, T ) T1 and since l D N |= M C by hypothesis, we have N l |= M C; thus the recursive call is Entailed([C | X], T , M, N l) at Line 6 returns true by the induction hypothesis. 2. If l M <π m1 then m1 must be a negative literal by deﬁnition of <π, and since N l D |= M C, we have N l D |= M m1 (C \ m1). By Proposition 5.15, (l, T ) T2. Since M C is normalized, so is M m1 (C \ m1), thus the preconditions of is Entailed at Line 14 are met and the call returns true by the induction hypothesis.

Now assume that C = m1 C , where m1 = min <π {m C}, and that l is positive.

If m1 is negative then (l, T ) T2, Line 14 is reached and returns true as in the previous case. Otherwise by Theorem 3.10 there exists a positive literal m2 in C such that m2 M C lc is a tautology. But since m1 is positive, by deﬁnition of <π, C must be a positive clause and m2 M C lc = m2 M lc. This implies that (l, T ) T3. Since [N l D |Y] c [M C |X], the preconditions for the call to is Entailed([C | X], T , M, N l) at Line 17 are met and by the induction hypothesis, this call returns true.

5.2.2 Backward c-Subsumption.

Backward c-Subsumption handles the removal from a c-tree T of all the c-clauses [D | Y] Cc(T) that are c-subsumed by a given c-clause [C |X], under the assumption that [C | X] itself is not c-subsumed by a c-clause stored in T. The principle of prune Entailed (Algorithm 5) is very similar to that of the is Entailed algorithm: it is a depth-ﬁrst traversal of T with a rewriting of literals. The main diﬀerence is that the roles of [C | X] and T are reversed: the literals of a branch of T are rewritten using the negative literals of C. When the c-subsumption test succeeds, the algorithm cuts the corresponding branch in T before exploring the remaining branches. In this algorithm, the clause N stores the already explored negative literals in the branch of T under investigation and several cases are distinguished depending on the form of the minimum literal m1 in C. The branches ending with are systematically deleted from the output tree. The role of algorithm prune Inf (Algorithm 4) is to complete the exploration of each clausal branch of the c-tree so that the -comparison between these and C can be done (as explained in the previous section,

Prime Implicate Generation in Equational Logic

the incompatibility of <π and prevents the -test from being performed directly on the tree). In practice, once the test C N fails, it also fails in all the subsequent recursive calls. Thus a sub-procedure containing only Lines 1 and 5 of prune Inf is used from this point on, producing the same result more eﬃciently. Finally, algorithm prune Included (Algorithm 3) can be seen as a simpler version of prune Entailed, where inclusion is tested instead of e-subsumption. It is the counterpart of algorithm is Included used in is Entailed, and is based on the same principle but with a swap in the roles of the constraint and the constraint tree.

Example 5.17 To illustrate how these three algorithms work, let us consider again the c-tree T of Figure 2 and the c-clause [C2 | X2] = [g(b) a | c a], which is such that is Entailed([C2 | X2], T, 2, 2) = as seen in Example 5.11. To remove the clauses in T that are subsumed by [C2 | X2], we call prune Entailed([C2 | X2], T, 2, 2). The result is the c-tree T without the branch for the c-clause [g(b) a | f(d) f(c) c a], which is the only c-clause in T that is redundant w.r.t. [C2 | X2]. The inner working of this call is described in Table 3.

The correction of prune Entailed is stated in Theorem 5.20. The intermediate termination and correction results concerning prune Included and prune Inf are stated respectively in Proposition 5.18 and Proposition 5.19.

Algorithm 3 prune Included(X, T)

Require: T is a constraint tree, X is a constraint. Ensure: C(Tout) = {Y C(T)|X Y}, where Tout = prune Included(X, T).

1: if X = then

4: if T = then

5: return T

7: m1 min <π {m X}

8: T1 {(l, T ) T | l = m1}

9: Tout1 {(l, prune Included(X \ {m1} , T )) | (l, T ) T1

prune Included(X \ {m1} , T ) = }

10: T2 {(l, T ) T \ T1 | l <π m1}

11: Tout2 {(l, prune Included(X, T )) | (l, T ) T2

prune Included(X, T ) = }

12: return Tout1 Tout2 (T \ (T1 T2))

Proposition 5.18 Let T be a constraint tree and let X be a constraint. The algorithm call prune Included(X, T) terminates and if Tout = prune Included(X, T), then C(Tout) = {Y C(T) | X Y}.

Proof. The termination of prune Included is the consequence of the strict decrease of size(T) at each recursive call. Let Tout = prune Included(X, T). If Tout = then C(Tout) =

Echenim, Peltier & Tourret

Call Assignments and tests Next call(s) prune Entailed([C2 |X2], T, 2, 2) m1 g(b) a Line 10 (1) T T1 {(g(b) a, Tα)} prune Entailed([C2 |X2], Tα, 2, m1 g(b) a Line 6 g(b) a) prune Entailed([2|X2], Tα, Line 2 g(b) a, g(b) a) prune Inf([C2 |X2], Tα, g(b) a) Line 1 prune Inf([C2 |X2], Tγ, Tout1 Line 5 (2) g(b) a f(a) c)

C2 g(b) a f(a) c

prune Included(X2, ) none (3) (continued) Tout1 Tγ Line 5 C2 g(b) a prune Included(X2, T α) m1 c a Line 11 (4) T1 T2 {(f(d) f(c), T δ)} prune Included(X2, T δ) m1 c a Line 9 T1 {(c a, )} prune Included( , ) (5) (continued) T2 (6) Comments (1) Tα is the subtree of T below the literal g(b) a. The other child of T is not modiﬁed. (2) Tγ = ( , ) is the subtree of Tα below the rightmost literal f(a) c. (3) The tree is not pruned since X2 = . (4) ( , T α) Tα, T δ is the child of T α. (5) This branch is pruned: is returned and discarded in the previous call. (6) The branch containing g(e) c is left unchanged since it belongs to T δ \ (T1 T2).

Table 3: Running of the Call prune Entailed([C2 |X2], T, 2, 2)

and the proposition holds no matter the original values of T and X. Otherwise, if Tout = { } then C(Tout) = { } and the proposition is true only if X = . Since Line 2 is triggered when X = before anything else, necessarily Tout = , a contradiction with the current hypothesis.

In the general case, we consider the two inclusions separately.

Left-in-Right Inclusion. Let us consider the case C(Tout) {Y C(T) | X Y}, by taking Y C(Tout) such that Y = l Y , where (l, T out) Tout and Y C(T out). This is suﬃcient since the base cases are covered in the previous paragraph. Since Tout = , we know that X = thus m1 = min<π {m X} exists. There are three cases to examine:

Prime Implicate Generation in Equational Logic

If Y C(Tout1) then T out = prune Included(X \ {m1} , T ) where (l, T ) T1, hence l = m1. By the induction hypothesis Y C(T ) and X \ {m1} Y , thus X m1 Y (= Y) and Y C(T1) C(T).

If Y C(Tout2) then T out = prune Included(X, T ) where (l, T ) T2 thus l <π m1. By the induction hypothesis Y C(T ) thus Y C(T) and X Y , thus in particular m1 Y hence m1 l Y ensuring that X Y.

If Y C(T \ (T1 T2)), then Y is of the form l Y, where (l, T ) T \ (T1 T2) and Y C(T ). By construction m1 <π l, hence for all l Y, m1 <π l and it is impossible to have X Y.

Right-in-Left Inclusion. To prove the right-in-left inclusion, we consider a constraint Y = l Y C(T) where (l, T ) T and Y C(T ) such that X Y. Again, the base cases are covered in the ﬁrst paragraph of the proof. If X = then X Y, a contradiction. Thus we can deﬁne m1 = min<π {m X} and distinguish three cases.

If l = m1 then X \ {m1} Y and (l, T ) T1, thus by the induction hypothesis Y C(T out) where T out = prune Included(X \ {m1} , T ) thus (l, T out) Tout1 Tout.

If l <π m1 then (l, T ) T2. Since X Y , by the induction hypothesis Y C(T out) where T out = prune Included(X , T ). Thus (l, T out) Tout2 Tout.

If m1 <π l then (l, T ) (T \ (T1 T2)) Tout.

In all three cases, Y C(Tout).

Algorithm 4 prune Inf([C |X], T, N)

Require: N.T is a normalized c-tree, [C |X] is a normalized c-clause. Ensure: Cc(Tout) = {[D|Y] Cc(T)|(C D N) X Y},

where Tout = prune Inf([C |X], T, N).

1: Tout1 {(l, prune Inf([C |X], T , N l)) | (l, T ) T

prune Inf([C |X], T , N l) = }

2: if C N then

3: return Tout1 {( , T ) | ( , T ) T}

5: return Tout1 {( , prune Included(X, T )) | ( , T ) T

prune Included(X, T ) = }

Proposition 5.19 Let [C | X] be a normalized c-clause, and N.T be a normalized c-tree. The call prune Inf([C | X], T, N) terminates and the output c-tree Tout = prune Inf([C | X], T, N) is such that:

Cc(Tout) = {[D|Y] Cc(T) | (C D N) X Y}

Proof. We proceed by double inclusion and induction. Let [D|Y] Cc(Tout).

Echenim, Peltier & Tourret

Assume ﬁrst that D = 2. If C N then Tout is returned at Line 3 thus [2 | Y] Cc({( , T )}) Cc(T) and C N D. Otherwise Tout is generated at Line 5 and [2 | Y] Cc({( , prune Included(X, T ))}), with ( , T ) T. By Proposition 5.18, Y C(T ) and X Y, hence the result.

Otherwise D is of the form l D where l = min<π(D) and [D |Y] Cc(Tout1), thus [D | Y] Cc(prune Inf([C | X], T , N l)) for some (l, T ) T. By the induction hypothesis, we have [D |Y] Cc(T ) (hence [D|Y] Cc(T)) and either C D N l, i.e. C D N, or X Y.

Now consider [D|Y] Cc(T) such that either C D N or X Y.

If D = 2 then [D|Y] Cc({( , T )}) Cc(T). If C N then Line 5 is reached and by hypothesis X Y, thus Y prune Included(X, T ) by Proposition 5.18, ensuring that [D|Y] Cc(Tout). Otherwise Line 3 is reached and again [D|Y] Cc(Tout).

Otherwise D is of the form l D , where l = min<π(D) and (l, T ) T. By hypothesis, either C D N in which case C D N l, or X Y. In both cases by the induction hypothesis [D | Y] Cc(prune Inf([C | X], T , N l)) thus [D | Y] Cc(Tout1) Cc(Tout).

Theorem 5.20 Let N.T be a normalized c-tree and let M C and N be normalized clauses. If M |= N, m |= N for all m C+ and is Entailed([C M |X], N.T, 2, 2) = false, then Cc(Tout) = {[D|Y] Cc(T) | [C M |X] c [D N |Y]} ,

where Tout = prune Entailed([C |X], T, M, N).

Proof. The termination of this algorithm is ensured because for all recursive calls, the value of |C| + size(T) strictly decreases.

Left-in-Right Inclusion. We ﬁrst prove that Cc(Tout) {[D | Y] Cc(T)|[C M | X] c [D N |Y]}. We consider a c-clause [D|Y] Cc(Tout) and distinguish several cases.

If C = 2 then Tout is generated at Line 2. By Proposition 5.19, either M D N or X Y, thus [M |X] c [D N |Y] and we have the result.

Otherwise C is of the form m1 C , where m1 is such that m1 N = min <π {m N | m C}.

If m1 N is a contradiction, then Tout is set to prune Entailed([C\m1 |X], T, M m1, N) at Line 6, and m1 |= N by Theorem 3.10. Since m1 is negative, (C \ m1)+ = C+ thus the preconditions of the recursive call are straightforwardly veriﬁed. By the induction hypothesis [(C \ m1) m1 M | X] c [D N | Y], thus [C M |X] c [D N |Y].

Otherwise, respectively by Theorem 3.10 and the hypothesis, m1 |= N both when m1 is negative and positive, hence C M |= N. If D = 2, then [D | Y] Cc(T ), and [C M | X] c [N | Y]. Otherwise D is of the form l D , where (l, T out) Tout and [D |Y] Cc(T out), and one of the following holds:

Prime Implicate Generation in Equational Logic

Algorithm 5 prune Entailed([C |X], T, M, N)

Require: N.T is a normalized c-tree, M C is a normalized non-tautological clause, M |= N, m |= N for all literals m C+ and is Entailed([C M |X], N.T, 2, 2) = false. Ensure: Cc(Tout) = {[D|Y] Cc(T) | [C M |X] c [D N |Y]},

where Tout = prune Entailed([C |X], T, M, N).

1: if C = 2 then

2: return prune Inf([M |X], T, N)

4: let m1 C such that m1 N = min <π {m N | m C}

5: if m1 N is a contradiction then

6: return prune Entailed([C \ m1 |X], T, M m1, N)

8: T {( , T ) T}

9: T1 (l, T ) T | l is negative m1 N l

10: Tout1 {(l, prune Entailed([C |X], T , M, N l)|

(l, T ) T1 prune Entailed([C |X], T , M, N l) = }

11: if m1 is positive then

12: T2 T \ (T1 T )

13: Tout2 {(l, prune Entailed([C \ Ll |X], T , M Ll, N l))|

(l, T ) T2 Ll = {m C | l N mc is tautological} prune Entailed([C \ Ll |X], T , M Ll, N l) = }

14: return Tout1 Tout2 T 15: else

16: return Tout1 (T \ T1)

1. (l, T out) Tout1, in which case there exists (l, T ) T such that l is negative, m1 N l and T out = prune Entailed(C, T , M, N l). Since M |= N by hypothesis, we have M |= N l. Furthermore, since N.T is a c-tree and l occurs in T, we must have l N, l <π l, hence, since l is negative, so is N l by deﬁnition of the ordering <π. Thus for all m C+, m |= N l. Now (N l).T is a normalized c-tree because N.T is normalized, hence the preconditions of the recursive call at Line 10 are all met, and [C M | X] c [D l N |Y] = [D N |Y] by the induction hypothesis.

2. (l, T out) Tout2, in which case m1 is a positive literal. By setting Ll = {m C | l N mc is tautological}, we then have T out = prune Entailed(C \ Ll, T , M Ll, N l). By Theorem 3.10, M Ll |= N l. If there exists an m (C \ Ll)+ such that m |= N l, then l N mc is a tautology because m |= N by the precondition of the algorithm. But by deﬁnition, such an m should belong to Ll and we have a contradiction. Thus, the preconditions of the recursive call at Line 13 are veriﬁed and by the induction hypothesis, [M Ll (C \ Ll)|X] c [D l N |Y], i.e., [M C |X] c [D|Y].

Echenim, Peltier & Tourret

3. (l, T out) T \ Tout1 and Tout2 is not computed, in which case m1 is negative and m1 N l. By Proposition 3.17 and Theorem 3.10, m1 |= D thus C |= N D.

Right-in-Left Inclusion. For the converse inclusion, let [D|Y] be a clause in Cc(T) such that [C M |X] c [D N |Y].

If C = 2, then since M |= N, either M D N or X Y. The tree Tout must be generated at Line 2 and, by Proposition 5.19, [D|Y] Cc(Tout).

Otherwise C is of the form m1 C where m1 is such that m1 N = min <π {m N | m C}.

If m1 N is a contradiction then m1 |= N by Theorem 3.10 and Tout is returned at Line 6. By the induction hypothesis [C \ m1 m1 M | X] c [D N | Y], and therefore [D|Y] Cc(Tout).

Otherwise we may have either D = 2, in which case [D | Y] Cc(T ) and the result is straightforward, or D is of the form l D for some (l, T ) T and [D | Y] Cc(T ).

1. If l is negative and m1 N l, then (l, T ) T1. In addition, T out1 is set to prune Entailed([C |X], T , M, N l) at Line 10. The preconditions of the recursive call are all met for the same reason as in the ﬁrst inclusion proof. By the induction hypothesis [D |Y] Cc(T out1) thus [D|Y] Cc(Tout1). 2. If m1 is negative and either l is positive or m1 N l then (l, T ) T \ T1 and Tout is set at Line 16, thus [D|Y] Cc(Tout). 3. If the previous conditions do not hold, then m1 is a positive literal. By Theorem 3.10, the clause Ll = {m C|l N mc is tautological} is such that Ll |= N l, and since M |= N, we have M Ll |= N l. Moreover (N l).T

is a normalized c-tree and for all m occuring in (C \ Ll)+, m |= N l for the same reason as in the previous inclusion. Hence the preconditions of the recursive call prune Entailed([C \ Ll | X], T , M Ll, N l) are veriﬁed. Since [C \ Ll M Ll |X] c [D l N |Y], by the induction hypothesis, [D |Y] Cc(T out2) and [D|Y] Cc(Tout2).

Remark 5.21 Note that sets of implicates generated by the main saturation algorithm (i.e., the clauses C such that the ﬁnal c-tree contains a c-clause [2 | X] with X c = C) can be eventually stored in c-trees with empty constraints. In this case, the -condition can be omitted when testing redundancy, since the goal is to remove all implicates that are redundant w.r.t. logical entailment. The obtained algorithms are very similar to (and simpler than) is Entailed and prune Entailed. They are omitted for the sake of conciseness.

6. Experimental Results

In this section, we present the diﬀerent tools and benchmarks used to conduct experiments, as well as the results obtained from those experiments.

Prime Implicate Generation in Equational Logic

6.1 Implementation

Our prime implicate generation method has been implemented in a research prototype written in OCaml7. The system, called c SP, is available at https://forge.imag.fr/docman/ ?group_id=683. The input formulæ are sets of equational ground clauses in the TPTP syntax v5.4.0.0 (Sutcliﬀe, 2009). Another version of the program, called c SP flat, implements additional reﬁnements that only apply to ﬂat clauses, i.e., to clauses not containing function symbols of an arity greater than 0. The system for non-ﬂat clauses is based on the Log Tk library (Cruanes, 2014) for the handling of term ordering and congruence closure. There are several options available for controlling the form of the generated implicates: -max-size, -max-neg and -max-depth limit the length of clause, the number of negative literals and the depth of the terms, respectively; -cov accepts only implicates that entail one of the clauses of the input formula (for generating a minimal cover of the input formula). To ensure termination, a restriction must be added to the terms introduced by the Assertion rules, since otherwise the rules are inﬁnitely branching, see Section 4. By default, c SP considers all the terms occurring in the initial formula. A ﬁnite set of terms can also be provided by the user in a TPTP input ﬁle with the extension .conf . The order in which the c-clauses are processed is ﬁxed by comparing the size of the constraints and of the clausal parts, in lexicographic increasing order. A more detailed description of the system was done by Tourret (2016).

6.2 Experimental Context

This section describes the reference tools and of the benchmarks used in the experiments.

6.2.1 Reference Tools.

Tools for the computation of prime implicates in propositional and ﬁrst order logic directly available from the web include only (to the best of our knowledge):

ritrie (Matusiewicz, Murray, & Rosenthal, 2009), a propositional tool that specializes in fast querying of implicates8.

primer (Previti, Ignatiev, Morgado, & Marques-Silva, 2015), a prime implicate generation tool based on satisﬁability encoding9.

Mistral (Dillig & Dillig, 2013), an SMT solver which can be used for performing abductive inferences10.

Thanks to the kindness of their respective authors, we also obtained two other tools:

Zres (Simon & Del Val, 2001), an implicate generation tool in propositional logic based on Resolution,

SOLAR (Iwanuma, Nabeshima, & Inoue, 2009), a prime implicate generation tool for ﬁrst order logic, including equational logic, based on Semantic Tableaux.

7. http://ocaml.org 8. http://www.cs.albany.edu/ritries/prototype.html 9. http://logos.ucd.ie/web/doku.php?id=primer 10. http://www.cs.utexas.edu/~tdillig/mistral/index.html

Echenim, Peltier & Tourret

We compared c SP with all these systems except for ritrie and Mistral. The former is because it was not eﬃcient enough, which can be explained by the fact that it was built to perform eﬃcient querying of an already generated set of prime implicates, rather than to compute eﬃciently the said set (which it can nevertheless do). The latter is because it cannot be compared with our work, because its prime implicate generation is not complete. We compared the systems on three sets of test problems, two of which are randomly generated due to the lack of existing benchmark in the targeted logics. These benchmarks are included in the archive containing the source code of c SP. In each case, the propositional equivalents of the problems were obtained by instantiating the transitivity axioms for all constant symbols appearing in them the reﬂexivity and commutativity axioms are encoded directly in the transformation by orienting and simplifying the equations. Thus the propositional tools have to handle much bigger inputs and they generate many more prime implicates than their counterparts handling more expressive logics (for instance they also compute the implicates of the transitivity instances). To recover the same results as the other tools, it would be necessary to replace the propositional variables by the corresponding equations and to remove all redundancies. This step is not performed here since it is straightforward (although costly), but in an application case, it would have to be performed to reach an intelligible result. Similarly, non-ﬂat clause sets can also be ﬂattened by adding all relevant instances of the substitutivity axioms and unﬂattened in a post-processing step that is omitted here.

6.2.2 Flat Random Benchmarks.

As far as we are aware, there are no benchmarks for ground ﬂat (i.e., without function symbols of an arity strictly greater than 0) equational logic. Our attempts with ﬂattened ground problems from the TPTP library did not succeed, because none of the available tools can generate all the prime implicates of such large formulæ with reasonable time and memory constraints. We thus created our own benchmark, made of a thousand randomly generated formulæ of 6 clauses build on 8 constants and containing between 1 and 5 literals (even such small formulæ can have very large set of prime implicates).

6.2.3 Non-Flat Random Benchmarks.

The formulæ in this benchmark contain function symbols and were generated using the following parameters:

a {1, 2}, is the maximal arity of the functions and a 5 is the size of the randomly generated signature11,

c {2, 3, 4} is the number of clauses in a formula,

d {1, 2} is the maximal depth of the terms,

l {2, 3} is the maximal number of literals in a clause (the minimum being 1),

The formulæ are stored in ﬁles that are named with the following convention: sa_d_c_l (e.g. s1_2_4_2). In total, this benchmark contains 144 formulæ.

11. By design, the signature contains at least two literals of arity zero.

Prime Implicate Generation in Equational Logic

6.2.4 Other Benchmarks.

These benchmarks are extracted from the SMT-LIB database (Barrett, Fontaine, & Tinelli, 2015) in the logic QF AX, i.e. closed quantiﬁer-free formulas over the theory of arrays with extensionality 12. These are synthetic benchmarks that model some properties of arrays with extensionality, namely:

the order in which the elements are stored in an array does not matter (storecomm benchmarks),

some swappings of elements between cells of an array are commutative (swap benchmarks),

swapping elements between identical cells of equal arrays generates equal arrays (storeinv benchmarks)

The creators of these benchmarks slightly altered them to falsify these properties, thus creating the benchmarks labeled with invalid13. Given that c SP cannot handle SMT-LIB inputs or the theory of arrays, we preprocessed the benchmarks by ﬁrst converting them to TPTP and then applying the algorithm described by Bonacina and Echenim (2010). As shown by Armando et al. (2009), these problems can be nontrivial to solve even for state-ofthe-art theorem provers like E (Schulz, 2013) and one cannot expect the entire set of prime implicates to be generated in reasonable time. We use them mainly to evaluate the impact of our redundancy-pruning technique on the number of Superposition inferences carried out by blocking the Assertion rules inferences (i.e. applying a ﬁlter blocking all implicates apart from the empty one), allowing the comparison of c SP with the E theorem prover.

6.3 Results

All of the experiments were run on a machine equipped with an Intel core i5-3470 CPU and 4 2 GB of RAM running Ubuntu 14.04. In a ﬁrst experiment we compare c SP with c SP flat and primer on the random ﬂat benchmark to observe the impact of the functional term representation (Log Tk) of c SP. Then we compare our tools to state-of-the-art solvers on the non-ﬂat benchmark. Finally, we observe the behavior of c SP on bigger formulæ.

6.3.1 Impact of the Handling Functional Terms.

Handling functional terms is costly. This can be seen on Figure 3, that compares the execution time of c SP on the random ﬂat benchmark with that of c SP flat and primer. As shown on Figure 3a, on average, c SP is ten times slower than c SP flat on the random ﬂat benchmark. This overhead induced by functional terms is easily explainable: the new term representation must handle nested terms, which prevents the use of a simple integer representation as is done in c SP flat. Moreover, the subsumption method is a bit more involved which plays a role in slowing down c SP compared to c SP flat. Figure 3b compares the execution time of c SP flat with that of primer on the same benchmark to illustrate the performance of c SP flat in ground ﬂat equational logic.

12. http://smtlib.cs.uiowa.edu/logics.shtml 13. For details on these benchmarks, we refer the interested reader to the paper by Armando, Bonacina, Ranise, and Schulz (2009).

Echenim, Peltier & Tourret

0 150 300 c SP-flat (s)

(a) c SP vs. c SP flat

0 150 300 c SP-flat (s)

(b) primer vs. c SP flat

0 150 300 c SP (s)

(c) primer vs. c SP

slower equal faster

c SP flat 12.3% 0% 87.7%

c SP 39.1% 0.4% 60.5%

(d) Proportion of formulæ that are slower/equal/faster on c SP flat/c SP than on primer

Figure 3: Time comparison of c SP, c SP flat and primer; random ﬂat benchmark

6.3.2 Performance Comparisons on Random Non-Flat Benchmark.

The experiment presented below is a comparison of the prime implicate generation systems Zres, primer and SOLAR with c SP flat and c SP on the random non-ﬂat benchmark.

The results are summarized in Table 4. Each line corresponds to a system. The column labeled successes indicates the percentage of tests that were completed before the 5 minute timeout. The four columns under the label SOLAR successes summarize average results on those tests on which SOLAR terminated before the timeout. The same goes for the columns under Zres successes , primer successes , c SP flat successes and c SP successes . Finally, the timeout columns expose the mean results on all interrupted tests. Columns labeled fail , time , inf. and PIs respectively give the percentage of formulæ on which the system timed out relative to this part of the benchmark, the mean execution time, mean number of

Prime Implicate Generation in Equational Logic

successes SOLAR successes Zres successes fail. time(s) inf. PIs fail. time(s) inf. PIs SOLAR 15% 0% 11.842 663190 506 74% 13.608 767160 455 Zres 52% 13% 0.695 X 2986 0% 12.474 X 13804 primer 53% 13% 0.794 X 2986 0% 3.770 X 13847 c SP flat 63% 4% 6.622 2275 74 2% 0.500 1737 159 c SP 76% 0% 0.042 99 21 2% 3.576 755 49 primer successes c SP flat successes fail. time(s) inf. PIs fail. time(s) inf. PIs SOLAR 75% 13.608 767160 455 76% 12.360 694523 460 Zres 2% 12.474 X 13804 19% 7.073 X 10405 primer 0% 8.016 X 18949 17% 7.590 X 15779 c SP flat 2% 1.480 2347 180 0% 14.290 6730 348 c SP 2% 4.296 851 49 3% 7.556 1004 62 c SP successes timeouts fail. time(s) inf. PIs inf. PIs? SOLAR 79% 11.842 663191 506 2452908 28152 Zres 33% 10.391 X 11338 X X primer 31% 7.671 X 16687 X X c SP flat 19% 8.795 5418 313 X X c SP 0% 10.193 1209 79 14714 538

Table 4: Test results summary; random non-ﬂat benchmark

slower equal faster

c SP flat 5.6% 41.7% 52.8%

c SP 23.6% 3.5% 72.9%

Table 5: Proportion of formulæ that are slower/equal/faster on c SP flat/c SP than on primer

inferences and mean number of prime implicates found for each set of tests. The last column under the timeout label is labeled PIs? because, due to the timeout, the implicates found are not guaranteed to be prime. Cells labeled with an X indicate that the corresponding data is not available. As shown in the successes column, c SP is the obvious winner in terms of the number of tests handled before timeout. The 15% of problems solved by SOLAR are the simplest of the random formulæ. The results show that SOLAR s approach is very costly both in terms of time and space. The high number of prime implicates this tool generates compared to those produced by c SP is due to the fact that SOLAR does not take into account the equality axioms in its redundancy detection. Thus for example, any literal t s also appears as s t, and f(s) f(t) is not detected as redundant w.r.t. s t. The huge

Echenim, Peltier & Tourret

number of prime implicates generated by Zres and primer stems directly from the lack of post-processing (conversion of the results back to equational logic)14. This prevents the detection of the purely equational redundancies, e.g. clauses redundant w.r.t. the transitivity axiom. Although Zres and primer are faster than c SP on the problems they both solve, they solve 52% and 53% of the benchmark respectively, while c SP solves 76% of them. The results in the c SP successes and c SP flat successes columns are globally higher than those in the Zres successes and primer successes columns, because the most diﬃcult formulæ are solved only by c SP and to a lesser extend by c SP flat. Since c SP solves more problems than c SP flat and does so faster and with fewer clauses processed, c SP is clearly better adapted to dealing with originally non-ﬂat formulæ. Incidentally, note that the overhead of c SP s term handling compared to that of c SP flat s (observed in the previous experiment) is more than compensated by the direct handling of non-ﬂat formulæ since on the random non-ﬂat benchmark c SP is faster than c SP flat. The number of inferences and generated non-redundant implicates when the tool times out illustrates the heavy cost of the c SP inferences and redundancy detection mechanism compared to that of SOLAR. It is a price that seems partly unavoidable to eliminate all redundancies, since this requires costly algorithms.

6.3.3 Impact of Normalization.

We also assessed the impact of the normalization mechanism on the QF-AX benchmark. This was done by comparing c SP with the E theorem prover, running c SP with a ﬁltering option (-max-size 0) to block the generation of any implicate besides the empty clause, eﬀectively turning c SP into a Superposition theorem prover. This way the main diﬀerences between c SP and E are the normalization of clauses and the redundancy pruning mechanism. On the one hand, the redundancy pruning algorithm used by c SP is weaker because it does not allow for equational simpliﬁcation or other n-to-one redundancy pruning rules. On the other hand, one-to-one redundancy testing is stronger since its uses logical entailment together with the usual ordering condition instead of subsumption. The comparison of c SP with the E theorem prover on these formulæ shows that the normalization approach can, in some nontrivial cases, reduce the number of processed clauses by an order of magnitude. Figure 4 presents the positive results of this experiment, i.e., the results of the storecomm and swap formulæ. Among these, only the formulæ on which both E and c SP (without Assertion rules) terminate before the timeout and without memory overﬂow were kept. Light gray squares represent the invalid formulæ, i.e. the satisﬁable ones, while dark gray crosses mark the unsatisﬁable ones. The line y = x is added in both plots. An interesting observation is that for the largest invalid formulæ, c SP needs to process a smaller number of clauses than E before terminating, even 10 times less in the case of the invalid swap formulæ. In addition, the unsatisﬁable swap formulæ were run with a timeout of 10 minutes (the triangles in Plot (4b)) and the corresponding results hint that this phenomenon could also be true for larger unsatisﬁable problems. This suggests that the redundancy pruning technique based on normalization and clausal trees could be proﬁtably integrated into stateof-the-art Superposition-based theorem-provers, at least for ground equational clause sets.

14. It should be noted that the mean number of prime implicates generated by Zres and primer sometimes diﬀer a lot. This is due to a bug in Zres which sometimes makes it incomplete.

Prime Implicate Generation in Equational Logic

700 800 900 1000 E (nb)

(a) storecomm formulæ

0 50000 100000 E (nb)

(b) swap formulæ

Figure 4: Comparison of the number of processed clauses for E and c SP.

However, it might not always be useful, e.g. Figure 5, plotting the storeinv formulæ where an opposite tendency is observed, although the storeinv formulæ on which neither c SP or E timeout represent only a tenth of that of the other two families, for which the results are positive.

0 1000 2000 E (nb)

Figure 5: storeinv formulæ - comparison of the number of processed clauses for E and c SP.

7. Discussion

In this section, we present potential applications of our work in AI, discuss related work, and provide some lines of future research.

7.1 Summary

The present work comprises three main contributions:

Echenim, Peltier & Tourret

The c SP calculus extends the classical Superposition calculus for ﬁrst-order logic with equality with two rules that allow the addition of abductive hypotheses to the generated clauses.

A clause storage data structure is deﬁned, the constrained clausal tree. It signiﬁcantly reduces memory consumption and allows the eﬃcient detection and removal of redundant clauses.

Two prototypes of prime implicate generation tools implement the calculi, storage method and their variants, one that handles only ground ﬂat terms and one that handles arbitrary ground terms.

Our main results are the following. On the theoretical side, we proved the deductivecompleteness of the calculus for full equational logic and the termination and correctness of the constrained clausal tree manipulation algorithms for ground equational logic. On the practical side we conducted an experimental evaluation of our prototypes (on ﬂat and non-ﬂat benchmarks). The diﬀerent experiments presented in Section 6 allow us to draw the following picture of our prime implicate generation algorithm:

1. c SP compares favorably with state-of-the-art prime implicate generation tools. As indicated by the results in Table 4, c SP solves more problems (and more eﬃciently) than all others available tools. Precisely, our best prototype is faster than the reference tool (primer) in 87.7% of the benchmark in ﬂat ground logic and 72.9% in non-ﬂat ground logic. However, none of the systems scale well: the formulæ for which complete sets of prime implicates can be eﬀectively computed are rather simple.

2. The normalization method used in our algorithms signiﬁcantly reduces the number of generated clauses compared to the state-of-the-art E theorem prover (although our inference engine is far less eﬃcient). This suggests that the integration of this technique to Superposition-based theorem-provers could be beneﬁcial.

3. Our experiments also suggest that it is always better to have a method tailored to the input formulæ rather than to preprocess them by ﬂattening and/or conversion to propositional logic or to use a tool for a more expressive logic. For example, on ﬂat formulæ, c SP flat is the best choice over c SP, while on non-ﬂat ones c SP gives the best results.

7.2 Applications in Artiﬁcial Intelligence

When they terminate, usual proof procedures in ﬁrst-order logic return a yes or no result, together with a formal justiﬁcation: either the input formula is valid, and in this case a proof is provided; or it is not, and in some cases a counter-example can be constructed. In contrast, the generation of prime implicates allows for open requests. It thus targets situations when the possible answers are not known, but have to be constructed by the program, as well as their justiﬁcation. This makes the reasoning task much more complex and signiﬁcantly increases the search space, but also allows for a wider range of applications, and for the conception of more intelligent programs, able to derive results that are not necessarily expected by human users. So far the implicate generation problem has been

Prime Implicate Generation in Equational Logic

tackled mostly for propositional and related logics, although many applications require more expressive logics for modeling systems or knowledge bases. Finding implicate generation algorithms that are capable of handling expressive logics is thus a relevant and important problem in Artiﬁcial Intelligence. In particular, being able to handle equalities eﬃciently is a prerequisite, since adding equality axioms would be very ineﬃcient. For instance the OWL Web Ontology Language (Patel-Schneider, Hayes, Horrocks, et al., 2004) includes atoms Same Individual(a1, . . . , an) that assert that all of the individuals ai (for i [1, n]) are equal to each other. We provide below some concrete examples of applications.

7.2.1 Diagnosis

Diagnosis, deﬁned as the design of techniques to determine whether the behavior of a system is correct (i.e., fulﬁlls its speciﬁcation) and to generate suitable explanations if it is not, is usually viewed as an important subdomain of AI. We target model-based diagnosis, in which the behavior of the system and its properties are modeled by logical formulas. For many applications, propositional logic is not expressive enough, and richer logics must be used instead: for instance, many veriﬁcation problems are based on ground equational logic or can be reduced to it (see, e.g., Cimatti, Griggio, & Sebastiani, 2011). The generation of prime implicates is useful in this context for explaining bad or unexpected behaviors of a system. The idea is to determine what the additional (if possible minimal) hypotheses that could be added to enforce the desired properties are. This allows one to identify missing conditions (if the additional hypotheses are fulﬁlled) or to give a hint of why the system does not behave as expected (if the additional hypotheses are false). We provide an example coming from program veriﬁcation. Consider a program that assigns the pointers to the tails of two lists l1 and l2 as follows:

tail(l1) l0; tail(l2) l1

Assume we want to check that the relation tail(tail(l2)) = l0 holds after the execution of the program. This problem can be naturally modeled in equational logic as follows. The function tail is represented by a function tail : heap list list, and the redirection operation is encoded by a function redir : heap list list heap, together with the following axioms:

tail(redir(h, x, y), x) y % The tail of x is redirected to y x x tail(redir(h, x, y), x ) tail(h, x ) % The tail of the other lists is not aﬀected by the redirection

The conclusion to be proven is

h 0 redir(redir(h0, l1, l0), l2, l1) tail(h 0, tail(h 0, l2)) l0

where h0 and h 0 are constant symbols denoting the initial and ﬁnal states of the heap. Trying to prove this goal from the axioms actually fails, which may come as a surprise to some users. Indeed, in the case where l1 = l2, the ﬁnal list l2 loops to itself (the tail of l2 is l2), and l0 is no longer accessible. The property can be proven if l1 is distinct from l2, which can be inferred by generating the prime implicate l1 l2 from the speciﬁcation and the negation of the conclusion.

Echenim, Peltier & Tourret

7.2.2 Computing Possible Explanations of Observations

Similarly, abductive reasoning also allows one to construct possible explanations of observed behaviors. Given an ontology O and a knowledge base K, both modeled by a set of axioms in ﬁrst-order logic with equality (e.g., an OWL database), and an observation o, implicates of O K o correspond to negations of explanations of o. For example, given the axioms

blue-eyed(father(x)) blue-eyed(mother(x)) blue-eyed(x)

the facts blue-eyed(alice) blue-eyed(bob) mother(carol) alice, and the observation blue-eyed(carol), we may infer the hypothesis: father(carol) bob. This is done by generating the prime implicate father(carol) bob from the above axioms and the negation of the observation (assessing the actual plausibility of the assumption is out of the scope of the present work, it may depend on heuristics or other observations). Formally, this implicate is generated by the c SP calculus as follows (Resolution steps may be simulated by Superposition inferences and reﬂection).

1 blue-eyed(father(x)) blue-eyed(mother(x)) blue-eyed(x) % axiom 2 blue-eyed(carol) % neg. observ. 3 blue-eyed(father(carol)) blue-eyed(mother(carol)) % Res., 1, 2 4 mother(carol) alice % axiom 5 blue-eyed(father(carol)) blue-eyed(alice) % Sup., 3, 4 6 blue-eyed(alice) % axiom 7 blue-eyed(father(carol)) % Res., 5, 6 8 [ blue-eyed(bob)|father(carol) bob] % Ass., 7 9 blue-eyed(bob) % axiom 10 [2|father(carol) bob] % Res., 8, 9

7.2.3 Extracting Relevant Consequences

Implicate generation can also be used to compute relevant consequences of a knowledge base, in cases where such consequences are not known in advance. Consider for instance the axiom

daughter(x, y) female(x) y mother(x)

The famous riddle If Teresa s daughter is my daughter s mother, who am I to Teresa? can be answered by considering the formula daughter(s, Me) daughter(mother(s), Teresa) and computing some of its prime implicates:

1 daughter(s, Me) % axiom 2 daughter(x, y) y mother(x) % axiom 3 Me = mother(s) % Res., 1, 2 4 daughter(mother(s), Teresa) % axiom 5 Teresa = mother(mother(s)) % Res., 2, 4 6 Teresa = mother(Me) % Sup., 5, 3 7 [Teresa Teresa |mother(Me) Teresa] % Ass., 6 8 [2|mother(Me) Teresa] % Reﬂ.

Prime Implicate Generation in Equational Logic

Clause 8 yields a ﬁrst solution mother(Me) Teresa. But another (equivalent) solution exists:

9 daughter(x, y) female(x) y mother(x) % axiom 10 [Teresa mother(Me) female(Me)| daughter(Me, Teresa)] % Ass., 9 11 [ female(Me)| daughter(Me, Teresa)] % Res., 10, 6 12 daughter(x, y) female(x) % axiom 13 female(mother(s)) % Res., 12, 4 14 female(Me) % Sup., 13, 3 15 [2| daughter(Me, Teresa)] % Res., 14, 12

Note that the computed implicates should only refer to the relevant symbols Me, Teresa and to the above relations, for example, they should not contain the auxiliary constant s. This motivates the fact that we should be able to compute speciﬁc prime implicates verifying user-speciﬁed criteria.

7.2.4 Dealing for Incomplete Information

Abducing equalities is also useful to deal with approximative, incomplete or even spurious information. Assume we are given an ontology O and knowledge base K, and that we want to check whether some property p holds. In some cases, property p will fail to be derived, due to unreported synonyms (e.g., misspelled names, duplicate identiﬁers,. . . ), aliases or missing deﬁnitions. This problem, that commonly arises in practice, may be detected by computing purely equational prime implicates of O K p, eﬀectively showing that p possibly holds provided some simple equalities are added in the knowledge base. Afterwards, one could seek conﬁrmation from other sources and update the database if needed. For instance, given the facts: mother(alice) carol mother(bob) carol

father(alice) dave father(bob) david

brother(x, y) (male(x) mother(x) mother(y) father(x) father(y))

and the request: who is the brother of Alice? , we may compute the plausible answer Bob , under the assumption that dave and david denote the same individual. This may be done by deriving the implicate dave david from the negation of the goal brother(x, alice). The variable x is uniﬁed with bob in the derivation, yielding the desired result. Similarly, if the fact father(bob) david is deleted, then the above answer can still be returned, under the condition that father(bob) dave. In the spirit of the previous examples, the ﬁrst-order prime implicate generation tool SOLAR (Nabeshima, Iwanuma, Inoue, & Ray, 2010) is used in non-equational ﬁrst-order logic to abduce hypotheses for the completion of biological networks (Rougny, Yamamoto, Nabeshima, Bourgne, Poupon, Inoue, & Froidevaux, 2015) and this technique is generalized into a method to abduce logical reasoning called meta-level abduction by Inoue (2016). Although the work presented in these papers does not rely on equational logic, its use could make meta-level abduction more powerful by giving it the possibility of unifying seemingly diﬀerent objects to explain observations, which could be particularly useful when data comes from several sources, as illustrated in the previous paragraph.

Echenim, Peltier & Tourret

7.3 Related Work

The prime implicate generation problem has been extensively investigated in the context of propositional logic (see e.g., Marquis, 2000). Standard algorithms are based mainly on reﬁnements of the Resolution rule (Leitsch, 1997; Robinson, 1965), because unrestricted Resolution permits to generate all the prime implicates of a set of clauses (Jackson, 1992; Kean & Tsiknis, 1990; Quine, 1955; Tison, 1967). The proposed approaches then focus on the deﬁnition of eﬃcient strategies to generate saturated clause sets, by considering literals incrementally, and on the deﬁnition of compact data structures for storing the generated sets of implicates, e.g., using tries (De Kleer, 1992; Fredkin, 1960) or Z-BDDs (Mishchenko, 2001; Simon & Del Val, 2001). Other approaches use decomposition-based methods, in the style of the DPLL procedure, for generating trie-based representations of sets of prime implicates (Matusiewicz et al., 2009; Matusiewicz, Murray, & Rosenthal, 2011). Recently, a new approach that outperforms previous algorithms has been proposed by Previti et al. (2015); it is based on satisﬁability solving and problem reformulation. The idea is to associate each literal l with a variable xl indicating whether l occurs in the considered implicate; using an adequate reformulation, the implicates correspond exactly to maximal models of formulæ (iteratively) built on these variables. There have been only very few approaches dealing with more expressive logics. Some extensions have been considered in modal logics (see e.g., Bienvenu, 2007; Blackburn, Van Benthem, & Wolter, 2007), and algorithms have been proposed for ﬁrst-order formulæ. Some of these approaches use unrestricted versions of the Resolution calculus (Knill, Cox, & Pietrzykowski, 1993; Marquis, 1991). Other procedures extend the semantic tableau method to search for hypotheses ensuring that all branches in the tableau can be closed (Mayer & Pirri, 1993; Nabeshima et al., 2010). However, none of them handle equality eﬃciently. More recently, algorithms were devised to generate sets of implicants of formulæ interpreted in decidable theories (Dillig, Dillig, Mc Millan, & Aiken, 2012), by combining quantiﬁer-elimination for discarding useless variables, with model building to construct sufﬁcient conditions for satisﬁability. The approach does not apply to equational formulæ with (uninterpreted) function symbols since this would involve second-order quantiﬁer elimination. For instance, generating the implicant a b from f(a) f(b) requires to solve the second-order quantiﬁer problem: f (f(a) f(b)) in order to get rid of the symbol f. Every existing prime implicate generation procedure in propositional logic can be employed to handle ground equational clauses by instantiating the variables occurring in the equality axioms by the terms occurring in the input formula and considering equations as propositional variables in the augmented formula. Systems designed to handle ﬁrst-order logic can also be used, simply by adding the equality axioms in the input clauses. In both cases, however, the encoding introduces many redundancies, since the axioms of equality will not be taken into account for redundancy testing. For instance, in both approaches, all logical consequences of these axioms will be generated as implicates. Furthermore, as explained in Section 3, an equational clause may possess many equivalent forms possibly exponentially many and every such form will be considered if the transitivity and substitutivity axioms are not taken into account15. Besides eﬃciency problems, a post-processing

15. It is clear that the commutativity and reﬂexivity axioms can be easy handled by the encoding, e.g., two equations a b and b a can be mapped to the same propositional variable.

Prime Implicate Generation in Equational Logic

step is thus necessary in order to obtain sets of prime implicates in ﬁrst-order logic with equality. Note that the experimental comparison in Section 6 does not take the preand post-processing steps into account.

The calculus presented in this paper is a form of Constrained Superposition calculus. Other such calculi (see, e.g., Althaus, Kruglov, & Weidenbach, 2009; Bachmair, Ganzinger, & Waldmann, 1994; Baumgartner & Waldmann, 2013) have been deﬁned to handle heterogenous problems, i.e., problems involving a combination of standard ﬁrst-order logical reasoning with reasoning in speciﬁc theories such as arithmetic16. In these approaches, constraints are used to isolate the part of the formula belonging to the considered theory from the ﬁrst-order part which can be handled by the Superposition calculus. External systems can be used afterwards to test the satisﬁability of such constraints. Our work departs from these approaches, because constraints are not used to postpone a part of the reasoning, but rather to collect asserted hypotheses. In particular, the underlying theory and semantics of the constraints are identical to those of the clauses, only the operational meaning diﬀers.

It is worth comparing the present procedure with our earlier works (Echenim & Peltier, 2016; Echenim, Peltier, & Tourret, 2013, 2014). The procedures devised by Echenim et al. (2013, 2014) only apply to formulæ that are ground and ﬂat, i.e., when the only atoms are equations between constant symbols. The inference rules used for deriving implicates depart from those used in the present approach because there is no distinction between abduced literals and standard ones. Both kinds of literals are handled in a completely uniform way, and the same rules are used both to detect contradictions and to add new hypotheses. On the one hand this may yield more compact representations of the clauses, but on the other hand this results in a less eﬃcient calculus, because most of the restrictions of the Superposition calculus (e.g., ordering constraints) have to be dismissed to ensure deductive completeness. The method described by Echenim and Peltier (2016) uses an explicit representation of abducible literals as constraints, as in the present paper, however such abducible hypotheses are generated in a completely diﬀerent way. Instead of using speciﬁc assertion rules to explicitly add new hypotheses in the derivations, this method works by considering residuals of failed uniﬁcation attempts as abductive hypotheses. Consider for instance the formula f(a) f(b). This method tries to unify f(a) and f(b) so that the Reﬂection rule can be applied; it fails (a and b denote distinct constants), but generates in the process a residual equation a b which cannot be solved. Adding this equation a b in the constraint allows one to ensure that the inference is applicable, under this additional hypothesis. In contrast, the present approach will ﬁrst rewrite the constant b into a, adding the equation a b in the constraint and then apply the Reﬂection rule on f(a) f(a). The advantage of the former method lies in the fact that it avoids any blind rewriting of the terms (in the above example a could be rewritten to any ground term smaller than a, see the description of the calculus in Section 4 and Remark 4.8 for more details). The use of uniﬁcation failures allows one to guide the discovery of the additional hypotheses that must be added to generate the empty clause. The advantage of the latter approach is that all the usual restrictions of the Superposition calculus are preserved. In the calculus by Echenim and Peltier (2016) these restrictions must be relaxed to ensure completeness. There is a trade-oﬀbetween these two

16. Which, usually, cannot be (eﬃciently) axiomatized.

Echenim, Peltier & Tourret

features. The experimental comparison shows that the latter approach seems to outperform the ﬁrst one, at least for ground ﬂat clauses (see Echenim et al., 2015; Tourret, 2016).

7.4 Future Work

The most promising direction in which to pursue the work presented in this paper is to implement a version of c SP based on a state-of-the-art equational theorem prover such as the E theorem prover to beneﬁt from all the clever improvements it contains. The extension of the implementation to the non-ground case also deserves to be considered. Furthermore, our redundancy detection algorithms could be extended to handle variables17. Finally, the method could be extended to handle reasoning modulo theories. Two approaches can be considered. The ﬁrst one consists in adding new axioms or inference rules to handle the theory-speciﬁc symbols, as done by, e.g., Waldmann (2001) for totally ordered divisible abelian groups. The other approach consists in handling theory reasoning within the constraints, as done by, e.g., Althaus et al. (2009), Baumgartner and Waldmann (2013), and using an external SMT solver to suggest simpliﬁcations, equivalences and abductive hypotheses for the terms of the considered theory.

Acknowledgments

The authors would like to thank the reviewers, for their insightful comments, as well as the creators of the external tools that were used during the experiments, for making them available. Sophie Tourret gratefully acknowledges ﬁnancial support from the National Institute of Informatics in Tokyo, Japan, at the time the paper was written, and from the University Grenoble Alpes, LIG, in Grenoble, France, at the time the research was conducted.

Althaus, E., Kruglov, E., & Weidenbach, C. (2009). Superposition modulo linear arithmetic SUP(LA). In Ghilardi, S., & Sebastiani, R. (Eds.), Proceedings of the 7th International Symposium on Frontiers of Combining Systems, Vol. 5749 of Lecture Notes in Artiﬁcial Intelligence, pp. 84 99. Springer.

Armando, A., Bonacina, M. P., Ranise, S., & Schulz, S. (2009). New results on rewrite-based satisﬁability procedures. ACM Transactions on Computational Logic, 10(1), 1 51.

Baader, F., & Nipkow, T. (1998). Term Rewriting and All That. Cambridge University Press.

Bachmair, L., & Ganzinger, H. (1994). Rewrite-based equational theorem proving with selection and simpliﬁcation. Journal of Logic and Computation, 3(4), 217 247.

Bachmair, L., Ganzinger, H., & Waldmann, U. (1994). Refutational theorem proving for hierarchic ﬁrst-order theories. Applicable Algebra in Engineering, Communication and Computing, 5, 193 212.

17. Note however that the entailment relation is undecidable for non-ground clauses, even without equality (Schmidt-Schauss, 1988).

Prime Implicate Generation in Equational Logic

Barrett, C., Fontaine, P., & Tinelli, C. (2015). The SMT-LIB standard: Version 2.5. Tech. rep., Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.

Baumgartner, P., & Waldmann, U. (2013). Hierarchic superposition with weak abstraction. In Bonacina, M. P. (Ed.), Proceedings of the 24th International Conference on Automated Deduction, Vol. 7898 of Lecture Notes in Computer Science, pp. 39 57. Springer.

Bienvenu, M. (2007). Prime implicates and prime implicants in modal logic. In Proceedings of the 22nd National Conference on Artiﬁcial Intelligence, Vol. 1, pp. 379 384. AAAI Press.

Blackburn, P., Van Benthem, J., & Wolter, F. (2007). Handbook of Modal Logic. Studies in logic and practical reasoning. Elsevier.

Bonacina, M. P., & Echenim, M. (2010). Theory decision by decomposition. Journal of Symbolic Computation, 45(2), 229 260.

Cimatti, A., Griggio, A., & Sebastiani, R. (2011). Computing small unsatisﬁable cores in Satisﬁability Modulo Theories. Journal of Artiﬁcial Intelligence Research, 40, 701 728.

Cruanes, S. (2014). Logtk: a logic toolkit for automated reasoning and its implementation. In 4th Workshop on Practical Aspects of Automated Reasoning.

Darwiche, A., & Marquis, P. (2002). A knowledge compilation map. Journal of Artiﬁcial Intelligence Research, 17, 229 264.

De Kleer, J. (1992). An improved incremental algorithm for generating prime implicates. In Proceedings of the National Conference on Artiﬁcial Intelligence, pp. 780 780. John Wiley & Sons ltd.

De Moura, L. M., & Bjorner, N. (2007). Eﬃcient E-matching for SMT solvers. In Pfenning, F. (Ed.), Proceedings of the 21st International Conference on Automated Deduction, Vol. 4603 of Lecture Notes in Computer Science, pp. 183 198. Springer.

Dershowitz, N. (1979). Orderings for term-rewriting systems. In Proceedings of the 20th Annual Symposium on Foundations of Computer Science, pp. 123 131, Washington, DC, USA. IEEE Computer Society.

Dershowitz, N., & Manna, Z. (1979). Proving termination with multiset orderings. Communications of the ACM, 22(8), 465 476.

Dillig, I., & Dillig, T. (2013). Explain: a tool for performing abductive inference. In Proceedings of the 25th International Conference on Computer Aided Veriﬁcation, Lecture Notes in Computer Science, pp. 684 689. Springer.

Dillig, I., Dillig, T., Mc Millan, K. L., & Aiken, A. (2012). Minimum satisfying assignments for SMT. In Madhusudan, P., & Seshia, S. A. (Eds.), Computer Aided Veriﬁcation, No. 7358 in Lecture Notes in Computer Science, pp. 394 409. Springer.

Echenim, M., & Peltier, N. (2012). A calculus for generating ground explanations. In Proceedings of the 6th International Joint Conference on Automated Reasoning, Vol. 7364 of Lecture Notes in Computer Science, pp. 194 209. Springer.

Echenim, Peltier & Tourret

Echenim, M., Peltier, N., & Tourret, S. (2013). An approach to abductive reasoning in equational logic. In Proceedings of the 23d International Joint Conference on Artiﬁcial Intelligence, pp. 531 537. AAAI Press.

Echenim, M., & Peltier, N. (2012). An instantiation scheme for Satisﬁability Modulo Theories. Journal of Automated Reasoning, 48(3), 293 362.

Echenim, M., & Peltier, N. (2016). A Superposition calculus for abductive reasoning. Journal of Automated Reasoning, 57(2), 97 134.

Echenim, M., Peltier, N., & Tourret, S. (2014). A rewriting strategy to generate prime implicates in equational logic. In Proceedings of the 7th International Joint Conference on Automated Reasoning, pp. 137 151. Springer.

Echenim, M., Peltier, N., & Tourret, S. (2015). Quantiﬁer-free equational logic and prime implicate generation. In Proceedings of the 25th International Conference on Automated Deduction, pp. 311 325. Springer.

Eiter, T., & Gottlob, G. (1995). The complexity of logic-based abduction. Journal of the ACM, 42(1), 3 42.

Fredkin, E. (1960). Trie memory. Communications of the ACM, 3(9), 490 499.

Ganzinger, H., & Korovin, K. (2003). New directions in instantiation-based theorem proving. In Proceedings of the 18th IEEE Symposium on Logic in Computer Science,(LICS 03), pp. 55 64. IEEE Computer Society Press.

Ge, Y., & Moura, L. M. D. (2009). Complete instantiation for quantiﬁed formulas in Satisﬁability Modulo Theories. In Bouajjani, A., & Maler, O. (Eds.), Proceedings of the 21st International Conference on Computer Aided Veriﬁcation, Vol. 5643 of Lecture Notes in Computer Science, pp. 306 320. Springer.

Inoue, K. (2016). Meta-level abduction. If Co Log Journal of Logics and their Applications, 3(1), 7 35.

Iwanuma, K., Nabeshima, H., & Inoue, K. (2009). Toward an eﬃcient equality computation in connection tableaux: a modiﬁcation method without symmetry transformation a preliminary report . Proceedings of the international workshop on First-order Theorem Proving, 556, 19.

Jackson, P. (1992). Computing prime implicates incrementally. In Proceedings of the 11th International Conference on Automated Deduction, pp. 253 267. Springer.

Jouannaud, J., & Kirchner, C. (1991). Solving equations in abstract algebras: a rule based survey of uniﬁcation. In Lassez, J.-L., & Plotkin, G. (Eds.), Essays in Honor of Alan Robinson, pp. 91 99. The MIT-Press.

Kean, A., & Tsiknis, G. (1990). An incremental method for generating prime implicants/implicates. Journal of Symbolic Computation, 9(2), 185 206.

Knill, E., Cox, P. T., & Pietrzykowski, T. (1993). Equality and abductive residua for Horn clauses. Theoretical Computer Science, 120(1), 1 44.

Leitsch, A. (1997). The resolution calculus. Texts in Theoretical Computer Science. Springer.

Prime Implicate Generation in Equational Logic

Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artiﬁcial Intelligence, 163(2), 203 232.

Marquis, P. (1991). Extending abduction from propositional to ﬁrst-order logic. In Proceedings of the International Workshop on Fundamentals of Artiﬁcial Intelligence Research, pp. 141 155. Springer.

Marquis, P. (2000). Consequence ﬁnding algorithms. In Handbook of Defeasible Reasoning and Uncertainty Management Systems, pp. 41 145. Springer.

Matusiewicz, A., Murray, N. V., & Rosenthal, E. (2009). Prime implicate tries. In Giese, M., & Waaler, A. (Eds.), Proceedings of the 18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 250 264. Springer.

Matusiewicz, A., Murray, N. V., & Rosenthal, E. (2011). Tri-based set operations and selective computation of prime implicates. In Kryszkiewicz, M., Rybinski, H., Skowron, A., & Ra s, Z. W. (Eds.), Proceedings of the 19th International Symposium on Methodologies for Intelligent Systems, pp. 203 213. Springer.

Mayer, M. C., & Pirri, F. (1993). First order abduction via tableau and sequent calculi. Logic Journal of the IGPL, 1(1), 99 117.

Mc Cune, W. (2005 2010). Prover9 and Mace4. http://www.cs.unm.edu/~mccune/ prover9/.

Mishchenko, A. (2001). An introduction to zero-suppressed binary decision diagrams. Tech. rep., In Proceedings of the 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning.

Nabeshima, H., Iwanuma, K., Inoue, K., & Ray, O. (2010). SOLAR: an automated deduction system for consequence ﬁnding. AI Communications, 23(2), 183 203.

Ngair, T. (1993). A new algorithm for incremental prime implicate generation. In Proceedings of the 13th International Joint Conference on Artiﬁcial Intelligence, Vol. 1, pp. 46 51. Morgan Kaufmann Publishers Inc.

Nieuwenhuis, R., & Rubio, A. (2001). Paramodulation-based theorem proving. In Robinson, J. A., & Voronkov, A. (Eds.), Handbook of Automated Reasoning, pp. 371 443. Elsevier and MIT Press.

Patel-Schneider, P. F., Hayes, P., Horrocks, I., et al. (2004). OWL web ontology language semantics and abstract syntax. W3C recommendation, 10.

Previti, A., Ignatiev, A., Morgado, A., & Marques-Silva, J. (2015). Prime compilation of non-clausal formulae. In Proceedings of the 24th International Conference on Artiﬁcial Intelligence, pp. 1980 1987. AAAI Press.

Quine, W. (1955). A way to simplify truth functions. The American Mathematical Monthly, 62(9), 627 631.

Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the ACM, 12, 23 41.

Rougny, A., Yamamoto, Y., Nabeshima, H., Bourgne, G., Poupon, A., Inoue, K., & Froidevaux, C. (2015). Completing signaling networks by abductive reasoning with pertur-

Echenim, Peltier & Tourret

bation experiments. In Proceedings of the 25th International Conference on Inductive Logic Programming.

Schmidt-Schauss, M. (1988). Implication of clauses is undecidable. Theoretical Computer Science, 59(3), 287 296.

Schulz, S. (2013). System Description: E 1.8. In Mc Millan, K., Middeldorp, A., & Voronkov, A. (Eds.), Proceedings of the 19th International Conference on Logic for Programming, Artiﬁcial Intelligence and Reasoning, Stellenbosch, Vol. 8312 of Lecture Notes in Computer Science, pp. 735 743. Springer.

Simon, L., & Del Val, A. (2001). Eﬃcient consequence ﬁnding. In Proceedings of the 17th International Joint Conference on Artiﬁcial Intelligence, pp. 359 370.

Sutcliﬀe, G. (2009). The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. Journal of Automated Reasoning, 43(4), 337 362.

Tison, P. (1967). Generalization of consensus theory and application to the minimization of boolean functions. IEEE Transactions on Electronic Computers, EC-16(4), 446 456.

Tourret, S. (2016). Prime Implicate Generation in Equational Logic. Ph.D. thesis, Ecole Doctorale MSTII, Grenoble Alpes University.

Voronkov, A. (1995). The anatomy of Vampire: Implementing bottom-up procedures with code trees. Journal of Atomated Reasoning, 15 (2), 237 265.

Waldmann, U. (2001). Superposition and chaining for totally ordered divisible abelian groups. In Gor e, R., Leitsch, A., & Nipkow, T. (Eds.), Proceedings of the 1st International Joint Conference of Automated Reasoning, Vol. 2083 of Lecture Notes in Computer Science, pp. 226 241. Springer.

Weidenbach, C., Afshordel, B., Brahm, U., Cohrs, C., Engel, T., Keen, E., Theobalt, C., & Topic, D. (2001). System description: SPASS version 1.0.0. In Proceedings of the 16th International Conference on Automated Deduction, Lecture Notes in Computer Science, pp. 378 382. Springer.