copyright notice & caveat
accesses since May 9, 1996

A TAXONOMY OF AUTOMATED THEOREM PROVING ENVIRONMENTS

GORDON BEAVERS
University of the Ozarks
HAL BERGHEL
University of Arkansas
Abstract

In this paper we (a) draw attention to the role that normal forms play in various Automated Theorem Proving (ATP) procedures and (b) introduce analogous ATP procedures with complementary normal forms. Since this role is most easily examined in propositional logic, our discussion will be so limited. However, the dual propositional ATP procedures generalize to first order logic in a manner analogous to the way propositional resolution and propositional tableau procedures do. We consider each of resolution, semantic tableaux and Wang's algorithm as a consequence relation following the example of Gentzen's sequent calculus. These familiar procedures are the paradigm ATP's depending on specific normal form implementations and as such are suggestive of further procedures.

INTRODUCTION

First a definition for well-formedness of our object language is provided. The vocabulary for propositional logic consists of the following:

i. a countable infinitude of propositional variables: p,q,r,...

with or without subscripts.

ii. the set of truth-functional operators: {-,&,v,-›,‹-›}

iii. parentheses: (,).

We define well-formed formulas, hereafter wff, inductively as follows.

w:0 all propositional variables are wffs

w:1 if A is a wff, then so is (-A)

w:2 if A and B are wffs, then so is (A º B)

w:3 nothing else is a wff

Where ' º ' is an element of {&,v,-›,‹-›}, and A,B,..., with or without subscripts, define a countable infinitude of meta-logical variables which denote arBitrary wffs. By convention, we will refer to wffs which contain no Binary connectives as atomic.

Central to this discussion is the notion of a consequence relation. A consequence relation is a set of ordered pairs of sets of wffs of

the language of propositional logic. The ordered pairs are regarded as statements of the meta-language written in the form,

t |- d, where t and d are sets of wffs, possibly empty, and having the interpretation d is a consequence of t. A consequence relation for propositional logic has the following properties:

reflexivity A |- A for any formula A,

weakening t

	            d        	   t |- d        
 		----------        ----------         
		t,{A} |- d        t |- d,{A}    

transitivity (cut)

    t1 |- d1,A     A,t2|- d2
    -----------------------
         t1,t2  |- d1,d2

where the dashed line indicates that the consequence relation below follows from the consequence relation(s) above.

As a notational convenience, we use expressions of the form "t,d" in place of "t U d", and "t,A" in place of "t U {A}".

Perhaps the most fundamental interpretation of t |- d is given by the model-theoretic semantics of the object language defined as follows. An interpretation, I, is a mapping of a propositional variable onto one of the truth values, true/false. Symbolically, we write I(p)=T for 'the interpretation of p is true', for arBitrary propositional variable, p. Similarly, an n-ary truth function is a mapping from an n-tuple of truth values onto a truth value. The truth functions of immediate interest will be those which correspond to our truth-functional operators. Specifically, let u,v is an element of {T,F}. The five truth functions are:

f-(u) = F if u=T, and T otherwise

f&(u,v) = T if u=v=T, and F otherwise

fv(u,v) = F if u=v=F, and T otherwise

f-›(u,v) = F if u=T and v=F, and T otherwise

f‹-›(u,v) = T if u=v, and F otherwise

If we use these definitions together with the inductive definition of well-formedness, we can see that interpretations of variables ultimately induce a truth-value, called an evaluation, onto a wff.

These evaluations, e, are defined inductively as follows: i. e(p) =df I(p), for all propositional variables p

ii. e(-A) =df f-(e(A))

iii. e(A º B) =df fº(e(A),e(B))

We augment these definitions with the coincidence theorem for propositional logic which ensures that evaluations of formulas are completely determined by the interpretations of contained propositional variables. We note that the operators -,&,v,-›,‹-›, discussed above correspond roughly to the ordinary language analogs 'not', 'and', 'or', 'if...then...', and '...if and only if...', respectively.

NORMAL FORMS

It is well-known that the set of truth functional operators

{-,&,v,-›,‹-›}, commonly referred to as the Principia Mathematica [8] connectives, form a truth-functionally complete set. That is, any truth-functional evaluation which can be expressed at all can be expressed by means of some wff which contains only Principia Mathematica connectives.

