Proof Transformation with Built-in Equality Predicate

1 Introduction

With the increasing strength .of Automated Deduction Sys­ tems the length and complexity of computer generated proofs has reached a degree where they have become almost impos­ sible to understand even for the expert This has led to a state where only specialists are capable to understand and check a proof found by an automated deduction system.

But whenever human beings are addressed, the need for easily understandable and clearly structured arguments is apparent. Therefore it is necessary to be able to present proofs in a better structured way. Ideally one would like the proof to be given in natural language, with a large variety of inference rules. As a preliminary step in this direction it is useful to transform the computer generated proofinto natural deduction which, although still a system of formal logic, has been devised to approximate as much as possible an intuitive form of reasoning.

The transformation of proofs into a natural deduction for­ mulation has Solved some of the problems, see [Andrews, 1980; Miller, 1983; Lingenfelder, 1986], but by and large the increasing length and complexity of the transformed proofs adds to their incomprehensibility rather than to reduce

· Supported by the Deutsche Forschungsgemeinschaft, SFB 314

Axel Pracklein*

Fachbereich Informatik U niversitiit Kaiserslautem Postfach 3049

D-6750 Kaiserslautem

phone: 49 631 205 3344

email: prckln@informatik. uni-kl.de

it. It is therefore paramount to be able to state the proofs in a hierarchically structUred way, as mathematicians do, formu­ lating subgoals and lemmata. There has been some success in structuring computer generated proofs, cf. [Lingenfelder, 1989; Pfenning and Nesmith, 1990; Huang, 1991], but all of these approaches are restricted to logics without equality.

We feel, however, that this is a severe restriction, as equal­ ity is essential for any natural coding of mathematical prob­ lems and of AI problems in general. Therefore, we generalize Lingenfelder's approach, so that proofs involving equational reasoning can also be structured automatically.

In section 2 the different calculi and proof representations are introduced. Section 3 extends the basic system of proof transformation so that equality reasoning is also covered. This fits well into the transformation approach, if equational reasoning is not dominating. Here equality is seen as a spe­ cific theory (in the sense of theory resolution [Stickel, 1985]) so that a further generalization to arbitrary theories can be envisaged.

The task of finding the underlying proof structure is pre­ sented in section 4. This can be accomplished by the elegant expedient of exploiting topological properties of the refuta­ tion graphs in order to come up with a well-organized proof. Structure can be imposed upon the proofs by introducing lemmata, both to avoid duplication of parts of the proof and to arrange a larger proof in a sequence of subgoals easier to understand. Another means of structuring a proof is its divi­ sion into several disjoint parts by employing the method of case analysis. This constitutes very often the only possi­ bility to use a conditional equation without having to fall back on a proof by contradiction.

2 Proof Formats

In this section we will describe the logical calculi used in this paper. Everything is standard first order predicate logic with equality, and we need resolution (with paramodulation) and a natural deduction system based on Gerhard Gentzen's calculus NK [Gentzen, 1935]. There are no differences from the usual way of defining these concepts as done for instance in [Gallier, 1986] or [Loveland, 1978].

Additionally, as our actual starting point of the proof transformation will not be a resolution proof, but rather the result of a graph-based theorem prover, we must introduce the representation of proofs as graphs .

2.1 Clause and Refutation Graphs with Equality

Definition: A clause graph consists of a set of literal nodes, that are partitioned into clause nodes. Each literal node is labeled with a literal; the distinction between the lit­ eral nodes and the literals themselves is needed because the same literal may be attached to several literal nodes. Finally the links of the clause graph connect disjoint sets of literal nodes, such that for all links the following conditions hold:

• (1t1) The literal nodes in a link are labeled with literals with unifiable atoms.
• (~ A link must connect at least one positive and one negative literal.

Definition: A clause graph is said to represent a clause setS if every clause node C has the form [-A(s) s~t A(t)] or there is a parent clause c'e s and a ground substitution 'Y such that the restriction of the literal labeling to C is a bijec­ tion between its literal nodes and the literals of ;C'. Clause nodes of the form [-A(s) s~t A(t)] are called equality clause nodes.

Definition: A deduction graph is a non-empty, ground, and acyclic clause graph. A cycle is a sequence of clause nodes and links CI.lll,C2, ... Cn.lln.CI. such that all the lli are different and they contain literal nodes with opposite sign in their respective neighbour clause nodes. A refutation graph is a deduction graph where all literal nodes belong to a link.

Definition: For a formula F and a clause graph r repre­ senting C(F), a relation !1 between the literal nodes of rand the atom occurrences in F is a clause graph relation if it is compatible with the relation established by the normaliza­ tion process, by which the clause form is constructed from the formula. It is obvious from this definition that the literal nodes of equality clause nodes are never related to atom oc­ currences of F.

2.2 Natural Deduction Proofs with Equality

In 1933, Gerhard Gentzen developed a formal system for mathematical proofs with the intention to describe as closely as possible the actual logical inferences used in mathematical proofs. To quote from [Gentzen, 1935]: "der moglichst ge­ nau das richtige logische Schlieflen bei mathematischen Beweisen wiedergibt ".

The actual form of the proof lines is taken from Andrews [Andrews, 1980], but they differ only in their syntax from Gentzen's rule system NK in [Gentzen, 1935].

Definition: A natural deduction proof line consists of a finite set of formulae, called the assumptions, a single formula, called conclusion, and a justification, written ()ill- F Rule 9t}. A finite sequence S of proof lines is a natural deduction derivation of a formula F from assump­ tions )if, ifF is the conclusion of the last line of S, jl is the set of assumptions of this last line, and every line in S is correctly justified by one of the rules of the calculus.

A proof line A= ()ill- F Rule 9t} within a sequence of proof lines is correctly justified iff )ill- F matches the lower part of Rule 9t and there are proof lines before A in the sequence matching the upper part of Rule 9t.

A finite sequence S of proof lines is a natural deduction proof of a formula F if it is a natural deduction derivation of F from an empty set of assumptions.

Now we list some rules of the natural deduction calculus, the letters F, G, and H represent formulae and )if represents a fmite set of formulae.

3 Proof Transformation

The construction of natural deduction proofs (NDPs), by humans and computers alike, is conducted in single steps. To prove any valid formula F one always starts with a line ( 1- F } . Such a line is obviously no proof, because it is not correctly justified. Now the proof is constructed by deriving subgoals until it is completed. In the intermediate states one may find completed subproofs, but also others that are not yet done. To formalize the procedure of the search for such a natural deduction proof, we use Generalized Natural Deduc­ tion Proofs as defined in [Lingenfelder, 1990].

3.1 General Procedure

Definition: A finite sequence S of proof lines is called a Generalized Natural Deduction Proof (GNDP) of a formula F, ifF is the conclusion of the last line of S, the last line of S has no assumptions, and every line is eitherjustified by a rule of the calculus, or it is justified by a proof (possibly in a different calculus) of its conclusion from its assumptions.

This allows lines not correctly justified within the calculus, but it is assumed that these lines are "sound", in the sense that (/\assumptions => conclusion) is a valid for­ mula. Such lines are called external lines, lines justified within the calculus are called internal. When no external lines are present in a GNDP, it is a normal NDP.

Definition: Given a refutation graph r justifying an ex­ ternal line of a GNDP with assumptions Fi and conclusion G, and a clause graph relation 6, relating all the literal nodes of r to atom occurrences in F1A F2A ... "'Fn =>G. Then a clause node is negatively polarized if any of its literal nodes is related to an atom occurrence in the theorem formula G. Otherwise the clause node represents an axiom and is said to be positively polarized. In particular equality clause nodes are positively polarized.

3.2 Transformation Rules

