Prime Implicate Generation in Equational Logic (extended abstract)

1 Introduction andMotivations

Abductive reasoning is the process of inferring, given a set of axioms A and a formula φ, a set of assertions H such that A ∪ H |= φ. The set H may be viewed as a set of hypotheses that are sufficient to ensure the validity of the entailment A |= φ, or as a set of explanations of φ. Such hypotheses must be economical and plausible, in particular H must be minimal w.r.t. logical entailment and A ∪ H must be satisfiable. Abductive reasoning has many applications in artificial intelligence, verification and debugging, e.g. for computing missing pre-conditions, spotting and correcting errors in a logical specification, or for dealing with approximative, incomplete or spurious information. The problem has been thoroughly investigated in propositional logic [Marquis, 2000], and very efficient algorithms have been proposed [Simon and Del Val, 2001; Previti et al., 2015], but only a few approaches handle more expressive logics [Knill et al., 1993; Marquis, 1991; Mayer and Pirri, 1993; Nabeshima et al., 2010]. In particular, none of them is able to deal with the equality predicate in an efficient way.

In the present paper, we tackle the problem of generating such a set H, when A ∪ {φ} is a set of first-order formulas with equality and H is a set of ground unit clauses. In this case, by duality, ¬H is a clausal logical consequence of A∪ {¬φ}, i.e., an implicate of A∪ {¬φ}, and the problems boils down to efficiently generating sets of (entailment-minimal) implicates or prime implicates.

We illustrate our approach by an example in verification. Consider the following toy program, redirecting the tail of a

∗This paper is an extended abstract of an article in the Journal of Artificial Intelligence Research [Echenim et al., 2017].

Algorithm 1: Example(List l1, List l2)

• 1 requires length(l1) ̸= 0;
• 2 requires length(l2) = 1;
• 3 let l1.tail = l2 ;
• 4 ensures length(l1) = 2;

nonempty list l1 to a list l2 of length 1. Assume we want to check that l1 is of length 2 after the program is executed. This post-condition does not hold, which may come as a surprise for some programmers. Indeed, if l1 = l2, then the tail of l1 is redirected to l1 yielding a cyclic list (hence length(l1) is either 1 or undefined, depending on the definition). The problem can be stated in first-order logic with equality as the following set of clauses S, where the tail function is represented by a function tail : heap × list → list, and where h, h′ : heap are constant symbols denoting the initial and final states of the heap and x, y : list, z : heap are universally quantified variables.

%Definition of the tail redirection operation % The tail of x is redirected to y: x ≃ nil ∨ tail(SetT ail(z, x, y), x) ≃ y % The tail of the other lists is not affected by the redirection: x ≃ nil ∨ x′ ≃ nil ∨ x′ ≃ x ∨tail(SetT ail(z, x, y), x′ ) ≃ tail(z, x′ ) %Definition of length length(z, nil) ≃ 0 x ≃ nil ∨ length(z, x) ≃ s(length(z, tail(z, x))) % Pre-conditions length(h, l1) ̸≃ 0 length(h, l2) ≃ s(0) % Negation of the post-condition length(h′ , l1) ̸≃ s(s(0)) % Translation of the program

h′ = SetTail(h, l1, l2)

The set S is satisfiable, the problem is to show that S is unsatisfiable under the hypothesis l1 ̸≃ l2, or equivalently that l1 ≃ l2 is an implicate of S.

2 Normalized Ground Clauses

Terms, atoms, literals and clauses are defined inductively as usual over a set of function symbols Σ and variables V. We assume, w.l.o.g., that the equality ≃ is the only predicate symbol. We use the symbol ▷◁ to denote either ≃ or ̸≃. Substitutions are functions mapping variables to terms, extended to any expression (terms, atoms, clauses, etc.) in the natural way and written in postfix notation. We assume given a reduction order ≻, i.e., an order among terms that is closed under substitution and context embedding, and contains the subterm ordering (this entails that ≺ is well-founded). The order ≺ is extended to atoms or literals by interpreting them as multisets of terms, and to clauses by the usual multiset extension. For any expression E, we denote by Ec the nnf of the negation of E, formally defined as follows: (s ≃ t)c = s ̸≃ t, (s ̸≃ t)c = t ≃ s, (∨ni=1 li)c = ∧ni=1 li c and (∧ni=1 li)c = ∨ni=1 li c .

