Consolution and its Relation with Resolution

1 Introduction

In the field of automated theorem proving, there are a number of calculi that have been proposed and imple­ mented for deducing the validity or, equivalently, the unsatisfiability of a formula of first order predicate logic. The best known such calculus is resolution [Robinson, 1965] which is (usually) restricted to formulas in clause form. Another major method for automated deduction is the connection method (see [Bibel, 1987]). We have to distinguish between the concepts of a calculus and a method. A calculus has fixed rules which are given once and for all. On the other hand, a method for de­ duction is a design philosophy for designing calculi. A method determines a class of calculi by providing means and concepts for the specification of calculi, and, usually, theorems which are useful for proving the adequacy of calculi specified with these means. Resolution is a _cal­ culus whereas the connection method is a method. A number of calculi, called connection calculi, have been developed on the basis of the connection method.

There has been a long discussion on the advantages and disadvantages of the connection method versus reso­ lution. Some clear advantages of the connection method are the greater directedness of its proof search and the fact that its calculi do not disrupt the structure of the input formula as resolution does. This means it pro­ vides more information that can be used by strategies for directing the proof search. On the other hand, the connection calculi developed so far lack an important fea­ ture that is present in resolution, namely the use of lem­ mata. In resolution, a clause that has been derived can be reused for resolution an_ arbitrary number of times. The lack of this feature makes a derivation in these con­ nection calculi for some classes of formulas considerably longer than in resolution (see [Eder, 1989]).

·Most of the research and work leading to this paper was done during a stay at ICOT in Tokyo. I want to thank Wolf­ gang Bibel for his help in the formulation of the method and

for valuable hints and discussions.

In this paper we introduce the method of consolution which is based on the connection method. We also spec­ ify a particular consolution calculus as a basic calculus which may still be enhanced. Consolution has a very close relationship to resolution. In fact, resolution is a restriction of consolution in the sense that a strategy can be imposed upon the consolution calculus to make it identical to resolution. Thus consolution provides a bridge between the connection method and resolution. It allows to combine the directedness of the proof search present in the connection method with the powerful tool of the use of lemmata present in resolution.

2 The connection method

We give here only a brief description of those concepts underlying the connection method which are relevant for consolution. As in resolution, a formula in normal form is represented by a set of clauses in the connection method. 1 But since the connection method is formulated as a method for proving validity rather than unsatisfia­ bility of formulas, we consider here the disjunctive nor­ mal form rather than the conjunctive normal form. So, a clause represents the existential closure of the conjunc­ tion of its literals, and a set of clauses represents the disjunction of the formulas represented by its clauses. A set of clauses is also called a matrix. A clause is usually depicted as a vertical column consisting of its literals. A matrix is depicted in two-dimensional representation as the columns depicting its clauses, written next to each other. For example, the formula

1 Actually, the connection method is not restricted to for­ mulas in clause form. Since, however, any arbitrary for­ mula can be transformed to clause form by a fast structure­ preserving transformation (see [Greenbaum et al., 1982; Eder, 1985; Plaisted and Greenbaum, 1986]), we shall for simplicity restrict ourselves to clause form formulas in this

paper.

is represented by the matrix

which is depicted as

A path through a matrix is a set of literals, exactly one taken from each clause. In our example there are four paths through the matrix, and {P, -.P, -.Q} is one of them. Two literals are complementary if one of them is the negation ofthe other. A connection in a set of clauses is a pair of literals which can be made complementary by instantiation, ie., by application of substitutions. A path is complementary if it contains two complementary literals. The connection method is based on the following theorem.

A formula in disjunctive normal form is valid if and only if there is a finite set of instances of its clauses through which each path is complementary.

A theorem prover implementing the connection meth­ od takes the clauses of the input formula and checks all paths through this set of clauses systematically for com­ plementarity. At each step, a connection is chosen in a path that has not yet been checked for complementar­ ity. If necessary, this connection has to be made comple­ mentary by unification, thus instantiating the involved clauses in the proper way. Moreover, it may be necessary to take into account more than one instance of a clause. In this case a new variant of the involved clause has to be considered. A detailed introduction to the connection method can be found in [Bibel, 1987].

3 Basic definitions

By a path in a matrix we mean a subset of a path through a matrix. Thus, a path in a matrix is a set of literals, at most one chosen from each clause. We shall also use the term partial path for a path in a matrix. An extension of a path p in a matrix M is a path q in M such that p ~ q. If c is a clause, p and q are finite sets of literals and P and Q are finite sets of finite sets of literals then we define

Pc is the set of (one-element) paths through the (one­ clause) matrix { c}. If M and N are disjoint matrices, ie., disjoint finite sets of clauses, then pq is a path in M U N for every path p in M and for every path q in N . Similarly, PQ is a set of paths in M U N for every set P of paths in M and for every set Q of paths inN. We call the set PQ the product of the sets P and Q.

