Reductions for non-clausal theorem proving.
This paper presents the TAS methodology as a new framework for generating non-clausal Automated Theorem Provers. We present a complete description of the ATP for Classical Propositional Logic, named TAS-D, but the ideas, which make use of implicants and implicates can be extended in a natural manner to first-order logic, and non-classical logics. The method is based on the application of a number of reduction strategies on subformulas, in a rewrite-system style, in order to reduce the complexity of the formula as much as possible before branching. Specifically, we introduce the concept of complete reduction, and extensions of the pure literal rule and ofthe collapsibility theorems; these strategies allow to limit the size ofthe search space. In addition, TAS-D is a syntactical countermodel construction. As an example of the power of TAS-D we study a class of formulas which has linear proofs (in the number of branchings) when either resolution or dissolution with factoring is applied. When applying our method to these formulas we get proofs without branching. In addition, some experimental results are reported. Copyright 2001 Elsevier Science B.V.
Introduction
Much research in automated theorem proving has been focused on developing satisfiability
testers for sets of clauses. However, experience has pointed out a number of disadvantages of
this it is not natural to specify a real-world problem in clause form, the translation
into clause form is not easy to handle and, although there a number of e#cient translation
methods, models usually are not preserved under the translation. In addition, clausal methods
are not easy to extend to non-classical logics, partially because no standard clause form can
be defined in this wider setting.
Non-clausal theorem proving research has been mainly focused on either tableaux methods
or matrix-based methods; also some ideas based on the data structure of BDDs have been
Partially supported by CICYT project number TIC97-0579-C02-02.
stands for Transformaciones de -
Arboles Sint-acticos, Spanish translation of Syntactic Trees Transformations