Definition 1 Given a clause C, we define the relation ≡C on terms as follows: for all terms s, t, s ≡C t iff C c |= s ≃ t. The C-representatives of a term s, literal l and clause l1 ∨ · · · ∨ ln are respectively defined by:

Definition 2 A ground clause C is normalized if:

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.

A conjunction of literals X is normalized if the clause X c is normalized.

Proposition 3 Any ground falsifiable clause C admits a unique equivalent normalized clause C↓, which is the ≺- smallest clause equivalent to C. Consequently, two clauses are equivalent iff either they are both tautological or they have the same normalized form.

3 AConstrained Superposition Calculus

This section contains the definition of the calculus for generating implicates, named cSP. It is based on the Superposition Calculus SP (see for instance [Nieuwenhuis and Rubio, 2001]) which is the most successful proof procedure for first-order logic with equality. The principle underlying cSP consists in applying 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. To keep track of the hypotheses that were used to derive a clause, the former are attached to the clauses as constraints. This yields the following definition:

Definition 4 A constraint is a conjunction (or set) of ground literals. The empty (tautological) constraint is denoted by ⊤. 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. Intuitively X denotes the set of hypotheses used to derive C. If C is empty, then [C |X] is equivalent to X c , and X c is an

implicate of the clause set under consideration.

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σ;

Figure 1: Inference Rules for cSP.

The set of inference rules defining cSP are given in Figure 1. The notation u[t] is used to denote a term containing a subterm t (u denotes the context). We may then write u[s] to denote a term obtained from u[t] by replacing t by s. The symbol ▷◁ (≃ or ̸≃) must denote identical symbols in the premise and in the conclusion of the rule. The rules are parameterized by the order ≺ and by:

• A selection function sel that maps every clause C to a set of selected literals in C. The set sel(C) must contain all ≻-maximal literals or at least one negative literal.
• A set of normalized constraints X, closed under subset. Intuitively X denotes the set of abductible formulas, i.e., formulas that are allowed to be added as hypotheses.

The use of ≻ and sel is standard, it aims at pruning the search space by restricting inferences, whereas the set X allows one to control the addition of hypotheses into the search space. The reader may consult [Nieuwenhuis and Rubio, 2001] for missing definitions and more details about the superposition calculus.

A crucial feature of the Superposition calculus is the availability of a general criterion for detecting redundant clauses. In SP, a clause is considered redundant if all its instances are entailed by ≺-smaller instances of existing clauses. The definition for cSP is similar, with two differences: first the constraints of the entailing clauses must be included in that of the considered clause, and second the literals occurring in this constraint can also be used in the entailment test, provided they are smaller than the considered clause. Formally:

Definition 5 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 unsatisfiable 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 , and
• X|⪯Cσ,D1θ1, . . . ,Dnθn |= Cσ.

A set of c-clauses S is cSP-saturated if every c-clause deducible by the rules of cSP in one step is redundant w.r.t. S. A cSP-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 finite number of applications of the rules in cSP, (iii) S∗ is cSP-saturated.

The following theorem states the soundness and deductive completeness of cSP.

Theorem 6 Let S be a set of standard clauses and S∗ be a cSP-saturation of S. For every X ∈ X, X c is an implicate of S iff S∗ contains a c-clause of the form [2|X ′ ] with X ′ ⊆ X .

4 On the Storage of Implicates

Sets of implicates are huge, thus being able to store those sets in a compact way and to detect redundant implicates efficiently is a critical feature. We begin by devising an efficient algorithm for testing entailment between ground equational clauses.

Definition 7 Let C, D be two falsifiable ground clauses. The clause D E-subsumes C, written D ≤E C, iff the two following conditions hold:

1. for every negative literal t ̸≃ s ∈ D, t⇂C- = s⇂C-;
2. for every positive literal l ∈ D, there exists a positive literal m ∈ C such that m⇂C-∨lc is a tautology.

Theorem 8 Let C and D be two ground clauses. If C and D are falsifiable, then D |= C iff D ≤E C.

Based on the entailment test of Definition 7, we define a trie-like data structure to store implicates and algorithms to remove redundancy inspired from [De Kleer, 1992]. A clausal tree is a tree whose edges are labeled by literals and whose leaves are labeled by either ⊥ or ⊤. Each path from the root of the tree to a leaf can be associated with a clause defined as the disjunction of all the literals labeling the edges along the path. The set of clauses associated with the tree is the set of clauses associated with a path from the root to a ⊤-leaf. This representation ensures that the prefixes of the clauses will be shared, thus reducing the amount of consumed memory. Note that the edges pointing to a ⊥-leaf are useless and may be deleted (a node with no successor may be labeled by ⊥).

