Efficient Algorithms to Detect and Restore Minimality, an Extension of the Regular Restriction of Resolution.
A given binary resolution proof, represented as a binary tree, is said to be i>minimal if the resolutions cannot be reordered to generate an irregular proof. Minimality extends Tseitin"s regularity restriction and still retains completeness. A linear-time algorithm is introduced to decide whether a given proof is minimal. This algorithm can be used by a deduction system that avoids redundancy by retaining only minimal proofs and thus lessens its reliance on subsumption, a more general but more expensive technique.Any irregular binary resolution tree is made strictly smaller by an operation called i>Surgery, which runs in time linear in the size of the tree. After surgery the result proved by the new tree is nonstrictly more general than the original result and has fewer violations of the regular restriction. Furthermore, any nonminimal tree can be made irregular in linear time by an operation called i>Splay. Thus a combination of splaying and surgery efficiently reduces a nonminimal tree to a minimal one.Finally, a close correspondence between clause trees, recently introduced by the authors, and binary resolution trees is established. In that sense this work provides the first linear-time algorithms that detect minimality and perform surgery on clause trees.
Introduction
The regular restriction of binary resolution [14] states that a resolution
step resolving on a given literal should not be used to deduce a clause
containing that literal. In other words, that resolution step should not
be an ancestor of such a clause in the binary derivation tree. We extend
this restriction so that it applies also when a reordering of the resolutions
brings such a clause below that step. We use rotations of edges
in the binary tree to reorder the resolution steps, and require that the
rotations neither weaken what is proved nor increase the size of the
tree. If a binary resolution proof cannot be made irregular by such
rotations, we call it minimal.
This extension of regularity depends on sequences of rotations, and
thus appears to be expensive to compute. However we characterize it
with a condition that can be checked efficiently by examining the static
tree. The condition is stated in terms of history paths in the binary
resolution tree. Each history path tells the story of a given literal. The
tail of the history path is a leaf of the tree and it tells where the
literal was introduced in an input clause. The history path is said to
close at the node where its literal is resolved away. When one history
path closes at a node that occurs in another history path, and the two
paths are disjoint, we say the first history path directly precedes the
other. The precedes relation on history paths is the reflexive transitive
closure of directly precedes. History paths and the precedes relation are
basic in our understanding of how binary resolution trees behave when
rotations are performed. We provide simple conditions on history paths
that characterize when one node can be rotated below another (we say
it is visible from the other) and when one node cannot be rotated from
below another (we then say it supports the other.) By examining the
history paths in a static tree, we can decide much about what can and
cannot be accomplished by sequences of rotations.
In particular, we can say whether rotations can convert a regular tree
to an irregular one. A theorem prover can use this ability to screen the
proofs it builds, and retain only the minimal ones. Since every clause
with a non-minimal proof is subsumed by some clause with a minimal
proof, this theorem prover uses minimality to lessen its reliance on sub-
sumption. The runtime of full subsumption grows with the number of
retained clauses, which may become very large, while detecting minimality
depends linearly on the size of each proof tree, which is typically
much smaller.
Instead of using minimality simply as a filter, a theorem prover can
convert a non-minimal proof to a minimal one, using operations defined
in this paper. Consider the branch of an irregular derivation tree that
makes it irregular. This branch contains the node where some given
literal is resolved and, further down, contains a clause in which that
literal occurs. Why resolve the literal away, only to have it reappear
later? We can remove this resolution but otherwise reconstruct the
branch as closely as possible to the original, with this literal appearing
additionally in some of the clauses. The constructed tree is smaller
and the result it proves is at least as general as the original one. We
call this operation surgery, and define a second operation, splay, which
rearranges a non-minimal tree so that it is irregular. Both operations
run in time linear in the size of the tree. A combination of both operations
will eventually reduce any non-minimal tree to some minimal
one.
The first section below presents the regular restriction on binary
resolution trees. In that section we introduce the surgery operation for
irregular binary resolution trees. Then minimal binary resolution trees
are introduced. This section also discusses our rotations and the set of
rotation equivalent trees, which is all of the trees that can be generated
from a given tree by a sequence of these rotations. In the following sec-
tion, we discuss the "precedes" relation of history paths, and use that to
define the "holds" relation on nodes. We then relate holds and visibility
by showing that if the nearest common descendant of two given nodes
holds one of them, then that one is not seen by the other, i.e. it cannot
be rotated below the other. Based on this condition, we give an efficient
algorithm for deciding visibility. We show how a theorem prover can
be restricted to retain only minimal proofs and disregard non-minimal
ones, decreasing the number of proofs that must be considered. Then
we show the splay operation for efficiently converting a non-minimal
proof into an irregular one, so that surgery can further convert it to a
minimal one. Thus another theorem prover can efficiently convert its
non-minimal results to minimal ones if desired. In the next section we
use history paths to characterize support: the condition where one node
in a binary resolution tree must be a descendant of another after any
sequence of rotations.
Both minimality and surgery were first developed for clause trees [5].
The clause tree is a tool for developing ideas in automated reasoning,
and the binary resolution tree is an efficient, compact data structure
to implement clause trees. In the second last section we show the close
relation between binary resolution trees and clause trees. Thus, this
paper provides the first efficient algorithm for surgery in clause trees.
We close with some remarks on the relation between clause trees and
binary resolution trees, and related work.
This paper is an extension of [13].
2. Binary Resolution Trees
We use standard definitions [2] for atom, literal, substitution, unifier
and most general unifier. In the following a clause is an unordered disjunction
of literals. We do not use set notation because we do not want
multiple occurrences of a literal to collapse to a single literal automat-
ically. Thus our clauses can be viewed as multisets. An atom a occurs
in a clause C if either a or :a is one of the disjuncts of the clause.
The clause C subsumes the clause D if there exists a substitution '
such that C' ' D (as sets, not as multisets). A variable renaming
substitution is one in which every replacement of a variable maps to
another variable, and no two variables map to the same variable. Two
clauses C and D are equal up to variable renaming if there exists a
variable renaming substitution ' such that Two clauses are
standardized apart if no variable occurs in both. Given two parent clauses
which are standardized
apart (a variable renaming substitution may be required) their resolvent
is the clause (C 1 - C 2 )' where ' is the most general unifier of
g. The atom resolved upon is a 1 ', and the set of
resolved literals is g.
It is convenient to define a mapping ae of literals for the resolution
operation. This is used later to define history paths.
(Resolution mapping). For each resolution operation we
define the resolution mapping ae from each occurrence of a literal c in
each parent clause to either the atom resolved upon if c is a resolved
literal, or otherwise to the occurrence of c' in the resolvent.
The reader may be missing the usual factoring operation on a clause,
which consists of applying a substitution that unifies two of its literals
with the same sign and then removing one of these literals. This
operation is not needed in binary resolution trees, however, since if a
clause contains two identical or unifiable literals, both can be resolved
upon whenever the clause is used in a resolution. By allowing several
literals to be resolved on, instead of merging them before the resolu-
tion, we have just one type of internal node in our binary resolution
tree, instead of two. (De Nivelle uses resolution nodes and factorization
nodes [3].) Moreover, an implementation is free to merge or factor
literals if desired. Factoring may be seen as an optimization if the factored
clause can be used in several resolution steps, since the factoring
is done only once.
A binary resolution derivation is commonly represented by a binary
tree, drawn with its root at the bottom. Each edge joins a parent node,
drawn above the edge, to a child node, drawn below it. The ancestors
(descendants) of a node are defined by the reflexive, transitive closure of
the parent (child) relation. The proper ancestors (proper descendants)
of a node are those ancestors (descendants) not equal to the node itself.
If T and H are nodes in a tree then path(T ; H) is the unique path from
T to H . Here, T is called the tail and H the head.
Definition 2. A binary resolution tree on a set S of input clauses is
a labeled binary tree. Each node N in the tree is labeled by a clause
label, denoted cl(N ). Each node either has two parents and then its
clause label is the result of a resolution operation on the clause labels
of the parents, or has no parents and is labeled by an instance of an
input clause from S. In the case of a resolution, the atom resolved upon
is used as another label of the node: the atom label, denoted al(N ).
Any substitution generated by resolution is applied to all labels of the
tree. The clause label of the root of the binary resolution tree is called
the result of the tree, result(T ). A binary resolution tree is closed if its
result is the empty clause, 2.
a-d
a:b-d-e
d:b-c-e
e:b-c-f-g
c:a- b-b-f-g
a: b-b-f-g
b:f-g
-a-b-e
c-d
e-f-g
a-b-c
h:-a
-b
-g
-a-h
-h

