GORDON BEAVERS*University of the Ozarks | HAL BERGHEL**University of Arkansas |

The purpose of this paper is three-fold. First, we draw attention to the role that normal forms play in various Automated Theorem Proving (ATP) procedures. Second, we expand upon these procedures by introducing complementary normal forms and inferencing techniques which correspond to them. Third, we introduced a generalized form of resolution which offers an alternative to nonclausal inferencing. Finally, we outline a 'dynamic' ATP environment which selects from among competing inferencing mechanisms based upon 'best fit' with the problem domain. Since this role is most easily examined in propositional logic, our discussion will be so limited. However, the procedures discussed below generalize to first order logic in a manner analogous to the way propositional resolution and propositional tableau procedures do. |

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)

t_{1}|- d_{1},A A,t2 |- d2 --------------------------------- t_{1},t2 |- d_{1},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

f_{v}(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.

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

{-,&,v,-›,‹-›}, commonly referred to as the Principia Mathematica [12] 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 B_{1} v B_{2} v ,...,v B_{m} , 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.

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, 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 B_{1}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 -B_{1} v ... v -B_{j} , 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, f, 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 P_{1},...,P_{k} and conclusion, C, by testing the equivalent
expression A = P_{1} & ... & P_{k} & -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 [8] and later incorporated into the kernel of the high-level programming language Prolog by Colmerauer and Kowalski. For further discussion, see [5]. THE SEMANTIC TABLEAU

The Semantic Tableau, or Truth Tree, is another approach to inferencing which is convenient and, efficiency notwithstanding, relatively easy to automate [2]. 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.) Close all paths which contain a formula and its negation

<if all paths are closed, 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.

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 t_{1} and d_{1} of t and d, respectively, &(t_{1}) -›
v(d_{1}) is derivable from the axioms:

- A -› (B -› A)
- (A -› (B -› C)) -› ((A -› B) -› (A -› C))
- (-B -› -A) -› (A -› B)

using the rules modus ponens and substitution. The notation &(t_{1}) and
v(d_{1}) stand for the conjunction of the elements of t_{1} and the disjunction of
elements of d_{1}.

The deduction and compactness theorems for propositional logic yield that t |-
d just in case |- &(t_{1}) -› v(d_{1}). 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.

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,t_{1}|- t_{2}B,t_{1}|- t_{2}========================== AvB,t_{1}|- t_{2}(&:R) t_{1}|- t_{2},A t_{1}|-t_{2},B =========================t

_{1}|- t_{2},A&B (&:L) A,t_{1}|- t_{2}B,t_{1}|- t_{2}------------- ---------- A&B,t_{1}|- t_{2}A&B,t_{1}|- t_{2}(v:R) t_{1}|- t_{2},A t_{1}|- t_{2},B ----------- ----------- t_{1}|- t_{2},AvB t_{1}|- t_{2},AvB (-:L) t_{1}|- A,t_{2}========== -A,t_{1}|- t_{2}(-:R) A,t_{1}|- t_{2}=========== t_{1}|- -A -› t_{2}

The double lines indicate B_{i}-directional implication.

Hao Wang implemented the following algorithm for propositional logic on an IBM 704. He reported his results in Wang [11]. 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:

t_{1}|- t_{2},A&B ----------------------- t_{1}|- t_{2},A t_{1}|- t_{2},B

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

AvB,S1 |- t_{2}----------------------- A,S1 |- t_{2}B,S1 |- t_{2}

5. t_{1} |- 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:

- translate into negation normal form. & on the left and v on the right are replaced by commas,
- eliminate embedded & on the right and v on the left using distribution laws to get DNF on left and CNF on the right,
- &(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.

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 |- f, (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 ... (pvt_{1})(-pvt2)... infer
...(t_{1}vt2)(pvt_{1})(-pvt2)...

iv. t|-A iff f |- 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 |- f, (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 close) 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).

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|-f, when t is in CNF, the dual of the resolution procedure determines a valid consequence relation, f|-t, when t is in DNF. Similarly, whereas a valid consequence relation is found to exist by the tableau procedure for t|-f, when t is in DNF, the dual of the resolution procedure determines a valid consequence relation, f|-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.

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) | |

CNF | Resolution | Dual Tableau |

DNF | Tableau | Dual 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.

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 is:

-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:

- pv-qvr, -pvq, p, -r |-
- pv-qvr, -qvr, -pvq, -r, p |-
- pv-qvr, -q, -qvr, -pvq, -r, p |-
- pv-qvr, -q, -p, -qvr, -pvq, -r, p |-
- pv-qvr, -q, (), -p, -qvr, -pvq, -r, p |-

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 close).

