Towards an Advanced Implementation of the Connection Method

1. GROUND-LEVEL FEATURES

While in [2] and [5] some techniques have been introduced to enhance the performance of the Con­ nection Procedure for normal form matrices of pro­ positional logic, their adaptation to non-normal form will be dealt with in the following para­ graphs. A detailed discussion of these and further

issues may be found in [8].

1.1. Definition:

Given an occurrence Lr of a literal L at some position r, rwe define the clausal core of Lr, in symbols cc(L ) , as the set: cc(Lr) := {Ks I Ks is an element of a clause in

which Lr occurs}

Note that in the non-normal form case a matrix is a set of clauses, which may contain submatrices, which in their turn may contain clauses and so on. Now it becomes important to distinguish between whether a literal is an element of a clause (in the set-theoretic sense) or only occurs within it, "to occur" referring to the transitive closure of the

is-element-of relation.

As an example consider the clause {R,K,{{{L, stance, R,K are elements of the clause while L,M,

M},N},{O,P}}} of a main matrix. Here, for in­ N,O,P only occur within it. Examples of clausal cores are cc(K)={R,K} and cc(L)={R,K,L,N},

Recall that in the course of a connection proof subgoals are stored to be handled later. If any such subgoal is a literal then it is contained in the clausal core of some path literal. This enables an easy access to a relevant part of the clausal core of path literals.

The following proposition together with the subsequent theorem have an immediate application to reducing the number of paths to be checked for

complementarity.

1.2. Proposition:

Given a path p through an arbitr~ry matrix M. (a) If there is an occurrence L of a literal s.t. r s I r s the set N(L ) := !K in p L in cc(K )} is not empty, then (p\N(L )) U {Lr} is a path through ~· (b) Furthermore, if p contains an occurrence L of

• a rliteral, then p is complementary if (p\N(Lr)) U {L } is complementary. r u
• (c) If there are occurrences L and -L of !iter­ als then p isucomplementary if both (p\N(L )) U {Lr} and (p\N(-L )) U {-L } are complementary.

1.3. Theorem:

Given a partial path p and a clause c selected for extension, then (1)-(3) hold:

1. The continuations of p through the occurrence Ls of a literal inc need not be checked for com­ plementarity if there is an occurrence Lr of the literal L which appears both among the stored sub­ goals and in the clausal core of a path literal.
2. If p does not contain an occurrence of the literal . ~ but c contains an occurrence -Lu and a subgoal L exists which is in the clausal core of a path literal, then only the continuations of p through -Lu must be checked for com~lementarity.
3. If c contains an occurrence K of a literal and p contains an occurrence Ks of the same literal then we can exclude c as a clause suitable for extension.

Part (1) and (3) of the theorem are dynamic applications of factorization, while (2) is a dy­ namic application of a generalized form of 6.1.T in [2], which expresses an idea due to Prawitz.

An unreflected combination of part (1) of the theorem and ditchmarking [2] would result in an erroneous proof procedure, as pointed out in [5] as an open problem. This has now been solved by stor­ ing the occurrence Lr together with all the infor­ mation needed for a future checking for complemen­ tarity of the paths containing Lr.

2. THE CONCEPT OF WEAK UNIFICATION

In order to prove a formula F of first-order logic using the connection or resolution method it is, in general, necessary to consider, at least implicitly, several copies (obtained by renamings of variables) of each clause. Such a formula . F which we shall, for simplicity, here assume to be in normal form is valid iff there exists a set of copies of its clauses which can be made tionally complementary by substitution bles. So if c and d are two different clauses of F then we have to look for proposi­ of varia­ copies of unifiable connections between literals of c' and d', respec­ tively, where c' and d' are obtained from c and d by applying the current substitution generated so

far in the proof process.

It is necessary for an efficient proof proce­ dure to eliminate, before actually establishing the ·proof, all searches for connections which can be recognized in advance as not unifiable by taking into account a single copy of each clause. This leads us to the concept of weak unification. A similar but weaker concept has been introduced in [11] under the name of weak substitution.

2.1 Definition:

or literals L and M are called weakly if there are substitutions + and t such Mt · Two terms unifiable that L+

A set {L,-M} of literals occurring in two (not necessarily different) clauses of a formula F is called a weakly unifiable connection, for short a w-connection, if L and M are weakly unifiable.

Obviously, L and Mare weakly unifiable iff two copies L- and M- of L and M, respectively, with disjoint sets of variables are unifiable. Hence any connection between literals of clauses c' and d' as above must correspond to a w-connection of F. So we first determine, using a unification algorithm, the set of w-connections of F. In the main part of the proof procedure we then only need to consider con­ nections corresponding to w-connections.

