Recognizing Unnecessary Inference

1 Introduction

Intelligent reasoners expend much effort deciding what information is necessary for the problem at hand. When a conclusion is drawn we decide if it contains new and relevant information. It is well known that the perfor­ mance of automated reasoning systems can be enhanced by eliminating unnecessary formulas. In such systems conclusions drawn from unnecessary formulas are also unnecessary. Failure to prevent the generation of these formulas can lead to rapid combinatorial explosion [Wos, 1988].

In this paper we concentrate on the problem of recog­ nition of unnecessary formulas in the context of reso­ lution based systems. In such systems several strategies have been developed that allow for the deletion of clauses without sacrificing completeness. Common strategies in­ clude subsumption, tautology elimination, and demodu­ lation. The subsumption strategy eliminates clauses that are instances of other clauses. The demodulation strat­ egy pertains to clauses containing the equality predicate. Using this strategy demodulators are used to rewrite clauses that are subsequently deleted.

Unfortunately these strategies fail to recognize other frequently generated unnecessary formulas. A less obvi­ ous way in which resolution based systems produce un­ necessary formulas is related to skolemization. Skolem functions have the effect of automatically creating names for new objects, but sometimes too many names are ereated, leading to the generation of unnecessary formulas. In section 2 we will discuss some specific examples to clarify why and how this happens.

Another cause of unnecessary formula generation is due to the presence of permutative predicates. By a per­ mutative predicate we mean one that is logically equiva­ lent under any permutation of some subset, s, of its ar­ guments where lsi > 1. In the case of a binary predicate this implies the relation is reflexive. A simple example is the Equal predicate where

holds. In clause form this axiom becomes