However, with the uncontroversial definitional equivalences

(A‹-›B) =df (A-›B) & (B-›A) , and

(A-›B) =df (-AvB)

it becomes clear that this set is also truth-functionally redundant, for -› and ‹-› are eliminable without loss of truth-functional expressiveness. The truth-functional independence of {-,&,v} is interesting primarily because it makes it possible to express wffs in normal form.

There are two basic normal form representations of wffs in propositional logic. A conjunctive normal form (CNF) is a conjunction of the form A1 & A2 & ... & An where each Ai, 1<=i<=n, is an elementary disjunction of the form B1 v B2 v ,...,v Bm, m>=1, where each Bj, 1<=j<=m, is atomic. Conversely, a disjunctive normal form (DNF) is a disjunction of elementary conjuncts. It is well-known that for any arBitrary wff, A, there exist formulas in both CNF and DNF which are truth-functionally equivalent to it. That is, e(A) = e(CNF(A)) = e(DNF(A)), for all wffs, A. DeMorgan's laws together with the associative, commutative and distributive laws for & and v, familiarity of which is assumed, are adequate to illustrate this point.

For simplicity of exposition, we also introduce a third normal form, negation normal form (NNF), which is defined inductively as follows:

(i) A conjunction or disjunction of atomic formulas is in NNF

(ii) if A and B are in NNF then so is A ± B

where ± is an element of {&,v}. It is easy to see that every wff has an NNF equivalent. We return to the notion of normal forms in the next section.

MODEL-THEORETIC SEMANTICS

The inductive definitions for wff and wff-evaluation described above provide the foundation of a model-theoretic semantics for propositional logic. Consider an interpretation, I, of propositional variables and a corresponding evaluation, e, induced by I onto some formula A. If e(A) = t under I, I is said to be a model of A. It follows that for an arBitrary interpretation, I,

i. I is a model of p if and only if I(p) = t

ii. I is a model of (-A) if and only if I is not a model of A

iii. I is a model of (A º B) if and only if

(I is a model of A) ? (I is a model of B)

where ? is the metalanguage equivalent of º. If there exists at least one interpretation which is a model of a formula, the formula is said to be satisfiable. Following convention, we say that if all (no) interpretations are models of a formula, the formula is tautologous (contradictory).

We can generalize the notion of model to a set of formulas, t, without difficulty. We will say that any interpretation is a model of a set of formulas just in case it is a model of each of the formulas individually. If there exists at least one interpretation which is a model of t, t is said to be satisfiable.

We further extend the analysis to the level of argument form. Let t be a set of formulas and A be an individual formula. If for all interpretations, I, which are models of t are also models of A, a valid consequence relation is said to hold between t and A. By convention we refer to the formulas of t as premises and to A as the conclusion of an argument form designated by t|-A.

As mentioned above, any wff can be transformed into an equivalent formula in either CNF or DNF. It is appropriate that we here introduce two observations concerning model-theoretic properties of normalized expressions:

(1) Any formula in CNF is tautologous iff each elementary disjunction contains both a propositional variable and its negation.

and, conversely,

(2) Any formula in DNF is contradictory iff each elementary conjunction contains both a propositional variable and its negation.

BINARY RESOLUTION

Binary resolution, in one of its myriad forms, is at the heart of most modern inference engines and logic programming translators (e.g., Prolog, Parlog,etc.). In its simplest form, Binary resolution relies upon a single rule of inference - a generalization of the law of disjunctive syllogism (from formulas of the form A v B and -A we may conclude B), the general form of which is:

             A v B1 v ... v Bk, -A v C1 v ... v Cl 
          ------------------------------------------ 
                B1 v ... v Bk v C1 v ... v Cl

for atomic formulas A,Bi,Cj, 1<=i<=k and 1<=j<=l.

As is evident from the syntax, generalized disjunctive syllogism only applies to wffs in CNF. Aside from its transparent validity, disjunctive syllogism also has the advantage of excluding contradictory atomic formulas from consideration.