There is another advantage of weak unifica­ tion. If we check two literals L and M for weak unifiability then the unification algorithm gives us a most general unifier ' of L- and M- as above. Let + be the current substitution. In order to establish a new connection between L and M we have to find out whether L-+ and M-+ are unifiable. Let t denote the most general unifier of these two literals. Then, after the proof procedure has taken into account the connection {L-,M-}, +t is the new current substitution. Now the point is that + can be obtained as a supremum of + and ' in a lattice of equivalence classes of substitutions by the following theorem the non-trivial proof of which is given in (6]. There are similarities with the lattice of equivalence classes of terms intro­ duced in [9] although a direct relationship does not seem to exist.

2.2 Theorem:

For substitutions + and t let + ~ t iff there is a substitution t such that +t = f. We say that two idempotent substitutions + and t are equivalent to each other iff + ~ t and t ~ + · Then the set of equivalence ciasses of idempotent substitutions together with an added greatest ele­ ment is a complete lattice.

Determining the supremum of + and · in this

lattice amounts to a unification of pairs of terms. It takes less time than a unification of {L,,Mf}· Incidentally, if F is valid then its set of w­ connections is spanning (in one copy of F), a fact which may be taken advantage of for the elimination of useless alternatives in the course of proof.

Another property which can be checked by look­ ing at just one copy of the matrix is whether a clause contains a pure literal. The simplest case is that the clause contains a literal which does not have a w-connection with any literal of the matrix. Then we can delete the whole clause (with all its copies) from the matrix. But there are

other cases in which we can also do this.

2.3 Definition:

Let c be a clause ofF, c' an instance of c (i.e., c' is obtained from c by substituting consistently all variables of c by closed terms), and La liter­ al of c'. Then we call La pure literal of c' in F if, for all literals M of F and substitutions +, {L,M+} is not complementary. Note that L is not a literal of F. If there is a pure literal of c' in F then we call c' a pure instance of c in F. c is called a p-clause of F if every possible instance of c is a pure instance.

2.4 Proposition:

A formula F in normal form is valid iff the formula obtained from F by deleting all p-clauses of F is valid.

is a p-clause although each of its literals has a w-connection. Our concept of p-clauses is a gener­ alization of pure-reduction (see [2]), It allows us to look ahead for all possible connections with

this clause.

The following proposition provides a way of testing for p-clauses as follows. Let us call a set k of w-connections of F a brush of c in F if c={L 1 , ··· ,Ln} is a clause of F and k has the form {{L 1 ,K 1 }, ··· ,{L ,K }} where K 1 , ··· ,K are arbitra­ ry Iit~rals of ¥. ~ is called ~onsistRnt if the set {{L1,M 1 }, ··· ,{Ln,Mn}} is unifiable where M 1 , ··· ,Mn are obtained from K 1 , ··· ,Kn by suita­ ble renamings of variables. Th~n c is a p-clause iff no brush of c is consistent. The number of unifications needed for a consistency check of a brush of c is equal to the number of literals in c and the number of brushes of c is the product of the numbers of w-connections of the literals of c. So the amount of time needed to determine whether a clause is a p-clause can be estimated in advance which in turn gives information for the control of the proof process.

3. ON THE NUMBER OF COPIES NEEDED OF A CLAUSE

In ce rtain special cases bounds can be given for the number of copies needed of a clause. Howev­ er, this is not true in general since first-order logic is undecidable. A few simple estimates are the following.

• If maximum in F, c variables needed of F contains no function symbols, k is the of 1 and the number of constants occurring is a clause of F and n is the number of occurring in c then at most kn copies are c. This fact is useful if the number n of variables occurring in c is small. However, already the case where F contains only the three terms x, y and fx (and no constants) is undecidable as can be seen by Skolemization of the formulas of the unde­ cidable (w.r.t. validity) prefix class 3V3.
• If F has only one clause with more than one literal and there are no w-connections within this clause then only one copy of this clause is needed. This is not the case if there is a weak connection within the clause as can be seen from

• If a valid matrix F has two clauses with two literals in each clause then it has the form

As an example we give the matrix For its connection proof, shown on the right, we need two copies of each clause. The dotted line indicates factorization and the horizontal line in the fourth clause indicates splitting of this clause. This example illustrates the importance of factorization and splitting. Without these features we would have to consider four copies of the first clause and three of the second.

Since all these properties apply to very spe­ cial cases of formulas only, and thus will not be applicable directly to the input formula in prac­ tice, their relevance lies in a dynamic application in the course of the proof process. Namely the re will arise subproblems which may well be long to one of these simple cases.