4 Consolution in propositional logic

The idea behind consolution is the following. In order to prove the validity of a given formula using the connection method, all paths through its matrix have to be checked for complementarity. At each stage of a connection proof a certain set of paths has already been checked for com­ plementarity whereas all the remaining paths still have to be processed this way. In consolution at each stage of a proof process, this remaining set of paths yet to be checked for complementarity is represented. It would be inefficient, however, to explicitly represent each path of this set since the number of paths in general increases exponentially with the number of clause instances. In­ stead, this set of paths is coded in the form of a set of partial paths. Each partial path encodes the set of all its extensions through the whole matrix. So one partial path may encode many paths through the matrix. Let us consider an example which for simplicity is taken from propositional logic.

Suppose we want to prove the validity of the formula

The following tree is a proof tree of this formula by con­ solution.

Each node of the tree is marked with a set of (partial) paths in the matrix M

representing the given formula. A leaf of the proof tree is marked with the set Pc of all one-element paths through some clause c of the formula, ie. Pc = {{L} I L E c}. Since every path through the given matrix M is an ex­ tension of a path through c for every c E M, the set P c encodes the set of all paths through M. Thus the marks Pc of the leaves reflect the fact that at the beginning of the proof process all paths through M still have to be checked for complementarity.

The inference rule, also called consolution, takes the set of partial paths from each premise and com­ bines these sets into a new set, called the consol­ vent. This combination can be regarded to con­ sist of two parts. The first part consists of build­ ing the product PQ of P and Q. For example, if P = {{P}, {Q}} and Q = {{-,P}, {Q}} then PQ = { {P, -,p}, {P, Q}, {Q, -,P}, {Q}}. The second part of the inference rule consists in simplifications of PQ. One such simplification is the elimination of complementary paths. To continue the illustration of our example, this means that the complementary path {P, -,p} is removed from PQ. Actually, both parts are to be seen as a single operation, a remark which bears its relevance on the effi­ ciency of implementation. But for the ease of the reader's understanding we will continue to make the distinction.

The proof in our example is completed by applying consolution once again to the result of the previously illustrated step and the remaining leaf { { -,Q}}. The resulting empty set is the criterion of a successful deriva­ tion (as in resolution). To summarize, for a formula F in disjunctive normal form, a proof ofF is a derivation of the empty set from the sets Pc (c E M) with the consolution rule, where M is the set of clauses of F.

While this explains the essentials of the calculus, the following additional details complete its description. Above we have used a single simplification which is elim­ ination of complementary paths. This is all needed for completeness and soundness of the calculus. For effi­ ciency, it is necessary to incorporate at least the following simplification (since otherwise a huge number of paths will quickly be generated in practice). Any path pin PQ may be replaced by any subset of p. Both simplifications may be applied simultaneously. So in our present exam­ ple, the first consolvent { {P, Q}, {Q, -,P}, {Q}} may be further reduced, for instance to {{Q}}. Note that three distinct paths have been replaced by a single one in this case. In general, the number of paths may be reduced considerably this way. If we incorporate this simplifica­ tion into the derivation shown above, the following proof tree of the same formula results.

In summary, any consolution calculus must, among its simplifications within the consolution rule, include the elimination of complementary paths. While it is not ab­ solutely necessary, the shortening of paths is understood to be always included in consolution. As an aside we mention that such an inclusion amounts to an extension of the basic calculus. A further extension of consolution might include Prawitz' matrix reduction, but no investi­ gation has been made yet into this possibility.

Note that consolution allows a systematic checking of paths. If we enumerate the paths through a matrix in any given order then a consolution derivation can check them one after the other in this order. A suitable appli­ cation of shortening of paths will make this systematic checking more efficient by allowing to check more than one path in one step. Systematic checking of paths is not possible with resolution since there at each step the paths are shortened to length 1.

5 Consolution in first oder logic .

The lifting of consolution to first order logic is done in much the same way as it is done for resolution. In this section we give a formal description of consolution for full first order logic.

By a path set we mean a finite set of finite sets of lit­ erals. We shall use this term even if these sets of literals are not paths in some particular matrix.

Definition 5.1

A path set Q is obtained f~:om a path set P by elimi­ nation of complementary paths if there is a set of con­ nections in elements of P and a most general unifier u of this set of connections such that Q is the set of non­ complementary elements of P u.

Definition 5.2

A path set Q is obtained from a path set P by shortening of paths if there is a surjective mapping f : P ~ Q such that f(p) ~ p holds for all pEP.

Definition 5.3

A path set 'R is obtained from a path set P by simpli­ fication if there is a path set Q such that Q is obtained from P by elimination of complementary paths. and such that 'R is obtained from Q by shortening of paths.

