A Superposition Oriented Theorem Prover

ABSTRACT

A theorem proving procedure is described which combines the approach of locking resolution with that of rewriting systems. Indeed, both the binary resolution and a complete restriction of paramodulation are embodied by an extension of the rewriting operation called superposition. Experimental results are reported and compared with literature automated proofs.

I - INTRODUCTION

We describe in this paper a theorem-proving procedure for first-order logic with equality which combines the approach of locked resolution with that of Term Rewriting Systems .

In 1971, R.S. Boyer introduced a restriction of resolution (without oaranodulation) called "locking" which involves an index ordering of literals within clauses [Bo] . This index ordering restriction was somehow refined and extended to paramodulation under the name of 0 E-resolution by J.A. Loveland [Lo]. Independently in some other works, paramodulation w~s specifically controlled by favoring one direction in the substitution of · equals : a subterm u within a clause can be re­ placed by an equal only if u matches with a cer­ tain side of an equation a=B, for instance a and not B. The concept of demodulation and the equation marking one(atom term locking) have thus been introduced [WR] [La].

In the procedure described herein, we use this notion of unidirectional paramodulation but with an increased selectivity : indeed, the sub­ term u of an equation y=o can be replaced only if u belongs to a certain side of that equation, for instance y and not o. The restriction is developed on the basis of the o 1 E-resolution and has the completeness property.

Its strongly oriented character induces us to consider the restricted paramodulation as a form of superposition (the rewriting operation). We achieve this in using a new formalism of clauses that we call "equational clauses", each literal being converted into an equation. We will show that superposition on to equational clauses embodies not only paramodulation but also binary resolution and will so constitute our major rule of infe­ rence.

L. Fribourg

L.I.T.P 2, Place Jussieu 75251 PARIS Cedex OS France

II - I-ORDERING

The reader is assumed to be familiar with the notions of E-insatisfiability and classical resolu­ tion. In this section, we will summarize the defi­ nitions and results attached to the index ordering deduction by resolution and paramodulation, which is named 0 1 E-deduction in [Lo], and here simply noted as I-deduction.

In I-deduction, a positive integer is assigned to each literal occurrence of the given set S of clauses. Within a clause, literals are disposed from left to right in non- .decreasing index order. Such ordered clauses are called I-clauses. Within an I-clause, only the leftmostoccurrence of identi­ cal literals is retained (merging low rule) and positions among literals of like index are inter­ changeable.

Def : given an I-clause C, if the rightmost literar- L and other literals having the sane index are unifiable with the most general unifier a , an I-factor of C is the I-clause Co obtai­ ned from C by instanciating literals, indexing them as in C and merging them low.

Def: if c 1 : (C' 1 ,L 1 ) and c 2 : (C2,L 2 ) are I-clauses such that the rightmost literal L 1 of c 1 and the complementary one ~L 2 of c 2 are uni­ fiable with m.g.u. o , an I-binary resolvent C of c 1 and c 2 is the I-clause such that :

• (I) the set of literals is {Cjo,Czo}
• the literals of C are indexed as their parent literals and are merged low.

Def : if c 1 : (Cj,s=t) and c 2 :(C2,L 2 ) are I-clauses such that the rightmost literal L 2 of c 2 contains : either

• (i) a subterm s' at occurrence unifiable with the left-hand side s most literal of c 1 (with m.g.u.o) u which is of the right-
• or (ii) a subterm t' at occurrence v which is unifiable with the right-hand side t of the rightmost literal of cl (with m.g.u n), then an I-paramodulant C of c 1 into c 2 is the

I-clause such that :

• (I) the set of literals of C is

(2) the literals of C are indexed as their parent literals - except the descendant of L 2 which receives the index N +1 , where N is the highest index assigned to an I-clause of S - , and they are merged low.

Def : for a given set S of I-clauses, the set of~nctionnally reflexive axioms is the set defined as sF= {f(x 1 , ... ,xn) = f(x1, .·. ,xn) for all n-adic function letters f o~curring in S }

Theorem [Lo] : if S is a finite E-unsatis­ fiable set of I-clauses, then there exists a deduc­ tion of the empty clause (0) from S u {x=x} u sF by I-resolution, I-factoring and I-paramodulation.

III - EQUATION MARKING

In order to control even more the I-paramodu­ lation rule, we shall mark the equatioDs nearly the same as Lankford does in term locking [La].But unlike [La] , marking does not affect each equa­ tion and descendant clause marking is not induced by parent clause marking.

Def : an I-clause is marked when its right­ most literal, being an equation, has one and only

one underscored side .

In our procedure, starting with a given set of (marked) I-clauses, the descendant clauses are marked through a binary resolution or factoring when an equation becomes the rightmost literal or through a paramodulation when the paramodulated literal is an equation . In every case, the side to be marked is freely chosen. For instance, the I-clause (b=c,Pa) can be resolvedagainst the I­ clause (~Pa) into either (~=c) or (b=~).

The equation marking enables us to distin­ guish four types of paramodulation. First, two cases of paramodulation can be defined, depending on whether the paramodulant is obtained (i) by a matching with the marked side of the active equa­ tion or (ii) by a matching with the unmarked side. Then for each of these cases, two new subcases can be defined, depending on whether (j) the paramodu­ lated literal is not an equation, or is an equation whose marked side contains the matched subterm ; (jj) the paramodulated literal is an equation whose unmarked side contains the matched subterm. A para­ modulation satisfying both cases (i) and (j) is said to be a)-typed.