Now suppose that the unit clause Equal( a, b) is gen­ erated. It resolves with c1 to produce the clause Equal(b, a). In general if P is permutative and P(a1,a2, ... an) is generated then resolution based systems tend to generate all formulas of the form P(aj,,ah, .. . ajJ, where it,h, ... jn is a permutation of 1, 2, ... , n. Thus we can end up with n! such formu­ las. Often many of these formulas are not required for the proof.

The main result discussed here can be viewed as a generalization of subsumption. This result can be used to develop new deletion methods and to show that these methods do not sacrifice completeness. Using deletion methods we have developed, we were able to prove cer­ tain theorems from Hilbert's axioms for geometry. These theorems present a significant challenge to automated systems due to the constructive nature of the proofs . For a discusion of these theorems see [Benanav, 1988] .

In section 2 we discuss an example that illustrates a subtle way in which resolution systems generate unnec­ essary formulas and present informal arguments as to why these formulas are unnecessary. In later sections we define more precisely what we mean by unnecessary clauses and how to recognize them.

2 The Naming Problem

In mathematical arguments one often sees inferences that assert the existence of some object and give it a name. Subsequently, other inferences are made that re­ fer to the object by this name. This process is so natural that we pay little attention to it and perhaps underesti­ mate its importance. In this section we show how reso­ lution creates more names than is necessary and in the process generates far too many formulas.

The usual way to express constructive statements in predicate logic makes use of existential quantifiers. In resolution based systems existential quantifiers are re­ moved and replaced with functions. For example, con­ sider the axiom,

Al. Any line contains at least two distinct points.

This can be expressed in predicate logic as

To skolemize this formula the variables x1 and x2 are replaced with functions Pl(yl) and P2(yl) respectively, and the existential quantifiers are removed. After these replacements we get the formula,

Proofs often contain statements that begin with the phrase, "Let A be the ... ". This phrase has the effect of generating a name for an entity that can be asserted to exist. Skolemization has this same effect of generat­ ing names for things. For instance, consider the axioms consisting of Al and

A2. a is a line.

which are represented in clause form by the formulas,

The clause Line(a) resolves with each of the other clauses, yielding

The new clauses produced contain two new constants, Pl(a) and P2(a). The corresponding human proof might contain the following argument: "Since a is a line, there must be two distinct points on it. Let's call those points Pl(a) and P2(a)."

Suppose that we add to the two previous axioms, the axiom,

A3. There exists two distinct points on the line a.

This is represented in clause form as,

After resolving Line( a) with the other clauses, the database would contain the clauses G1, G2, and Ga. We claim that the clauses in G2 are unnecessary. To see this consider how an intelligent reasoner might argue. From axiom A3 we know there exists two distinct points on the line a. Let's call those points q1 and q2 . From axioms Al and A2 we know that a must contain two distinct points. But this is just what axiom A3 says. Therefore no new names are created.

The redundant nature of this inference becomes clear by considering the corresponding deduction without first converting the axioms to clause form. They are repre­ sented in non-clausal form by the formulas,

Note that by substitution and modus ponens we can infer Fa from F1 and F2 . If the initial set of formulas is F1, F2, and Fa, then deducing Fa from F1 and F2 is redundant. However, the clauses G2 , generated by the resolution inference rule, are not the same as the clauses Ga.

It should be remarked that the fact that the clauses G2 are redundant has nothing to do with the equality predicate, although the clauses G1 contain the Eq sym­ bol. We can easily construct a similar example where the equality predicate is not present. For example, we encounter the same problem if we begin with the axioms

A4. For any line there is a point not on the line.

A5. The point Pt is not on the line a.

To illustrate the proliferation of such unnecessary clauses, consider in addition to those in G1, the clauses,

These clauses represent the axiom,

A6. Through any two distinct points there is a line. As before, the clauses G2 can be produced. Then the clauses

-,Point(x)V-,Point(y)V Eq(x, y)V Line(L(x, y)) Point(p1(a)) Point(p2(a)) -,Eq(pl (a), P2( a))

resolve to form the clause,

Since the clauses in G2 are unnecessary this clause is also unnecessary. However note that it resolves with the clauses in G1 to produce the unnecessary clauses,

On(p1 (L(p1 (a), P2( a))), L(p1 (a), P2( a))) On(P2(L(Pl (a), P2( a))), L(Pl (a), P2( a))) Point(p1 (L(p1 (a), P2( a)))) Point(p2(L(p1 (a), P2( a)))) -,Eq(pl (L(p1 (a), P2( a))), P2(L(p1 (a), P2( a))))

and the process continues ad infinitum.

3 What is an Unnecessary Clause?

There are several different ways in which a clause can be unnecessary. For example, consider the clauses,

Suppose we are using the hyperresolution inference rule to deduce the empty clause. Recall that to deduce a clause from a set of clauses by hyperresolution, at m06t one clause, C, in the set can contain both positive and negative literals. The other clauses can contain only p06itive literals. All negative literals in C should be resolved away. For this example it will be important to note that P V ·Q and -,p do not resolve by hyperresolution.

Note that we can obtain a proof by resolving P with ·P. The other clauses, S1 = {PVQ, PV·Q, R} are not needed for a proof. Given an inference rule I and a set of clauses S, we say that a set of clauses S' ~ S is simply unnecessary if whenever there is a proof of the empty clause from S using I, there is also a proof from S - S' using I . In this sense the clause Pis simply unnecessary since we can obtain the empty clause from S- { P} using hyperresolution.

Not only is it possible to obtain a proof from S- S1, but in fact there is a hyperresolution proof that does not use any clause from S1. However using hyperresolution there is no way to obtain the empty clause without using the clause P somewhere in the proof. (By binary reso­ lution we can obtain such a proof). We say that a set of clauses S' are absolutely unnecessary with respect to I and a set of clauses S if whenever there is a proof of the empty clause there is also a proof that does not contain any clause from S'.

There is an important difference between absolutely unnecessary clauses and simply unnecessary clauses. If a clause is found to be simply unnecessary it means that it can be deleted from the original set of clauses. How­ ever, if it gets generated again it cannot necessarily be removed. On the other hand if a clause is absolutely un­ necessary then whenever it is generated it can be deleted.

One further sense of unnecessary is illustrated by the clause R. In fact there is no proof that uses R to derive the empty clause. In such a case we say R is completely irrelevant .

Progress in development of methods to recognize any of these classes of unnecessary formulas could lead to sig­ nificant improvements in the performance of automated reasoning systems. In this paper we will examine the question of how to determine whether a set of clauses are absolutely unnecessary. In the remainder of this pa­ per we will use the term unnecessary to mean absolutely unnecessary.

4 Recognizing Absolutely Unnecessary Clauses

To see how one might show a set of clauses to be abso­ lutely unnecessary consider the clauses,

and let s = sl us2 us3 where s3 is a set of clauses which do not contain P2(c) and d. Since S1 is unsatisfiable, s2 is unnecessary for deriving the empty clause from s by binary resolution. The question is whether there is a method for determining that S2 are unnecessary without having to first obtain a proof.

Note, if all occurrences of P2(c) in S2 are replaced by P1(a) and all occurrences of dare replaced with b then S2 becomes the same as S1. Based on this observation it is easy to show, by induction, if C follows from S then we can also derive a clause C' from S- S2 where C' is C with all occurrences of P2(c) replaced by P1(a) and all occurrences of d replaced with b. For example, note that we can derive P2(c) by resolving P2(c)VQ(d, d) with P2(c)V·Q(d, d). Also note that by replacing P2(c) by P1(a) in the clause P2(c) gives the clause P1(a). We can also derive P1(a) by resolving P1(a)VQ(b, b) with P1(a)V·Q(b, b). From these observations it follows that if we can derive the empty clause from S we can also derive it from s - s2 since the empty clause replaced with anything just gives the empty clause.

A convenient way to express replacement is with the use of rewrite rules. A rule I--+ r applies to to term t if a subterm s of t mat~hes the left-hand side I with some substitution u (i .e. s = lu). To apply the rule the occurrence of the sub term s in tu is replaced with ru. For any set of rules R we write t :::::> R u to indicate a term t rewrites to u by a single application of a rule in R . A derivation is a sequence of rewrites; if t :::::> · · · :::::> u in zero or more steps we say u is derivable from t; if no rule can be applied to t we say that t is irreducible. A set of rules R is terminating if no infinite derivations are possible. We extend these definitions to clauses in the appropriate way.

For example let r 1 be the rule P2( c) --+ P1 (a) and let r2 be the rule d--+ b. Using this terminology we can say that the clause P2(c)VQ(d,d) rewrites to P1(a)VQ(b,b) using the rules r1 and r2. We can also say that P1(a)VQ(b,b) is irreducible by r1 and r2. We can now state a conjecture as follows:

Conjecture Let S be a set of clauses and R a set of rewrite rules such that the set of clauses S', obtained by rewriting all clauses in S to irreducible forms, is con­ tained in S. Then all clauses reducible using R are un­ necessary.

In the example just shown, we take R = { r1, r2} . Rewrit­ ing the clauses in S using R gives the irreducible clauses S1 which are contained in S. All the clauses in S2 are reducible using R and are therefore unnecessary.

Except for certain subtleties the above conjecture il­ lustrates the basic approach to showing clauses to be unnecessary. We are given a set of clauses S. We at­ tempt to find a set of rewrite rules R and use these rules to form a set S' obtained from S. If everything in S' is subsumed by something in S then any clause reducible by R is unnecessary. In order to clarify the conjecture we must answer the questions,

1. What properties do the rewrite rules have to have?
2. How do we form the set S' from S and R?

It turns out that the answer to the first question is that the rewrite rules have to be terminating and no rule in R should contain the negation symbol. The termination condition assures us that we do not have rules such as a - b and b - a both in R. The second condition as­ sures us that we do not have rules such as .,p- Q and P-Q.

The answer to the second question is that we form a set which we call the Terminal Overlap Closure of S and R. In the example we have been discussing all the rules and clauses were ground. In the case where the rules and clauses are not ground we must take into consideration clauses that may overlap with rules in R. For example, we may have a rule P(x, a)- Q(x) in Rand a clause in S of the form P(b, y)V R(y) . Although P(b, y)V R(y) does not rewrite using P( x, a) - Q( x), the left hand side of the rule, P(x, a), unifies with the literal P(b, y) and must be taken into consideration. In the next section we show how to compute the terminal overlap closure and indicate why this is the appropriate set.

5 Terminal Overlap Closure

We begin by defining the clause overlap of a clause C and a rule, 1- r. We assume that C and 1- r have no variables in common. Let r be a nonempty set of nonvariable subterms inC that unify with I and let A be the most general unifier (m.g.u.). Let C' be the clause formed by replacing every occurrence of lA in CA by rA. Then C' is a clause overlap of C and 1- r.

Example 1 If C is a ground clause and I - r is a ground rule then there is only one clause overlap, formed by applying I - r at every possible position in C. For example, the overlap of /(a)- a and P(f(a), f(a))VQ(/(a)) is P(a,a)VQ(a).

Example 2 When several subterms unify with the left hand side of a rule then there may be several clause overlaps of the clause and the rule. For example, consider the clause

and the rule

Since the identity substitution is an m.g.u. of {/(a, b)} then

is a clause overlap of c2 and r1. Likewise { x ~ a} is an m.g.u. of {f(a,b),f(x,b)} so

is also a clause overlap of c2 and r1.

Example 3 Another example of multiple overlaps can be illustrated by the clause

and the rule

In this case

are all unifiable. Therefore there are three overlaps of C and r,

1. P(f(a, y, c))VQ(g(b, z))
2. P(g(y,c))VQ(f(a,b,z))
3. P(g(b, c))VQ(g(b, c))

Next we define the Clause Overlap Closure 1 of a set of clauses S and a set of rules R to be the smallest set CC such that S C CC and if C E CC and C' is a clause overlap of C ~d some rule in R then C' E CC.

The Terminal Overlap Closure of a set of clauses S and a set of rules R is the set of all irreducible clauses that are in the clause overlap closure of S and R.

Example 4 Let S consist of the clauses,

and let R consists of the rules

Notice that both c4 and c5 are irreducible in Rand thus are in the terminal overlap closure. However c6 rewrites to

by r2 and thus is in the clause overlap closure but not in: the terminal overlap closure. Likewise c7 is not in the terminal overlap closure since it rewrites by r3 to

This clause is irreducible and is therefore in the terminal overlap closure. Since the subterm g(x,y) of c4 unifies with the left hand side of r 2 ,

is in the clause overlap closure. Since it is irreducible it is also in the terminal overlap closure. Now the subterm f(gl(x), y) of c9 unifies with the left hand side of ra.

is in the clause overlap closure. Again, since it is irre­ ducible it is also in the terminal overlap closure. Up to renaming of variables these are the only clauses in the terminal over lap closure.

1 The term "overlap closure" is used in [Gut tag et al., 1983] to denote a similar operation, but on a set of rewrite rules.

6 The Generalized Subsumption Theorem

We now state the generalized subsumption theorem and some important lemmas. We assume throughout that the set of rules R contain no negation symbols.

Theorem (Generalized Subsumption Theorem) Let R be a terminating set of rules. Let St and S2 be sets of clauses such that every clause in the terminal overlap closure of S1 and R is subsumed by a clause in S2. Then if there is a resolution refutation from St there is a refutation from s2 which contains only terms that are irreducible with respect to R. In other words, any clause that reduces by R is unnecessary.

This theorem applies to most common resolution strate­ gies with factoring. For example, the theorem holds if we are using DR-resolution with factoring. We will elab­ orate further how this theorem can be applied. First we will briefly indicate why the theorem holds.

The proof of this theorem is based on the following crucial lemma:

Lemma (Clause Overlap Closure Lemma) Let R be a set of rules. If C is a resolvent of C1 and C2 and C' is in the clause overlap closure of C and R then we can construct a Cf in the clause overlap closure of C1 and R, a C~ in the clause overlap closure of C2 and R , and a resolvent C" of C1 and C2 such that C" subsumes C'.

For example let S and R be the clauses and rules from example 4. Note that c6 is a resolvent of c4 and c5 . Also as shown, C7 is a clause overlap of cs and R. Note also that Cg is a clause overlap of c4 and Rand that it resolves with c5 giving c7 . Since c5 is in the clause overlap closure of c5 and R, the lemma holds for this example.

Based on this lemma we can show the following:

Lemma (Terminal Overlap Closure Lemma) Let R be a terminating set of rules. If C is a resolvent of C1 and C2 and C' is in the terminal overlap closure of C and R then we can construct a Cf in the terminal overlap closure ofC1 and R, a C~ in the terminal overlap closure of C2 and R , and a resolvent C" of C1 and C2 such that C" subsumes C'.

To prove this lemma we first use the previous lemma to construct clauses Cf in the clause overlap closure of C1 and R and a clause C~ is the clause overlap closure of C2 and R which resolve to a clause C" which subsumes C'. Next it can be shown that either Cf and C~ are irreducible or we can construct a clause overlap Cf' of Cf and R and a clause overlap C~ of C2 and R that resolve to a clause C 111 that subsumes C". We continue to construct clause overlaps in this manner. Since R is terminating, it can be shown that this construction must eventually terminate with clauses that are irreducible.

Now the generalized subsumption theorem follows by a simple induction argument based on this lemma. For full details of these proofs see [Benanav, 1989] .

7 Deletion Methods

Consider the way in which subsumption strategy works. Each time a new clause is generated a check is made to determine if the clause is subsumed by a previously generated clause. If it is, then the clause is deleted. Deleting clauses in this way is called forward subsump­ tion. Likewise is is also possible that the newly generated clause will subsume previously generated clauses. Delet­ ing these clauses is called backward subsumption.

More generally, we need to check whether a newly gen­ erated clause is unnecessary and whether it's appearance causes other clauses to become unnecessary. Deleting a new clause will be called forward deletion and deleting previous clauses will be called backward deletion.

In this section we discuss how the generalized sub­ sumption theorem can be used to develop methods for forward and backward deletion of clauses. There are sev­ eral methods which can be developed that do not sac­ rifice completeness, ranging from general methods that apply to any set of clauses to more specific methods that apply to clauses with certain special properties. The most general methods are probably too expensive to use for many clause sets.

First, suppose that S1 is the starting set of clauses, S2 is the set of clauses which have been derived from sl ' and R is a set of terminating rules such that everything in the terminal overlap closure of S1 and R is subsumed by something in S2. (When we begin R is empty) . If c is a clause generated from s2 which is reducible by R then C is unnecessary and can be deleted. If C is irreducible then we can attempt to find a set of rules R' such that C is reducible by R', R U R' is terminating, and everything in the terminal overlap closure of sl and R u R' is subsumed by something in S2 · Subsequently, any rule reducible by R U R' can be deleted.

To illustrate this we consider the example discussed in section 2. We assume that the starting set of clauses , S1 , consists of the clauses G1 , G3 and some other clauses that do not contain the symbols Pl or P2 . Since these symbols are skolem functions no other clauses will con­ tain them except possibly some equality substitution ax­ ioms. We show, however , in [Benanav, 1989] that the equality substitution axioms for skolem functions are simply unnecessary.

As before, we can derive the clauses, G2 · Let S2 = S1 U G2 and let R consists of the rules

By the generalized subsumption theorem, if it can be shown that everything in the terminal overlap closure of S1 and R is subsumed by something in S2 , then anything reducible by R is unnecessary. In particular the clauses G2 are unnecessary. Computing the terminal overlap closure of S1 and R gives the clauses S1 and the clauses,

Note that G4 are subsumed by G3 . Therefore we have shown that everything in the terminal overlap closure of S1 and R is subsumed by something in S2 .

Although axiom A3 is not an axiom of geometry, this example illustrates what actually happens when when resolution-based systems are run on a set of clauses rep­ resenting Hilbert's axioms for geometry. The axioms A1, A2, and A6 are three such axioms and are represented by the clauses G1 and 2. These clauses produce the clauses 2 which can be shown to be unnecessary by the generalized subsumption theorem.

We have shown how to use the generalized subsump­ tion theorem to show that a set of clauses is unnecessary however, we have not indicated a method for finding the appropriate set of rules, [{. There are two difficulties associated with finding these rules. First, it may be dif­ ficult to show that R U R' is terminating. In fact, the termination problem has been shown to be undecidable. Nevertheless, much research has been devoted to this problem and several excellent methods for proving ter­ mination are available (see [Dershowitz, 1987] for a sur­ vey). Another difficulty is testing that everything in the terminal overlap closure of S1 and R U [{ is subsumed by something in S2 · In cases where the terminal overlap closure of S1 and R U R' is finite we can simply check that each clause is subsumed by a clause in S2 · But if the terminal overlap closure of S1 and RUR' is very large this can be computationally expensive. In fact, checking whether a term is subsumed by another term is NP-hard.

There are several ways to circumvent these difficulties. For example, we can require that the right hand sides of all rules be ground terms that are not reducible by other rules. In such cases it is easy to show that the rules will be terminating and the terminal overlap closure of S1 and R will be finite. In addition, we can require the left hand side of the rules to be ground terms not reducible by other rules. Then to check that everything in the terminal overlap closure of S1 and R U R' is subsumed by a clause in S2, one need only compute the terminal overlap closure of S 1 and R'.

It is not always necessary to construct rules in the ac­ tual implementation of deletion strategies based on the generalized subsumption theorem. For example in the case of permutative predicates it may be possible to de­ termine that only one permutation of each formula need be retained. For a discussion on efficient methods that partially solve the naming problem and the permutative predicate problem see [Benanav, 1988].

8 Conclusions

In this paper we have shown how resolution systems tend to generate unnecessary clauses and have presented a theorem which can be used to show certain clauses are unnecessary. To apply this theorem one must be able to construct a terminating set of rules that have a special relationship to the starting set of clauses and the derived set of clauses. Namely, everything in the terminal over­ lap closure of the starting set of clauses and the set of rules must be subsumed by a clause in the derived set of clauses. In general these rules can be difficult to find, however by placing appropriate restrictions on the kinds of rules used, efficient methods can be developed.

Unfortunately, this theorem alone does not allow for the deletion of other kinds of unnecessary clauses that can be generated. In order to determine the full range of applicability of this theorem more experimentation needs to be done. In addition, we believe that further investigation of methods for deletion of other kinds of un­ necessary clauses, such as those that are irrelevant, can signifigantly enhance resolution based systems. In fact, any reasoning system will need to devote computational resources to these matters in order to be effective.

Acknowledgments

I would like to thank my advisor David Musser for his helpful suggestions on drafts of this paper and for several useful discussions I had with him regarding the ideas in this paper. I would also like to thank the developers of LMA and ITP for providing a powerful automated reasoning program which has been an invaluable tool for this research.