The inference rule

if there exists a variant Q' of Q which does not have any variables in common with P such that 'R is obtained from the product PQ' by simplification.

We say then that the path set 'R is a consolvent of the path sets P and Q.

Definition 5.4

A derivation of a matrix M is a finite sequence (Po, ... , Pn) of path sets such that the following con­ ditions hold.

1. For all k = 1, ... , n, the set PA: equals Pc for some c E M, or 'PA: is a consolvent of Pi and 'Pj for some i,j < k.

2. Pn = 0.

Theorem 5.1

A formula in disjunctive normal form is valid if and only if there is a derivation of its matrix by consolution.

Proof: In order to prove correctness, let us assume that F is a formula and M its matrix. Further assume that (Po, ... , Pn) is a derivation of M by consolution. To each finite set p of literals we attribute a formula Fp as follows . Let Fp be the disjunction of all literals of p. To each path set P we attribute a formula Fp as follows. Let Fp be the existential closure of the conjunction of all Fp with pEP. It then holds that {-,Fp,-,FQ} ~ ..,pR if n is a consolvent of P and Q (The proof is exactly the same as the proof for the soundness of the resolution rule). Moreover, Pc ~ F for all c E M. By induction on j it follows that F1'; ~ F for all j = 0, .. . , n. In particular for j = n, the set Pi is the empty set and therefore Fp. is the empty conjunction, ie., the verum T. SoT ~ F which means that F is valid.

For the proof of completeness we shall see in the next section that every set of clauses for which there is a resolution refutation, also has a consolution derivation. From the completeness of resolution it then follows that also consolution is complete.

q.e.d.

In the completeness proof note the duality between proving validity of a formula in disjunctive normal form and proving unsatisfiability of a formula in conjunc­ tive normal form. On the level of clauses and matri­ ces there is no difference between affirmative and refu­ tational proving. In fact any refutational calculus can just as well be formulated in an affirmative way and vice versa, and it would not even make a difference in the codes of implementations.

6 Relations to resolution

If we look at the last proof tree shown in Section 4 then we see that its path sets contain only one-element paths. If we replace each path with the single literal which it contains then we obtain the tree

Note that this tree is a resolution refutation of the given clause set. In this way any resolution refutation of a set of clauses can be obtained by consolution. To be more specific, the following holds.

Theorem 6.1

Let M be a matrix and let (co, ... , cn) be a resolution refutation of M. Then (Pc 0 , · ·· , Pc,.) is a consolution derivation of M.

Proof: The only non-trivial part of the proof is to show that Pe is a consolvent of Pc and Pd if e is a resolvent of c and d. So let e be a resolvent of c and d and let co U do be the set of literals resolved upon where co ~ c and do ~ d. 2 · Let d' be the clause obtained from d by seperating apart the variables of c and d. So, d' is a variant of d. Let d0 be the corresponding variant of do. Then Pd' is a variant of Pd, and PcPd' is the set of all {I, J} such that I E c and J E fl. Let K be the set of all pairs (I, J) such that I E co and J E d0. Then the set Q defined as

is obtained from PcPd' by elimination of complementary paths (choosing as connections the elements of K). For each path {I, J} E Q we define

Then the range off is Pe· So Pe is obtained from Q by shortening of paths. Thus Pe is a consolvent of Pc and Pd.

From this theorem it follows that consolution can sim­ ulate resolution step by step (and therefore consolution is complete as indicated in the last section). On the other hand, consolution is much more general than resolution because it can handle paths of arbitrary lengths. In fact, resolution can be seen as one consolution strategy where all paths are shortened to length 1 in a certain way at each step. Other strategies of consolution are given by the connection calculi that have been developed so far. They involve paths of arbitrary lengths.

As a further remark we point out that the sets re­ sulting by consolution from paths in a given matrix are not always paths in the matrix as in the example shown above. Rather they may also be the union of such paths even in propositional logic. For illustration, the reader may also think of paths in a matrix that has multiple occurrences of clauses.

7 Conclusion

Consolution is a method for clause form theorem prov­ ing. We have proved that the consolution calculus pre­ sented here is complete and sound and that it can sim­ ulate resolution step by step. It is more general than resolution because resolution allows only paths of length 1 whereas consolution allows paths of arbitrary length. This advantage becomes most apparent from the fact that consolution allows a systematic checking of paths as any connection calculus does. Such a systematic check­ ing of paths is not possible in resolution since there the paths are shortened to length 1 in every step. On the other hand, consolution provides the powerful tool of the use of lemmata which is present in resolution but lack­ ing in previous connection calculi. A consolvent that has once been derived can be used as a parent in any number of further consolution steps.

2 We assume that factorization is included in the resolution rule as in [Robinson, 1965]