Negative Hyper-Resolution for Proving Statements Containing Transitive Relations

NEGATIVE HYPER-RESOLUTION FOR PROVING STATEMENTS CONTAINING

TRANSITIVE RELATIONS

Tamas Gergely

Institute for Applied Computer Science,P.O.Box. 146. Budapest, H-1502. Hungary

ABSTRACT

A modified version of PHR-- resolution comprising negative hyper-resolution and paramodulation is introduced to reduce the search of statements that contain transi­ tive relations.

Let R be a symbol of transitive relation and let a nucleus contain the literal tRp, and let a factor of an elec­ tron be of the form C V r t 1 Rt 2 .Moreover let us suppose that tU = t u, where U is a simultaneous most general Onifier for the corresponding clash. Then the resolvent of this clash contains the subclause (C V pRt 2 )U. Th~s rule of deduction is

said to oe TPHR - rule.

It is shown that TPHR-- resolution is complete. More precisely, it is shown that the empty clause o can be deduced from a set G of clauses which contains the axiom of transitivity TrR for the relation R by using PHR-- resolution iff o can be deduced from the set G- {TrR} by using

TPHR-- resolution. .

The efficiency of the use of TPHR-­ rule is illustrated by examples.

l, INTRODUCTION

When using resolution method to prove statements with transitive relations the main difficulty is the usage of the axiom of dransitivity, i.e. the clause TrR=-, xRyV-, yRzVxRz where R is a relation syfribol.

The inconvenience while working with this clause is of two kinds. First, Tr can be resolved with a great number ofR "outsider" clauses, Second, the resolvents contain a new variable y which is not in connection with any other variable of the clause to be resolved. Note that if Tr is applied several times then we have ~ore such new variables, So the number of pos­ sible usage of resolution and paramodula­ tion rules further grow resulting in an uncontrollable growth of the number of

generated clauses.

Konstantin Vershinin

Institute of Cybernetics of Ukrainian Academy of Sciences, Kiev, USSR

The possibility for the strategy of positive hyper-resolution was shown in [3] to reduce the search to some extent. Some further ideas on this subject can be found in [1] · In the present paper we show how to avoid the explicit use of tran­ sitivity axiom within the strategy of neg­ ative hyper-resolution. This strategy is chosen because it can be combined with paramodulation as it is shown in (2] and because each derivation of the empty clause can be easily transformed into direct proof of the statement in question by using negative hyper-resolution (cf. [4] ),

Recall that under negative hyper­ resolution strategy we divide the set of all clauses into two parts: clauses of nucleus (which contain one or more pos­ itive literals) and electrons (which consist of only negative literals). Re­ solvents are always electrons.