Figure

1. An irregular binary resolution tree.
For the binary resolution tree in Figure 1,
:gg. The labels of a node N are
displayed beside the name of the node and separated by a colon, e.g.
the node N 4 has atom label c, and clause label a - b - b - f - g. The
order between the parents of a node is not defined.
If instead of labelling the internal nodes by atoms, one labels each
edge with the complement of the literal resolved upon, a binary resolution
tree would become a semantic tree, and the leaves of the binary
resolution tree would become failure nodes of the semantic tree.
Using the resolution mapping ae for each resolution operation in the
tree, we can trace what happens to a literal from its occurrence in the
clause label of some leaf, down through the tree until it is resolved
away. Clearly if all literals are eventually mapped to the atom label
of some internal node, the clause label of the root is empty. In this
case by soundness of resolution, the clause labels of the leaves is an
b:
a-d
d:a-c
c:a-a-b
a:b
c-d
a-b-c
-b
-a-h
-h

Figure

2. Surgery: Operation 5 on Figure 1.
unsatisfiable set. Thus we are primarily concerned about tracing the
"history" of a literal starting from its appearance in a leaf.
Definition 3 (History Path). Let the nodes (N occur in a
binary resolution tree T such that N 0 is a leaf whose clause label contains
a literal a, and for each is a parent of N i . Let
ae i be the resolution mapping from the parents of N i to N i , and let
occur in cl(N i ). Suppose N n either is the root of T , or has
a child N such that ae a is mapped by the resolution at N to the
atom resolved upon at N . Then (N is a history path for a.
The history path is said to close at N if N exists, and then N is written
as close(P ). The node N n is the head, the leaf N 0 is the tail and a is
the literal of P , written head(P ); tail(P ) and literal(P ), respectively.
For example in Figure 1, (M for c which
closes at N 4 . The two history paths for b in Figure 1, corresponding to
the two occurrences of b, are (M 3
Both of these close at N 6 . The only which does not close is the one for
f , which is
Definition 4 (Regular). A binary resolution tree T is regular if there
does not exist a node N of T and a descendant M of N , such that
al(N) occurs in cl(M ).
The tree in Figure 1 is irregular because al(N 1 ) is a and a occurs
in cl(N 4 ). Irregular trees are never necessary. Why resolve away the a
twice? One could choose to leave out the resolution at N 1 , leaving the
a in the clause, do the other resolutions as necessary (not all will be
necessary) and later resolve a away, as was done at N 5 . Operation 5
makes this idea more formal.
A new binary resolution tree T 0 is constructed from T in which M 0
and all of its ancestors, and possibly other M i are removed. However
all leaves of T 0 are also leaves of T . Thus every history path in T 0
has a corresponding history path in T . The converse cannot be true,
since the history paths of T through M 0 do not exist in T 0 . A new
sequence (N 0
n ) is defined in which either N 0
M i is removed) or N 0
i corresponds to N i in T .
Operation 5 (Surgery on irregular trees). Let T be an irregular binary
resolution tree with being the path of
nodes from N 1 to the root N n , and with being the first
node in this path whose clause label contains a. Let N i\Gamma1 and M i\Gamma1 be
the parents of N i for be the parents of
so that a occurs in the clause label of N 0 with the same sign as in
cl(N
Procedure
all ancestors of N 0 be in T 0 . (M 0 and all of its
ancestors are removed.) Let N k be the node at which some history
path P a for a in N j closes, if k exists.
For do
If there is a history path in T 0 containing N 0
for which the corresponding
history path in T closes at N i then
Put M i\Gamma1 and all its ancestors into T 0 .
i as a new node in T 0 which is the child of N 0
Let the resolution at N 0
i be defined so that the history paths of
i that close at N 0
i correspond to history paths of T that close at
Let the history path corresponding to P a also close at N 0
k .
(That is, the same literals as far as possible are resolved at N 0
i as
at N i with one possible addition.)
else
There is no history path containing N 0
which corresponds To a
path that closes at N i .
. (M i\Gamma1 and all of its ancestors are removed.)
endif
endfor
Note that if the occurrence of a in N j is never resolved away, i.e. its
history path continues to the root, then the two literals corresponding
to a may occur in the root of T 0 . However, they are both at least as
general as a.

Figure

2 shows the effect of surgery on Figure 1. Surgery is performed
at using N 4 as N j . M are not needed in T 0 . By insisting
that both occurrences of a are closed at the same node, we ensure that
does not have a in its result when T does not. Thus N 0
5 closes both
history paths for a from N 0
Theorem 6. Let T be an irregular binary resolution tree on a set
S of clauses and T 0 is constructed by Operation 5. Then T 0 is also a
binary resolution tree on S, T 0 is smaller than T and the result of T 0
subsumes the result of T .
Proof. We use the following lemma: If clauses C 1 and C resolve to give
clause C 2 subsumes C 1 then either the resolution of C 2 and
C is not possible and C 2 subsumes R 1 , or it is possible and its result,
This assumes that all literals from C resolved in the
first resolution are also resolved in the second, and furthermore that
literals from C 2 are resolved in the second resolution if they correspond
(in the subsumption) to literals from C 1 resolved in the first resolution.
Each leaf in T 0 has the same label as a leaf in T and therefore T 0
is defined on S. Also, each internal node is defined by a resolution of
its parents, so T 0 is a binary resolution tree. Note that cl(N 0
subsumes cl(N 1 ) - a because cl(N 1 ) contains all the literals in cl(N 0 )
except possibly a. Using repeated applications of the lemma, it follows
that cl(N 0
cl(N j ) since a occurs in cl(N j ). Then cl(N 0
the result of T 0 subsumes that of T . Since M 0 is not in
T 0 and since all other nodes in T 0 are taken at most once from T , it
follows that T 0 has fewer nodes than T . 2
Theorem 7 (Completeness [14]). If S is unsatisfiable there exists a
closed regular binary resolution tree on S. Furthermore the smallest
closed binary resolution tree is regular.
Proof. If S is unsatisfiable, there exists a closed binary resolution tree
[11]. If it is irregular, apply Operation 5 repeatedly until it is regular.
This process must terminate since the tree is smaller at each step.
If the smallest closed binary resolution tree is not regular, surgery
can be applied to it, making a smaller closed tree. 2

Figure

3. A binary tree rotation
3. Minimal Binary Resolution Trees
A rotation of an edge in a binary tree is a common operation, for
example with AVL trees [1]. Before we apply it to binary resolution
trees, we review the operation on binary trees. Given the binary tree
fragment on the left of Figure 3, a rotation is the reassignment of edges
so that the tree on the right of Figure 3 is produced. The parent C of
becomes the child of E and the parent B of C becomes the parent
of E. If E has a child in T , then C takes that child in T 0 . In other
words, the edges (B; C), (C; E) and (E; F ) if it exists, are replaced by
the edges (B; E), (E; C) and (C; F ) if necessary.
Operation 8 (Edge Rotation). Let T be a binary resolution tree with
an edge (C; E) between internal nodes such that C is the parent of E
and C has two parents A and B. Further, suppose that no history path
through A closes at E. Then the result of a rotation on this edge is the
binary resolution tree T 0 defined by resolving cl(B) and cl(D) on al(E)
giving cl(E) in T 0 and then resolving cl(E) with cl(A) on al(C) giving
cl(C) in T 0 . Any history path closed at C in T is closed at C in T
similarly any history path closed at E in T is closed at E in T 0 . Also,
the child of E in T , if it exists, is the child of C in T 0 .
A rotation may introduce tautologies to clause labels of internal
nodes. For instance, if al(C) occurs in cl(D) then cl(E) in T 0 may
be tautological. However the clause label of the root is not changed
(Corollary 11). We prove a slightly more general result first, which is
also used later.
Definition 9. Let T 1 and T 2 be two binary resolution trees defined
on the same set of input clauses. Then T 1 and T 2 close history paths
similarly if there is a one-to-one and onto mapping - from nodes in T 1
to those in T 2 , such that:
1. If N is a leaf then -(N) is a leaf and both are labeled with instances
of the same input clause. Thus there is a natural one to one cor-
respondence, from literals in cl(N) to those in cl(-(N )). Moreover
this mapping of literals provides a mapping from history paths in
T 1 to those in T 2 , defined so that they start from the same literal
in the input clause, up to variable renaming. We represent these
other two mappings also with -. We require for all history paths P
in T 1 that tail(-(P
up to variable renaming.
2. For every history path P of T 1 , P closes at a node N if and only if
closes at -(N ).
Thus two binary resolution trees close history paths similarly if they
resolve the same literals against each other, albeit in a possibly different
order.
Lemma 10. If two binary resolution trees T 1 and T 2 close history
paths similarly, the result of T 1 and the result of T 2 are the same, up
to variable renaming.
Proof. Note that result(T 1 ) and result(T 2 ) are composed entirely of
literals from history paths that do not close, and since the same history
paths are closed in each, the same literals are not resolved away. Also
the composition of mgus in T 1 and that in T 2 are unique up to variable
renaming since, given a node N , the same literals are unified at N and
-(N ), up to variable renaming. 2
Corollary 11. Given a binary resolution tree T with an internal node
C and its child E, Operation 8 generates a new binary resolution tree
and cl(E) up to variable renaming.
Proof. Observe that Operation 8 produces a tree which closes history
paths similarly. 2
A rotation changes the order of two resolutions in the tree. Rotations
are invertible; after a rotation, no history path through D closes at
C, so another rotation at (E; C) can be done, which generates the
original tree again. We say that two binary resolution trees are rotation
equivalent if one can be generated from the other by a sequence of
rotations. For instance, the first binary resolution tree in Figure 4 is
produced by rotating the edge (N 4 ; N 5 ) in Figure 1. The second tree

Figure

4. From Figure 1 rotate
in

Figure

4 is then produced by rotating the edge (M 4 ; N 5 ). Thus both
trees are rotation equivalent to Figure 1. Rotation equivalent is an
equivalence relation. It is not surprising that rotation equivalent binary
resolution trees must close history paths similarly, but the converse is
true as well.
Theorem 12. Two binary resolution trees T 1 and T 2 are rotation
equivalent if and only if they close history paths similarly.
Proof. Since one rotation of T 1 creates a binary resolution tree that
closes history paths similarly to it, so too does the sequence of rotations
creating T 2 .
The converse is proved by induction on the number of internal nodes.
Suppose T 1 and T 2 close history paths similarly. Then they must have
the same number n of internal nodes since they have the same number
of leaves. If no rotation is possible and the theorem
holds. Let N be a node in T 1 with parents L 1 and L 2 that are leaves.
Then in T 2 , -(N) has proper ancestors -(L 1 ) and -(L 2 ) which also are
leaves, and -(N) closes only history paths with tails -(L 1 ) and -(L 2 ).
We create T 0
2 by rotating edges so that -(L 1 ) and -(L 2 ) are parents of
-(N ), if this is not already the case. Let C be either parent of -(N) and
let A and B be the parents of C. If -(L 1 ) and -(L 2 ) are both ancestors
of C then neither is an ancestor of the other parent of -(N ). But -(N)
must close a history path from that other parent, contradiction. Thus
the edge (C; -(N)) can be rotated, since not both A and B contain a
history path closing at -(N ). This rotation reduces the total number
of non-leaf ancestors of -(N ). After a finite number of such rotations,
both parents of -(N) are leaves. Call this tree T 0
.
Let T
1 be T 1 with leaves L 1 and L 2 deleted, and let T
2 be T 0
2 with
leaves
close history paths
similarly since T 1 and T 0
close history paths similarly. By induction T  and T
are rotation equivalent. The sequence of rotations to convert
1 to T
will also convert T 1 to T 0
2 which is rotation equivalent to T 2 .We focus on the set of rotation equivalent trees that do not contain
an irregular binary resolution tree. Any tree in this set is said to be
minimal, since surgery cannot be applied to make it smaller.
Definition 13. A binary resolution tree T is minimal if no sequence
of rotations of edges generates a tree T 0 that is irregular.
Theorem 14. If a binary resolution tree T on S is non-minimal, there
exists a minimal binary resolution tree T 0 on S which is smaller than
T and the result of T 0 subsumes the result of T .
Proof. If T is not minimal, apply Operation 8 and Operation 5 so that a
regular tree is produced. If this tree is minimal then let T 0 be this tree.
Otherwise repeat from the beginning until T 0 is defined. This process
must terminate because the tree is getting smaller at each application
of Operation 5. Also the old result is subsumed by the new result at
each step. 2
Thus a smallest binary resolution tree is minimal. Goerdt has shown
[4] that a smallest regular binary resolution directed acyclic graph
(DAG) may be exponentially larger than an irregular binary resolution
DAG. Thus by considering only regular or minimal binary resolution
DAGs, a theorem prover may not find the smallest proof, and hence
may require more inferences to prove a given theorem. However in most
cases we believe that the space of minimal binary resolution DAGs is
much smaller than the space of all binary resolution DAGs and that
considerable time can be saved by restricting to minimal ones. (Similar
arguments can be made for and against most restrictions of resolution,
including set-of-support and hyperresolution.)
4. Checking Minimality
Determining whether a given binary resolution tree is minimal seems
to be labourious, since the straightforward application of the definition,
as is done in the proof of Theorem 14, checks every possible sequence
of rotations, and there can be exponentially many. In this section we
give an efficient algorithm for determining visibility - which nodes can
be rotated below which - so deciding minimality is efficient.
Definition 15 (Visible). In a given binary resolution tree with internal
nodes N and M , we say that M is visible from N , and that N
can see M , if there exists a sequence of rotations such that M is a
descendant of N . Otherwise M is invisible from N .
Thus a node can see the nodes that can be rotated below it. Although
this is a property defined in terms of rotations, it is possible to inspect a
static tree, without doing any rotations, to determine visibility. Because
of this, visibility can be computed in linear time. That static property,
holds, is defined after one more concept, precedes.
Definition directly precedes a history
path Q if P and Q have no nodes in common, and P closes at
some node in Q. We write P OE Q. Moreover we say P precedes Q, and
there is a sequence of history paths (P
directly precedes P i+1 for
A history path P precedes a node N if N closes some history path Q
and P OE   Q.
The precedes relation is the reflexive and transitive closure of directly
precedes. In particular a history path precedes itself, even though
it does not directly precede itself. Also note that precedes defines a
partial order on the set of history paths.
In most cases a rotation does not change the precedes relation on
history paths.
Lemma 17. Let the history path P precede the history path Q in
the binary resolution tree T and let P be the images of
and T respectively after a rotation of the edge (C; E) as in Definition 8.
Further suppose that the head of Q is not C. Then P 0 precedes Q 0 in
Proof. Let and TD be the subtrees of T rooted at A; B and
C respectively. If close(P ) and head(Q) are in the same one of these
subtrees, the rotation has no effect on whether P ! Q. We know that
head(Q) is a proper descendant of close(P ). Also head(Q) is not C so
head(Q) must be a descendant of E.
Now if tail(P ) and tail(Q) are in the same subtree,
then the rotation does not affect P OE   Q because the node of Q which
P precedes is also in that subtree. Let P 1 be the path closing at that
node. Thus P OE   P 1 OE Q. We have these cases, which are illustrated
in

Figure

5.
1. tail(Q) is in . If tail(P ) is in closes at C. After the
rotation,
1 , which is one node longer, closes at C in T 0 . P 0 OE
Otherwise tail(P ) is in TD . Let P 0 denote the path through B
closing at C. After the rotation P 0 OE   P 0
2. tail(Q) is in TB . If tail(P ) is in after the rotation P 0 OE
Otherwise if tail(P ) is in TD then after the rotation, P 0 OE   P 0
3. tail(Q) is in TD . Since no path through A closes at E, we know
tail(P ) is not in . Thus tail(P ) is in TB . After the rotation,
directly hold an
internal node M of a binary resolution tree if M is the first node that
occurs on both P 1 and Q 1 , (i.e. the parent of M does not occur on
both.) We say that P and Q hold M if there exist history paths P 1 and
directly hold M . A
node N holds M if P and Q hold M and both P and Q close at N .
Also, if P and Q hold M and are in a set of history paths, we say
that the set holds M .
The following theorem relates invisible, a property that depends on
all rotation equivalent trees, to held, a property that can be checked
by examining just the one tree of interest.

Figure

5. Cases of Lemma 17
Theorem 19. The nearest common descendant of M and N holds M
if and only if M is invisible from N .
Proof. ()) We show that if the nearest common descendant of M and
holds M , then after a rotation, the (possibly new) nearest common
descendant of M and N holds M . Thus M can never be a descendant of
N for if it were then the nearest common descendant would be M , and
a node cannot hold itself. Cases in the proof of the forward direction
are in

Figure

6.
Let F be the nearest common descendant of N and M , and let the
rotated edge be (C; E), and let nodes A; B and D adjacent to it be as
defined in Operation 8. Let P and Q hold M and close at F , while P 1
and directly hold M , and P 1 OE   P and Q 1 OE   Q. Consider the case
where F 6= E, so that after the rotation F is still the nearest common
descendant of M and N . By Lemma 17, P 0
Suppose M 6= E. Then after the rotation, M is still the first common
node on P 0
1 , so F still holds M . Now suppose that
Without loss of generality assume that P 1 contains C and Q 1 contains
D. (Case 1a) If P 1 contains B then after the rotation, P 0
hold E, so F holds M . (Case 1b) If P 1 contains A then consider the
path and closing at C. After the rotation, P 0
that P 0
hold E, so again F holds M .
Now suppose that Consider the case (Case 2) where M is
an ancestor of C so that N is either E or an ancestor of D. Since no
history path can contain A and C and close at E, M 6= C. For the
same reason, P and Q contain B and close at E. (Case 2a) If M is an
ancestor of A then the paths that directly precede P and Q close at C
and hold M . Thus C holds M . After the rotation the nearest common
descendant of M and N is C, and C still holds M . (Case 2b) Otherwise
if M is an ancestor of B then after the rotation the nearest common
descendant of M and N is E and E still holds M .
Finally consider the case (Case is an ancestor of D.
(Case 3a) If N is either E or an ancestor of B then after the rotation,
holds M and is still the nearest common descendant of N and
M . (Case 3b) If N is C or is an ancestor of A, then consider path
R with head at B which closes at C. After the rotation, the nearest
common descendant of M and N is C, while R 0 directly precedes both
after the rotation.
Conversely, suppose that M is not held by the nearest common
descendant F of M and N . If then M is a descendant of N
and therefore visible from M . If F is the child of M then the edge
can be rotated, making M a descendant of F and therefore of
N . Assume that there exists a path (N
A
A
A
A
Case
3a
Case
R'
R
Q'
Q'
A
A
Q'
Case
A
A
A
Case
1a
Case
R
R'
A
A
Case
2a

Figure

6. Cases of Theorem 19
so that N i\Gamma1 and K i\Gamma1 are the parents of N i , for
use induction on n. Without loss of generality N 0 is
chosen so that al(N 2 ) occurs in cl(N 0 ); thus a history path through N 0
closes at N 2 . If there exists i in ng such that no history path
through N i\Gamma2 closes at N i then the edge (N can be rotated,
shown as Rotation 1 in Figure 7. We say that N i has been rotated
to the side of the path(M; F ), and so M is now closer to F and the
theorem holds by induction.
Thus for each i in path through N i\Gamma2 closes
at N i . If there is no j in ng such that N j is held by F then
in particular N n\Gamma1 is not held so the edge (N can be rotated.
But then the distance from M to the nearest common descendant of
M and N is and the theorem holds by induction. Choose
the smallest j in ng so that N j is held by F . Note that j 6= 1 by
assumption. If there is a history path through K j \Gamma2 closing at N j then
this path and the path through N j \Gamma2 closing at N j directly hold
Thus held by F , contradicting the definition of j. Therefore no
such path through K j \Gamma2 exists and the edge can be rotated as
illustrated in Rotation 2 of Figure 7. If is closer to F
after the rotation; we say that N j has been rotated off the top of the
path(M; F ), and the theorem holds by induction. Otherwise consider
the history paths through N j \Gamma2 closing at N j . If one of these includes
another includes K j \Gamma3 then N j \Gamma2 is held by F after the
rotation. This means that N j \Gamma2 was held by F before the rotation,
contradicting the definition of j. Thus the edge N j \Gamma2 N j can be rotated.
The result of this rotation is that N j will be rotated either to the side of
the path(M; F ), or closer to M . By a second induction on the distance
from M to N j , N i will eventually be rotated off the top or to the
side. Thus the distance from M to F will decrease by the constructed
sequence of rotations. 2
The sequence of rotations, constructed in the proof of Theorem 19
rotates the visible node M to below the node N that can see it. Thus
if the tree were regular but non-minimal, the rotations would make
it irregular, exposing the non-minimal parts. Using surgery, we can
remove all non-minimal sections of a tree, and reconstruct a minimal
tree from the pieces left behind.
Unfortunately the number of rotations required to expose a non-
minimality may be quadratic in the length of the path in the tree.
Since the trees are not balanced, this is quadratic in the size of the tree
in the worst case. Later we give a linear time operation, called splaying,
to bring a visible node to a descendant. In the next section, however,
we detect and avoid non-minimal trees.
Rotation 1: to the side
F
F
Rotation 2: off the top
F
F

Figure

7. Rotations in the proof of Theorem 19
5. Minimality as a restriction
Now we turn our attention to a theorem prover that keeps only minimal
binary resolution trees. Since every non-minimal tree is subsumed by
some minimal tree, this strategy uses the minimal criteria to reduce
redundancy, lessening reliance on subsumption.
Definition 20. Let T be a binary resolution tree. Then atoms(T
fal(N)jN is a node of Tgis called the set of atoms of T . A subbrt of T
is a binary resolution tree whose node set consists of a node of T called
the root of the subbrt, and all of its ancestors. For a subbrt T 0 of T ,
is a node of T 0 and visible from the root of Tg is
called the set of visible atoms of T 0 .
Theorem 21. Let binary resolution tree T consist of a root node R
and two subbrt's T 1 and T 2 . T is minimal if and only if
1. T 1 and T 2 are minimal,
2. no atom in cl(R) is in atoms(T ),
3.
4.
Proof. Assume that T is minimal. If T 1 or T 2 were not minimal, then
there would be a sequence of edge-rotations which would make the
subbrt irregular. The same sequence performed on T would make T
irregular as well. Hence the first condition is true. If the second condition
were false, then T would be irregular immediately. Assume that the
third condition is false. Then there are two nodes,
whose atom labels are the same, and M is visible from R. Hence M
can be rotated below R, without rotating any edges in T 2 . Now M
is the descendant of N , making T irregular. The fourth condition is
symmetric to the third.
Conversely, assume that T is not minimal. Then there is a sequence
of rotations that create an irregular tree T 0 . Node N has a descendant
M 1 in T 0 such that al(N) occurs in cl(M 1 ). Since the rotations do not
change cl(R), if al(N) occurs in the result of T 0 , it occurs in cl(R) in T
and then T violates the second condition. Thus al(N) does not occur in
cl(R) so there is a descendant M of N in T such that
If M and N are in the same T i then T i violates the first condition.
Assume M and N are in different T i . Since M has been rotated below
is visible from N in T , and by Theorem 19 M is not held by the
nearest common descendant R of M and N . Thus M is visible from R.
Therefore al(M) is in vis(T i ) while al(N) is in atoms(T 3\Gammai ). 2
Any theorem prover based on binary resolution that keeps only minimal
trees has already satisfied the first condition in Theorem 21 for
any newly constructed tree, since only minimal trees are used in the
construction. It is easy to check that the new result does not contain
an atom in atoms(T ). What is left is to find is an easy way to calculate
those atoms in each subbrt T i which are visible from the root of T .
The idea in Procedure 22 is that a node is visible in a subbrt T i if
and only if it is not held by the root of T , by Theorem 19. So for each
node N we need to calculate the history paths going through it that
precede the root. If some of these paths go through one parent of N ,
and some go through the other, then N is held by the root; otherwise
N is visible from the root.
In each procedure call visible(N; PN ), the first argument N is a
node in the tree and we want to know whether or not it is held by the
root. Initially it is one of the parents of the root, but as we traverse
upward it becomes instantiated with each ancestor of this parent. The
invariant we maintain is that the second argument, PN , is the set of
paths that include N and precede the root. The paths through the
parent of the root that precede the root are simply those whose heads
are that parent, so the invariant is easy to establish in the first place.
Suppose N has parents A and B. To calculate the paths PB through B
that precede the root, we start with PN , and remove those paths that
go through A if there are any. If there are none then PB is PN . If there
is some path in PN through A, we need to add to PB any path with
head at B, since these paths precede that path through A, and thus
precede the root.
Since we know that the paths in PN must go through at least one
of the parents of N , we assume that B is that parent.
Procedure 22 (Visible). Given a node N in a binary resolution tree
and a set PN of history paths that precede the root of the tree, vis(N; PN )
returns the atoms labels of nodes at and above N visible from the root.
Procedure vis(N; PN )
If (N is a leaf) return OE
Let A and B be the parents of N and partition PN into PA and
PB , which are the sets of paths which go through A and through B,
respectively. Assume without loss of generality that B is chosen so
that PB is nonempty.
Let CA and CB be the history paths with head at A and B respectively.
if PA is nonempty then
//N is held
return
else
and N is not held, so it is visible
return
endif
The third and fourth conditions in Theorem 21 require us calculate
which is done by calling vis(R i is the root of the
binary resolution tree, R 1 and R 2 are the parents of R, and R i is the
set of paths with heads at R i .
Procedure 22 runs in a number of set union calculations which is
proportional to the number of nodes in the tree. With hashing, these
operations can in principle be performed in time proportional to the
size of the clauses. Hence vis is a linear time algorithm, which is as fast
as one could expect.
We have implemented a prototype theorem prover for propositional
logic. It resembles OTTER[9], but it retains only minimal binary resolution
trees (so that the recursive calls in the first condition of Theorem
21 are not needed), whereas the proofs built by OTTER correspond
to non-minimal trees in some cases. Our implementation actually builds
binary resolution DAGs, instead of trees, to save space. This is important
because bottom-up theorem provers are limited by space as well
as by time. Note that Procedure 22 traverses the entire implicit tree,
so it may visit a single stored node more than once. Thus its runtime
is not guaranteed to be linear in the size of the DAG. The prototype
includes another restriction, discussed in [6], which ensures that from
each set of rotation equivalent binary resolution trees, exactly one is
found.
6. Restoring Minimality
There are two basic ways to restore minimality. If a binary resolution
tree is irregular then the surgery operation will remove the non-
minimality. For a binary resolution tree that is regular but non-minimal,
some rotations need to be done to make it irregular - we call this
exposing the non-minimality. This irregularity involves two internal
nodes M and N that resolve upon the same atom a and neither is a
descendant of the other but (at least) one is visible from the other.
Suppose M is visible from N . When M is rotated below N , one parent
of M becomes a descendant of N . Since a occurs in that parent's clause
label, surgery from N can be done.
In the proof of the converse of Theorem 19 we gave a quadratic
length sequence of operations for moving visible nodes down to become
descendants. Operation 24, called splaying, performs this with a linear
number of rotations. It is related to the splay operation [12] for binary
trees in that it brings a node closer to the root. In our case, to splay a
binary resolution tree at M , we divide the descendants of M into two
sets: the observers O for those that can see M , and the non-observers O
for those that cannot. Then we rearrange the tree so that all the nodes
in O are ancestors of M , leaving just those nodes in O as descendants
of M . Thus M is brought as close to the root as possible. This is done
in a way that guarantees N is an ancestor of M , so that surgery can
be accomplished.
The first step in the splay is to determine which descendants of M
can see M , as computed by Procedure 23.
Procedure 23 (Obs). Given a node M in a binary resolution tree T
such that P 1 is the complete set of history paths containing both M
and one parent of M and P 2 is the paths containing M and the other
returns the set of proper descendants of M that
can see M , called the observers of M .
Procedure obs(M;
if M is the root of T then
return OE
else
Let D be the child of M and K be the other parent of D.
Let C 1 be the paths from P 1 that close at D and C 2 be the paths
from P 2 that close at D.
Let K be the paths that contain both K and D.
holds M
return
else if C
return fDg [ obs(D; K[
else
endif
endif
The invariant of Procedure 23 is every pair of paths one from P 1
and the other from P 2 holds M . Then if we ever find a descendant D
that closes a member of each, then D holds M and so cannot see M ;
otherwise D can see M . To maintain the invariant as we go from M to
D, if D closes paths in P i we need to add to P i all of the paths K that
come from K through D, because each one of these paths precedes a
path that contains M . If D does not close any path through P i , then
we have nothing to add to P i . In either case we remove from P i any
path that closes at D since these do not contain D.
Operation 24 uses the same code as is in Procedure 23 (but not the
procedure itself) to decide how the resolutions below M should be re-ordered
in the new tree. The parents S 1 and S 2 of M are considered
stubs to be built upon. The observers of M are put into one of two
queues Q 1 and Q 2 , and the non-observers are put into Q 3 . Along with
each node put in the queue, we also put the subtree rooted at the other
parent of the node, so that the resolution can be reconstructed later.
Those put into Q 1 become descendants of S 1 , while those in Q 2 become
descendants of S 2 . After this is done, the two subtrees are joined by
a resolution corresponding to M . Finally all of the nodes in Q 3 are
made descendants of M . Each of the resolutions is done so that all
of the history paths closed at a node in the given tree are closed at
the same node in the constructed tree. Thus the resulting tree closes
history paths similarly with the given tree.
Operation 24 (Splay). A splay at an internal node M in a binary
resolution tree T produces a new binary resolution tree T 0 such that
all descendants of M cannot see M in T 0 .
Operation
Initially are three empty queues.
Initially P 1 is the set of history paths through M and one parent S 1
of M , while P 2 is the set of history paths through M and the other
parent S 2 of M .
call splay1(M;
return processQ(
Procedure splay1(M;
if M is the root of T then
return
else
Let D be the child of M and let K be the other parent of D.
Let C 1 be the paths from P 1 that close at D and C 2 be the paths
from P 2 that close at D.
Let K be the paths that contain both K and D.
holds M
enqueue D and the subtree rooted at K into Q 3
else if C
enqueue D and the subtree rooted at K into
else
enqueue D and the subtree rooted at K into
endif
endif
The resolutions must be done so that the resulting binary resolution
tree closes history paths similary with T .
Procedure processQ(T ; Q)
If Q is empty then
return T
else
dequeue T 1 and N from Q leaving Q 1
construct T 2 by resolving T and T 1 making them parents of N
return
endif
For example, the binary resolution tree in Figure 8 shows the result
of performing a splay from the node M = N 5 on the second tree in

Figure

4. The subtrees S 1 and S 2 are the leaves labelled a- b -:c, and
h, respectively. The descendants of N 5 are M 4
which N 3 and N 4 are put into Q 1 , while M 4 is put into Q 2 . These end
up above N 5 in the resulting tree. The only non-observer, N 6 , is put
into Q 3 and ends up below N 5 .
Lemma 25. If T is a binary resolution tree and M is an internal node
of T , then the result T 0 of splay(T ; M) is a binary resolution tree. T 0 is
defined on the same set of clauses as T ; is the same size as T and has
the same result as T .
Proof. T 0 closes history paths similarly with T . 2
Operation 26 (Splay Surgery). Let T be a binary resolution tree T
containing a pair M;N of nodes such that al(M) = al(N) and N can
see M
Procedure
if M is a descendant of N in T then
return surgery(N)
else
return
endif
To see that a splay actually brings M below N , so that surgery is
possible, suppose that the nearest common descendant of M and N is
not M . Thus either N is that nearest common descendant or N and M
are on different branches. N is either D or an ancestor of K at some
point in splay1. We also know N can see M so it must be put into one
of the queues Q 1 or Q 2 , and cannot be part of Q 3 . Thus when the tree
a-d
a:b-d-e
d:b-c-e
e:b-c-f-g
-a-b-e
c-d
e-f-g
a-b-c
a: b-b-f -b
g: a- b-b-f
-g
c:a- b-b-f-g
h:-a
-a-h

Figure

8. Result of Operation 24 at N5 on Figure 4
is rebuilt, N is put in while we are processing either Q 1 or Q 2 . M is
put in after Q 1 and Q 2 are empty, so it is below N .
Returning to our example, after the splay, the node N 5 in Figure 8 is
below N 1 and surgery from N 1 can be done. The result of this surgery
is the same as that shown in Figure 2. Notice that in this example we
also have the option to splay at N 1 and do surgery from N 5 , since N 1
is also visible from N 5 . The resulting tree would be different: it would
not require the leaf :a - h nor :h, and its result would have been f .
Thus surgery does not always produce a more general result, but always
produces a smaller tree.
Splay surgery does a linear number of set operations since it does
at most n resolution steps where n is the length of a branch, and then
performs surgery, which itself does a number of resolutions limited by
the length of a branch. Thus it is effectively a linear time algorithm.
7. Support
Often a node that is visible from another can be rotated so that it is not
a descendant, but sometimes no sequence of rotations can bring a node
from below another. In this case we say the node supports the other,
since it is always beneath it. Support, like visibity, is a property that
depends on the entire set of rotation equivalent trees. In this section
we characterize support in terms of history paths, so it can be checked
by examining a static tree.
Definition 27 (Support). A node N in a binary resolution tree T
supports a node M if after every sequence of rotations, M is an ancestor
of N .
Definition 28 (Tightly holds). Two history paths
tightly hold a node N if there exist two sequences
of history paths such that for
directly holds M ,
and for no pair does the head of P i equal
the head of Q j . A node N tightly holds M if both P and Q close at N .
Tightly holds is the special case of holds, where no two paths in the
sequences have the same head except the bottom two. This turns out
to be the exact condition for one node being below another after every
sequence of rotations.
Theorem 29. A node N tightly holds M if and only if N supports
M .
Proof. ()) We show that if N tightly holds M before a rotation, it
also does afterwards, and thus must be a descendant of M . Consider a
rotation of edge (C; E) where nodes A; B; C; D and E are defined as in
Definition 8. We will indicate the image of any history path P after the
rotation by P 0 . At first assume that fC; Eg is disjoint from fM;Ng. By
. Before the rotation all heads of
paths in the sequences were distinct so they must be distinct after the
rotation, unless there is a new path in either of the sequences. There is
one case where such a new path occurs. (In Lemma 17, the new path
introduced when tail(Q) is in .) In that
case the head of new history path was not on path(M; N ). Thus the
heads of paths of the new sequences (P 0
are
distinct except head(P 0
Also M is still directly held
by
1 so N tightly holds M .
Now suppose fC; Eg is not disjoint from fM;Ng. (Case 1) If
then without loss of generality let P 1 contain A and Q 1 contain B.
We know that P 1 does not close at E since the rotation is possible.
Suppose first that Q 1 does not close at E, as in Figure 9.1a. Then
after the rotation C is directly held by P 0
1 and so is tightly
held by N . Now suppose Q 1 closes at E, as in Figure 9.1b. Note that
there must exist Q 2 since otherwise E holds N and and so Q 1 and P 1
both close at and then the rotation is not possible. After the
A
C=N
A
Qm
Pn
Q'n
Case
2b A
A
Case
3a
A
A
Case
A
A
Case
1a A
A
Case
1b A
C=N
A
Pm
Qn
Q'n
Case
2a

Figure

9. Cases showing tightly hold is invariant under rotations
Case 1
Case 2
A
A
A

Figure

10. Cases showing support implies tightly holds
rotation, C is directly held by P 0
2 , and so is still tightly held
by N . (Case close at N , and
either they both include A, as in Figure 9.2a, or they both include B
as in

Figure

9.2b. In either case, after the rotation, N tightly holds
M by the sequences (P 0
(Case
then assume without loss of generality that C is in P 1 and
D is in Q 1 . If A is also in P 1 as in Figure 9.3a, then there is a path
with head at B and P 0 OE P 1 . After the rotation, the sequences
ensure that N tightly holds M . If B
is in P 1 , as in Figure 9.3b, then after the rotation the paths (P 0
and (Q 0
tightly holds M . (Case Finally if
then either Pm and Q n both contain C or both contain D. If they both
contain C then note that they both contain the same parent B of C,
else the rotation is not possible. Then after the rotation, B is a parent
of E and although P 0
are one node shorter than before, N
tightly holds M by the paths (P 0
both contain D, then after the rotation there is no change to the
history paths; thus N tightly holds M .
We induct on the length of path(M;
is the parent of N i+1 for
1. If is a parent of N and then a rotation of the edge (M; N) is
possible unless there exist history paths that tightly hold M and close
at N . Suppose k ? 2. First assume (case 1) that N k does not support
. Then by the first half of this theorem N k does not tightly hold
and so the edge (N can be rotated. Since M must remain
an ancestor of N; M must be an ancestor of B in the rotation, as shown
in

Figure

10.1. Thus the path from M to N is shorter, and by induction
tightly holds M in the new binary resolution tree. By rotating the
edge back again, one sees that N tightly holds M in T , because tightly
holds is invariant under rotation. As this case is covered, from now on
we assume that N k supports N k\Gamma1 .
Next assume (case 2) that N k does not support N k\Gamma2 . Then N
does not support N k\Gamma2 , for otherwise N k supports N k\Gamma1 supports N k\Gamma2
and, by transitivity of support, there is a contradiction. By the first half
of this theorem, we may rotate the edge (N k\Gamma2 ; N k\Gamma1 ). Then we may
rotate the edge (N k\Gamma2 ; N k ), since N k does not tightly hold N k\Gamma2 . In
this second rotation, N k must remain a descendant of N k\Gamma1 so it must
be as shown in the third binary resolution tree in Figure 10.2. Thus
path(M; N) is shorter, so by induction N tightly holds M . Because
tightly holds is invariant under rotation, N tightly holds M in T also.
From now on we assume that N k supports N k\Gamma2 . By similar arguments
we assume that N k supports each of N
(Case If the edge (M; N 2 ) can be rotated in T then path(M; N)
is shorter in the resulting tree T 0 and by induction N tightly holds M
in T 0 . Since tightly holds is invariant under rotation, N tightly holds
in T .
Finally if the edge (M; N 2 ) cannot be rotated then there are paths
from each parent of M closing at N 2 in T . We know by induction that
tightly holds N 2 and assume that (P are
the paths that make this so. Assume without loss of generality that
includes M . Then Q 1 must include the other parent of N 2 since N 2
is the first node that P 1 and Q 1 have in common. No matter which
parent of M is in P 1 , there is a path closing at N 2 containing M and
's other parent. Call this path Q 0 . Since the head of Q 0 is M , it is
distinct from the heads of the other P i and Q j in the sequences. Thus
tightly holds M by the paths (Q
In this final theorem, we relate the notions of visibility and support.
Theorem 30. In a binary resolution tree, a node M is invisible from
a node N iff there is a support S of M on path(M; N ).
Proof. ()) Let D be the nearest common descendant of M and N .
Consider the path sequences by which D
holds M . Consider the least i and j such that head(P i
and let S be the node where P i and Q j both close. These i and j must
exist since the head(Pm the heads of paths before
are distinct, S tightly holds M and thus S supports M .
be the
sequences of paths by which S tightly holds M . Since S is on path(M; N ),
and S is a descendant of M , S must be an ancestor of the nearest
common descendant D of M and N . Thus there are paths R
such that S is on R 1 and R k closes
at D. Thus D holds M via the sequences
8. Relation to Clause Trees
The results in this paper were developed after we understood clause
trees [5], and then primarily as a means to implement clause trees.
We eventually found that most of our ideas from clause trees could be
expressed in binary resolution trees. Binary resolution trees are simpler
in some ways since they are easier to implement, but more often clause
trees are easier to use when exploring new ideas. In particular, visibility
and support can be read almost directly from a clause tree, whereas the
properties held and tightly held are somewhat harder to see in binary
resolution trees. We use whichever is appropriate. In this section we
relate the two.
Refering once again to the example, the rotation equivalent binary
resolution trees in Figures 1, 4 and 8 all correspond to the first clause
tree in Figure 11. The binary resolution tree in Figure 2 corresponds
the second clause tree in Figure 11. A reader familiar with clause trees
will note that the second clause tree in Figure 11 can be constructed
directly from the first by adding a merge path between the a atom
nodes and then doing surgery to remove the subtree beyond the tail of
the new merge path.
Some of the correspondences between binary resolution trees and
clause trees are obvious. The leaves of a binary resolution tree are the
clause nodes of the clause tree; both are labeled by an instance of an
input clause. The internal nodes of a binary resolution tree are the
atom nodes of a clause tree. A history path in a binary resolution tree,
which we associate with a literal, corresponds to a labeled edge in a
clause tree, also associated with a literal. If the history path is not
closed, it corresponds to an edge incident with an atom node leaf; a
closed history path corresponds to an edge incident with a closed atom
node.
_
a
c d a
e
f
_
_
a
c d a
_
_
_

Figure

11. Clause trees corresponding to Figures 1, 4, and 8 and to Figure 2
Minimal clause trees correspond to minimal binary resolution trees
whose result does not contain two identical atoms. The minimal condition
on clause trees does not allow any legal unchosen merge path
or legal tautology path, including leaf to leaf paths. A minimal binary
resolution tree may correspond to a clause tree with a legal unchosen
leaf to leaf merge path, or legal leaf to leaf tautology path. This is
because the regularity condition in binary resolution trees requires one
of the nodes to be internal.
Finally, visibility (resp. support) between internal nodes in a binary
resolution tree correspond to visibility (resp. support) between closed
atom nodes in a clause tree. Table I shows a number of the corresponding
notions.

Table

I. Corresponding notions
Clause Trees Binary resolution trees
clause node leaf node
internal atom node internal node
edge history path
open leaf atom node literal in result
cl(T
internal-to-internal surgery splay surgery
internal-to-leaf surgery surgery
merge path two history paths closing together
equivalence classes of reversal equivalent equivalence classes of rotation equivalent
minimal (up to leaf-to-leaf) minimal
visible internal atom nodes visible
support on internal atom nodes support
path reversal no structural change
no structural change rotation (change in derivation)
merge set all history paths closing at a given node
9. Related, Past and Future Work
Regularity is one of the most important restrictions and some form
of it is used in many theorem proving methods related to resolution,
including tableau [10], and all variants of model elimination[8].
Permuting inference steps has been investigated by Kleene [7], in the
context of Gentzen's sequence calculus, both classical and intuitionistic.
Kleene's permutations sometimes increase the size of the proof. It is
interesting to note he defines the ancestor relation between instances
of formulas in each inference, allowing him to state which instances of
formulas in the deduction belong to a given instance in the end sequent.
This is analagous to our notion of history paths.
In the context of binary resolution derivations, de Nivelle [3], has
two types of nodes: resolution nodes have two parents and factoring
nodes have one. He defines four types of edge rotations, depending on
the type of nodes incident with the edge. We disallow the rotation
where a factorization node is parent to a resolution node, because in
this case the size of the derivation must be increased. His application
is to construct resolution games which are then used to show various
completeness results for restrictions of resolution based on ordering
literals. Both de Nivelle's paper and ours show that basic properties
of resolution may be exposed by considering the set of trees equivalent
modulo permutations.
The main contribution of this paper is to present the minimal restriction
of resolution, originally developed in terms of clause trees, using
the well known proof format of binary resolution derivations. The original
motivation for doing so was to implement bottom up algorithms
for constructing minimal clause trees. A direct implementation, based
on the structural definition of clause trees was done, but each new tree
needed its own storage space and the visibility algorithm was cumber-
some. To remedy both of these problems we used the notion of binary
resolution derivations and implemented each new clause tree as a single
storage cell with two parent clause trees. (For propositional logic this
solves the space problem, since each tree can be used as part of other
trees.) The surprising result is that visibility can be expressed easi-
ly, and requires a linear algorithm using this data structure. We then
determined to explain as much of our clause tree work as we could
using binary resolution trees, to make them more accessible to readers
familiar with resolution. This task turned out to be difficult until we
discovered that edge rotations, history paths and the "precedes" relation
between history paths are the fundamental concepts needed. Then
we related visibility and support to history paths using the "holds" and
"tightly holds" relations. In retrospect the authors still believe that it
is easier to work conceptually with clause trees. We have anecdotal evi-
dence, from a graduate course in automated reasoning given two times
by the second author, once with clause trees only and once with binary
resolution trees followed by clause trees, that the intuitions for support
and visibility are quite understandable using either data structure.
We are presently developing the full theorem provers described here,
one to use minimality as a restriction and another to use splay and
surgery to improve proofs after they are constructed by resolution.
Redundancy elimination by subsumption is always an important consideration
for theorem provers. Unfortunately the minimal restriction
is not complete with full subsumption. For instance one can not refute
with a minimal binary resolution tree if one resolves p
against :p-q, generating q, and then uses back subsumption to remove
before the resolution between :p - q and :p - :q is done. The
latter resolution is part of the only minimal binary resolution refutation
of these clauses. The former resolution step leads to a binary resolution
tree in which p is resolved at two different nodes on one branch.
However, we have discovered [6] that one can retain completeness by
giving up some of the power of minimality, without giving up any of
the power of subsumption.
The space of minimal binary resolution trees is interesting for the
following reasons: (1) it is refutationally complete, (2) it extends the
well known regularity restriction of resolution (3) it contains the smallest
binary resolution tree, (4) non-minimal (sub)trees can be identified
in time linear in the size of the tree, and (5) non-minimal trees can be
reduced to minimal ones efficiently.



--R

An algorithm for the organizaton of information.
Symbolic Logic and Mechanical Theorem Proving.
Resolution games and non-liftable resolution orderings
Regular resolution versus unrestricted resolution.
Clause trees: a tool for understanding and implementing resolution in automated reasoning.
Bottom up procedures to construct each minimal clause tree once.
On the permutability of inferences.
Mechanical theorem proving by model elimination.
Otter 3.0 users guide.

A machine-oriented logic based on the resolution principle

Extending the regular restriction of resolution to non-linear subdeductions
On the complexity of derivation in propositional calculus.
--TR
clause tree;resolution;binary tree;regularity;theorem proving