There is a subset of CNF which is important from the point of view of the automation of Binary resolution. This is the class of Horn clauses, or CNF expressions in which the disjunctions contain at most one unnegated formula. In terms of CNF, we may view Horn clauses as conjunctions of disjunctions of the form Ai v -B1 v ... v -Bj, for non-negative i,j. We refer to the case when i=1 and j=0 as an assertion or fact. When i=1 and j>=1, we have a conditional expression or rule. Goals are created when i=0 and j>=1. Finally, we define the empty clause, ƒ, as the special case when i=j=0. Since there can be no more than one unnegated disjunct, the set of Horn clauses is a proper subset of CNF expressions.

We complement the notion of Horn clause with the notions of clause and dual clause. By clause, we refer to the disjunction of atomic formulas (as in the elementary disjuncts of CNF expressions, above). A dual clause, on the other hand is a conjunction of atomic formulas.

While this limitation renders Binary resolution for Horn clauses essentially incomplete for propositional logic, it offers considerable computational advantage. From a procedural point of view, a single unnegated disjunct may always be used as the 'entry point' into a clause set while all negated disjuncts may be consistently interpreted as procedure calls. This simple procedural interpretation allows a straightforward implementation of resolution. It is important to recognize that resolution is defined for CNF expressions generally, and not just for Horn clauses. However, the automation of resolution is exceedingly difficult for non-Horn clause expressions.

An illustration of Binary resolution appears below. Consider the following Horn clause:

(A v B) & (-A v C) & (-B v C) & -C

We then proceed by means of Binary resolution as follows:

(A v B) , (-A v C) , (-B v C) , -C , -B (A v B) , (-A v C) , (-B v C) , -C , -B , -A

(A v B) , (-A v C) , (-B v C) , -C , -B , -A , A



By convention, we refer to each successive line as the resolvent of the earlier line. Since the reduction was complete, i.e. produced the null clause, , the Horn clause is not satisfiable. This is to say that there is no interpretation under which the evaluation of the formula becomes True. This technique may be easily extended to determine whether a consequence relation exists between premises P1,...,Pk and conclusion, C, by testing the equivalent expression A = P1 & ... & Pk & -C for satisfiability where A is in CNF. Since for any consistent set of premises, P, and putative conclusion, C, P |- C if and only if it is not the case that P |- -C, resolution is amenable to indirect proof strategies.

Automated resolution was first suggested by RoBinson [4] and later incorporated into the kernel of the high-level programming language Prolog by Colmerauer and Kowalski. For further discussion, see [3].

THE SEMANTIC TABLEAU

The Semantic Tableau, or Truth Tree, is another approach to inferencing which is convenient and, efficiency notwithstanding, relatively easy to automate [1]. As with Binary resolution, the tableau is ideally suited for indirect proof strategies whereby the premises of an argument form together with the negation of the conclusion are tested for joint satisfiability. The tableau rules of passage are tree-like in form (hence the nickname truth tree) as is shown in the following rule schemata for CNF expressions:

(1) (A & B)                   (3)        -(A & B)                
     -----                                   | 
       |                                  |------|  
       A                                 -A     -B                
       B 
                                             
(2) -(A v B)                      (4)     (A v B)                     
      -----                                  |
        |                                 |-----|
       -A                                 A     B
       -B                                

(5) --A
    ---
     |
     A

A tableau or truth tree is constructed according to the following flow chart:

(1) List the premises and negation of conclusion

(2.a.) Erase all occurrences of double negation

(2.b.) clause all paths which contain a formula and its negation

<if all paths are claused, stop (argument form is valid); else proceed>

(3.a.) Apply reduction rule (from above) to all unchecked formulas

<if all formulas are checked, stop (argument form is invalid)>;

else proceed to (2.a.)

To illustrate, consider the following tableau (node labels added for clarity):

	1) (A & (-B v C))  [check]  *premise*
	2) (B & (-A v -C))  [check]  *premise*
	3) -(-A v -B)  [check] *negated conclusion*                      
	4) A
	5) -B v C  [check]
	6) B
	7) -A v -C  [check]
	8) --A  [check]
	9) A
	10) --B  [check]             
	11) B
          |
   |------+-------|
12) -B          3) C
                  |
         |--------+--------|
      14) -A            15) -C