The transformation rules are to be read as follows: the lines before the arrow (~) are replaced by those following it in the next generalized NDP of the sequence. Some of the rules add a new internal line which is simply written below its parent lines. In the description, jl is a list of assumption formulae, capital letters indicate single formulae, a,~. y, ... are used as labels for the lines, the justification Rule 9t stands for an arbitrary rule of the natural deduction calculus, and the justifications 1t, 1t', 1t 1, and 1t2 represent proofs of the respective lines. For all these rules one must make sure that the proofs 1t', 1t 1, or 1t2 can be constructed from 1t. If the proof is given in form of a refutation graph this can be accomplished automatically.

The rules can be divided into three classes. Internal rules introduce new internal lines without any relation to current external lines, this corresponds to forward reasoning. Exter­ nal rules try to reduce a current external line, this realizes backward reasoning. Mixed rules depend on both, external and internal lines, reducing an external line in the light of previously derived formulae.

As we are mainly concerned with the effect of equality reasoning in a proof, we will now state the rules handling the application of an equation.

This is not the complete set of transition rules; all the other rules necessary to describe a complete system for proof transformation can be found in [Lingenfelder, 1990].

3.3 Proof Transformation System with Equality

The complete set of transformation rules constitutes a proof system for natural deduction proofs. This means that for any valid formula F, there is a fmite sequence of GNDPs starting with ( 1- F) and ending with an NDP for F. Every element in this sequence can be constructed from its pr~decessor by application of one of the transition rules.

The transformation rules are selected according to appropri­ ate heuristics, making use of the information in a given proof, for instance a previously computed refutation graph. In [Lingenfelder, 1990] it is shown how a proof represented as a refutation graph without equality can guide the "search" for a natural deduction proof. In this context, search means to transform the given, graph-represented proof into the natu­ ral deduction calculus, rather than to fmd an original proof.