The idea developed below is as fol­ lows. Let some electron clause c contain literal ., t 1 Rt.J. This means that statement t 1 Rt 2 shouid ne proved. If a nucleus con­ tains a positive literal of the form t Rt' and U is the most general unifier ot the terms t 1 and t' then the statement ( t'Rt 2 lu mighE be proved instead of the original one. Now we formally develop all the constructions necessary.

2. TPHR-- RULE

First we formulate the so called PHR~ rule of resolution type which comprises both negative hyper-resolution and para­ modulation. As usually, negative clauses are electrons, all the rest are nucleus. Factorization is allowed only for the

electrons.

Let DVL V.,.VLkVt 1 =p 1 V ··· Vt =p be a nucleust where D ~onsists oWlymof negative literals. Let c 1 vrM 1 , ··· ,ckv r ~ ,ck+l v ~~+1 (til , ··· ,ck+m\7 1 ~+m ( t~ l be electron factors and let a simulta­ neously most general unifier exist for

this clash i.e. there should exist such a substitution u that L 1 U»M 1 u, ··· , Lku .. ~u, t 1 U»t.iu, ··· ,tku·tko. (Here · is tne s9mbol of graphic ~den~ity.) Then the resolvent of the above clash is the clause ( Dvc 1 v ··· vckvck+lV·Mk+l<p~v ··· vck+mv ~~+m(Pm )U.

It is shown in [2] that PHR~resolu­ tion is complete for the first order cal­ culus with equality. Let us modify PHR~rule as follows.

Definition 2.1: Let R be the symbol of a transitive relation and let the nucleus contain literal tRp and let the electron factor have the form CV ..., t 1 Rt 2 thereby tU=t U where U is a simultaneous most genetal unifier of the corresponding clash. In this case the subclause lCV lpRt 2 l U comprises the resolvent of the clasfi to be considered. This deriva­ tion rule is said to be TPHR- - rule.

3. COMPLETENESS OF TPHR~RESOLUTION

We show that TPHR~resolution is com~ plete for the first order logic with equality. More precisely we show that for a set G of clauses that contains the axiom of transitivity (TrR) for a relation R the clause o is der~vable by the use of PHR-- reso.lution iff o is derivable from G- {Tr } by the use of TPHR=resolution. Note tftat the "only if" part of this sta­ tement is obvious.

Definition 3.1: T-rule is the derivation rule which permits to obtain the clause < c 1 vc 2 v -,p 1 Rp;tu from the clauses c 1 v t 1 Rp 1 , c 2 'V , t 2 Rp 2 , where U is the most general unifier for t 1 and t 2 ·

Now we formulate the analogon of the lifting lemma to the T-rule.

Lemma 3.2: If w is such a substitution that t w - t w and U is the most general unifiet of t~e terms t 1 and t 2 then the clause c 1 v c 2 v, p 1 Rp 2 subsumes the clause C wVC Q v -,p wRp w. In other word, th~ re~ult of ~sin~ T-rule to two given clauses subsume the result of using T-rule to any instances of the two given clauses. Proof is obvious.

Note that if the starting set of the clauses contains axioms of functional reflexivity which we always suppose then lifting works for paramodulation as well. So the investigation can be re­ stricted to the ground case.

Let G be a set of clauses and let us suppose that some clause C can be derived from G by the use of PHR-- resolution,i.e. G IPHR_c · We represent this derivation in a tree form where the root is c, the leaves are instances of starting electrons. To each node of the tree a nucleus and usage of PHR-- rule correspond, i.e. to each node so many arrows go in as many the number of the electrons existing in the corresponding clash are. From each node one arrow goes out. This tree is said' to be the derivation tree of clause c. It is clear that the axiom of transitivity TrR. is a nucleus, i.e. to the resolution wi~h TrR such a node corresponds in the deri­ va~ion tree, where one arrow goes in ~ince TrR contains a unique positive li­ teral).

Let leaf D of the derivation tree contain literal., t R t , to the off­ springs of which t~e axfom of transitivity is applied n times (i.e. the path in the derivation tree from D to the root goes through n nodes corresponding to TrR). Let us substitute literal .., t 1 R t 2 with the clause · t 1 Rx 1 V · x 1 Rx 2 V ·.. V . ..., x Rt 2 , where x.l, . · . , x are new var~a­ bleE, and from tne path £Porn D to the root let us eliminate n nodes corresponding to the usage of TrR to the offsprings of the literal t 1 R~ 2 ·

It is obvious that the tree obtained after such reconstruction is still a derivation tree for the clause c.

Let us do the aboves for each such leaf of the tree that contains literal to the offsprings to which the axio~ of tran­ sitivity has been applied. Let LG be a family of leaves of the reconstructed tree. Some of the leaves contain clauses of the length of the transitive part. It is obvious that the reconstructed tree does not contain nodes corresponding to TrR.This corresponds to the fact that resolution with nucleus TrR can be lifted up,i.e. it can be done in the beginning.Thus we have

Lemma 3.3: Let G be a set of clauses, T be a derivation tree of the clause c from G, L be the set of leaves of T, L' that of the reconstructed tree T'. Then L' I PHir C and the corresponding tree T' does not contain nodes corresponding to TrR.

Now we are ready to prove the main

Theorem 3. 4: If G IPHR- D then G- {TrR}ITPHR_o Proof: Let T be a derivation tree of the clause C from G and let T' be a reconstruc­ ted ground tree of derivation of c. We show how T' can be transformed into the deriva­ tion tree by the use of TPHR~resolution so that the leaves of the new tree become instances of the starting clauses,i.e. they should not contain transitive parts.

The proof of the possibility to do such transformation is done by induction on the sum S(T'l of the length of trans­ itive parts of the leaves.

Base of induction: S(T') o, i.e. tree T has not contained resolution with TrR. This case is trivial.

Induction step: Let SlT')>O and for all trees T with S lT) < StT') let us suppose that the possibility of the transformation is proved. Since s (T'J :::> 0 then there exists such a leaf D in T' the length of the transitive part of which is greater than 0. Let this leaf be of the form

D=D 1 V ·t 1 Rs 1 v -,s 1 Rs 2 v ··· v -,snRt 2 ·

Let us consider the path P from D to the root of the tree. The following two cases are possible:

Case 1. On the path P literal -, t 1 Rs 1 has been resolved earlier than IS Rs .Le~ literal ·t 1 Rs 1 be resolved(possibty ~fter having usea paramodulation several times responding lit~ral tiRs of the nucleus, where term t' is the result obtained after

for the term t ) in the node N with the cor­ making all p6ssible paramodulations in t 1 .

Let us substitute leaf D in T' by the clause D 1 v,s 1 Rs 2 v .·. v-,s Rt 2 · We get tree T l . It is Obv~ous tha\! L TT l)l PHR- C 1 , where c 1 subsumes c. Indeed, all possible paramodulationsfor t should be done together with the re~olution in the node N.

Moreover S(l' i> < S ( T 'l . Thus according to the inductive hypothesis T' can be transformed into the derivati6n tree TJ of clause c; with TPHR-- resolution wnile c' subsumes c . But the starting set of ~lauses for t 1 contains the clause D 1 V , s 1 Rt.7 together with D 1 V.., t 1 R t 2 · NOw we suBstitute leaf D in T' by the

clause D 1 V-, t 1 R t 2 ·

Let us execute all possible resolu­ tions and paramodulations connected with literals from Dl and ·s 1 Rs 2 , ··· ~s Rt 2 in T'. In node N insteaa or PHR- -nruie let us use TPHR~rule. Then obviously literal -, t 1 R t 2 is substituted by literal , s R t · The derivation T' will be a dertvati6n of the clause whfch subsumes DJV ls 1 Rt 2 · Moreover S(T2J<S(T'). Thus ~ can be transforme9 into tree T 2 of the derivation with TPHR - resolution of the clause which subsumes D 1 Vls,Rt 1 · Let us substitute all starting occcrrences of DJV·s 1 Rt 2 in TJ by the tree T 2 · Obviously tne tree thus ootained is the required one.

Case 2. On the considered path literal, s 1 Rs 2 has been resolved earlier than , t 1 Rs 1 · Let , s 1 Rs 2 be resolved with s 1 Rsi in some node N. Then literal lt]Rs 1 was resolved with literal t1Rsl in the node N'. On the path from N toN' let the paramodulations be executed from lit­ erals p 1 = q 1 , ... , pk = qk into the term s such that s' is tne result of these p~ramodulation~. Let the paramodulations be executed in the nodes N , ··· , N in the respective order from left to rig~t, i.e. the occurence of the left part of the equivalence is substituted by the right one.

Now let us substitute leaf D in T' by the clause D 1 v,slRs 2 v ··· v,snRt 2 ·

Let us execute all possible para­ modulations in T' connected with term t 1 and do the resolution in the nodes N ana N'. Then on the path from N to N' let us inverse the order of paramodulations, i.e. the order of nodes become as follows N , ·.. ,N . Simultaneously the "direction\> of each Paramodulation is also changed, i.e. now they are executed from right to left. Let us use these paramodulations to the terms] of literal ·1s]Rs 2 · Obviously we get li ~eral , s Rs · Then in the node N' we execute res6lution with the nucleus having been earlier inN. The tree thus obtained is a derivation of the clause which subsumes clause c.

Moreover S(T') < s (TJ. Thus T' can be transformed intottee T , which is a derivation by the use bf TPHR-- resolution of the clause which subsumes c. But the clause D 1 y, s 1 Rs 2 while not being a start­ ing one occurs as a leaf in T 1 .

The rest is analogous with case 1.

Now we illustrate the efficiency of using TPHR~rule by examples.

4. EXAMPLES

4.1. Let us take a topological theorem with all its necessary definitions as shown below.

"Let E be a set. Let E be a metric space.

Definition 1: Let X,Y be sets. Y is a subset of X iff every element of Y is an element of X too.

Definition 2:Let X be a subset of E. X is open in E iff for any point z of X there exists an· open sphere included in X, with the center in z.

Definition 3: Let z be a point of E and let A be a set. A is the neighpourhood of z iff A is a subset of E and there exists a set Y which is open in E so that z is a point of Y and Y is included in A.

Each subset of a set is a set.

Theorem: Let A be a subset of E. Then A is open in E iff A is a neighbourhood of every point of A."

From this text the following set of clauses can be obtained

1. -: xRy V · yRz V xRz

2. SStA,El

3. <Plx ,AJV P (x , f 1 ( xJJ

5.·SS(A,E)V P~z ,A)

4. ·P (x,AlV f t XJM

6. -,SSfA,EJV;OSt~,z) V IVRA

8. lP(x ,AJV · P (z ,f 1 txU V f 2 tx,z)R fl ( X)

7. ·Ptx,AlV -, p t z,f~tx)) V 0S t f 2 rx,z), z)

where v,c,y,z are variable symbols, A,E, z are constant symbols, f , f are S~olem functions, R, SS, P, 0~ are binary relation symbols. The latters are of the following meaning

R (x,y J stands for SSiA,E) stands for P (x,AJ stands for OS (v,x) stands for "x is included in y" "A is a subset of E" "x is a point of A" "v is an open sphere with center in x".

Due to transitivity of relation R we use the infix notation, i.e. we write xRy instead of R(x ,y J ·

In order to prove the theorem the strategy of negative hyper-resolution has been applied for. While this done three levels of possible resolvents have been obtained ( see Table lJ.

Note that due to unforeseen circumstances nucleus 1 did not participate in the deduction.

Literal·SS ~,E) is present in all clauses, but resolution with nucleus 2 eliminates it. So having obtained re­ solvent {· SS!A,E )} the proof seeking process is considered to be successfully terminated.

Note that clause 15 is subsumed by clause 14 ·

Having noticed that no further pos­ sibilities for resolution are available nucleus 1 was called into the process and the deduction went on. Namely, the number of resolvents of level n+3 was of n! The empty clause o was obtained at the eighth level.

Yet if we go on with the deduction by using TPHR~rule we obtain the re­ solvents presented in Table la, which is the continuation of Table 1.

Table la .

It is evident that the hereby described deduction is much simpler than that within which nucleus 1 i.e. the transitivity axiom of relation R is used.

4.2. Let us now take a theorem from the field of commutative rings having the following text.

"Let R be a commutative ring with unit element. Let a,btR. The ideal generated by the element a is denoted as a.R. Let x~a.R iff alx (where atx means that a divides x, i.e. ~zx=a.z. Here · is the binary operation of multiplying in the r .ing R.

Product of ideals a.R and b.R is a set denoted as ca.Rlo (b.Rl such that Xt(a.Rlo (b.R) iff 3:U3:V lX = U. V/\ Uio a.R 1\ v ~ b.R I

Intersection of ideals a.R n b.R has the usual set-theoretic meaning.

Theorem: ;a.R ~ o t_ b.R ) ~ a.R n b.R"

From the above text we have the following set of clauses.

1. · ;a.R: oCb.Rl ~ a.R n b.R

2 · 1 x=y. z vy I x

3. -; x=y . z vz 1 x

4 . l y I X vx~ y. R

5. l x~y .R v· YIX

6. Xi:AVA!C'B

7. ., x 0 t B 1/ A ~ B

8. -, xc;A V '1 X E. B V X t A n B

9 . ., z e <a.Rl otb.R) v' z = f 1 (z). f 2 (z)

10 · ., z ~ ta.RJO(b.RI vf~=)(:a.R

11. · z Ha.R J o lB.RJvf~Hb.R

where a,b,R,x are constant symbols and f 1 ,f 2 are 0 Skolem functions.

Here 1 is the unique electron while the other clauses (2-lll form the nucleus.

Note that the binary relation symbol is transitive, though the axiom claiming this property is absent. The proof of the theorem, i.e. the deduc­ tion of o by the use of TPHR~rule con­ sists of 79 resolvents ( including subsu­ mation J .

The derivation tree containing only the necessary resolvents is shown on Fig.l.

However if the. transitivity axiom of I is attached to the above set of clauses the number of resolvents will be more than 100 (including subsumation)on the seventh level already.