As the algorithm makes clear, the lack of open paths after rules have been applied to all remaining formulas indicates that the argument form is valid.

HILBERT OR FREGE SYSTEMS

Another standard consequence relation is defined by the axiomatic or Hilbert style presentation of propositional logic. In this case t |- d just in case for finite subsets t1 and d1 of t and d, respectively, &(t1) -› v(d1) is derivable from the axioms:

  1. A -› (B -› A)
  2. (A -› (B -› C)) -› ((A -› B) -› (A -› C))
  3. (-B -› -A) -› (A -› B)

using the rules modus ponens and substitution. The notation &(t1) and v(d1) stand for the conjunction of the elements of t1 and the disjunction of elements of d1.

The deduction and compactness theorems for propositional logic yield that t |- d just in case |- &(t1) -› v(d1). The standard soundness and completeness results for classical logic show that axiomatic consequence and model-theoretic consequence are identical. We observe that normal forms play no role in Hilbert systems.

We now proceed to an abbreviated Gentzen style presentation of propositional logic, that is, yet another way of presenting the notion of consequence relation in propositional logic.

GENTZEN SYSTEMS

The Gentzen system for classical propositional logic has the structural rules reflexivity, weakening and transitivity given above and logical rules of inference for the connectives. Since we are considering only formulas in NNF we present inference rules for only -, & and v, those rules being.

(v:L)   A,t1 |- t2       B,t1 |- t2   
==========================
AvB,t1 |- t2
(&:R)   t1 |- t2,A       t1 |-t2,B 
=========================

t1 |- t2,A&B (&:L) A,t1 |- t2 B,t1 |- t2 ------------- ---------- A&B,t1 |- t2 A&B,t1 |- t2 (v:R) t1 |- t2,A t1 |- t2,B ----------- ----------- t1 |- t2,AvB t1 |- t2,AvB (-:L) t1 |- A,t2 ========== -A,t1 |- t2 (-:R) A,t1 |- t2 =========== t1 |- -A -› t2

The double lines indicate Bi-directional implication.

WANG'S ALGORITHM

Hao Wang implemented the following algorithm for propositional logic on an IBM 704. He reported his results in Wang [7]. The algorithm essentially delivers a cut-free proof using the & and v rules of Gentzen's sequent calculus. We modify Wang's original rules to get:

  1. Translate the formula into negation normal form. & on the left and v on the right are replaced by commas,
  2. Eliminate negations using the rules for negation in the Gentzen sequent calculus given above.
  3. eliminate & on the right using the splitting rule:
	     t1 |- t2,A&B
	-----------------------
	t1 |- t2,A    t1 |- t2,B       

4. eliminate v on the left using the splitting rule:

	     AvB,S1 |- t2
	-----------------------
	A,S1 |- t2    B,S1 |- t2    

5. t1 |- t2 is a theorem if some formula occurs on both sides of the turnstile. The initial sequent is a theorem iff all the splits are.

These rules allow sequents containing complex formulas to be decomposed into sequents containing simpler formulas. The final result is a finite tree of sequents with the sequents at the leaf nodes containing only atomic formulas. The sequents at the leaf nodes can be tested for theoremhood by rule 5. If all the leaf node sequents are theorems then the sequent at the root is a theorem.

Wang's procedure can be viewed as essentially producing DNF on the left and CNF on the right so that rather than producing a tree and using the decision procedure just given, one might instead use the following procedure:

  1. translate into negation normal form. & on the left and v on the right are replaced by commas,
  2. eliminate embedded & on the right and v on the left using distribution laws to get DNF on left and CNF on the right,
  3. &(Si)|-v(Sj) is a theorem iff each dual clause on the left is either a contradiction or has a atomic formula in common with each clause on the right.

RESOLUTION & TABLEAU REVISITED

We offer here an alternative description of Binary resolution in the light of our discussion of Gentzen systems. The behavior of Binary resolution may be described by the following algorithm:

i. Given a set of premises t and a conclusion A, then t |- A just in case t, -A |- ƒ, (i.e., t & -A is contradictory), use the Gentzen rule for negation given above.

ii. Put t, -A in CNF using DeMorgan's law and distributivity.

