Reducing the Derivation of Redundant Clauses in Reasoning Systems

1 Introduction

The derivation of redundant information is one of the greatest obstacles to the efficiency of reasoning programs. Wos (1988) reports an attempt to prove SAM's lemma (see Guard 1969) using hyperresolution, where 6000 clauses identical to retained clauses and 5000 clauses being proper instances of retained clauses were generated. Even if these redundant clauses can be removed after their generation, they must be processed with demodulation, subsumption, and other procedures. Moreover, the test on subsumption, being a very useful means for removing reduncancies, is rather expensive as Chang & Lee (1973), Eisinger (1981), and some others remark. A strategy to prevent the generation of redundant clauses, or at least to reduce the amount of newly generated unneeded clauses, would thus prove very useful for increasing the power of reasoning systems.

On closer inspection of the proof of SAM's lemma it turns out that many of the 6000 duplicates are generated by double resolution with a clause of the form Pxy v -.Pyx. Such a duplicate is identical to its own "grandfather" in this resolution derivation. More general, we will deal with the situation that a resolvent is subsumed by one of its own ancestors, which we will call ancestor subsumption. Ancestor subsumption is a particular kind of forward sub­ sumption (Overbeek 1975), that is the subsumption of a newly deduced clause by a given clause. One of the paper's objectives is to characterize clause sets that admit ancestor subsumption. This approach is based on the following observation: A resolvent of two clauses cannot be subsumed by one of its parent clauses, unless the other parent is self­ resolving. This can be easily seen for the ground case: let C={LJL2.-·LnJ and D={ -LJ.K2.--.Kn) be ground clauses and assume, C subsumes the resolvent R={K2 ·.. .Kn.L2 ·..· Ln). Then LJER must hold and from LJE {L2 ·.. LnJ now follows LJE {K2.--.Knl· Hence Dis a tautology. We will generalize this observation in the following way: A resolvent R cannot be subsumed by an ancestor C, unless the set of ancestors of R contains a cycle (the notion of a cycle was introduced by Shostak (1976)). Noncyclic clause sets thus have the nice property of excluding ancestor subsumption. A prominent example for this class of clause sets is Schubert's Steamroller (see Stickel 1986). Linear resolution has the property that the later a clause is derived in the linear deduction, the more ancestors it possesses. Provided that a given clause set is known to disallow ancestor subsumption, a linear strategy thus seems most preferable in order to reduce the generation of subsumed clauses.

Another question addressed by this paper is closely related to the first problem. The characterization mentioned above provides a means to avoid the generation of subsumed clauses only for noncyclic clause sets. But for other clause sets we can at least give a criterion to decide, which clauses have to be considered as potential subsumers in the sub­ sumption test. Being not self-resolving, for example, a clause can be excluded from being subsumer of its own "child".

As cycles in clause sets are heavily responsible for the generation of redundant information, a technique to remove such cycles would prove very useful. This paper considers two approaches. A certain class of cycles (cycles represen­ ting the logical equivalence of some literals) can be made harmless by using them only as demodulators. Consider for example a clause set containing the two clauses -J'vQ and -.Qv P. which form a cycle and give rise to an endless resolution derivation. These two clauses express that P and Q are equivalent literals, which therefore can be substituted for each other without changing the truth value of the whole clause set. Replacing for instance each occurrence of P in the clause set by Q yields an equivalent clause set, where the two cycle clauses have become tautologies. This approach is in fact a demodulation on literals instead of terms. The well­ known problems with term rewriting, however, arise with literal demodulation, too. Directing equations to rewrite rules requires the existence of a well founded ordering on terms. Thus, according to the same reason, why the equation fxy = fyx cannot be directed to a rewrite rule, the equivalence Pxy =Pyx cannot be used as a demodulator. The second approach, which overcomes the problem with directing equivalences, consists in using cycles as the basic theory for performing theory resolution. The cyclic clauses, for instance the symmetry clause Pxy v -J'yx, disappear in a theory box, enabling in this case resolution between the clauses Pab and -.Pba.

2 Basic Notions

In the following we assume the reader to be familiar with the standard terminology of First Order Logic. The few basic notions of clause graphs used in this paper can be found for instance in Eisinger's (1988) thesis. Clauses are always considered as sets of literals, but written without set braces. The empty clause is denoted by 0.

Let o/be a denumerable set of variables. A substitution cr is an endomorphism on the term algebra, which is identical almost everywhere on o/and thus can be represen­ ted as a finite set cr = (XJ-7t], ... .Xn-7tnl· A substitution p is called a renaming substitution, iff p is injective on its domain and o/p~o/. A literal or clause Lis called a variant (or a copy) of the literal or clause K, if there exists a re­ naming substitution p, such that Lp=K. Two substitutions cr,'t are compatible, if there exists some substitution A. with crA. = 'tA.

3 Cycles in Clause Sets

This chapter provides a characterization of clause sets admit­ ting ancestor subsumption. Our main result is as follows: Clause sets admitting ancestor subsumption possess cycles, whose elements are the far parents of the subsumed clause.

First, we define the two basic notions of ancestor subsump­ tion in terms of circular derivations and of cycles. The proofs of the following lemmata and theorems can be found in the full version, Socher (1988), of this paper.

3.1 Definition:

A clause is self-resolving, if it resolves with a copy of itself.

The following lemma determines those clauses that possibly produce subsumed resolvents. For any clause D we define the deduction relation -7D between clauses C and R by C -7D R, iff R is a resolvent of C and D.

3.2Lemma:

Let C be a unit clause and D , R be clauses with C -7 D R.

1. If R is a variant of C, then D is self-resolving.
2. If R is an instance of C, that is, CJ1=R for some substitution Jl, then D = LKJ ... Kn. and L, Ki have the same predicate symbol, but different polarity for all i E (l..n}.
3. If C subsumes R, that is, C/1~ for some substitution Jl, then D = LKJ .. .KmMJ ... Mn. and L, Ki have the same predicate symbol, but different polarity for all i E (l..n}. ·

The next lemma shows that clauses, which only produce subsumed clauses, are tautologies.

3.3 Lemma:

Let D be a clause.

1. Suppose for all clauses C the following holds: C-7D R implies that C and R are variants. Then D is a tautology, IDI = 2, and Dis function and constant free.
2. Suppose for all clauses C the following holds: C-7D R implies that R is an instance of C. Then D is a tautology and IDI = 2.
3. Suppose for all clauses C the following holds: C-7D R implies that C subsumes R. Then D is a tautology. ·

In the following we will generalize lemmata 3.2 and 3.3, that is, we want to determine those clause sets fJJ, which - possibly or only - produce subsumed clauses. It will tum out that the appropriate generalization of self-resolving and tautologous clauses are cyclic clause sets.

We generalize the deduction relation to clause sets fJJ, by C-7vf?., iff there is a sequence C -7£ 1 C1 -7£ 2 ··· -7£n R such that (E1, .. ,E0 } = fJJ.

A path in directed graph is an alternating sequence (N1, It ·.... ,Nn-l.In-1· Nn) of nodes and links, such that li goes from Ni to Ni+l· It is called cyclic, if N1=N0 · A directed graph is called cyclic, if it contains a cyclic path.

A semicycle tJJ is a directed graph, whose nodes are labelled with clauses and whose links are R-links, labelled with substitutions and which satisfies the following conditions a) to c). (Note that we do not distinguish between a node and its label.)

1. Each node of tJJhas the following form (figure 1):

with m incoming R-links and n outgoing R-links, and m>O, n~ holds.

1. There is a node Co such that each cyclic path of tJJ passes Co. There is a substitution 't, which is a common instance of all substitutions of the R-links going into Co and there is a common unifier cr for all other links of tJJ.
2. cr and t are compatible, with common instance X· The substitution X is called the cycle substitution of tJJ.

The semicycle tJJ is called complete, if <J is an instance of 't, that is Lcr = Kcr for all literals L and K joined by a link going into CQ. Let tJJ be a semicycle consisting of only one clause C. Then cr is the identity substitution andC is self-resolving. If, moreover, tJJ is complete, then C is a tautology. tJJ is called a cycle, if each node has exactly one successor.

A cycle is just what Shostak (1976) and (1979) calls a loop. This notion also corresponds to the notion of recursive predicates in the terminology of deductive databases (Vieille 1987, Ohlbach 1988) and logic -programming.

3.4 Example:

The clause sets tJJ 1 , tJJ 2 , and 'Dj, which are shown in figure 2, are semicycles; tJJ1 is a cycle. It can be seen that each node of a cycle may be chosen to be the special clause Co. As to semicycles, still several, but in general not all nodes have this property. For instance the clauses -,rw and sw cannot be chosen to be Co.

The previous examples illustrated that in general there are several possibilities to choose a clause of a semicycle to be the special clause Co. The cycle substitution, however, is independent of this choice, according to the definition of semicycles.

The following two theorems provide a characterization of clause sets producing subsumed clauses. It turns out that those clause sets have a "cyclic" structure, varying from the weakest form for clause sets producing some ancestor subsumed resolvent to the strongest form of a cycle for clause sets producing only copies as resolvents.

3.5 Theorem:

Let C be a unit clause, let tJJ be a set of clauses and let C~vR.

1. If R is a variant of C, then tJJ is a semicycle.
2. If R is subsumed by C, then tJJ contains clauses Dl···.Dn such that for each Di. iE {1, .. ,n-1} the following hold:
3. (i) there exist literals Ki and Li and an R-link between Li and Ki+l·
4. (ii) Ln and K 1 are literals with the same predicate symbol, but different polarity. ·

3.6 Theorem:

Let tJJ be a set of clauses.

1. Suppose for all clauses C the following holds: C~vR implies that C and R are variants. Then tJJ is a complete cycle, all clauses of which are function and constant free.
2. Suppose for all clauses C the following holds: C~vR implies that R is an instance of C. Then tJJ is a complete cycle.
3. Suppose for all clauses C the following holds: C~vR implies that C subsumes R. Then tJJ is a complete semicycle. ·

Note that the definition of the deduction relation ~D does not capture ancestor resolution, which is part of complete linear strategies.

3.7 Example:

Let '])be the clause set, which is shown in fig. 3.

']) allows a linear deduction with ancestor resolution as follows:

where the last step is an ancestor resolution step. But 'lJ is not a semicycle.

The following lemma shows that it is sufficient to look for cycles in an initial clause set during a resolution deduction, as "new" cycles cannot be generated by resolution. For any clause setS. 9t(S) denotes the resolution closure of S. that is the smallest clause set containing Sand closed under the resolution operation.

3.8 Lemma:

Let S be a set of clauses. Then S contains a semicycle, iff 9t(S) contains a semicycle. ·

4 Removing Cycles From Clause Sets

Besides being the very reason for the undecidability of first order logic, cycles in clause sets also turned out to be a main source of reduncancy for clause set resolution. Thus the question arises as to what extent cycles can be excluded from producing lots of unneeded clauses. A first approach to this question is due to Bibel (1981). He showed that under certain conditions, similar to those allowing the deletion of tautologies in clause graphs, cycles can be removed from clause sets. We will consider here two approaches, both restricted to proper cycles. However, we will also show by means of SAM's lemma, that in particular cases there exists also an appropriate treatment of semicycles.

The first idea in order to shut down this source of reduncancy is to use cycles not directly for resolving. Instead, they are taken as literal demodulators (Wos 1967): Cycles, expressing the equivalence of literals, can be transformed into rules, in the same way as equations can be directed yielding rules. Consider for example a clause set containing among others the two clauses -J'vQ and ---.QvP. These two clauses represent the formula P=Q. which can be directed yielding for instance the rule P~Q. Application of this rule means substituting Q for each occurrence of P and -.Q for each occurrence of -.P. (Note that this effect can be achieved also with an ordering restriction (Loveland 1978), which precludes resolution with the Q and -.Q literal in the two clauses.) However, the method of literal demodulators applies only for cycle clauses that can be directed, such as ground clauses or clauses with different predicate symbols. Thus, a lot of relevant clause sets does not allow this approach. For instance, the (cyclic) clause -.PxyvPyx, expressing the symmetry of P, cannot be directed.

Another approach, which overcomes the problem with directing equivalences, is based on the idea of "compiling" cycles into a theory serving as the basis for theory resolution. Theory resolution, first proposed by Stickel (1985), is a generalization of ordinary resolution. The literals resolved upon need not be syntactically complementary, it is sufficient for them to be complemen­ tary under some theory. In particular, each clause C = ( L J, .. .Ln} defines a theory iJ'c. in which, for instance, the set of literals (-.LJ, ..· -.Ln} is complementary. Taking clauses (or clause sets) as a particular theory to perform theory resolution is essentially the same idea as Ohlbach's (1988) link resolution. The set lJ'c in general is not computable. Yet, in order to perform theory resolution on a clause set S, it is sufficient to compute the resolution closure 9t(S) of S.

4.1 Lemma:

LetS be a set of clauses and DE rrj be a clause, which is not a tautology. Then there is some clause CE 9t(S), such that C subsumes D. ·

In order to find the substitutions cr, which make a set (LJ, .. .Ln} of literals complementary under the theory tTs. or, equivalently, which map the clause D:=(-.LJ, .. ,-.Ln} onto an element of tTs. it is sufficient, according to the previous lemma, to find some cr and a clause CE 9t(S), such that C subsumes Dcr. Thus, having a finite resolution closure 9t(S), the setS guarantees the number of tJ's­ resolvents of two clauses to be finite. In particular, this is the case for cycles that produce only copies as resolvents, since these cycles are function free. The next lemma shows that the theory of a complete, function free cycle '1J with cycle substitution cr can be completely described by the equivalence of all literals of 'lJcr.

4.2 Lemma:

Let ']) be a complete, function free cycle with cycle substitution cr. Then 9t('1J) = ( ---,LcrKcr I Land K are literals occurring in 'lJ}. ·

4.3 Examples:

a) Let 'D = { -,Pxy Qxy, -,Quv Puv). 'D is a complete and function free cycle with cycle substitution cr={x~u. y~v). The theory of 'D consists of the formula Puv = Quv.

