A Hierarchical Approach to Theorem-Proving

1. Introduction

A considerable amount of recent work in theorem-proving has been concerned with methods for increasing the power of inferences which can be made in special cases. This appears to be in response to the widespread recognition that general purpose theorem provers, particularly those using resolution [10] as their inference rule, have extreme difficulty with particular aspects of proofs for which there are fairly effective algo­ rithms and heuristics. Oustanding exam­ ples are equality, commutativity, and associativity. It is generally recog­ nized that such properties are n.ore efficiently dealt with if they are some­ how 'built in' to the theorem prover, rather than proviced in the form of axioms. There is, however, an under~ standable reluctance to destroy general­ ity or completeness by ad hoc mechanisms.

The usual approach has been to search for methods of replacing an axiom or a set of axioms with an inference rule. This has resulted in a number of suggest­ ed methods for treating equality [1,2,5, 6,7,8,11,12], associativity and commuta­ tivity [1,4,15], and other properties [14,16]. One of the problems with equality is that proving two terms equal is in general as difficult as proving an arbitrary theorem -- equality is undecid­ able, and any theorem can be expressed using just the equality predicate. Associativity is not as difficult, but the fact that there are an infinite num­ ber of ways of unifying terms involving associative functions gives rise to significant problems.

Recently we have been looking at a method of incorporating axioms into inference rules which approaches this problem in a different way. The idea is to split an unsatisfiable set S of clauses into two disjoint subsets, say u and S-U, and to use a theorem prover working on clauses of U to generate inference rules which are applicable to clauses of s-u. If these inference rules are generated on demand, this method is not necessarily restricted to values of U for which an equivalent finite set of inference rules are known. In this paper we discuss a simple inference rule called U-genera~ized-resolution which is com­ plete for any subset U of S.

* This work was supported by grant number N0014-75-C-0571 from the Office of Naval Research; and by ERDA, contract number EY-76-C-02-3077.*000.

This approach grew out of some discus­ sions with David Yarmush and Norman Rubin concerning the problem of equality. It was suggested that an appropriate general­ ization of resolution to deal with equali­ ity consisted of generalizing the unification procedure so that literals could be unified if they had the same predicate and a substitution could be found which would make the arguments equal, rather than identical. Since equality is in general undecidable, such a procedure would require the use of a theorem-prover within the unification procedure. We discuss this approach to equality, which we call U-equality-gener­ alized resolution, in Section 2. The more general approach, which we call U-generalized resolution and which gives a framework for dealing with properties other than equality, is treated in Sec­ tion 3.

2. U-Equality-generalized Resolution

Given two clauses (written as sets of literals)

we can infer

if we can prove

and ).. is the most general simultaneous unifier (mgsu) of the pairs of terms

If (4) is deduced from a set U of clauses, we refer to (3) as a U-e1uality-generaliz­ ed resolvent of (1) and 2).

In a similar way, from the clause

we can infer

if we can prove

and and

It is clear that for any inconsistent set S of clauses, the inference rules of U-e-g-resolution and U-e-g-factoring are sound and complete if U is any subset of S to which is added the equality reflex­ ive axiom x = x, since any resolvent or factor can be obtained by U-e-g-resolu­ tion or U-e-g-factoring using just the clauses x = x inferred from U. What we would like to be able to do is to prove completeness results for sets U when U-e-g-resolution and U-e-g-factoring is only permitted on clauses of s-u or their U-e-g-resolvents or U-e-g-factors. A preliminary result of this form is given in (5); this says that if U contains just the axioms of equality, possibly together with some or all positive equality unit clauses from S, a refutation of (S-U) u {x = x} can be obtained by U-e-g-reso­ lution alone if S has a refutation tree. We say that a set of clauses has a refu­ tation tree if and only if it has a refu­ tation graph, using the terminology of Shostak [13], which is a tree (i.e. each bridge connects exactly two literals); having a refutation tree is equivalent to having a unit refutation or an input refutation. This result shows that, at least in the case when S has a refutation tree, the use of the equality axioms can be restricted to within the unification procedure.

This method of dealing with equality would appear to have a number of advan­ tages over other methods such as para­ modulation. These include:

• o The application of aimless infer­ ences involving equality substitutions is restricted to cases when such substitu­ tions will permit a resolution which would not be possible in the absence of the equality clauses.
• o The equality subproblem is specified by two terms which must be made equal. In heuristic search terms this is a problem with a well defined start node and a well defined goal node, and so should be

subject to more powerful techniques such as bi-directional search, and operator­ difference methods (such as those used with considerable effectiveness in FDS [9], for example). Note that in the standard resolution approach, the goal node is the null clause, which does not provide very much information which can be used for heuristic guidance.

• o Properties such as associativity and commutativity are specified by positive equality unit clauses, so that their use can be restricted to within the equality­ prover. The use of specialized tech­ niques for dealing with these properties, such as the use of parenthesis-free nota­ tion, can therefore be restricted to within the equality-prover.

So far, investigations carried out to determine the effectiveness of this equal­ ity method are very encouraging. For sets of clauses with input refutations, some results are given in 15]. A more exten­ sive, but also a more complex, set of experiments have been carried out by Rubin [12]. This involved the construc­ tion of a theorem-proving/programming system called DILEMMA, using e-g-resolu­ tion (called coercion), . evaluatable pred­ icates, and heuristic guidance functions. This was used to prove theorems in geometry, giving results similar to those of the well known work of Gelernter [3]. In fact in some respects the results were superior, since the construction proce dure used by Gelernter dropped out auto­ matically from the unification procedure.

3. U-generalized-resolution

U-generalized resolution can be defin­ ed in the following way. From the

clauses

we will infer

if we can deduce the clause