iii. Use inference rule: from ... (pvt1)(-pvt2)... infer ...(t1vt2)(pvt1)(-pvt2)...

iv. t|-A iff ƒ |- is derivable.

We note that the completeness of the resolution rule depends on using CNF on the left and having the null clause as the consequent.

Conversely, the tableau's behavior may be viewed in this way:

i. given a set of premises t and a conclusion A, then t |- A just in case t, -A |- ƒ, (i.e., t & -A is contradictory). Use the Gentzen rule for negation given above.

ii. put t, -A in DNF using DeMorgan's law and distributivity.

iii. t|-A iff each dual clause contains a contradiction.

Note that the construction of tableau amounts to putting t, -A in DNF and that once in DNF on the left of |- determination of theoremhood is immediate, i.e., just check each dual clause for a contradiction, if there is a single dual clause that does not contain an atomic formula and its negation (equivalently, a path that does not clause) then you do not have a theorem and a valuation witnessing this fact can be read off the dual clause. Note also the contrast with resolution: resolution starts with CNF and uses the inference rule to get the empty clause (that is, a clause containing a contradiction) whereas tableau finish with DNF after which there is nothing to do but read the answer (at least in the propositional case).

DUALS OF RESOLUTION AND TABLEAU

Each of the Binary resolution and semantic tableau procedures has a dual procedure. Since both resolution and tableau are refutational (i.e., indirect) procedures their duals will be non-refutational (i.e., direct) procedures. That is, while the resolution procedure determines the existence of a valid consequence relation, t |- ƒ, when t is in CNF, the dual of the resolution procedure determines a valid consequence relation, ƒ |- t, when t is in DNF. Similarly, whereas a valid consequence relation is found to exist by the tableau procedure for t |- ƒ, when t is in DNF, the dual of the resolution procedure determines a valid consequence relation, ƒ |- t, when t is in CNF.

Dualizing the arguments justifying resolution and tableau yields the non-refutational procedures dual resolution (DNF on the right) and dual tableau (CNF on the right). The appropriate conversion routines can be shown to be:

dual resolution:

i. put in DNF on right

ii. inference rule: from ... (p&S1)(-p&S2)...

infer ...(S1&S2)(p&S1)(-p&S2)...

iii. condition for determination of theorem:

null dual clause.

dual tableau

i. use inference rules to get CNF on right

ii. theorem just in case each clause contains

pv-p, for some p.

OBSERVATIONS

The characterization of resolution and tableau-based inferencing and their dual procedures given above is in terms of the normal form representation which underlies the inferencing and the proof strategy. The distinction between CNF and DNF and Direct vs. Indirect proof yields the following pairwise comparison:

indirect(LH)direct(RH)
CNFResolutionDual Tableau
DNFTableauDual Resolution

Wang is a mixed system (right and left sides).

The most commonly used ATP procedures, resolution and tableau, are indirect in style (left-sided). We have shown that there are corresponding direct procedures (right-sided). Wang's algorithm, in contrast, is two-sided since it incorporates operations for both the left and right hand sides. Analyzing these procedures in terms of the normal forms used illustrates the similarities and emphasizes the differences. Each of these procedures are amenable to automation.

ILLUSTRATION OF THE INFERENCING TECHNIQUES

Consider the following valid argument form

(A) p-›(q-›r), p-›q |- p-›r

We now give a proof of this argument in each of the afore-mentioned systems.

resolution

First, we observe that the negation normal form (Horn clause equivalent) of (A) is:

-pv-qvr, -pvq |- -p, r

which by Gentzen's negation rule:

-pv-qvr, -pvq, p, -r |-

which is the CNF/indirect proof representation of the argument form consistent with the above classification.

We then proceed by means of Binary resolution:

tableau

Once again, the indirect proof equivalent to (A) in negation normal form is:

-pv-qvr, -pvq, p, -r |-

which converts to the following DNF equivalent

(p&-r&-p&-q) v (p&-r&-p&r) v (p&-r&q&r) |-

since an atomic formula and it's negation appear in each disjunct (path) the DNF expression is necessarily false (all paths clause).

Wang