b) Let 'D= { -,Pxy Pyx). 'Dis function free, but not complete. By adding a copy of the clause -,Pxy Pyx, a complete cycle 'lJ is obtained.

Then 9\('D) = 9\('lJ) = {-,Pxy Pyx, -,Pxy Pxy) is finite and thus the number of rrv -resolvents of any ·two clauses is finite, too.

c) Let 'D={-,Pf(j(x,y), z) Pf(xf(y,z))).

Then 9\('D)= 'D u {-,Pf(j(j(x,y),z),u) Pf(xf(yf(z,u))), ... ) is infinite and the number of fJ'v-resolvents of two clauses is infinite, too.

Taking into account the tight connection between '£­ unification (see Biirckert, Herold & Schmidt-SchauB 1987) and theory resolution for equational theories, the previous examples' behaviour is not surprising, as the number of most general unifiers under the theory of commutativity is finite, whereas it is infinite under associativity (see Herold & Siekmann 1985).

5 Conclusion

In this chapter we want to show by means of an example, how the information about cycles in clause graphs can be used to reduce the search space in resolution theorem proving. The predicate logic formulation of SAM's lemma (without equality) leads to a clause setS, consisting of a set of the 11 units {U}. ... ,Uu)

{min(O x 0), max (x 0 x), max(a b dj), min(d] CJ 0), min(a b dz), min(dz cz 0), min(cz be), min(cz a f), max(c] e g), max(cJ f h), -,min(g h CJ ))

