TERMINATOR

Introduction

There are presently two main groups of theorem proving calculi: In those of the first kind the theorem prover starts with a given set of logical formulas and creates new formulas by the application of certain deduction rules as for example resolu­ tion, paramodulation, natural deduction ruJ.es etc , until the theor em or a refutation has been de rived. Recently new calculi like Andrews' mating calculus [1] or Bibel's matrix calculus [ 2 ] have been develo­ ped which initially do not deduce any new formulas, but only test certain path conditions ensuring sa­ tisfiability or unsatisfiability of the initial formula set.

Kowalski's connection graph proof procedure [ 8 ] in its original formulation is of the first kind: A connection graph consists of the nodes labeled by clauses in conjunctive normalform and links (connec­ tions) between complementary unifiable literals representing possibl e resolution steps . A deduction is performed by the selection of a link, creating the corresponding resolvent, inserting it into the graph and deleting the selected link, potentially causing further deletions of links and c lauses. This proof procedure can be transformed into a cal­ culus of the second kind: If the clause set is unit refutable, i.e. the empty clause can be derived by successive resolution steps with one-literal clau­ ses, the clause graph has to contain a special sub­ tree (refutation tree or terminator situation) which just r epr esents this chain of unit resolutions.

Examples:

Each box in fig. 1 r epresents a literal , a string of boxes is a clause, and complementary unifiable boxes (literals) are connected by a link. If all unifiers attached t o the links in fig. 1 a) are compa­ tible , thi s represents a one- l evel t erminator situa­ tion , since it immediately allows for the derivation of the empty clause . Similary fig. 1 b) represents a two-level terminator situation (a kernel which is connected to a one-level t e rminator situation) and fig. 1 c) a 3-level terminator situation if all uni­ fiers are compatible.

In general a connection graph is a refutation tree if:

• Every literal of a clause is attached to exactly one link.
• The unifiers of the links are compatible.
• The graph is cyc l e free.

A unit refutable clause set S is unsatisfiable , iff there exists a refutation tree for the factored set S [ 6 ]!

Of course the knowledge of the existence of such a refutation tree is of little practical use unless a fast method for extracting it from a given graph is known. An exhaustive and unsophisticated search for such a terminator configuration is prohibitively expensive in large graphs, hence the task of the presented TERMINATOR algorithm is an efficient ex­ traction of a refutation tree (if it exists) from a given clause graph .

The Algorithm

The first attempt to implement an n- l evel termi­ nator algorithm used a recursive technique: A non­ unitclause C was selected and examined for a one­ level situation. If this first test failed, the algorithm was called recursively for other non­ unitclauses connected to C, trying to find a chain of unit resolutions which resolves away all literals except for that one connected to C, and the one­ l evel t est for C was performed once again taking advantage of this new information. Unfortunately the algorithm was rather inefficient because no results of former TERMINATOR calls had been stored , and therefore the same part of the clause graph had to be examined again and again. Hence only the n = 1 case was within practical limits.

Whereas the old algorithm worked from inside the refutation tree to the leaf nodes (unitclauses) , our new algorithm works just in the opposite direc­ tion and stores all information it has generated for later use. We shall present the working of the algorithm using a few examples,and a full descrip­ tion is given in [lo].

The input clauses are divided into the set of unitclauses (UNITS) and the set of non-unitclauses (NON-UNITS) . NON-UNITS are sorted according to inc­ reasing literal number . For each element c of NON­ UNITS, of which every literal except at most one is connected to at least one element of UNITS a compa­ tibility test is performed. An example will illustra­ te this test:

Suppose C has four literals: C = <Ll L2 L3 L4>. Each literal Li may be connected to a set of unit­ clauses complementary to Li and let Ui be the set of unifiers associated with these connections .

fig. 2

We start with the first literal and compute the set of "merged" unifiers:

u 12 =u 1 * u 2 ={oio=o 1 * o 2 , o 1 Eu 1 , o 2 Eu 2 } where o 1 * o 2 is a most general merge substitution (resp. unifier, see below) of o 1 and o 2 . Similarly we calculate u 123 = u 12 ·* u 3 and u 1234 = u 123 * u 4 . If u 1234 * ¢, then every element of u 1234 allows us to resolve away the whole clause, i.e. a proof is found. If u 1234 =¢but u 123 * ¢ we apply every substitution of u 123 to literal L4 thus generating new unitclauses and insert them into the UNITS-list.

With this step we deduce in fact new formulas, but we only use them as a compact representation of the merged unifiers with three additional advanta­ ges:

1. A very simple and fast subsumption test [lo] between the unitclauses allows us to detect whe­ ther the result of a unit resolution chain is an instance of the result of another chain.
2. 2 . The treatment of the input unitclauses is just the same as the treatment of the deduced ones which simplifies the data- and control structu­ res.
3. Heuristic valuation of the unitclauses allows for further pruning the search space.
4. If u 1234 * ¢, we create new uni tclauses in the

same way applying u 12 * u 4 to L3, u 1 * u 34 to L2 and u 234 toLl. The links of the initial graph now provide the information to be able to attach all the new unitclauses to complementary literals in other clauses , (or respectively other literals in the same clause , if it is selfresolving) .