We consider a total ordering <π on ground literals, defined as follows: if l1 is a negative literal and l2 is a positive literal then l1 <π l2, and if l1, l2 are literals with same polarity then l1 <π l2 iff l1 ≺ l2. To enforce maximal sharing and minimize the size of the tree, we assume that the literals occurring along a path in the tree are ordered w.r.t. <π, i.e., for any path e1, . . . , en in the tree, if e1, . . . , en are edges labeled by literals l1, . . . , ln respectively, then l1 <π . . . <π ln.

When a new implicate C is generated, we need to test whether it is a consequence of a previously generated implicate (forward subsumption). If this is the case, then C is redundant and can be dismissed, otherwise we need to delete in the clausal tree all branches corresponding to an implicate that is a logical consequence of C (backward subsumption). We briefly sketch algorithms for performing these two tasks. The formal definitions of the algorithms can be found in [Echenim et al., 2017] together with detailed proofs of their properties.

Forward Subsumption. Beside the new generated clause C and the clausal tree T, we also consider two input clauses N and M that are both initially empty. The clause N contains the literals occurring in the parent nodes in the recursive calls and the clause M permits to keep track of the negative literals of C in recursive calls after having used them a first time to rewrite literals in the tree.

The algorithm is based on a depth-first traversal of the tree which is best described as a non-deterministic recursive algorithm. The algorithm returns true if the tree contains a single node labeled by ⊤ (representing the empty clause) and backtracks if the tree is not ⊤ and C = 2 (base cases). Otherwise, an edge e starting from the root of the tree is chosen. Let l be the literal labeling e and let T ′ be the subtree pointed by e:

• If it is clear that l |= M ∨ C, then we add l into N and we proceed to 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).
• If the relation between l andM∨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 corresponding to e.
• 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 algorithm backtracks.

Backward Subsumption. This handles the removal from a clausal tree T of all the clauses D that are E-subsumed by a given c-clause C, under the assumption that C itself is not subsumed by a clause stored in T. As the previous one, the algorithm performs a depth-first traversal of T with a rewriting of literals. The main difference is that the roles of C and T are switched: the literals of a branch of T are rewritten using the negative literals of C. When the subsumption test succeeds, the algorithm cuts the corresponding branch in T before exploring the remaining branches.

5 Experimental Results

Our prime implicate generation method has been implemented in a research prototype called cSP, written in OCaml, based on the LogTk library [Cruanes, 2014] for term ordering and congruence closure. We also implemented another version of the program, called cSP flat, that only handles flat clauses, i.e., clauses not containing function symbols of an arity strictly greater than 0, with additional refinements that only apply to this fragment.

We compared cSP and cSP flat with the most efficient available systems for generating implicates of logical formulas, namely primer [Previti et al., 2015] and Zres [Simon and Del Val, 2001], two propositional prime implicate generation tools based on satisfiability encoding and resolution respectively, and SOLAR [Iwanuma et al., 2009], a prime implicate generation tool for first order logic based on semantic tableaux. Equality is not built-in in these systems, thus the equality axioms had to be added into the considered formula: reflexivity, commutativity, transitivity and substitutivity. For Zres and primer, these axioms must also be grounded and transformed into propositional logic by flattening.

We compared the systems on two randomly generated sets of (flat and non-flat respectively) equational ground clauses of small size. Figure 2 compares the execution time of cSP on the random flat benchmark with that of cSP flat and primer. It shows that cSP flat is the most suitable tool to handle such problems.

Table 1 compares Zres, primer and SOLAR with cSP flat and cSP on the random non-flat benchmark. For each system, we isolate the benchmarks for which the system is able to generate all implicates, and we specify for all systems the failure rate on those benchmarks (i.e., the percentage of formulas for which the system is not capable of generating all implicates in the allocated time, namely 5 min.), the time needed to generate all prime implicates in case of success, the number of inferences and the number of implicates generated. As shown in the 'successes' column, cSP is the obvious winner in terms of the number of tests handled before timeout.

More detailed experimental results are presented in [Echenim et al., 2017].