and the following 6 non unit clauses:

(C1) -,min(x y z) min(y x z)

(Cz) -,max(x y z) max(y x z)

(C3) -,min(x y u) -,min(y z v) -,min(x v w) min(u z w)

(Cs) -,max(x y z) min(x z x)

(C6) -,min(x z x) -,max(x y XJ) -,min(y z y 1)

-,max(x y 1 zJ) min(z X] zJ)

In the following we describe a refutation of this clause set using positive hyperresolution together with theory resolution, as in chapter 4. The cyclic clauses C1 and Cz, describing the symmetry of the min and max predicates, are used for theory resolution, as in example 4.3.b). The same holds for the clause Cs, which is neither self-resolving nor a member of a cycle. The clauses C3 and C4, describing the associativity of the min predicate, form a semicycle, which produces copies in the following way: Let (D1, Dz, D3)

resolve with C3 to the unit clause D4. Then (D1, Dz, D4) resolves with C4 to a copy of D3. The resolution closure of the semicycle 'D={C3, C4} being not finite, this cycle cannot be used directly for theory resolution. But C3, C4 can be used to produce instances of rrv in the folllowing way:

from C3, U6, U7:

from C4, U6, U7:

-,min(dz e w) min(O b w)

-,min(O b w) min(d2 e w)