used in this context. Recently, path dissolution [6] has been introduced as a generalisation of
the analytic tableaux, allowing tableaux deductions to be substantially speeded up.
The central point for e#ciency of any satisfiability tester is the control over the branching,
and our approach is focussed on the previous reduction of the formula to be branched as much
as possible before actually branching. Specifically, we introduce the concept of complete
reduction, and extensions of the pure literal rule and of the collapsibility theorems. On the
other hand, another interesting point in the design of ATPs is the capability of building
models provided the input formula is satisfiable.
A non-clausal algorithm for satisfiability testing in the classical propositional calculus,
named TAS-D, is described. The input to the algorithm need not be in conjunctive normal
form or any normal form. The output is either "Unsatisfiable", or "Satisfiable" and in
the latter case also a model of the formula is given.
To determine satisfiability for a given formula, firstly we reduce the size of the formula
by applying satisfiability-preserving transformations, then choose a variable to branch and
recursively repeat the process on each generated task. This feature allows:
. to obtain useful information from the original structure of the formula.
. to make clearer proofs.
. to extend the method to non-classical logics which do not have a widely accepted normal
form.
Although our intention in this paper is to introduce the required metatheory, TAS-D
is currently being tested and we are obtaining very promising results. In our opinion, the
results of these tests allow to consider the TAS framework as a reliable approach to Automated
Theorem Proving. TAS ideas are widely applicable, because apply to di#erent types of logics;
flexible, because provide a uniform way to prove soundness and completeness; and, in addition,
easily adaptable, because switching to a di#erent logic is possible without having to redesign
the whole prover. In fact, it has been already extended to Classical First Order Logic [4],
Temporal Logic [5] and Multiple-Valued Logic [1, 2].
The structure of the paper is as follows:
1. Firstly, the necessary definitions and theorems which support the reduction strategy are
introduced in Section 2.
2. Later, the algorithm TAS-D is described in Section 3.
3. Finally, a comparative example is included in Section 4, which shows a class of formulas
which has linear proofs (in the number of branchings) when either resolution or dissolution
with factoring is applied [3, 7]. When applying TAS-D to these formulas we get
proofs without branching.
1.1 Overview of TAS-D
TAS-D is a satisfiability tester for classical propositional logic; therefore it can be used as a
refutational ATP method and, like tableaux methods, it is a syntactical model construction.
The reduction strategies are the main novelty of our method with respect to other non-clausal
ATPs; like these methods, TAS-D is based on the disjunctive normal form. Its power
is based not only on the intrinsically parallel design of the involved transformations, but
also on the fact that these transformations are not just applied one after the other, but
guided by some syntax-directed criteria, described in Sections 2.2 and 2.4, whose complexity
is polynomial. These criteria allow us:
1. To detect subformulas which are either valid, or unsatisfiable, or equivalent to literals.
2. To detect literals # such that it is possible to obtain a equisatisfiable formula in which
# appears at most once. Therefore, we can decrease the size of the problem as much as
possible before branching.
By checking these criteria we give ourselves the opportunity to reduce the size of the problem
while creating just one subproblem; in addition, such reductions do not contribute to exponential
growth. However, the most important feature of the reductions is that they enable
the exponential growth rate to be limited.
As an ATP, TAS-D is sound and complete and, furthermore, as a model building method,
it generates countermodels in a natural manner.
1.2 Preliminary Concepts and Definitions
Throughout the rest of the paper, we will work with a classical propositional language with
connectives {-, #} and their standard semantics; V denotes the set of propositional
denotes the set of literals; if # is a literal then # is its opposite literal; we will
also use the usual notions of clause, cube, implicant, implicate and negation normal form
(nnf). S # A denotes that S is a subformula of A, and S # A denotes that S is a proper
subformula of A.
An assignment I is an application from the set of propositional variables V to {0, 1}; the
domain of an assignment can be uniquely extended, preserving the standard semantics, to
the whole language. A formula A is said to be satisfiable if there exists an assignment I such
that 1, in this case I is said to be a model for A; formulas A and B are said to be
equisatisfiable if A is satisfiable i# B is satisfiable; formulas A and B are said to be equivalent,
denoted A # B, if assignment I ; |= denotes the logical consequence;
finally, the symbols # and # mean truth and falsity.
The transformation of a formula into nnf is linear (by repeated application of De Morgan
rules, the double negation rule and the equivalence A # B # -A#B), so in the following we
will only consider formulas in nnf. In addition, by using the associative laws we can consider
connectives # and # to have flexible arity, and expressions like A 1 # A n or A 1 #A n
to be well formed formulas.
We will use the standard notion of tree and address of a node in a tree. An address # in
the syntactic tree of a formula A will mean, when no confusion arises, the subformula of
A corresponding to the node of address # in will denote the address of the root node.
Similarly, when we say a subformula B of A we mean an occurrence of B in A; if B # A,
denotes the address of the node corresponding to B in
is a set of literals, then # 1 , # 2 , . , # n }.
is a set of literals in A and #}, then the expression A[#]
denotes the formula obtained after substituting in A, for all #, every occurrence of # by #,
and # by #.
and C are formulas and B # A, then A[B/C] denotes the result of substituting in
A any occurrence of B by C. If {# 1 , . , # n } is a set of literals in A and C i are formulas, then
the expression A[# 1 /C 1 , . , # n /C n ] denotes the formula obtained after substituting in A, for
all i, every occurrence of # i by C i .
If # is an address in A and C is a nnf, then the expression A[#/C] is the formula obtained
after substituting in A the subtree rooted in # by C.
Adding Information to the Tree: #-lists and
#-sets
The idea underlying the reduction strategy is the use of information given by partial assignments
(extensively used in Quine's method [8]) just for unitary assignments but, as we will
show, in a powerful manner.
We associate to each nnf A two lists 2 of literals denoted (the associated
#-lists of A) and two sets, denoted
c
c
whose elements are obtained out of
the associated #-lists of the subformulas of A.
The #-lists and the
#-sets are the key tools of our method to reduce the size of the
formula being analysed for satisfiability.
2.1 The #-lists
In a nutshell, are, respectively, lists of implicates and implicants of A. The
purpose of these lists is two-fold: firstly, to transform the formula A into an equivalent and
smaller-sized one (Section 2.2), and secondly, by means of the
c
# b sets (Sections 2.3 and 2.4),
to get an equisatisfiable and smaller-sized one. Their formal definition is the following:
1: Given an nnf A, are recursively defined as follows:
In addition, elements in a # 0 -list are considered to be conjunctively connected and elements
in a # 0 -list are considered to be disjunctively connected, so that some simplifications are
applied. Namely, if {# 0 (A), then # 0 (A) is simplified to #, and if {# 1 (A),
then is simplified to #.
We use lists in lexicographic order just to facilitate the presentation of the examples. The reader can
interpret them as sets.
The intuition behind the definition is easy to explain, since in # 0 (
we intend to
calculate implicates (for it is # 0 ), and since the union of the implicates of each conjunct is a
set of implicates of the conjunction, then we use S , and so on.
Example 1:
2.
3. ps # st
2.2 Information in the #-lists
In this section we study the information contained in the #-lists of a given formula. Our
first theorem states that elements of # 0 (A) are implicates of A, and elements of # 1 (A) are
implicants of A, and follows easily by structural induction from the definition of # b -lists.
Theorem 1 Let A be a nnf and # be a literal in A then:
1. If # 0 (A), then A |= # and, equivalently, A # A.
2. If # 1 (A), then # |= A and, equivalently, A # A.
As an immediate corollary of the previous theorem we have the following result on the
structure of the #-lists:
Corollary 1 For every nnf A we have one and only one of the following possibilities:
. There is b # {0, 1} such that # b
. #, and then A #.
The following corollary states a condition on the # 1 -lists which directly implies the satisfiability
of a formula.
then A is satisfiable, and if # 1 (A), then any assignment
I such that is a model for A.
On the other hand, the following result states conditions on the #-lists assuring the
validity or unsatisfiability of a formula.
Corollary 3 Let A be a nnf, then
1. If
in which a conjunct A i 0
is a clause such that # 1
A #.
2. If A = W n
in which a disjunct A i 0
is a cube such that # 0
A #.
Proof:
1. Let
using the results of Theorem 1, if A i 0
Therefore:
_
_
2. It is similar to the previous one.
Definition 2: If A is a nnf, to #-label A means to associate to each node # in A the ordered
Let us name those formulas whose #-lists allow to determine either its validity or its
(un)satisfiability.
Definition 3: A nnf A is said to be
. finalizable if one of the following conditions holds:
1.
2.
This definition will be applicable to the current formula when it is detected to be
(un)satisfiable. The following three definitions are referred to subformulas of the current
formula which are detected to be either valid, or unsatisfiable, or equivalent to a literal.
. # 1 -conclusive if one of the following conditions holds:
1.
2.
and a disjunct A i 0
is a cube such that # 0
. # 0 -conclusive if one of the following conditions holds:
1.
2.
and a conjunct A i 0
is a clause such that # 1
. #-simple if A is not a literal and #
#(rs, nil )
#(nil, qst )
#(qrs, nil )
s

Figure

1: The tree
The previous results state the amount of information in the #-lists which is enough to
detect (un)satisfiability; when all these results are applied to a given formula, the resulting
one is said to be #-restricted, and its formal definition is the following:
Definition 4: Let A be an nnf, then it is said that A is #-restricted if it satisfies the following
conditions:
. it is not finalizable,
. it has no subtree which is either # 0 -conclusive, or # 1 -conclusive, or #-simple,
. it has neither # nor # leaves. 3
From the previous results we can state that if A is a nnf, then by repeatedly applying the
following sequence of steps we get a #-restricted formula:
1. #-label.
2. Substitute subformulas B # A by either # (if B is # 1 -conclusive), or # (if B is # 0 -
conclusive), or a literal # (if B is #-simple).
3. Simplify logical constants (# or #), as soon as introduced, by using the 0-1-laws.
4. Check for (un)satisfiability of A (namely, chech whether A is finalizable).
Example 2: Given the formula
a linear transformation allows to get a nnf which is equivalent to its negation, A, depicted in
Fig. 1 (for readability reasons, leaves are not labelled in the figures).
When #-labelling A, the method finds that node 6 (the right-most branch) is s-simple.
The s-simple subtree is substituted by s and then formula B in Fig. 2 is obtained.
New applications of the #-lists to get information (up to equivalence) of a formula A are
given by the following theorem and its corollary.
3 Although the input formula is supposed not to contain occurrences of logical constants, they can be
introduced by the reductions as we will see.
#(rs, nil )
#(nil, qst )
r s

Figure

2: The tree TB .
Theorem 2 Let A be a nnf and # be a literal in A, then:
1. If # 0 (A), then A # A[#]
2. If # 1 (A), then A # A[#]
Proof: 1. Let I be an assignment; we have to prove that
. If Theorem 1 (item 1) since # 0 (A), we have that A # A,
therefore Now the result is obvious.
. If
The second item is proved similarly.
As an immediate consequence of the previous theorem, the following satisfiability-preserving
result can be stated, which will be used later:
Corollary 4 Let A be a nnf. If # 0 (A), then A and A[#] are equisatisfiable.
Furthermore, if I is a model of A[#], then the extension I # of I such that I #) = 1 is
a model of A.
The following theorem allows to substitute a whole subformula C of A (not just literals
as in Theorem 2) by a logical constant.
Theorem 3 Let A be a nnf, C # A then:
1. If
2. If
3. If # 0 (A) and # 0 (C), then A # A[C/#]
4. If # 0 (A) and # 1 (C), then A # A[C/#]
Proof:
1. By Theorem 1, we have A # A and C # C. Let I be an interpretation, then
The rest of the items are proved similarly.
2.3 The
#-sets
In the previous section, the information in the #-lists has been used locally, that is, the
information in # b (#) has been used to reduce node #, by using Theorem 1. In this section, the
purpose of defining a new structure, the
#-sets, is to allow the globalisation of the information,
in that the information in # b (#) can be refined by the information in its ancestors.
Given a #-restricted nnf A, we define the sets
c
whose elements are
pairs (#) where # is a filtered # b -list associated to a subformula B of A, and # is the address
of B in A. In Section 2.4 we will see how to transform the formula A into an equisatisfiable
and smaller sized one by using these sets.
The definition of the
#-sets is based on the Filter operator which filters information
in the #-lists according to Theorems 2 and 3. Specifically, some literals in the #-lists can
allow to substitute a subformula by either # or # as a consequence of Theorem 3; on the
other hand, when this theorem is not applicable, it is still possible to delete the rest of which
are dominated, as an application of Theorem 2. In fact, the dominated literals will not be
deleted, but framed, because they will be used in the extension of the mixed collapsibility
theorem.
Given a #-restricted nnf A and B # A we have:
. Filter(# 0 (B)) is:
1. #, if there is a literal
A.
This is a consequence of Theorem 3, items 1 and 3.
2. The result of framing any literal
A.
This is a consequence of Theorem 2, items 1 and 2 resp.
. Filter(# 1 (B)) is
1. #, if there is a literal
A.
This is a consequence of Theorem 3, items 2 and 4.
2. The result of framing any literal
A.
This is a consequence of Theorem 2, items 2 and 1 resp.
Definition 5: Let A be a #-restricted formula. For b # {0, 1}, the set
c
recursively
defined as follows:
. If # is a literal, then
c
c
. Otherwise,
c
a subformula of A and # b (B) #= nil}
In the following example we present a step-by-step calculation of
c
-sets.
Example 3: Consider the formula A whose #-labelled tree appears below,
#(nil, rs )
r s
# (nil, ps )
r #(nil, q )
s q
#(nil, qrs )
s
For this tree, we have
c
Literal p in nodes 3111, 3112 and 311 is framed because of its occurrence in # 0
literal -
s in node 3112 is framed because of the occurrence of s in # 1
On the other hand, the
c
for A is the following:
c
q-s, 22122),
q-r, 221), ( -
qrs, 222), ( -
q, 22), (-p-q, 2), (s, 3)}
Node 211 is substituted by # because of the occurrences of -
q in # 1 (2) and q in # 1 (211); and
node 22121 is substituted by # because of the occurrences of p in # 1 (2) and -
Finally, the occurrences of -
are framed because of the occurrence of - p in # 1 (2), and the
occurrences of -
q are framed because of the occurrence of - q in # 1 (2).
#b
#-sets and meaning-preserving results
In this section we study the information which can be extracted from the
#-sets. This is
stated in Theorem 4, and in its proof we will use the following facts about the
#-sets of a
given #-restricted nnf A:
. No element in
c
is (#), since A is a #-restricted nnf and cannot be finalizable.
. If (# c
# b (A), then # is not the address of a leaf of A (since
c
c
all literal #).
. If # 0 (A), then (# c
and the list # does not have framed literals. (Just
note that a literal # is framed in (#) from the information in the #-lists of its
ancestors).
The following theorem states that, as the #-labels, the
#-labels also allow substituting
subformulas in A by either # or #.
Theorem 4 Let A be a #-restricted nnf then
1. If (# c
2. If (# c
Proof:
1. Suppose (# c
let C be the subformula at address #. By the definition of
c
there exist a formula B such that C # B # A and a literal # satisfying
By Corollary 1, using that # 0 (C), that the address # cannot correspond to a leaf,
and that A is a #-restricted nnf (specifically, A does not have #-simple subformulas),
we get that # 1
Note that, clearly, it is enough to prove that B # B[C/#].
Firstly, we will prove that, under these hypotheses:
(a) If # 1 (B), then # 1 (B[C/#]).
(b) If # 0 (B), then # 0 (B[C/#]).
Proof of (a): By induction on the depth of # in B, denoted dB (#).
(i) If dB to commutativity and
associativity).
It cannot be the case that
(D), we would have # 1 (C), which contradicts the fact that # 1
Therefore, we must have consequently, B[C/# D. Now,
using again # 1 we have that # 1 (D)
and, therefore, # 1
(ii) Assume the result for dX us prove it for dB
then the result is obvious.
by the induction hypothesis we
have that # 1 (B 1 [C/# 1 (B[C/#]).
by the
induction hypothesis, # 1
- The cases C # B 2 are similar.
The proof of (b) is obtained by duality.
Finally, we prove B # B[C/#] by considering the two possibilities in (1) above:
. If # 0 (C) and # 1 (B), then
B[C/#] by Theorem 3
# B[C/#] by (a) and Theorem 1
. If # 0 (C) and # 0 (B), then
B[C/#] by Theorem 3
# B[C/#] by (b) and Theorem 1
2. The proof is similar.
Note that this theorem introduces a meaning-preserving transformation which allows substituting
a subformula by a constant. The information given by the #-lists substitutes subformulas
which are equivalent to either # 1 -conclusive) or # 0 -conclusive); however, under
the hypotheses of this theorem, it need not be true that # is equivalent to either # or #.
A be an nnf then it is said that A is restricted if it is #-restricted and
satisfies the following:
. There are not elements (#) in
c
. There are not elements (#) in
c
If A is a nnf, to label A means #-label and associate to the root of A the ordered pair
c
c
Note that given a #-restricted nnf, A, after calculating (
c
c
the (un)satisfiability of A or an equivalent and restricted nnf by means of the substitutions
determined by Theorem 4, and the 0-1-laws.b
#-sets and satisfiability-preserving results
The following results will allow, by using the information in the
#-sets, to substitute a nnf A
by an equisatisfiable and smaller sized A # with no occurrences of some literals occurring in A.
A complete reduction theorem
To begin with, Corollary 4 can be stated in terms of the
#-sets as follows:
Theorem 5 (Complete reduction) Let A be a nnf such that (# c
then A is satisfiable
if and only if A[#] is satisfiable. Furthermore, if I is a model of A[#],
then the extension I # of I such that I #) = 1 for all # is a model of A.
Note that this result allows to eliminate all the occurrences of all the literals appearing in
#, that is why it is named complete reduction. Its usefulness will be shown in the examples.
Generalised pure literal rule
The introduction of the
#-sets allows a generalisation of the well-known pure literal rule for
sets of clauses. Firstly, recall the standard definition and result for a formula in nnf:
Definition 7: Let # be a literal occurring in a nnf A. Literal # is said to be pure in A if #
does not occur in A.
A be a nnf and # a pure literal in A then A is satisfiable i# A[#] is satisfiable.
Furthermore, if I is a model of A[#], then the extension I # of I such that I #) = 1 is a
model of A.
Our
#-sets allow to generalise the definition of pure literal and, as a consequence, to get
an extension of the lemma above.
Definition 8: Let A be a nnf. A literal # is said to be
#-pure in A if it satisfies the following
conditions:
1. # occurs in
c
2. All the occurrences of # in
c
are framed.
Next theorem is a proper extension of Lemma 1 (for it can be applied even when # and #
occur in A).
Theorem 6 (Generalised pure literal rule) Let A be a nnf, let # be a
#-pure literal in
A and let B be the formula obtained from A by the following substitutions:
(i) If (# c
with #, then node # in A is substituted by #].
(ii) If (# c
with #, then node # in A is substituted by #.
Then A is satisfiable if and only if B is satisfiable. Furthermore, if I is a model of B, then
the extension I # of I such that I #) = 1 is a model of A.
Proof: By Theorem 2, and the definition of the
#-sets, we have that
(a) If (# c
in addition, we have #, then
A # A[#])]
(b) If (# c
and if, in addition, we have #, then
A # A[#])]
Therefore, if we consider the formula A # , obtained when applying the equivalences of items
(a) and (b), we get that literal # is pure in A # . Now, by an application of Lemma 1 to A # we
get the formula B, which completes the proof.
In the rest of the section we introduce the necessary definitions to extend the collapsibility
results introduced in [9].
Collapsibility theorems
Definition 9: Let A be a nnf and # 1 and # 2 literals in A. Literals # 1 and # 2 are 0-1-bound if
the following conditions are satisfied:
1. There are no occurrences 4 of either # 1 or # 2 in
c
have that # 1 # i# 2 #.
2. There are no occurrences of either # 1 or # 2 in
c
we have
that
From the definition of
#-sets we have that:
Remark 1: If # 1 and # 2 are 0-1-bound in A, then every leaf in A with a literal in {# 1
has an ancestor # in A which is maximal in the sense that its associated #-lists satisfy one
of the following conditions:
is an ancestor of #, then none of the literals # 1 , # 2 , # 1 , # 2 occur in
the #-lists associated to # .
is an ascendant of #, then none of the literals # 1 , # 2 , # 1 , # 2 occur
in the #-lists associated to # .
We will use the following notation in the proof of the collapsibility results, where # i are
literals, and b # {0, 1}:
Theorem 7 (Collapsibility) Let A be a nnf and let # 1 and # 2 be literals in A. If # 1 and # 2
are 0-1-bound, then A is satisfiable if and only if A[# 1 /# 1 /#] is satisfiable. Furthermore,
if I is a model of A[# 1 /# 1 /#], then any extension I # of I such that I # 1 is a model
of A.
Proof: The if part is immediate. For the only if part, let us suppose A is satisfiable.
Let I be a satisfying assignment for A. If there is nothing to prove; so, let us
consider prove that A is also satisfied by an assignment I # such that I # 1
From Remark 1, A can be considered as a formula in the language with the following set
of atoms
that is, in A every leaf is either a formula in S # or a literal # 1
Note that if S 1 then we have that I(S 1
Let I # be the assignment obtained from I by changing the values on # i as follows:
I
4 In this section, when we say an occurrence of #, we mean an unframed occurrence of #.
This assignment satisfies I # (S 1 coincides with I in
the rest of leaves. Therefore I # is a satisfying assignment for A with I # 1
This result is a generalisation of van Gelder's collapsibility lemma, which treats the case
in which all the occurrences of # 1 are bound as # 1 # 2 and # 1
# 2 can be represented by a single literal with # 1 # 2 , see [9] for the details. Our result
drops the requirement that all the occurrences in the defining subset of # 1 and # 2 have to be
children of a # node and the occurrences in the defining subset of {# 1 , # 2 } have to be children
of a # node.
Obviously, the previous result can be straightforwardly extended to the case of n literals
which can be collapsed into one.
Definition 10: Let A be a nnf and let # 1 , . , # n be literals in A, literals # 1 , . , # n are
0-1-bound if the following conditions are satisfied:
1. In
c
there are no occurrences of # 1 , . , # n and if (# c
{1, . , n}, then we have that # i # i# j #.
2. In
c
there are no occurrences of # 1 , . , # n and if (# c
{1, . , n}, then we have that # i # i# j #.
Corollary 5 (Generalised collapsibility) Let A be a nnf, and let # 1 , . , # n be literals 0-
1-bound in A then A is satisfiable i# A[# 1 /# n-1 /# 1 /# n-1 /#] is satisfiable.
Furthermore, if I is a model of A[# 1 /# n-1 /# 1 /# n-1 /#], then any extension I #
of I such that I # j is a model of A.
Example 4: van Gelder's reduction lemmas cannot be applied to the formula in Example 3,
but it is collapsible in the sense of Theorem 7. We had the following
#-sets:
c
c
q-s, 22122),
q-r, 221), ( -
qrs, 222), ( -
q, 22), (-p-q, 2), (s, 3)}
Specifically, p and q are 0-1-bound.
In order to state the generalisation of mixed collapsibility we need the following definition:
Definition 11: Let A be a nnf, b # {0, 1} and let # 1 and # 2 be literals in A. Literal # 1 is
b-bounded to # 2 if the following conditions are satisfied
1. In
c
(A) there are no occurrences (neither framed nor unframed) of either # 1 or # 1 .
2. If (# c
(A), then we have that
. If # 1 #, then # 2 #.
. If # 1 # then # 2 #.
By this definition if # 1 is b-bound to # 2 in a formula A, then every leaf of A belonging to
has an ascendant # in S #
(A).
Theorem 8 (Mixed collapsibility) Let A be a nnf and # 1 , # 2 literals in A,
1. If # 1 is 0-bound to # 2 , and A # is the formula obtained from A by applying the following
substitutions
. If (# c
is substituted in A by # 1 /# 1 /#].
. If (# c
is substituted in A by # 1 /# 1 /#].
then A is satisfiable if and only if A # is satisfiable. In addition, if I is a satisfying
assignment of A # , then any extension I # of I such that I(# 1
assignment for A.
2. If # 1 is 1-bound to # 2 , and A # is the formula obtained from A by applying the following
substitutions
. If (# c
is substituted in A
by #.
then A is satisfiable if and only if A # is satisfiable. In addition, if I is a satisfying
assignment of A # , then any extension I # of I such that I(# 1
assignment for A.
Proof: 1. Note that A can be considered as a formula in the language with set of atoms
that is, in A every leaf is either a formula in S #
(A) or is a literal # 1 , # 1 }.
Let I be a satisfying assignment for A:
1. if we have, by Theorem 2, that
and for every leaf S in S # 1 # 2 ,0
(A) we have, again by Theorem 2,
2. If
(A) we have, by Theorem 2,
Consider the assignment I # , obtained from I by changing only its value on
obviously, we have I(S) # I # (S).
By monotonicity of boolean conjunction and disjunction, we have
I #
Conversely, let I be a satisfying assignment for A # and let I # any extension of I such that
I Theorem 2, for every leaf S in S # 1 # 2 ,0 (A) we have
and for every leaf S in S # 1 # 2 ,0 (A) we have
2. The proof is similar.
Example 5: Following with the formula in Example 2, for the formula B in figure 2, we had
c
c
therefore the first subtree can be pruned, obtaining the tree in Fig. 3.
#(rs, nil )
# (nil, qst )
r s

Figure

3: The tree TC .
variables r and s can be deleted by Theorem 5 of complete reduction (for (rs, #
c
storing the information to be able to generate a model (if it
exists) of the input formula.
In addition, p is 1-bounded to t; therefore, by Theorem 8 of mixed collapsibility, (1) and
(3) can be substituted by # and the information (p = t) is stored.
The resulting formula is q # t, which is finalizable (for # 1 (q # Specifically,
it is satisfiable and a model is
We can deduce that the input formula in Example 2 is non-valid (for its negation is
by collecting the stored information we get the following countermodel
two possibilities:
the information
Splitting a formula
We finish the section by introducing a satisfiability-preserving result which prevents a branching
when suitable hypotheses hold. The splitting, as we call it, results as a consequence of
the following well-known theorem.
Theorem 9 (Quine) A is satisfiable if and only if A[p/# A[p/#] is satisfiable. Further-
more, if I is a model of A[p/#], the extension of I with the assignment is a model
of A; similarly, if I is a model of A[p/#], the extension of I with the assignment
a model of A
If no satisfiable-preserving reduction can be applied to a restricted conjunctive nnf, then
we would have to branch. The following definition states a situation in which the formula has
not to be branched but split.
be a restricted nnf; A is said to be p-splittable if J p #J
where
Corollary 6 Let
be a restricted and p-splittable nnf. Then A is satisfiable if
and only if  V i#Jp A i [p/#  V i#J p
A i [p/#]  is satisfiable. Furthermore, if I is a model of
A i [p/#], then the extension of I with the assignment is a model of A; similarly,
if I is a model of
then the extension of I with the assignment
model of A.
This result can be seen as a generalisation of the Davis-Putnam rule with the following
advantages:
. It is applicable to nnf, not only cnf.
. It can be shifted to non-classical logics.
. Its interactions with the reduction strategies turn out to be extremely e#cient.
The advantage in the use of this transformation is that the problem is not branched but split
in two subproblems where the occurrences of p are substituted by logical constants.
Now, we can describe the algorithm of the prover following the steps we have applied in
the previous examples.
3 The TAS-D algorithm
In this section we describe the algorithm TAS-D and its soundness and completeness are
proved. The flowchart of the algorithm appears in Figure 4; we have to keep in mind that:
. TAS-D determines the (un)satisfiability of the input formula. Therefore, it can be
viewed as a refutational ATP.
. The data flow of the algorithm is a pair (B, M) where B is a nnf, and M is a set of
expressions is a literal not occurring in B.
. The elements in M define a partial interpretation for the input formula, which is used
by CollectInfo, if necessary. This interpretation is defined as follows:
In general, due to the second condition, M might define more than one interpretation,
depending on the choosing of I(# ).
The operators involved in the algorithm are described below, the soundness of each one
follows from the results in previous sections:
The initialisation stage: NNF
The user's input A is translated into nnf by the operator NNF; specifically,
where B is a nnf which is equivalent to A.
A
(B, M)
Reduce
Finalizable?
Root #?
Parallel
Update
SPReduce
SubReduce
QBranch
Unsat.
Model
Satisfiable
#-restrict
-restrict

Figure

4: Flowchart of the TAS-D algorithm.
The Update module
The di#erent stages in the algorithm transform subtrees of the input tree; in each trans-
formation, the labels of the ascendant nodes (of the transformed node) are deleted; Update
processes these trees by recalculating the missing labels and giving as output either a restricted
nnf or a finalizable formula. From another point of view, this stage updates the formula in
the sense that it prunes those subtrees that can be directly deduced to be equivalent either
to #, or #, or a literal.
The #-restrict operator
The input of #-restrict is a pair (B, M), where B is a partially labelled formula, possibly
with logical constants.
Given a nnf B we have that #-restrict(B, M) = (C, M) where C is the #-restricted
formula obtained from B as indicated in Definition 4.
The
#-restrict operator
The input of
#-restrict is a pair (B, M) where B is a #-restricted formula. We have
where C is the restricted formula obtained from B as indicated in Definition 6.
Parallelization
The input of Parallel is a pair (B, M), where B is a restricted formula and
We have
Parallel(
_
Since a disjunction is satisfiable i# some disjunct is satisfiable, each pair independently
passed to Reduce, the following module in the algorithm.
The Reduce module
The input of Reduce is the labelled syntactic tree of a restricted nnf
. In this stage
we decrease, if possible, the size of B before branching, by using the information provided by
the
#-labels and the #-labels. Specifically,
. the
#-labels of the root node allow, using the SPReduce operator, to substitute B by
an equisatisfiable formula in which some propositional variables have been eliminated;
. the #-labels of a proper subtree X allow, using the SubReduce operator, to substitute
the subformula X by an equivalent formula in which the symbols in its #-lists occur
exactly once.
The SPReduce operator
A restricted nnf B is said to be SP-reducible if either it is completely reducible (i.e. there is
an element (# c
or it has
#-pure literals, or it has a pair of 0-1 bound literals, or
it has a literal b-bound to other literal; for these formulas we have
obtained by applying the following items:
1. If (# c
Theorem 5.
2. If # is
#-pure in B, then C is the obtained formula after applying in B the substitutions
in Theorem 6, and M
3. If # and # are 0-1-bound, then C is the obtained formula after applying in B the
substitutions in Theorem 7, and M
4. If # is b-bound to # , then C is the obtained formula after applying in B the substitutions
in Theorem 8, and
The SubReduce operator
The input of SubReduce is a restricted, not SP-reducible nnf A; its e#ect can be described
as an application of Theorem 2 up to associativity and commutativity. The formal definition
needs some extra terminology, included below:
Definition 13: Let a such that is not SP-reducible, and consider
W .
The integers denoted by m(# j ), defined below, are associated to A:
where | - | denotes the cardinality of a finite set.
It is said that A is #-reducible if m(#) > 1 and
associated with A }
Let A be #-reducible and consider is defined as
follows, by application of Theorem 2
A is subreducible if it has a subformula B such that one of the following conditions holds:
.
.
. B is #-reducible for some literal #.
By Theorem 2 we have that the subreduction preserves meaning, therefore
where C is obtained by traversing the tree A depth-first in order to find the first subtree B
indicated above, and
1. Apply Theorem 2, if either
2. Substitute B by B # , otherwise.
The interest of using sub-reductions is that they can make possible further reductions.
It is this use of reductions before branching one of the main novelties of this method with
respect to others; specifically, the unit clause rule of the Davis-Putnam procedure is a special
case of SP reduction; also [9] uses a weak version of our sub-reductions in his dominance
lemma, but he only applies the substitutions to the first level of depth of each subformula.
The Split operator
The input of Split is a pair (B, M) where is a restricted and p-splittable nnf
which is neither SP-reducible nor subreducible; we have
These two tasks are treated independently by the Update process.
Branching: the QBranch operator
The input of QBranch is a pair (B, M) where B is a restricted nnf which is neither SP-
reducible, nor splittable, nor sub-reducible, nnf. We have:
These two tasks are treated independently by the Update process.
Our experimental tests show that the best results are obtained when choosing p as the
propositional variable with more occurrences in the formula being analysed (this information
can be easily obtained from the
#-sets).
Collecting partial results: CollectInfo
The CollectInfo operator collects the outputs of Update for each subproblem generated by
either Parallel, or Split, or QBranch, and finishes the execution of the algorithm:
. If all the outputs of the subproblems are #, then CollectInfo ends the algorithm with
the output Unsatisfiable.
. If some of the subproblems outputs (#, M), then CollectInfo ends the algorithm with
output Satisfiable and a model, which is built from M.
. If some of the subproblems outputs (A, M) satisfying
ends the algorithm with output Satisfiable and a model is built from
where # is the first element of # 1 (A).
3.1 Soundness and completeness of TAS-D
The termination of the algorithm just described is obvious, for each applied process reduces
the size and/or the number of propositional variables of the formula. Specifically, in the
worst case, in which no reduction can be applied, the only applicable process is QBranch
which decreases by one the number of propositional variables in the formula.
Now, we can prove the soundness and completeness of TAS-D.
Theorem 10 TAS-D(A)=Satisfiable if and only if A is satisfiable.
Proof: It su#ces to show that all the processes in the algorithm preserve satisfiability.
Process NNF clearly preserves the meaning, for it is the translation into nnf; all processes in
the modules Update and Reduce preserve either meaning or satisfiability, by the results in
Section 2. To finish the proof, one only has to keep in mind that the subproblem generating
processes (Parallel, Split, QBranch) are based in the following fact: a disjunction is satisfiable
if and only if a disjunct is satisfiable. So, the process CollectInfo preserves satisfiability
as well.
3.2 Some complete examples
Example Consider the formula
The result of Update(NNF(-A)) is = (B, ?), where
#({(pr, #)}, {( pq r , 1), ( pq, 2)} )
Now, as we have
c
reduction can be applied wrt p and as a
consequence we get Update(SPReduce(B, and then the output
is "-A is Unsatisfiable", therefore A is valid.
Example 7: Consider the formula
we have
#(ps, nil )
s q
# (nil, rs )
r s
with
c
c
the reduction module does not apply to this tree, that is, (B, ?) is the input of QBranch. We
apply QBranch wrt variable p and obtain,
The subproblem C 1 is studied below:
After #-restrict we get the following tree
# (nil, rs )
r s
as
For the second subproblem C 2 we have
#(qs, nil )
rs )
r s
for which
c
c
#-restrict's output is fed into SPReduce; the formula can be completely reduced,
for (qs, # c
therefore, by applying substitutions [q/#] and [s/#] and simplifying the
logical constants we get,
which is # 0 -conclusive. Therefore, Update(C 2
As all the subproblems generated by QBranch output #, then CollectInfo produces the
output "-A is Unsatisfiable", therefore A is valid.
Example 8: Let us study the satisfiability of the formula in Example 4:
# (nil, rs )
r s
#(nil, ps )
s q
#(ps, nil )
s
The
c
-sets for the previous formula are the following:
c
c
An application of
#-restrict substitutes (211) and (22121) by #, the result is an
equivalent formula B:
#(nil, rs )
r s
r s q
#(nil, qrs )
#(ps, nil )
s
c
c
Once again, the # in
c
allows to substitute (232) by #, obtaining the equivalent
formula C:
#(nil, rs )
r s
s
c
c
Therefore, Update(A, Now SPReduce can be applied, for literals p and q are
0-1-bound, we substitute all the occurrences of p by #, i.e. #-restrict(SPReduce(C,
(D,
# (nil, rs )
r s
# (nil, rs )
r s
s
c
c
After substituting (311) by # we get :
# (?,{(rs, 1), (qrs, 2), (qs, 3)} )
#(nil, rs )
r s
#(nil, qrs )
In this formula q is 1-bounded to s and, SPReduce substitutes branches at addresses 2 and 3
by #; then
As r # s is finalizable, for its # 1 #= nil, the stage CollectInfo ends the algorithm with
output "A is Satisfiable" and the model determined by
any interpretation I such that is a model of A. Note
that I # defined as I # is also a model of A.
4 A comparative example
To put our method in connection with other existent approaches in the literature, we will
study the collection {T n } of clausal forms taken from [3], we also use their notation for the
propositional variables. Consider, for instance, T 3 below:
each clause contains atoms of the form p i
, where # is a string of +'s and -'s. The superscripts
in each clause always form the sequence 1,2, . , n. The subscript of each literal is exactly
the sequence of signs of the preceding literals in its clause. When T n is built from T n-1 ,
each
is added both positively and negatively. It is easy to see that T n has 2 n
propositional variables, 2 n clauses, each of which contains n literals.
In [3], Cook and Reckhow described the family {T n , n # 1} and showed that the study
of its satisfiability is intractable for analytic tableaux but can be handled in linear time by
resolution. In [7], Murray and Rosenthal showed that dissolution with factoring provides
proofs for this class that are linear in the number of input clauses, |T n |.
When we apply TAS-D to test the satisfiability of T n we get that it is subreducible. For
instance, formula Reduce(T 3 ) can be expressed equivalently as the formula
Thus, #-restrict reduces the previous tree, for there are four # 0 -conclusive subtrees
(namely, the conjunctions p 3
simplifying the four # leaves, we get #. Therefore,
when using TAS-D we can detect the unsatisfiability of the formulas T n with no branching at
all.
Conclusions
We have presented a non-clausal satisfiability tester, named TAS-D, for Classical Propositional
Logic. The main novelty of the method, in di#erence to other approaches, is that
the reductions applied on each formula are dynamically selected, and applied to subformulas
like in a rewrite system, following syntax-directed criteria. Specifically, we have introduced
extensions of the pure literal rule and of the collapsibility theorems. This fact increases the
e#ciency, for it decreases branching.
As an example of the power of TAS-D we have studied a class of formulas which has linear
proofs (in the number of branchings) when either resolution or dissolution with factoring is
applied; on the other hand, when applying our method to these formulas we get proofs without
branching.

Acknowledgments

The authors would like to thank Jos-e Meseguer and Daniele Mundici for their valuable comments
on earlier drafts of this work.



--R

A reduction-based theorem prover for 3-valued logic
Reducing signed propositional logics.
The relative e
Reduction techniques for translating into clause form by using prime implicates.
Implicates and reduction techniques for temporal logics.
Dissolution: Making paths vanish.
On the relative meris of path dissolution and the method of analytic tableaux.
Methods of logic.
A satisfiability tester for non-clausal propositional calculus
--TR
A satisfiability tester for non-clausal propositional calculus
Dissolution
On the relative merits of path dissolution and the method of analytic tableaux
Implicates and Reduction Techniques for Temporal Logics

--CTR
Jun Ma , Wenjiang Li , Da Ruan , Yang Xu, Filter-based resolution principle for lattice-valued propositional logic LP(X), Information Sciences: an International Journal, v.177 n.4, p.1046-1062, February, 2007
P. Cordero , G. Gutirrez , J. Martnez , I. P. De Guzmn, A New Algebraic Tool for Automatic Theorem Provers, Annals of Mathematics and Artificial Intelligence, v.42 n.4, p.369-398, December 2004
P. Cordero , G. Gutirrez , J. Martnez , I. P. De Guzmn, A New Algebraic Tool for Automatic Theorem Provers, Annals of Mathematics and Artificial Intelligence, v.42 n.4, p.369-398, December 2004
SAT problem;prime implicates/implicants;non-clausal theorem proving