Equality Elimination for the Inverse Method and Extension Procedures

1 The inverse method

The inverse method of theorem proving in sequent cal­ culi has been proposed by Maslov in the 1960s. The method is based on the bottom-up 1 search in sequent calculi. The inverse method is completely local [Maslov and Mints, 1983; Degtyarev and Voronkov, 1994b] and can be efficiently implemented both for classical and non­ classical logics [Voronkov, 1992]. In terms of efficiency, it is competitive with resolution 2 · The inverse method requires no normal forms which can be an advantage for interactive provers.

The introduction of equality in the inverse method has not yet received proper attention. In this paper we

· Supported by a grant from the Swedish Institute.

ton leave from Kiev University.

*Supported by a TFR grant .

1 Bottom-up search means the search from axioms to the goal.

2 In fact, the inverse method can be simulated by res­ olution using structure-preserving clause-form translation [Maslov, 1983; Boy de la Tour, 1990].

Andrei Voronkovt

Computing Science Department Uppsala University Box 311, S-751 05 Uppsala, Sweden

consider the inverse method with equality. Our approach is based on equality elimination.

The structure of this paper is the following. In this section we briefly discuss introduction of equality in the inverse method in general. In Section 2 we introduce main definitions and notation. In Section 3 we define the equality elimination method and give several exam­ ples. In Section 4 we show how one can generalize our technique to the connection method.