In the following, we will abbreviate these two lines by: from C3, C4, U6, U7: min(dz e w) = min(O b w) If the theory of some clause Cn or Em is used, then "with T(Cn)" or "with T<Em)" is added to the from-line.

The result of resolving { c3,c4) with the two units is a complete cycle, which is added to the theory box.

Proceeding this way, only the clause c6 is needed to pro­ duce "ordinary" resolvents. Of course, there is also the pos­ sibility to produce copies of already retained cycles. Taking into account these reduncancies, a total 660 copies or inst­ ances of already present clauses are generated in the proof.

The proof of SAM's lemma consists of 8 steps:

from C3, C4, U6, U7, with T(Cz, Cs):

E1: min(c2 b w) = min(e d1 w)

from C6, U7, U9, U4, Uz, with T(Et. Ct. Cz): U12: min(dt e g)

from C3, C4, U8. U3, with T(Cs): Ez: min(cz a w) = min(f dt w)

from C3, C4, U8, Us:

E3: min(c2 dz w) = min(f b w)

from C3, C4, U6. U7, with T(Ct. E3):

E4: min(f e w) = min(O c1 w) from C3, C4, U8. U12, with T(E3): Es: min(f e w) = min(f g w) from C6. U9, Uw. Ut. Uz, with T(E4, Es, Cs): Un: min(g h q)

Clause U 13 contradicts clause U 11. and the proof is complete.

Acknowledgement

I would like to thank my colleague Norbert Eisinger for thoroughly reading this manuscript. His comprehensive knowledge of the field, particularly about many examples and counterexamples that arise in theorem proving, resulted in improvements of the paper.