IV- COMPLETENESS OF a)-TYPED PARAMODULATION

Theorem : If S is a finite E-unsatisfiable set of marked I-clauses, there exists a deduction of 0 from S u {x=x} U sF by I-factoring, I-bina­ ry resolution and I-paramodulation of type a).

The proof is given in [Fr ].

V - LINK WITH REWRITING SYSTEMS

The a)-typed paramodulation appears as a directed kind of paramodulation where the equations are treated as a one way-replacement from the marked side to the unmarked one. Now in Term Rewriting Systems [KB] [HO], equations are also used unidirec­ tionnally, but then from left to right. In order to imitate Rewriting, we may have to invert the sides of an equation so that the side to be marked becomes the left-hand one. We are entitled to do so, provided that we extend the resolution and factoring rules so that they are no longer submit­ ted to the order of the sides within equations (thus we can factorize (a=b,b=a) into (a=b) and resolve (Q=a) against (afb))~ Henceforth, marking an I-clause will only consists of choosing a left­ right orientation for the righmost equation.

Since the marked side of the equation is on the left, the a)-typed paramodulation. of an · equa­ tion E 1 into an other one E 2 involves the matching of the left-hand side of E 1 with a subterm r in the left-hand side of E . In Rewriting language, this is a superposition oi E 1 on E 2 - provided that r is not a variable.

Let us consider now the a~paramodulation of an equation s=t into a literal P which is not an equation. P is either (1) an atom A or (2) a negation ~A . In order to continue with the com­ parison between superposition and a)-paramodulation, we have to superpose s=t on P , which implies assimilating the matched term in P to a subterm of an equation left-hand side. This is achieved by writing Pin the form of(l')A=true or (2')A=false, where "true" and "false" are new constant symbols. This leads us to define a new formalism (noted[ EC]) of special clauses, called equational clauses, in which every literal has an equational form.

Def : given anI-clause C : (L 1 ,L 2 , · .. ,L) , the as5;Ciated equational clause is tfie index nor­ dered set D : (E 1 ,E 2 , ... ,En) where, for 1,;k,on , Ek is

• s=t , if Lk is the equation s=t
• E(s ,t)=false , if Lk is the inequation sit (Eisa new equality symboU
• P(t 1 , ... ,tn)=true, if Lk is the atom P(t 1 , ... ,tn) where P is any n-adic rela­ tion symbol except "="
• For 1$ k$n , Ek is indexed as Lk .

Thus in [EC] formalism, the a) - paramodula­ tion can be viewed as a rewriting operation of superposition extended to the variable subterms and involving the rightmost literal of equational clau­ ses.

Furthermore the transposition into [EC] of the binary resolution also appears as a kind of superposition ! Let us consider two resolvable I-clauses C : (c 1 ,A) and C' : (c 2 , ~A) inferring (C 1 ,c 2 ) . The associated equational clauses are D i (o 1 ,A=true) and D' (D 2 ,A=false). The superposition of D on D' infers the equational clause (o 1 ,o 2 ,true=false) or (o 1 ,o 2 ,false=true). If we add a rule enforcing the deletion of each literal true=false or false=true (trivial removal rule) , then we can retrieve the associated resolvent (01 ,02) .

The [EC ] transposition of the a)-paramodulation completeness theorem is :

Theorem : if S is a finite E-unsatisfiable set of oriented equational clauses, there exisfs a deduction of D, from S u {E(x,x)+true } u S by superposition, factoring and trivial removal.

So far, the orientation of term equalities has been used as a means of restricting paramodu­ lation. Yet, the original idea behind orientation is to simplify terms by applying equality units [KB,Sl].

This idea has been incorporated in [EC] by authorizing term simplifications within the rightmost literals. Our procedure then has the fea­ tures of a Knuth-Bendix algorithm running on equa­ tional clauses ; still it is a form of locking resolution when restricted to clauses without term equality [Gr et al].

VI - EXPERIMENTAL RESULTS

The implemented program of Superposition on Equational Clauses (SEC) is written in LISP and runs on INRIA's HB 68. It has been developed as an extension to the system KB written by J.M. Hullot [HH,HO], now a part of the FORMEL system. We pre­ sent the most noteworthy examples with, for each one, the equivalent literature results of a theorem prover chosen for its specific competiti­ veness. By comparison, SEC proofs are often impres­ sively shorter - with regard to the number of gene­ rated clauses. The last example -which fails - is included to point out that so far, for very rich sets of initial axioms, SEC runs out of space.

examples

• if S is a subset of group_yuch that xy-IE S for every x,y E S, then x E S
• 2 2 in a group, if x =e for every x, the group is commutative
• 3 in an ordered field, if x > 0 then x- 1 > 0
• 4 in a ring -x.-y = x.y for every x and y
• 5 a subgroup of index 2 is normal
• 6 Grau's three axioms are sufficient to define a ternary Boolean algebra
• 7 if H and K are subgroups of G, then HK is a subgroup of G iff HK = KH

VII - CONCLUSION

The reduced length of our experimental proofs convinces us that the described approach constitu­ tes a progress in the handling of equality in reso­ lution oriented systems. Our procedure efficiency is due to :

1. the combination of locking resolution with a strong, new and complete restriction of paramodu­ lation
2. the use of a new formalism of equational clauses which unifies the two research processes of para­ modulants and binary resolvents into the one of superposants.
3. the use of equality units as simplifiers.