The first natural generalization of the inverse method to include equality has been made by Maslov [Maslov, 1971]. It was based on theorems proven in [Kanger, 1983; Lifschitz, 1968] about the specialization of proofs in the sequent calculus with equality (but without free vari­ ables!) . According to these theorems, all equality rea­ soning steps can be moved on top of the proof so that they precede all other steps. This gives the characteri­ zation of the inverse method with equality which in fact coincides with hyperresolution (on classical logic), but with a different initial set of clauses (closed collections in Maslov's terminology). While in the inverse method without equality the initial sequents correspond to ax­ ioms of the sequent calculus, in the equality case initial sequents are those derivable from axioms exclusively by equality rules. [Kanger, 1983] called such sequents "di­ rectly demonstratable" . In later papers the role of these sequents play (instantiated} equational mated sets [Gal­ lier, 1992] or £-complementary eq-connections [Bibel, 1987]. We call their analog solution clauses.

Let us come back to results on the specialization of se­ quent proofs. Is it possible to generalize these results on proofs with free variables (metavariables in Maslov's ter­ minology)? In this case equality rules become paramod­ ulation rules. Direct lifting from the ground case is now impossible without functional reflexivity axioms. As we shall show, the use of free variables is possible both for the traditional formulation of the inverse method and for the formulation proposed in our paper.

In the original presentation of the inverse method by Maslov, unification has been made by using arbitrary (not only most general} substitutions which made lifting from the ground case unnecessary 3 · Even in the paper

3 1n terms of resolution, such a treatment of unification gives unrestricted resolution [Lloyd, 1987] - a calculus with too high non-determinism.

[Maslov and Mints, 1983] evaluated in [Lifschitz, 1989] as a "very clean explanation of the inverse method" it was only noted that "likewise the definition of a most general unifier, at each step one could select minimal substitutions". However, the proof of completeness in the [Maslov and Mints, 1983] reformulation of the in­ verse method is made using unrestricted substitutions given by an arbitrary saturation of the Herbrand uni­ verse. Arbitrary substitutions are also used in [Lifschitz, 1989] where the most general unifiers are only used for factoring.

An alternative approach would be to take into ac­ count the results of [Kanger, 1983; Lifschitz, 1968] on the specialization of sequent proofs. These results allow one to restrict oneself to simultaneous paramodulation only. "Simultaneous" means that in the application of the equality rules from the conclusion to the premise all occurrences of the "into-term" are replaced by the "from-term". As it has been shown in [Benanav, 1990], for simultaneous paramodulation lifting is possible with. out the functional reflexivity axioms.

We do not, however, use simultaneous paramodulation here. Instead, we use very refined strategies of dealing with equality - orderings, basic restriction and selec­ tion function. It happens that these severe restrictions on the equality part of the proof is enough to preserve completeness using most general unifiers.

Our method is also directly applicable to so called "ex­ tension procedures" [Prawitz, 1983], including tableaux methods [Fitting, 1990; Degtyarev and Voronkov, 1994b], mating or connection methods [Andrews, 1986; Bibel, 1987; Degtyarev and Voronkov, 1995] and their generalization - consolution [Eder, 1991]. We shall il­ lustrate such an application of our method in Section 4.

The major difference of our treatment of equality rea­ soning for the connection method is that instead of checking paths through an extension of the input formula for E-complementarity (i.e. for the existence of a rigid E-unifier) we first generate a set of E-complementary paths using ordinary unification, and then look for an appropriate extension. Thus, we split extension proce­ dures into two separate processes: equality elimination and search for an extension. The two processes are con­ nected by solution clauses generated in the equality elim­ ination part. This allows us to use strong sides of both equality reasoning methods known so far and extension procedures.

2 Preliminaries

We present here a brief overview of notions and prelimi­ nary definitions necessary for the paper. We assume the basic knowledge of substitutions and unification.

Let E be a signature and X a set of variables. T(E, X) will denote the set of all terms in the signature E with variables from X.

A literal is either an atomic formula or a negation of an atomic formula. We shall always write s of; t for the literal ...,(s = t) . .

A clause is a finite set { £1, ... , Ln} of literals, de­ noted £ 1 , ... , Ln. If L is a literal, C a clause, L, C will denote the clause { L} U C. An equation is an expression s = t, where s, t E T(E, X). By a ground expression (i.e. term, equation, clause etc.) we mean an expression con­ taining no variables. We write A[s] to indicate that an expression A contains s as a subexpression and denote by A[t] the result of replacing particular occurrences of s in A by t. By Aa we denote the result of applying the substitution a to A.

We shall sometimes denote tuples of equations s1 = t1, · ·· , Sn = tn by 8 = f. The over bar notation f can also be used to denote sequences of terms. Substitu­ tions (} with the domain x1, ... , Xn will be denoted by [x10/x1, ... ,xnO/xn]·

Let >- be a partial ordering on T(E, X). It is called a reduction ordering iff

1. >- is well-founded;
2. if s >- t then u[sa] >- u[ta], for all terms s, t, u and substitutions a.

We assume that reduction orderings are total on ground terms of T(E, X) .

Following [Bachmair et al., 1992] we distinguish terms occurring in the original formula from terms introduced by substitution by using closures, i.e. pairs C ·a, where C is a clause, a a substitution. The clause C will often be identified with the closure C · c, where c is the empty substitution. For any expression E, the set Var(E) is defined as the set of all variables occurring in E. Two closures cl . al and c2 . a2 are variants iff cl is a variant of C2 and C1a1 is a variant of C2a2.

When we use notation f= or 1-, they state for truth and provability in classical first order logic with equality, respectively.

A formula is in skolemized negation normal form iff it is constructed from literals using connectives/\, V and the quantifier 3. There is a structure-preserving trans­ lation of formulas without equivalences into formulas in skolemized negation normal form with the same number of occurrences of atoms.

3 The equality elimination method

For the rest of this section we assume that 'Y is a closed formula in skolemized negation normal form to be proven (the "goal"). We assume that all different occurrences of quantifiers in 'Y bind different variables. For exam­ ple, 'Y cannot have the form 3xA V 3xB. All formulas in this section are assumed to be sub formulas of "(. We shall identify subformulas and superformulas with their occurrences in 'Y· For example, in the formula 'Y of the form A 1\ (A VB) the second occurrence of A is consid­ ered a subformula of (A VB), but the first occurrence of A is not. The occurrence of a subformula cp of "( is called conjunctive iff it is the occurrence in a subformula cp 1\ t/J or in t/J 1\ cp. A conjunctive superformula of cp is a superformula 4 t/J of cp that is conjunctive. The least conjunctive superformula of cp is the conjunctive super­ formula t/J of cp such that any other conjunctive super­ formula of cp is a superformula of t/J. Let us note that conjunctive superformulas do not necessarily exist. For example, 'Y has no conjunctive superformula. Any for­ mula having a conjunctive superformula has the unique least conjunctive superformula.

4 tp is a superformula of '1/J iff '1/J is a subformula of tp (not necessarily proper).

We can enumerate all conjunctive subformulas "(1 , ... , 'Yn of 'Y, for example in the order of their occur­ rences in 'Y· Thus we can unambiguously use "the kth conjunctive (sub)formula" 'Yk of 'Y·

Let A1 , ... , An be a set of predicate symbols not oc­ curring in 'Y· We say that Ak (x1, ... , Xm) is the "(-name for a subformula cp of 'Y iff

1. The least conjunctive superformula of cp is 'Yk.
2. x1 , . . . , Xm are all free variables of 'Yk in the order of their occurrences in 'Yk.

If a "(-name of a formula cp exists, then it is unique. Note that different formulas may have the same "(-names. Also note that some subformulas of 'Y do not have "(-names. We can use the set of "(-names of a subformula. The set of -y-names of a formula cp is either 0 or a singleton {Ak(X1 , .. . , Xm)}.

The following example illustrates least conjunctive su­ performulas and "(-names:

Example 3.1 Let 'Y be the formula

All subformulas of 'Y and their "(-names are shown in Figure 1 at the end of this paper.

Lemma 3.1 Let cp be a subformula of 'Y· Then

1. If 1/J is the least conjunctive superformula of cp then F V(cp :::> 1/J) .
2. If there is no conjunctive superformula of cp then f=V(cp:::>"f).

This lemma partially explains the need for introducing least conjunctive superformulas. There are deterministic chains of inferences in sequent systems, where formulas with V or 3 occur. For example,

By restricting ourselves to conjunctive superformulas only, we eliminate these deterministic chains, making them in one step. 5

Now we can formulate our deductive system for the inverse method. The proof-search consists of two parts:

5 This simple but powerful idea of restricting to con­ junctive superformulas (see [Voronkov, 1992]) has been suc­ cessfully implemented in the theorem prover described in [Voronkov, 1990] and in a theorem prover for intuitionistic logic implemented by T. Tammet (private communications). In the framework of tableau theorem proving there were many papers using the idea of permutability of inference rules in sequent calculi (see e.g. [Shankar, 1992]}. In fact, the least conjunctive superformula of rp is a superformula t/J of rp prov­ able from rp and such that all inference rules applied in the proof of t/J from rp are permutable with all other rules. The use of conjunctive superformulas allows one to get rid of non­ conjunctive subformulas before the proof-search, unlike the dynamic use of permutabilities as in [Shankar, 1992].

the equality solution part and the sequent proof part. We encode formulas by their "(-names. Then sequents (i.e. sets of formulas) become clauses (i.e. sets of literals, obtained as the union of corresponding sets of "(-names). In the first part of the proof, we try to solve equalities in the formula, generating a set of closures not containing equality. A closure not containing equality will be called a solution clause. Solution clauses C · u will always be written in the ordinary clause notation, i.e. as Cu. This set of solution clauses is obtained by basic superposi­ tion from initial closures defined below. In the second part, the usual sequent style proof search by the inverse method is performed. The solution clauses generated in the first part are used as the initial clauses in the se­ quent part. Hence the name "equality elimination" for our method: we eliminate equality in the first part of the proof.

Initial closures are generated according to one of the three rules:

1. Whenever a literal s =/: t occurs in 'Y and C is the set of "(-names for this occurrence of 8 =/: t, the closure 8 = t, C · c is an initial closure.
2. Whenever s = t occurs in 'Y and C is the set of "(-names for this occurrence of s = t, the closure 8 =/: t, C · c is an initial closure.
3. Let literals P(8I , ... , sn) and -.P(t1, ... , tn), where P is different from =, occur in 'Y and where C1,C2 are their sets of "(-names. Let the substi­ tution u rename variables such that variables of P( 81, ... , 8n)u, cl (7 and P(tl, ... , tn), c2 are dis­ joint. Then the closure 81U =/: t1, .. . , snu =/: tn, C1u, C2 ·cis an initial closure.

The equality elimination method consists of five infer­ ence rules. The basic superposition rules are defined as in [Bachmair et al., 1992]. We always assume that premises of rules have disjoint variables (this can be .achieved by using variants) . The first three rules derive closures from the initial closures defined above. Applications of the first three rules form the equational solution part of the proof. The aim of the equational solution part of the proof is to generate solution clauses that are used as axioms of the sequent part of the proof. The sequent part of the proof uses the last two rules. The aim of the sequent part of the proof is to derive the empty clause.

Basic right superposition

where

1. p is a most general unifier of su1 and s' u2 ;
2. tu1p ;t SU1Pi
3. VU2P ;t u[8 1 ]C72Pi
4. s' is not a variable.

(We call attention to the fact that variables of the premises must be disjoint.)

Basic left superposition

with the same conditions as for basic right superpo­ sition and one additional restriction: u[s'] =F v must be the leftmost disequation in the second premise. 6

Equality solution

where p is a most general unifier of sa, ta and s =F t is the leftmost disequation in the premise.

• Conjunction rule This rule is used in the sequent part of the proof, thus it is only applied to clauses, con­ taining no equality. Let <p 1\ 1/J be a subformula of 7, and N"', N.p and N"'""' be sets of 7-names of <p, 1/J and <p 1\ 1/J, respectively. Let x be all variables of <p 1\ 1/J. Let clauses r, ~ have no occurrences of equality. Then the following is a conjunction rule:

where 0 is a most general unifier of s and f.

• Factoring rule This rule is also used in the sequent part of the proof, thus it is only applied to clauses, containing no equality. Let the clause r, A, B have no occurrences of equality. Then the following is a factoring rule

where 0 is a most general unifier of A, B.

The following theorems are true about the method:

Theorem 3.1 (Soundness) If there is a derivation of the empty clause from the initial closures then 'Y is prov­ able.

Theorem 3.2 (Completeness) If 'Y is provable then there is a derivation of the empty clause from the initial closures.

Proofs of these two theorems may be found in [Degt­ yarev and Voronkov, 1994c].

Consider an example (the formula is taken from [Maslov, 1971]):

Example 3.2 The formula to be proven is

There are two conjunctive sub formulas with the following names:

6 According to our definitions, a clause is a set of literals, so the use of the leftmost disequation is not quite correct, but this restriction can easily be formalized using the selec­ tion mechanism [Bachmair and Ganzinger, 1994]. The proof­ theoretic justification of this possibility is given in [Degtyarev et al., 1995].

The corresponding conjunction rule is

where 0 is a most general unifier of s, t. The initial closures are

4. f(x) =F f(f(y)), A2(x), A1 (y) · c

The first two closures are generated by equations in the goal, the last two by pairs G, --.G.

As the order >- we consider the recursive path ordering with f > b > a. The equality elimination part of the proof consists of applications of basic superposition and equality solution:

5. A2(x) · [bfx] (equality solution from 2)

6. b =F a,A1(x),A1(y),A1(z) · [f(f(y))fx] (left superposition from 1,3)

1. a =F a,A1(x),A1(y),A1(z),A1(v) · [f(f(y))fx,bfv] (left superposition from 1,6)

8. A1(x),A1(y),A1(z),A1(v) · [f(f(y))fx,bfv]

(equality solution from 7)

1. A2(x),A1(y) · [f(y)fx]

(equality solution from 4)

The clauses which can be used in the sequent part of the proof are the following:

The sequent part of the proof only uses the conjunction rule and the factoring rule:

1. A1 (f(f(y))), A1 (y), A1 (b) (factoring from 8')

11. A1(f(f(b))),A1(b)

(factoring from 10)

12. A1(f(f(b))) (conjunction rule from 5',11)

13. A1(f(b)) (conjunction rule from 9',12)

14. A1(b) (conjunction rule from 9',13)

15. D (conjunction rule from 5',14)

There are many optimizations not considered in this paper. The most powerful one is subsumption that can be applied in both parts of the proof in order to prevent generation of unnecessary clauses. Subsumption for the basic strategy has been explained in [Degtyarev, 1982; Bachmair et al., 1992]. In the sequent part of the proof we can use ordinary subsumption, or even a stronger subsumption for sequent proofs proposed in [Voronkov, 1992].

4 The connection method

The equality elimination method is very general and can be applied to other automated reasoning methods, for example the connection method. In order to illustrate it, we consider Example 3.2 in the connection method. We shall refer to definitions and statements from [Gallier, 1992]. The connection method is considered in more detail in [Degtyarev and Voronkov, 1995].

As in [Gallier, 1992], we try to establish unsatisfiability of the negation of the goal formula

Denote the matrix_ of this formula via M ( x). Accord­ ing to Theorems 4.3 and 7.7 of [Gallier, 1992] this for­ mula is inconsistent iff there is a path-acceptable equa­ tional mating for some amplification M(xl)l\ ... 1\M(xn)· Consider the set of vertical paths through this amplifica­ tion. According to Definition 4.4 of [Gallier, 1992], the set of vertical paths vp(A) through amplification A is the set of sets of literals defined inductively as follows:

Denote

From the above definition of vp it follows that the set vp(M(x1) 1\ ... I\ M(xn)) has the form

Note now that the solution clauses used in Example 3.2 define the following set of inconsistent instantiated par­ tial paths:

Indeed, any of these partial paths contains an incon­ sistent instantiated mated set (see [Gallier, 1992]) of M(xl) 1\ ... 1\ M(xn)· For example, for the second of these partial paths it will be the instantiated mated set

The composition of these instantiated mated sets forms an equational mating. It remains to find an instantiated amplification for which this mating is path acceptable. Such amplification can be extracted from the sequent part of the proof. The instantiated amplification for our example is shown in the following picture:

Thus, in this amplification n = 3, x1 = b, x2 = f(J(b)) and xa = f(b) . Note that this tree can be easily changed into a tableau proof of 'Y.

5 Conclusion

The equality elimination method is a general method of reasoning in first-order logic with equality. It is based on the following general version of Herbrand theorem [Degtyarev and Voronkov, 1995]: a formula 'Y is prov­ able iff there is a matrix M of 'Y and a substitution q such that every path through M a contair.s an instance of a solution clause. Equality elimination was origi­ nally introduced in [Degtyarev and Voronkov, 1994a] as a method of handling equality in logic programs. Later, it has been applied to the tableau method [Degtyarev and Voronkov, 1994b] and the connection method [Degtyarev and Voronkov, 1995]. In [Degtyarev et al., 1995] a combi­ nation of equality elimination and basic folding has been introduced which allows to transform equational logic programs into recursive logic programs without equal­ ity.