The clauses in NON-UNITS are examined several times, constantly producing new unitclauses, either until the proof is found or until a certain boundary value is exceeded. If a terminator situation is found, the datastructures we use to represent the units and the links allow for an immediate extrac­ tion of the refutation tree which is then used to generate an ordinary resolution proof.

The TERMINATOR is called from the MKR-Procedure at the beginning of the search for a proof and, if it does not find an immediate proof it is called again each time a certain number of steps has been performed by other components of the system, hence the overall behaviour amounts to a tightly control­ led and sophisticated bidirectional search . In par­ ticular the other link selection mechanisms in the system prefer those resolution and paramodulation steps which are expected to transform a non-unit refutable clause graph into a unit refutable one. A second application of the TERMINATOR is the gene­ ration of unitclauses, for instance the rewrite component of the system can decide that a specific unit equation might be useful as a rewrite rule and charges the TERMINATOR to deduce, if possible , the desired equation from a conditional equation .

The Compatibility Test

The bottleneck of the terminator algorithm is the compatibility test: We have a set A with n sub­ stitutions and a set B with m substitutions. Now the task is to unify each substitution in A with each substitution in B, i.e. to compute the most general merge substitution for each such pair.

A unifier for two substitutions o and T is a sub­

o * A := A oo = A oT is called the merge substitution

stitution A such that ADO = AOT of o and T.

There are fast unification algorithms known for the unification of terms, the most recent are even linear [7] . The unification of substitutions was first investigated in [11]. But for lAl =nand lBI = m you still have to perform n*m such operations and in many applications this number may be greater than loS, for this reason the known methods are out of the question. Hence we have developed a very fast merging algorithm for large sets of substitu­ tions which exploits special conditions present in the terminator problem. The goal is to find a repre­ sentation for the substitutions which allows the direct access from each substitution o in set A to those in set B which are compatible with o.

The working of the algorithm will be illustrated with the following examples; a full description is given in [lo].

Example 1

Since only links between unitclauses and non-unit­ clauses are being considered, we know that the single literal of the unitclause is not present in the resolvent after resolution upon such a link. Therefore only the substitution components for va­ riables of the non-unitclause are relevant for the resolvent . Hence it is admissible to discard all other substitution components. Because of this it is possible to represent the remaining components in a table using a fixed ordering of the variables occuring in the non-unitclause . This representation will be cal l ed a T-representation.

For example 1 we obtain:

In this case it is easy to see that the unifica­ tion of the corresponding terms in the table is sufficient to get a most general instance of the substitutions.

In this example it is:

The main problem, howeve r is the merging of two non-singleton sets A and B of substitutions. Let us suppose we have two lists A and B with three ele­ me nts in each list:

Example 2: T-representation:

The representation is then changed a second time: Equal terms occurring in different substitutions but in the same column of the T-representation are stored only once. The substitutions themselves are represented by pointers to their terms . These terms also have pointers back to the substitutions in which they occur ; and from the terms of group A links to every unifiabl e term in the same pos i t i on of group B are generated. In addition the unifiers for these single terms are attached to the links . We call this representation the P-repre sentation .

P-representation of example 2 :

The complexity of the merging algorithm is a func­ tion of the task of gene rating the links between unifiable terms, which can be further improved by grouping the terms into lists of variables, con­ stants, ground terms (without variables) and compo­ sed t e rms. Then we can exploit the fact that some single-term-unifiers are trivial (variables with constants etc . ) whereas others are impossible (con­ stants with ground terms) .

On the basis of the P-represe ntation it is now easy to extract for a substitution a in group A all compatible ones in group B:

For every term of o and e very link attacheq to thi s term you attach the single-term-unifie r correspon­ ding t o this link at every substitution of group B in which the term pointed to by the link occurs:

For example 2 we obtain:

All those substitutions in B with exactly p compa­ tible single-term-unifiers are compatible with a, where p is the length of the T-representation (= number of variables in the non-unit clause) . (In example 2:p=3 . ) For example 2 we obtain three compatible pairs of substitutions:

Although the generation of the single-term links i s not linear in general, the algorithm shows a l inear (-n) behaviour in most practical examples, i . e. in­ stead of n*m operations onl y n operations are gene­ rally performed .

Summary

With the terminator algorithm three main goals have been achieved:

1. In reality nothing has to be done twice, because all relevant intermediate results (merged substi­ tutions) can be stored without requiring too much space.
2. 2 . The compatibility test is enormously reduced in complexity, allowing the fast unification of millions of pairs of substitutions.
3. Arbitrary rules for pruning the search space by deleting unitclauses can easily be incorporated into the algorithm.

These are the main advantages compared to similar methods for the extraction of refutation trees re­ spectively graphs, likes. Sickel's graph unrolling [12] or Chang and Slagle's usage of rewrite rules [ 4]. Although their calculi are complete for non­ unit refutable clause sets as well, their practical usefulness is questionable, unless their efficiency problems are solved.

The implementation of the terminator algorithm has considerably increased the performance of the MKR-Procedure. For instance we have solved SAM's Lemma , a famous problem in automatic theorem pro­ ving , which was first proved by an interactive theorem prover [5], and later by the automatic theorem prover at Argonne National Lab. It had to deduce 22000 clauses before finding a proof [ 3]. The TERMINATOR generated only 190 unitclauses be­ fore the proof was found [ 9 ].