After an application of rule E-= replacing t by s in a goal formula F a refutation graph for F(s) can be constructed by removing the equality clause node [-L(s) s#t L(t)] and the equation clause node [s = t] unless used elsewhere. Then in all the literal nodes adjacent to L(t) t is substituted by s. Now the link at -L(s) is combined with that at L(t), thus closing the gap resulting from the removal of the equality clause node. The resulting graph proves the formula F(s).

Similarly, when E-=.l is applied, the polarization of the clause node [S:;t:S] is changed from positive to negative. Note that the refutation graph has no negatively polarized part when a proof by contradiction is represented. The structure of the graph remains unchanged.

Example: In this example we show a refutation graph for F(t), which equals Pt"' (AvB), and the resulting graph prov­ ing F(s): Ps A (AvB). The negatively polarized clause nodes are drawn with double boxes.

3. 4 Application of Transition Rules

As an example of the proof transformation procedure, we use a part of the subgroup criterion. The formula F to prove is

The refutation graph, the clause graph relation, and the ground substitution have been automatically generated by the theorem prover MKRP, see [Ohlbach and Siekmann, 1989; Lehr, 1988]. Below the refutation graph is shown; theory clause nodes are indicated by dashed lines.

The transformation process is started with the "trivial" GNDPforF

After some transformation steps not involving equality, the following GNDP is constructed:

At this point the external line 13 cannot further be pro­ cessed by external rules. A consultation of the refutation graph tells us that the literal node corresponding to Sia is only connected to a theory clause node. Therefore Sia must be derived using the rule of equality. As a preliminary opera­ tion we must isolate the equation fiae = ia, using internal rules, then E-= can be applied. Now the GNDP takes on the form shown below:

order case, with one more application of an equality rule to produce the final natural deduction proof.

4 Structuring the Proof

4.1 General Procedure

An initial "trivial" generalized natural deduction proof (GNDP) is constructed to start a transformation process as described in section 3. Now some of the transformation rules, EA for instance, lead to additional external lines, and as a consequence to a division of the refutation graph accord­ ing to the splitting theorem [Lingenfelder, 1990]. In the simplest case the refutation graph proving FA. G is "cut" through the clause [-F -G], such that the two resulting components are refutation graphs for F and G, respectively. In general, however, the two components may have a non­ empty intersection, and this is similarly the case for the other rules leading to a division of the refutation graph. The splitting theorem does not take this into account, so that these shared subgraphs are always duplicated and therefore processed more than once.

This does not matter if the intersection is comparatively small, when it may easily be copied and later used several times in the resulting subproofs. If it is relatively large and complex, however, it may be sensible to prove a lemma first and then use it in all the proof parts. In order to formalize such a procedure, the transformation rule E-Lemma is intro­ doced.

This rule must of course be used with discretion, i.e. only when specifically called for by a heuristic. In [Lingenfelder, 1990] it is explained in detail how topological properties of the graph induce lemmata. If paramodulation steps are repre­ sented using equality clause nodes in the refutation graph the search algorithm in [Lingenfelder, 1990] can be used un­ changed.

Another way to structure proofs is the division into the cases of a disjunction. This is formalized by the rule M-Cases. The most important case for its application in pure first order logic comes up, when an existentially quanti­ fied formula cannot be proven constructively. With built-in equality there is one additional reason for a case analysis. As the natural deduction calculus only allows the application of unit equations, special considerations are needed for condi­ tional equations. One solution of this problem could be the division of the proof into cases such that the equation is assumed to hold in one of them.

4.2 Equality Clause Nodes

Paramodulation steps of the computer generated proof are represented in the refutation graph using special "equality" clause nodes. For example the combination of a paramodula­ tion step Pa to Pb via a=b and a resolution step between Pb and some literal-Pb is simulated as a sequence of three reso­ lution steps of the unit clauses [Pa], [a=b], and [-Pb] with the equality clause node [-Pa a~ Pb]. This clause node de­ notes the trivial fact that Pa" a=b => Pb. The symmetry of the equality predicate is incorporated into the unification al­ gorithm and hence this additional property must not be con­ sidered in the graph. In the natural deduction calculus this fact is reflected by the existence of two symmetric rules for the application of an equation. Alternatively one might have chosen a rule axiomatizing the symmetry explicitly, viz.

But this does not comply with intuitive mathematical rea­ soning, where equations are rarely oriented and therefore such a symmetry rule never needs to be used explicitly.

Conditional equations, that is, equational literals in non unit clauses, need no special handling, because the only dif­ ference is that the negated equation in the equality clause ncxle is connected to a non unit clause node and therefore to a deduction graph. However, the formulation of the proof can be more difficult because the equation is not always true. One can either prove the equality as a lemma or divide the proof into cases, in one of which the equality holds.

The decision between these possibilities depends on gen­ eral considerations, as for example the complexity of result­ ing lemmata or the position of negatively polarized clause nodes in the graph. Yet there is one heuristic depending on equality. Case analysis is most profitable if the condition for an equation is itself an equation used for paramcxlulation. Then both obstructing conditions are removed in parallel.

Usually mathematicians employ case analysis only when the disjunction is an axiom or has been previously derived. Equality clause nodes, however, represent implications and therefore are unattractive for this purpose. But if -Pa or a*b is first derived from the contrapositive of Pa "a=b => Pb, a case analysis may be the best choice.

Often several equations ar~ successively applied to a for­ mula leading to chains of equality clause ncxles. If any of the chain links are separating, and therefore candidates for lem­ mata, only the links joining the chain to the rest of the graph should be selected. Otherwise the equality argument would be tom asunder.

A more syntactical criterion is the distinction between completion and rewriting steps, which can be made if the underlying paramodulation rule discriminates these steps according to the Knuth-Bendix algorithm. Completion steps are more important and substantial while rewriting steps can usually be considered a calculation rather than a proof.

The structuring procedure can be generalized to theory reso­ lution with arbitrary theories. A resolution step between two literals that are complementary in the given theory is repre­ sented with a clause node containing the residue and a syntac­ tically complementary literal for each resolution literal.

It is clear that this method can only handle proofs with a relatively small number of paramodulation steps. Otherwise a large number of equality clause nodes would obscure the structure of the proof. This is especially the case when paramodulation steps are performed into other equations. Therefore purely or even substantially equational proofs need special considerations due to their inherent internal structure.

4.3 Example

As an example we chose one of Pelletier's problems [Pelletier, 1986], which is among the simpler standard examples in equality theorem proving:

There are x andy such that any z equals x or .Y· If two distinct constants a and b have a property P then the property P holds universally. In first order notation with equality this is represented by the following formula:

The resolution and. paramodulation proof is first translated into a refutation graph. The clause nodes I 1 and 12 in the up­ per graph are both instances of the deduction graph below; a complete refutation graph can be obtained by inserting two copies of the deduction graph for 11 and 12. x and y, as well as w become Skolem constants in clause form, and therefore also in the refutation graph. They are named 1, 2, and 3 in the sequel.

The first operations performed in the transformation pro­ cess are automatic applications of rules introducing the Skolem constants in the theorem. The other Skolem con­ stants are introduced by need, whenever they appear in a sub­ graph that is currently worked with. Of course it may be necessary to isolate the existentially quantified formula frrst.

Now we know all the prerequisites for the structuring of this proof. At frrst we consider the subgraph which is used in two different copies in the refutation graph. Here the dis­ junction of free literal nodes (x = 1 v x = 3) cannot immedi­ ately be used as a lemma because the deduction graph con­ tains a negatively polarized clause node (T6). One heuristic to obtain a lemma in this case would be to use a maximal positively polarized subgraph of this deduction graph instead. This corresponds to a lemma P3 v 'lr/x (x = 1 v x = 3). Note that the variable situation allows the introduction of a uni­ versally quantified lemma.

Alternatively, we can split the proof into cases as the situ­ ation meets the conditions explained above. The instance 1=3 v 2=3 of axiom A5 is used, so that only a very small overlap remains in one of the resulting cases. Actually this overlap corresponds only to a trivial rewrite step.

It remains to be checked whether the two cases of the proof should be further structured. The links AI and A2 are found to be separating in case 1, indicating a proof by analyzing the cases a=2 and a *2 or, alternatively, b =2 and b *2. The symmetry of the graph suggests, however, a division of the proof into cases a* 2 and b * 2. This reflects the reasoning "a* b, therefore it is impossible that both a and b are equal to 2. If a *2 ... ".The second case has exactly the same struc­ ture and can therefore be done using the same case analysis. Then the following global structure of the proof has become visible:

A proof in natural language might therefore read: let 1 and 2 be constants such that any z equals 1 or 2. In order to prove P as a universal property it suffices to show that it holds for an arbitrary constant 3. 3 must be either 1 or 2. We consider first the case 3 = 1. As a* b it is impossible that both equal2. If a *2 it must be 1, which equals 3, and there­ fore P3 holds because Pa holds. If on the other hand b * 2 then b must be 1, which equals 3, and therefore P3 holds be­ cause Pb holds. The second case (3 =2) can be handled anal­ ogously. Therefore P3 holds in all cases, and as 3 was cho­ sen arbitrarily P holds universally.

5 Conclusion

In this paper a method is described to transform a proof gen­ erated by a resolution-based theorem prover with a built-in paramodulation rule into a natural deduction proof in Gentzen's system NK. Starting from the basic proof trans­ formation and structuring mechanism published in [Lingenfelder, 1990], the necessary changes and additions are made to meet the special needs of equality reasoning.

Paramodulation steps are represented in the refutation graph by equality clause nodes and additional links for each application of an equation. The extension of this mechanism to arbitrary theory resolution appears to be straightforward. The most remarkable result is the fact that this basis allows to employ the structuring algorithm essentially unchanged. The only extensions were to handle conditional equations by case analysis or as a lemma and some specialized heuristics for the consideration of equational steps.

An open question with respect to the structuring of proofs is the presentation of proofs based only or mainly on the equality predicate. The representation of pure unconditional equality proofs in equality graphs, as in [Blllsius, 1986], seems to be a promising starting point to construct a procedure analogous to the algorithm described here.