**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

Binary resolution may be viewed as a procedure for introducing a new clause (from the two 'source' clauses) which is a result of eliminating the occurrences of a propositional variable and its negation while leaving a disjunction of everything else. We provide, below, a high-level description of a procedure which eliminates all occurrences of a propositional variable, irrespective of whether it is negated. This method is more efficient than resolution in many applications. We give here such a method which can be easily justified based upon the truth-value semantics of propositional logic. It can also be viewed as a surrogate for the non-clausal resolution methods introduced by Manna and Waldinger [6] and Murray [7].

We offer the following rules for generalization of resolution and dual-resolution:

(R) T(p) |-

==========================

T(f/p) |- and T(t/p) |-

(D-R) |- D(p)

=========================

|- D(f/p) and |- D(t/p)

Where the general case is:

(R) T(p) |- D(p)

==========================

T(f/p) |- D(f/p) and T(t/p) |- D(t/p)

where T(p) and D(p) focus attention on the variable p which need not actually appear in either T or D (although the rule would be of no use unless p appeared in at least one). T(t/p) signifies that each occurrence of p in T has been replaced by t (the 'true'). Likewise, T(f/p) indicates that each occurrence of p, if any, has been replaced by f (the 'false'). Justification of the rule intuitively follows from the observation that if T |- D then, for every interpretation of the variables in T and D, T -› D, must take on the value t. (For a proof of the completeness of nonclausal resolution for predicate logic, see [7].

We observe that, unlike the procedures presented above, generalized resolution does not require conversion to normal form and thus those resources can be conserved. The indiscriminate use of the rule, however, can lead to the consideration of every possible interpretation of variables. Thus, in broad terms, resolution (or its dual) will be more efficient when the clauses contain few elements and when each clause used in the derivation closely resembles the clause with which it will be resolved, i.e., when almost all of the elements of both clauses are identical. We will say that such derivations are 'directed'.

Generalized resolution, on the other hand, could prove more efficient in cases where no 'direction' presents itself. The use of generalized resolution then breaks the problem into two simpler problems for which a 'direction' may or may not be found.

Comparing the tableau (and its dual) to generalized resolution also gives some indication of the respective advantages. Tableau's split on 'or's in NNF, whereas generalized resolution splits the problem for distinct variables. Therefore, when T and D are long, and perhaps complex as well, but contain few variables, generalized resolution is expected to be more efficient. Conversely, when T and D contain many variables for the relative length and complexity of the formulas, the tableau procedure might be expected to be more efficient.

Resolution is an indirect procedure for theorem proving. That is, it begins with the assumption of premises and the negation of the putative conclusion. The top-level strategy is that if there is some interpretation of variables which is a model of both the premises, jointly, and the negation of the conclusion, then no valid consequence relation exists between the premises and the actual conclusion. After converting the collection of formulas into CNF, resolution then alters the clauses by 'resolving', if possible, an atomic formula of one clause with its negation in another clause. Resolution eliminates an occurrence of a literal and its negation. The procedure terminates affirmatively when the null clause results from the repeated application of the resolution rule to the clauses.

Resolution is improved by the generalized resolution procedure in that rather than eliminating the occurrence of an atomic formula and its negation, all occurrences of the literal are eliminated in a single operation. The generalization could be presented as an indirect procedure to preserve the analogy with resolution or as a direct procedure to draw attention to similarities with the dual resolution procedure. However, we present it as a two-sided procedure for clarity.

We again refer the reader to the valid argument

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

which, in NNF is:

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

Using generalized resolution to eliminate occurrences of p, we get

-q v r, q |- r .

Eliminating q, we get:

r |- r .

However, this example does not show the superiority of generalized resolution preferable to resolution; the 'pigeonhole' problem will serve that purpose. Haken [3] proves that "...for infinitely many disjunctive normal form propositional calculus tautologies e, the length of the shortest resolution proof of e cannot be bounded by any polynomial of the length of e." Haken further explains that the tautologies which he used were introduced by Cook and Reckhow [1] and encode the pigeonhole principle.

We give here the case that 3 pigeons will not fit into 2 holes unless some hole has 2 pigeons.

/\ \/ Hi,j |- \/ \/ \/ (Hi,k & Hj,k)

i=1,3 j=1,2 k=1,2 i=1,2 j=i+1,3

That is,

(H1,1 v H1,2) & (H2,1 v H2,2) & (H3,1 v H3,2) |-

(H1,1 & H2,1) v (H1,1 & H3,1) v (H2,1 & H3,1)

v (H1,2 & H2,2) v (H1,2 & H3,2) v (H2,2 & H3,2)

Since each variable occurs three times, we arbitrarily choose to eliminate the three occurrences of H1,1 with generalized resolution, yielding:

(H2,1 v H2,2) & (H3,1 v H3,2) |-

H2,1 v H3,1 v (H2,1 & H3,1) v (H1,2 & H2,2)

v (H1,2 & H3,2) v (H2,2 & H3,2) with 't' for H1,1,

and

H1,2 & (H2,1 v H2,2) & (H3,1 v H3,2) |-

(H2,1 & H3,1) v (H1,2 & H2,2) v (H1,2 & H3,2) v (H2,2 & H3,2)

with 'f' for H1,1.

Since the elimination of the singleton H1,2 will cut down on the growth of the number of consequences, we eliminate it next:

(H2,1 v H2,2) & (H3,1 v H3,2) |-

H2,1 v H3,1 v (H2,1 & H3,1) v H2,2 v H3,2 v (H2,2 & H3,2) ,

and

(H2,1 v H2,2) & (H3,1 v H3,2) |-

H2,1 v H3,1 v (H2,1 & H3,1) v (H2,2 & H3,2) ,

and

(H2,1 v H2,2) & (H3,1 v H3,2) |-

(H2,1 & H3,1) v H2,2 v H3,2 v (H2,2 & H3,2)

and 't' since the left side is false.

Eliminating all occurrences of the singleton H2,1 in the above three consequence relations yields:

true

H2,2 & (H3,1 v H3,2) |- H3,1 v H2,2 v H3,2 v (H2,2 & H3,2)

true

H2,2 & (H3,1 v H3,2) |- H3,1 v (H2,2 & H3,2)

(H3,1 v H3,2) |- H3,1 v H2,2 v H3,2 v (H2,2 & H3,2)

H2,2 & (H3,1 v H3,2) |- H2,2 v H3,2 v (H2,2 & H3,2)

Eliminating all occurrences of H2,2 yields:

true

true

H3,1 v H3,2 |- H3,1 v H3,2

true

true

(H3,1 v H3,2) |- H3,1 v H3,2

true

true

Eliminating all occurrences of H3,1 yields:

true

H3,2 |- H3,2

true

H3,2 |- H3,2

which completes the proof.

Anyone who has attempted to produce the corresponding resolution proof will immediately recognize that generalized resolution is much simpler because the user does not have to determine the sequence of resolutions which will eventually lead to the null clause. But at the same time, the reader will have noted the potential for exponential growth in the number of consequences which must be checked. In the worst case, generalized resolution could yield as many steps as there are interpretations over the variables (i.e., 2n for n variables).

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 conversion of an argument form into the schema, CNF |- f, is less complex than say, f |- DNF, then the dual resolution procedure would seem more appropriate. Our present work is in part 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.

In addition, we offer a 'generalization' of resolution which accommodates
conventional binary resolution as well as the NNf_{-}based resolution extensions.
In may be useful to tie all of these inferencing mechanisms together in the
following algorithm:

for any argument form t |- d,

Is t |- d easily converted into |- CNF or DNF |- ?

If yes, use tableau or dual-tableau;

else determine: Is resolution straightforward?

If yes, use resolution or its dual;

else, use generalized resolution.

Of course this algorithm is fragmentary and conceals the robust heuristics used in making these determinations which are currently being investigated by the authors. However, it does reveal the essential strategies involved.

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, together with the proposed generalization of resolution, provide a useful framework for such an investigation.

REFERENCES:

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

[1] Cook, S.A. and R. A. Reckhow: "The Relative Efficiency of
Propositional Proof Systems", *Journal of Symbolic Logic*, Vol. 44,
pp. 36-50 (1979).

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

[3] Haken, Armin: "The Intractability of Resolution", *Theoretical
Computer Science*, Vol. 39, pp. 297-308 (1985).

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

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

[6] Manna, Zohar and Richard Waldinger: "A Deductive Approach to
Program Systhesis", *ACM Transactions on Programming Languages and
Systems*, Vol. 2, pp. 90-121 (1980).

[7] Murray, Neil: "Completely Nonclausal Theorem Proving", *Artificial
Intelligence*, Vol. 18, No. 1, pp. 67-85 (1982).

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

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

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

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

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