from a set U of clauses, where 'A is the mgsu of the pairs

We call (10) a u-~eneralized resolvent of (8) and (9), or s~ply a U-g-resolvent. We will refer to clause (11) as the linking clause.

In the above definition we will normally not permit the L and M literals to be the constant literals "true" or "false", since every resolvent would also be aU-g-resolvent for any u. However, in the special case when (B) is null and when the U-g-resolvent (10) subsumes either AA or CA we will permit the M literal to be 'true'. We will then refer to (10) as a unary U-g-resolvent. Unless state<,l to the contrary, the term U-g­ resolution will be intended to include unary U-g-resolution.

Theorem. Given any unsatisfiable set S of clauses, and a satisfiable subset U of S, a refutation of s-u can be obtained by U-g-resolution and factoring.

Proof. Consider any resolution refuta­ t~on R of S, consisting of operations of factoring or resolution, and consider the resolutions of R in order. Each such resolution is between two clauses, each of which is either supported by (S-U), or is not. Each resolution in R is thus one of the followin9

• o between two (S-U)-supported clauses
• o between two non-(S-U)-supported clauses
• o between an (S-V)-supported clause and a non-(S-U)-supported clause

In the first case the resolvent is also a binary U-g-resolvent with the linking clause being a tautology containing only the resolved literal and its negation. In the second case we can regard the resol­ vent as part of the process of deducing a linking clause from U; this clause is also non-(S-U)-supported. In the third case we can construct the resolvent by U-g-resolution in the following way . If A u {L} is the (S-U)-supported clause and B U {IL} is the non-(S-U)-supported clause, with L being the literal resolved on, construct the U-g-resolvent of A U{L} abd A U {L} with B U {IL} U {IL} as the linking clause. Thus each resolvent in R can be constructed by U-g-resolution, which with factoring is therefore comple complete. 0

The above theorem, though showing that U-g-resolution is complete, does so by constructing U-g-resolution proofs which are as long as standard resolution proofs. However, it is clear that many resolution proofs contain sequences -of resolutions which can be accomplished by a single U-g-resolution. This can easily be seen with the aid of Shostak's representation of refutations in the form of refutation graphs [13]. For example, consider the following set of clauses (actually the clauses for a version of the theorem that in a group the left inverse is a right inverse) :

1. P(e,x,x)

• -1 2. P(x ,x,e)

o identity

• o left inverse
• P(u,v,x) ,P(v,w,y) ,P(u,y,z) ,P(x,w,z)
• o associativity
• P(u,v,x) ,P(v,w,y) ,P(x,w,z) ,P(u,y,z)
• o associativity

o negated theorem

• -1 5. P(a,a ,e)

A refutation graph for these clauses is shown below.

9 121

(Circles represent literals, touching circles are in the same clause, solid lines represent resolution steps, dotted lines represent merges.)

If we now assume U to contain, for example, the clauses numbered 1, 3, and 4 above, we can get a U- g-resolution proof in only 2 steps. This is shown below in the form of graph 'collapses', each of which corresponds to a U-g-resolution step:

(5)

derived

from U

Intermediate step

showing U-g-r of

( 5) with ( 2) ·

~ (__U-g-r of (5)

with (2)

Graph after one step.

D

Proof obtained

after 2 steps.

In fact it can be shown [5] that any refutation for which the refutation graph is a tree can be collapsed by U-g­ resolution without using any applica­ tions of U-g-resolution in which the two (S-U)-supported clauses are identical in the graph (we will call these weak U-g-resolutions).

Unfortunately, this result is not true in general. The following refutation graph, for example, in "rhich the clauses in U are shown with a double line around them, cannot be collapsed by (nonweak) U-g-resolution steps:

However, by duplicating the C clause. above, this graph can be collapsed by 4 U-g-resolution steps, still better than the best resolution refutation of 5 steps. An informal survey of a number of resolu­ tion graphs suggest that the number of weak U-g-resolution steps required is either zero or is very small. In fact we have not found a counterexample to the conjecture that if (S-U)-supported clauses can be duplicated, as in the above example, no weak U-g-resolutions will be required at all.

The use of U-g-resolution does not necessarily aid the search process required to construct a proof, though within U the search for a linking clause can be bidirectional rather than uni­ directional, as in U-e-g-resolution. It is our feeling that U-g-resolution will be most effective when the clauses of U have a structure which facilitates this search. In fact it is our feeling that the domain-independent approach to theorem proving will not prove to be fruitful in any case, so we are more interested in specialized applications of U-g-resolution. We anticipate that these specializations will come in the form of more efficient algorithms for inferring appropriate clauses from particular sub­ sets U. We feel that our results with U-e-g-resolution offer substantial evi­ dence that this approach is effective.

Another possibility is that the theorem proving technique used to deduce clauses from U could use U'-g-resolution as its inference rule, where U' c u. This suggests a possible scheme for a multilevel hierarchical theorem proving system, which we would expect to be organized along the following lines:

• o Each level would deal with problems whose solutions are expressed in a small number of powerful inference steps.
• o Each level would deal with a subset of the clauses concerned with a particu­ lar aspect of the problem, and would be concerned with solutions to the corres­ ponding subproblems.
• o Each level would use specialized techniques if these were known to be effective for the particular subproblem.

A hierarchical organization such as discussed here is somewhat more diffi­ cult to organize than a conventional single-level organization. In general it will not be possible for the lower­ level theorem prover to terminate its search, so some mechanism must be pro­ vided for it to resume later. A simple implementation would just use some kind of cut-off parameter which could be incremented if the proof was not success­ ful. A more sophisticated approach would be for the lower-level theorem prover to return resumption information, perhaps in the form of an incomplete search tree, or in the form of a suspended 'process'.