Wang's algorithm yields DNF on the left and CNF on the right. Once again, the negation normal form of (A) is:

-pv-qvr, -pvq |- -p,r

Which is further transformed by Wang's algorithm into the into the following six DNF sub-arguments

p |- p,r

p,q |- p,r

p |- p,r,q

p,q |- r,q

r,p |- p,r

p,r,q |- r

since in each sub-argument some atom appears on each side of the turnstile the original argument is a theorem.

In our notation, we create the Gentzen equivalent of a Wang derivation in this way. First, using distributivity

-pv-qvr, -pvq |- -p,r

is seen to be equivalent to:

-p v (-p&q) v (-q&-p) (r&-p) v (r&q) v F |- -pvr

Which is valid since each non-F (false) dual clause on the left shares an atomic formula with every clause on the right.

dual of tableau

The direct form of (A) is

|- (p-›(q-›r))-›((p-›q)-›(p-›r))

|- (p&q&-r), (p&-q), -p, r

|- ((-pvp)&(-pvq)&(-pv-r)), (p&-q), r

|- ((rv-pvp)&(rv-pvq)&(rv-pv-r)), (p&-q)

|- (rv-pvp)&(rv-pvqvp)&(pvrv-pv-r)&(-qvrv-pvp)&

(-qvrv-pvq)&(-qvrv-pv-r)

which is in CNF and is thus a theorem since each dual clause contains some atom and its negation.

dual of resolution

The direct form of (A) in DNF is:

-pv-qvr, -pvq |- -p, r

which by Gentzen negation is equivalent to:

|- p&q&-r, p&-q, -p, r

which is the DNF/direct proof representation of the argument form consistent with the above classification.

Using the dual resolution rule:

|- p & q & -r, p & -q, r, -p

|- p & q & -r, q & -r, p & -q, r, -p

|- p & q & -r, q, q & -r, p & -q, r, -p

|- p & q & -r, q, p, q & -r, p & -q, r, -p

|- p & q & -r, q, (), p, q & -r, p & -q, r, -p

CONCLUSION

The process of first transforming propositional logic argument forms into negation normal form and then considering how the standard ATP procedures treat these forms suggests several procedural extensions. This paper has presented the two most obvious extensions: dual resolution and dual tableau. These procedures (a) mirror resolution and tableau and (b) show that ATP need not be restricted to indirect proof strategies as is the current custom.

Consideration of the NNF of an argument can help guide automated inferencing. If it could be easily determined that the the conversion of an argument form into the schema, CNF |- ƒ, is less complex than say, ƒ |- DNF, then the dual resolution procedure would seem more appropriate. Our present work is motivated by the relationships between the simplicity of the normal form on the one hand and the most 'natural' inferencing technique on the other. The present study focuses our attention on this complex relationship and gives rise to the question of whether an algorithm may be developed which assigns to each problem an 'optimal' inferencing strategy. This question is currently being investigated by the authors.

While it cannot be determined at this point whether efficient automated theorem provers can be developed which will be 'intelligent' enough to select their own optimal strategies, we are confident that the present taxonomy provides a useful framework by means of which the logical alternatives may be compared and contrasted.

REFERENCES:

For a general discussion of the logical aspects of the topics covered above, consult references [5] or [6].

[1] Fitting, Melvin: First-Order Logic and Automated Theorem Proving, Springer-Verlag, New York (1990).

[2] Kleene, Stephen: Introduction to Metamathematics, Van Nostrand, New York (1952).

[3] Kowalski, Robert: Logic for Problem Solving, North-Holland, New York (1979).

[4] RoBinson, John: "A Machine-Oriented Logic Based on the Resolution Principle", Journal of the ACM, Vol. 12, pp. 23-41 (1965).

[5] Suppes, Patrick: Introduction to Logic, Van Nostrand, New York (1957).

[6] Mendelson, Elliott: Introduction to Mathematical Logic, Van Nostrand, New York (1964).

[7] Wang, Hao: "Proving Theorems by Pattern Recognition", Communications of the ACM, Vol. 3, No. 3, pp. 220-234.

[8] Whitehead, Alfred and Bertrand Russell: Principia Mathematica, Cambridge University Press, Cambridge (1910).