UNSEARCHMO: Eliminating Redundant Search Space on Backtracking for Forward Chaining Theorem Proving

1 Introduction

Automated reasoning is one of the most important topics for artificial intelligence and computer science. Among others, theorem proving technologies for first-order predicate calculus have been attracting much interesting [Robinson, 1965; Loveland, 1968; Manthey and Bry, 1988].

It is well-known that if ✁ ✂ is an unsatisfiable subset of a clause set ✁ , it is generally easier to show ✁ ✂ unsatisfiable than to show ✁ unsatisfiable. Obviously, the smaller such a ✁ ✂ is, the shorter a proof is. If forward chaining is used for reasoning about non-Horn clauses, it means that we need not consider every violated clause, but only those that can help us to find a refutation. It is obvious that invoking unnecessary non-Horn clauses will explode the search space exponentially.

SATCHMO (SATisfiability CHecking by MOdel generation) [Manthey and Bry, 1988] is potentially inefficient, since it uses all violated clauses to forward chaining. Addressing to this problem, two strategies have been developed. One is utilizing an intelligent strategy to only select those relevantlike non-Horn clauses for forward chaining, which is proposed in [Ramsay, 1991], refined in [Loveland et al., 1995] (SATCHMORE) and further improved in [He et al., 1998]

☎ This work is partially supported by the JapaneseMinistry of Education, Science, Sports and Culture and the Artificial Intelligence Research Promotion Foundation of Japan.

(✆ -SATCHMORE). The other method, proposed in [He, 2001] (called I-SATCHMO) is eliminating redundant searching space after unnecessary non-Horn clauses have been used for forward chaining by intelligent backtracking.

As indicated in [He, 2001], there are mainly two problems about the approach to select a suitable non-Horn clause for forward chaining. One is that it takes much overhead cost to decide whether a non-Horn clause is suitable or not. In general, the stricter the checking is, the more expensive the overhead cost is. The other is that any such strategy is only effective in a limited range and certainly fails in some more complicated cases. In fact, a non-Horn clause recognized as "relevant" by some advanced selecting strategy might be practically unnecessary to the refutation being made. In other words, there are always such irrelevant non-Horn clauses that can pass any relevancy test. These problems have been illustrated on some examples in [He, 2001].

The principle of the method of eliminating redundant searching space by intelligent backtracking is very simple: If one of the consequent atoms of a forward chaining clause used for forward chaining is found to be useless to the reasoning on backtracking, the use of this clause is known as unnecessary, and the remaining processing over the clause's consequence is immediately abandoned. It only takes a little overhead cost to find irrelevant non-Horn clauses and is compatible with the former strategy introduced above.

However, marking those consequent atoms contributed to derive antecendents of irrelevant forward chaining clauses as useful and mixing up the useful consequent atoms for different branches in a proof tree, I-SATCHMOmight make redudant search.

This paper introduces a solution for these problems. As we will see, in our improved method, for each node in the proof tree, only those indispensable consequent atoms to derive the refutation at the node are marked as useful. Thus, our method can show a refutation for a given unsatisfiable clause set without UNSEARCHing MOre than necessary (hence the acronym UNSEARCHMO). In other words, our method is one of the most efficient strategies for forward chaining theorem proving.

2 SATCHMO and I-SATCHMO

We assume familiarity with the details relating to SATCHMO [Manthey and Bry, 1988], SATCHMORE [Loveland et al.,

1995] as well as ✆ -SATCHMORE and limit ourselves to briefly ✝ reviewing the basic material needed for our presentation.

In this paper, a problem for checking unsatisfiability is represented by means of positive implicational clauses, each of which has of the form ✞ ✟ ✡ ☞ ☞ ☞ ✡ ✞ ✑ ✓ ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ (✢ ✡ ✤ ✦ ★ ). We refer to the implicit conjunction ✞ ✟ ✡ ☞ ☞ ☞ ✡ ✞ ✑ as the antecedent of the clause, with each ✞ ✩ being an antecedent atom. The implicit disjunction ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ is referred to as the consequent of the clause, and each ✕ ✪ is a consequent atom. A clause with an empty consequent, i.e., ✤ ✬ ★ , is called a negative clause and is written as ✞ ✟ ✡ ☞ ☞ ☞ ✡ ✞ ✑ ✓ ✮ , where ✮ means false. A clause with an empty antecedent, i.e., ✢ ✬ ★ , is written with consequent part only if it is a fact (Horn clause), and otherwise the antecedent atom true is added. Moreover, a given clause set is divided into two subsets. One is ✰ ✱ , the Backward Chaining component that is a decidable Horn clause set consisting of all negative clauses, facts and any Horn clauses selected by user. The other is ✳ ✱ , the Forward Chaining component that contains all the remaining clauses.

If goal ✴ (a conjunction of atoms) can be proven to logically follow the clause set ✁ , we denote that with ✁ ✵ ✴ . On the other hand, if ✷ is a ground atom set and ✞ a ground atom, ✞ ✸ ✷ indicates that atom ✞ is a member of ✷ . Because we utilizes forward chaining on non-Horn clauses same as SATCHMO, all of clauses must hold the so-called rangerestricted property 1 to guarantee the soundness for refutation.

Suppose that ✰ ✱ be a decidable Horn clause set and ✷ a ground atom set, then a conjunction (disjunction) of ground atoms is satisfiable in ✰ ✱ ✻ ✷ if all (some) of its members can be derived from ✰ ✱ ✻ ✷ , and else unsatisfiable. A ground clause ✆ ✓ ✱ is said satisfiable in ✰ ✱ ✻ ✷ if ✱ is satisfiable or ✆ is unsatisfiable in ✰ ✱ ✻ ✷ , and else violated.

It is well-known that a clause set ✁ is satisfiable if and only if we can find a model ❄ for ✁ . If ❄ is a model of ✁ , then each clause of ✁ is satisfiable in ❄ . Based on such consideration, to check whether a given clause set ✁ ✬ ✰ ✱ ✻ ✳ ✱ is satisfiable, SATCHMO goes to construct a model for this clause set by trying to satisfy all clauses in ✁ .

The reasoning made by SATCHMO to search a model for a given clause set ✰ ✱ ✻ ✳ ✱ can be graphically illustrated in a Proof Tree (abbreviated to PT hereafter) described as follows.

For the current node ❇ (initially the root node ❈ ✰ ✱ ❉ ), and the ground consequent atom set ✷ ❊ (initially empty):

1. If ✰ ✱ ✻ ✷ ❊ ✵ ✮ , create a leaf node ✮ below node ❇ . The process for the branch terminates.
2. If ✰ ✱ ✻ ✷ ❊ ❑ ✵ ✮ , select an instantiated ground violated clause ✞ ✟ ✡ ☞ ☞ ☞ ✡ ✞ ✑ ✓ ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ from ✳ ✱ . If no such clause exists, the process terminates to report that ✰ ✱ ✻ ✳ ✱ is satisfiable.

1 A clause is range-restricted iff every variable in its consequent also occurs in its antecedent. An important property of such clauses is that if its antecedent is satisfied by a set of ground atoms, then every consequent atom is certainly ground. As indicated by Manthey and Bry (1988) and Bry and Yahya (2000), any first-order clause set can be transformed into the same "meaning" range-restricted one.

1. For each a consequent atom ✕ ✩ of the selected violated ✳ ✱ clause, create a child node ✕ ✩ below the current node. Taking node ✕ ✩ as new current node, call this procedure recursively in depth-first strategy with the augmented ground consequent atom set ✷ ❫ ❴ , where ✷ ❫ ❴ = ✷ ❊ ✻ ❈ ✕ ✩ ❉ .

For node ❇ , where the ground consequent atom set is ✷ ❊ , if all branches terminate in a leaf node ✮ , it means that satisfying atom ❇ there will lead to a refutation anyway. In other words, ✰ ✱ ✻ ✷ ❊ cannot be extended as a model of ✰ ✱ ✻ ✳ ✱ . Such node is said to be unsatisfiable. When the node is the root node ❈ ✰ ✱ ❉ , then ✰ ✱ ✻ ✳ ✱ is unsatisfiable. Corresponding to creating node ❇ in ❬ ❡ , an atom ❇ is asserted into the reasoning database. On the other hand, when node ❇ is proven to be unsatisfiable, the atom ❇ will be retracted from the database. Moreover, whenever a node is proven unsatisfiable, the reasoning process will backtrack to its parent node if any.

Example 2.1 Consider the following propositional clause set ✁ ✬ ✰ ✱ ✻ ✳ ✱ .

The proof tree generated by SATCHMO is shown in Figure 1. It is obvious that SATCHMOmade some redundant search. In fact, a refutation can be derived from the subset consisting of ✰ ✱ and the only ✳ ✱ clause ❧ ❚ ❳ ♦ ✓ ✤ ✘ ✢ .

By the way, for the given clause set in this example, every violated ✳ ✱ clause used by SATCHMO is recognized as "relevant" by either SATCHMORE or ✆ -SATCHMORE, the proof tree generated by SATCHMORE or ✆ -SATCHMORE is the same as that shown in Figure 1.

The redundant search space can be cut down by intelligent backtracking presented in I-SATCHMO. As we have seen, a consequent atom ❇ is retracted from the reasoning database only if the node ❇ in the proof tree has been proven as unsatisfiable. Suppose that ✆ ✓ ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ be the violated ✳ ✱ clause used for forward chaining at node ❇ in the proof tree, then, node ❇ holds ✤ child nodes ✕ ✟ , ☞ ☞ ☞ , ✕ ✛ . If some consequent atom ✕ ✩ is found to be useless to the reasoning at the time being retracted from the database (hence node ✕ ✩ has been proven as unsatisfiable), i.e., it is useless to construct the partial proof tree below node ✕ ✩ , the same partial proof tree can be directly constructed below node ❇ , and therefore, at this point, we know that node ❇ can be proven as unsatisfiable just in the same way made at node ✕ ✩ . Since ❇ has been known as unsatisfiable, the remaining process for showing node ❇ unsatisfiable, i.e., the process on the consequent atoms ✕ ✩ ⑧ ✟ , ☞ ☞ ☞ , ✕ ✛ (if any), can be removed at once. On the other hand, the use of an ✳ ✱ clause ✆ ✓ ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ is necessary only if each ✕ ✩ ( ❷ ❸ ✕ ✩ ❸ ✤ ) is useful to constructing the partial tree below node ✕ ✩ .

Now we introduce I-SATCHMO how to decide what consequent atom is useful for the reasoning. Obviously, a consequent atom asserted can only be used to derive goal ✮ or antecedents of violated ✳ ✱ clauses. Therefore,I-SATCHMO marks an asserted consequent atom as useful whenever it contributed to derive goal ✮ or an antecedent of a violated ✳ ✱ clause.

The useful consequent atoms to derive goal ✴ can be found from the deriving tree of goal ✴ [He, 2001].

Definition 2.1 Suppose that a give clause set be ✁ ✬ ✰ ✱ ✻ ✳ ✱ , ✷ the current consequent atom set established by forward chaining, ✴ a goal such that ✰ ✱ ✻ ✷ ✵ ✴ . The deriving tree of goal ✴ with respect to ✰ ✱ ✻ ✷ , denoted by ❇ ❭ ❼ ❽ ❿ ➀ ➁ , is the result tree constructed as follows.

1. The root node is ✴ .
2. Suppose that ✞ ✟ ✡ ✞ ➂ ✡ ☞ ☞ ☞ ✡ ✞ ➄ ✡ ✕ ⑦ ✟ ✡ ☞ ☞ ☞ ✡ ✕ ⑦ ✪ is a node in the tree being constructed.
3. ➅ ➆ ➈ For each ✰ ✱ clause ❇ ✟ ✡ ☞ ☞ ☞ ✡ ❇ ➊ ✓ ➋ such that ➋ ➌ ✬ ✞ ✟ ➌ , where ➌ is a most general unifier of ➋ and ✞ ✟ , create a child node ❇ ✟ ➌ ✡ ☞ ☞ ☞ ✡ ❇ ➊ ➌ ✡ ✞ ➂ ➌ ✡ ☞ ☞ ☞ ✡ ✞ ➄ ➌ ✡ ✕ ⑦ ✟ ✡ ☞ ☞ ☞ ✡ ✕ ⑦ ✪ .
4. ➅ ➑ ➈ For each atom ✕ ✸ ✷ such that ✕ ✬ ✞ ✟ ↔ , where ↔ is a ground substitution (since ✕ is a ground atom), create a child node ✞ ➂ ↔ ✡ ☞ ☞ ☞ ✡ ✞ ➄ ↔ , ✕ ⑦ ✟ ✡ ☞ ☞ ☞ ✡ ✕ ⑦ ✪ ✡ ✕ ⑦ ✪ ⑧ ✟ , where ✕ ✪ ⑧ ✟ ✬ ✕ .
5. Repeat this procedure recursively until an empty leaf or a leaf such that all of its atoms hold " a0 " is derived. Such a leaf is called successful deriving leaf.

Since ✰ ✱ is decidable and ✰ ✱ ✻ ✷ ✵ ✴ , ❇ ❭ ❼ ❽ ❿ ➀ ➁ can be finally constructed with finding a successful deriving leaf. The consequent atoms that contributed to derive ✴ from ✰ ✱ ✻ ✷ are those atoms listed in the successful deriving leaf if any.

Example 2.2 Suppose that ✁ ✬ ✰ ✱ ✻ ✳ ✱ be the clause set given in Example 2.1. Consider the leftmost node ✤ in Figure 1, where ✷ ✛ ✬ ❈ ❙ ✡ ❳ ✡ ✤ ❉ . The deriving tree for goal ✮ , ❇ ❭ ❼ ❽ ❿ ➀ ➛ ➜ , is shown in Figure 2. To derive goal ✮ , only ✤ is useful.

The algorithm of I-SATCHMO to construct PT for checking whether a given clause set ✁ ✬ ✰ ✱ ✻ ✳ ✱ is unsatisfiable can be described as follows.

For the current node ❇ (initially the root node ❈ ✰ ✱ ❉ ) and the corresponding consequent atom set ✷ ❊ (initially empty):

1. If ✰ ✱ ✻ ✷ ❊ ✵ ✮ , create a leaf node ✮ under the current node, which means that node ❇ is proven unsatisfiable. Mark all consequent atoms listed in the successful deriving node in ❇ ❭ ❼ ❽ ❿ ➀ ➞ ➜ as useful.
2. If ✰ ✱ ✻ ✷ ❊ ❑ ✵ ✮ , select an instantiated ground violated clause from ✳ ✱ . If no such clause exists, the process terminates to report that ✰ ✱ ✻ ✳ ✱ is not unsatisfiable.
3. For the selected violated non-Horn clause ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ , mark all consequent atoms listed in the successful deriving node in ❇ ❭ ❼ ❽ ❿ ➀ ➞ ➠ as useful. Then, create a node ✕ ✩ below the current node for each ➡ such that ❷ ❸ ➡ ❸ ✤ . Taking ✕ ✩ as the new current node, call this procedure recursively in depth-first strategy with the augmented consequent atomset ✷ ❫ ❴ = ✷ ❊ ✻ ❈ ✕ ✩ ❉ . However, if ✕ ✩ has been found to be useless on backtracking, instead of each node ✕ ✪ such that ➡ ➤ ➥ ❸ ✤ , a special leaf node ➧ is created, where ➧ means that the process from there is pruned away. On the other hand, if all ✕ ✩ are marked as useful, the use of ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ is known as necessary. In either case, node ❇ is proven as unsatisfiable.

Example 2.3 Suppose that ✁ ✬ ✰ ✱ ✻ ✳ ✱ be the clause set given in in Example 2.1.

In the branch ❈ ✰ ✱ ❉ ✓ ❙ ✓ ❳ ✓ ✤ ✓ ✮ in Figure 1, only atom ✤ is used in forward chaining and marked as useful. In the same way, in the branch ❈ ✰ ✱ ❉ ✓ ❙ ✓ ❳ ✓ ✢ ✓ ✮ , only atom ✢ is used in forward chaining and marked as useful.

Since both ✤ and ✢ are proven to be unsatisfiable, its parent node, i.e., ❳ is proven to be unsatisfiable. We backtrack to node ❳ to retract ❳ . At that time, we know ❳ is not marked as useful in the reasoning. Therefore, it is useless for the reasoning and the use of the violated ✳ ✱ clause ❧ ❚ ❳ ♦ ✓ ❳ ✘ ❲ selected at node ❙ is unnecessary. I-SATCHMO prunes away the process to be made on the remaining consequent atom ❲ and backtracks to node ❙ at once.

Now, we know that ❙ is also not marked as useful in the reasoning, therefore the violated ✳ ✱ clause ❧ ❚ ❳ ♦ ✓ ❙ ✘ ❚ selected at the root node ❈ ✰ ✱ ❉ is unnecessary. Accordingly, we stop to process the remaining consequent atom ❚ .

In this way, the proof tree constructed by I-SATCHMO is shown in Figure 3. As we see, unnecessary ✳ ✱ clauses are split only once.

3 UNSEARCHMO

Since I-SATCHMO marks an asserted consequent atom as useful whenever it contributes to derive thea antecendent of a violated ✳ ✱ clause, those consequent atoms contributed to unnecessary violated clauses are also marked as useful.

This problem can be easily solved by improving the marking work as follows: an asserted consequent atom is marked as useful only when it contributes to derive goal ✮ or the antecedent of a violated ✳ ✱ clause that has been verified as necessary.

Moreover, without distinguishing the useful consequent atoms for different branches in proof tree, I-SATCHMO might mismark those consequent atoms that are useful for the refutation of unnecessary branches in a proof tree but useless for the necessary branches as "useful". In such cases, ISATCHMO also possibly makes some redundant search. Let us see the following example.

Example 3.1 Consider the following propositional clause set ✁ ✬ ✰ ✱ ✻ ✳ ✱ .

The proof tree generated by I-SATCHMO is shown in Figure 4.

Consider the leftmost node labeled with ♦ , where ✷ ➭ ✬ ❈ ➆ ✡ ♦ ❉ , the clause ➆ ✡ ♦ ✓ ✤ ✘ ✢ becomes violated and is used to forward chaining. Since both ✤ and ✢ are useful for deriving ✮ , the use of the clause is found to be necessary to the refutation, ➆ and ♦ are marked as useful. In this way, the process for the consequent atom ➨ (the sibling atom of ♦ ) and ➑ (the sibling atom of ➆ ) are made, respectively.

Obviously, the process for node ➑ in the above example is unnecessary. Although the consequent atom ➆ is useful for each branch from node ♦ , it is useless for any branch from node ➨ . It means that the refutation at node ➨ can be made without the consequent atom ➆ , that is, that can be made on the root node ❈ ✰ ✱ ❉ in the sameway. Therefore, the redundant process for the consequent atom ➑ can be eliminated.

Although the process made at the leftmost node ♦ is also unnecessary in a strict meaning, it is unavoidable unless we select atom ➨ first to process at node ➆ or we first select the last non-Horn clause for forward chaining. It is the wellknown nondetermination problem for theorem proving.

Now, we consider how to distinguish and manage the useful consequent atoms for different branches in a proof tree. Without the loss of generality, shown as in Figure 5, suppose that ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ be the violated clause selected at node ❇ and ✁ ❫ ❴ be the useful consequent atom set relative to ✕ ✩ for all ➡ such that ❷ ❸ ➡ ❸ ✤ . We consider how to derive the useful consequent atom set ✁ ❊ relative to node ❇ .

Since our reasoning procedure is depth-first one, ✕ ✩ ⑧ ✟ is not taken into processing until node ✕ ✩ has been proven to be unsatisfiable. Moreover, only when some of ✕ ✩ is found to be useless or all node ✕ ✩ ➅ ❷ ❸ ➡ ❸ ✤ ➈ are proven to be unsatisfiable, their parent node ❇ is proven to be unsatisfiable.

As we will know from the algorithm of UNSEARCHMO, when node ✕ ✩ is proven to be unsatisfiable, the useful consequent atom set ✁ ❫ ❴ for deriving the refutation at node ✕ ✩ has already been established. The useful consequent atom set ✁ ❊ for node ❇ is constructed according to the way how node ❇ is proven as unsatisfiable.

If node ❇ is proven as unsatisfiable in the way that all of ✕ ✩ ➅ ❷ ❸ ➡ ❸ ✤ ➈ are proven as unsatisfiable, then the use of the clause ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ is found to be necessary. In order to complete the refutation at node ❇ , the clause should be ably found to be violated there. Therefore, the useful consequent atoms to derive the antecedent ✆ are useful for our refutation. Moreover, in order to complete the refutation made at each node ✕ ✩ , each useful consequent atom for the refutation made at node ✕ ✩ , except ✕ ✩ itself (since it can be obtained by splitting ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ at node ❇ ), is also needed. Concludingly, in this case, the useful consequent atom set ✁ ❊ can be derived as follows.

where ✁ ➠ is the useful consequent atom set for deriving the antecedent ✆ .

On the other hand, if node ❇ is proven as unsatisfiable in the way that some of ✕ ✩ ➅ ❷ ❸ ➡ ❸ ✤ ➈ is found to be useless, then the use of the clause ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ is found to be unnecessary for the refutation made on node ✕ ✩ , i.e., ✕ ✩ ❑ ✸ ✁ ❫ ❴ . In other words, the refutation found at node ✕ ✩ can also be made at node ❇ without using the clause ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ;✕ ✛ . Thus, the useful consequent atom set ✁ ❊ for deriving a refutation at node ❇ is exactly the same as ✁ ❫ ❴ , i.e.,

In any case, when ✁ ❊ is derived, all of ✁ ❫ ❴ ➅ ❷ ❸ ➡ ❸ ✤ ➈ are remov ➾ ed from database.

Let us make a comparison of I-SATCHMO's method and our new strategy. When node ❇ is proven as unsatisfiable in the way that all of ✕ ✩ are proven as unsatisfiable, the two methods are exactly similar, the useful consequent atom set ✁ ❊ is obtained according to the formula (1). However, when node ❇ is proven as unsatisfiable in the way that node ✕ ✩ is found to be useless, the useful consequent atom set ✁ ❊ derived by I-SATCHMO is as follows.

✁ ❊ ✬ ❈ ✁ ❫ ➳ ➻ ❈ ✕ ✟ ❉ ❉ ✻ ➼ ➼ ➼ ✻ ❈ ✁ ❫ ❴ ➚ ➳ ➻ ❈ ✕ ✩ ➶ ✟ ❉ ❉ ✻ ✁ ❫ ❴ (3) Obviously, although the consequent atoms contained in ❈ ✁ ❫ ➳ ➻ ❈ ✕ ✟ ❉ ❉ , ☞ ☞ ☞ , ❈ ✁ ❫ ❴ ➚ ➳ ➻ ❈ ✕ ✩ ➶ ✟ ❉ ❉ are useful for the branches beginning from ✕ ✟ , ➼ ➼ ➼ , ✕ ✩ ➶ ✟ , but useless for the refutation made at node ✕ ✩ , and therefore is also useless to prove ❇ unsatisfiable.

As we have seen, if a consequent atom, except the last atom of the consequence, of a violated ✳ ✱ clause is found to be useful, then its next sibling atom will be taken into processing. Therefore, the fewer the useful consequent atoms are, the more efficient a refutation is. It is quite clear that the useful consequent atom set for any node derived by our new strategy cannot be reduced any further, i.e., it is a minimal one. Since we can keep a minimal useful consequent atom set for a refutation, our new strategy is one of the most efficient approaches for forward chaining theorem proving.

The algorithm of our prover UNSEARCHMO to construct PT for checking whether a given clause set ✁ ✬ ✰ ✱ ✻ ✳ ✱ is unsatisfiable can be described as follows.

For the current node ❇ (initially the root node ❈ ✰ ✱ ❉ ) and its corresponding consequent atom set ✷ ❊ (initially empty):

1. If ✰ ✱ ✻ ✷ ❊ ✵ ✮ , create a leaf node ✮ below node ❇ , which means node ❇ is proven unsatisfiable. The useful consequent atom set for node ❇ , ✁ ❊ , that consists of those consequent atoms listed in the successful deriving leaf in ❇ ❭ ❼ ❽ ❿ ➀ ➞ ➜ , is established.
2. If ✰ ✱ ✻ ✷ ❊ ❑ ✵ ✮ , select an instantiated ground violated clause ✆ ✓ ✕ ✟ ✘ ☞ ☞ ☞ ✘ ✕ ✛ from ✳ ✱ . If no such clause exists, ✰ ✱ ✻ ✳ ✱ is satisfiable.
3. For the selected violated non-Horn clause ✆ ✓ ✕ ✟ ; ☞ ☞ ☞ ; ✕ ✛ , create a node ✕ ✩ for all ➡ such that ❷ ❸ ➡ ❸ ✤ . Taking ✕ ✩ as the new current node, call this procedure recursively in depth-first strategy with the augmented consequent atom set ✷ ❫ ❴ ✬ ✷ ❊ ✻ ❈ ✕ ✩ ❉ . However, if ✕ ✩ is found to be useless on backtracking, instead of each node ✕ ✪ such that ➡ ➤ ➥ ❸ ✤ , create a special node ➧ . The useful consequent atom set for node ❇ , ✁ ❊ , is established according to the formula (2). On the other hand, if every ✕ ✩ for ❷ ❸ ➡ ❸ ✤ is found to be useful, the useful consequent atom set ✁ ❊ is established according to the formula (1). In either case, node ❇ is proven unsatisfiable.

Example 3.2 Suppose that ✁ ✬ ✰ ✱ ✻ ✳ ✱ be the clause set given in in Example 2.1. The proof tree constructed by UNSEARCHMO is shown in Figure 6. Redundant search space has been eliminated.

The proof of the correctness of our UNSEARCHMO is not difficult. Since UNSEARCHMO just cuts down some branches in the proof tree constructed by SATCHMO, if SATCHMO can show a given clause set unsatisfiable, then UNSEARCHMO can certainly show the same thing. This shows the completeness of UNSEARCHMO.

On the other hand, as we have indicated above, an asserted consequent atom ❇ is found useless at the time being retracted from the reasoning database, its parent node is able to be proven as unsatisfiable. Therefore, all remaining process to show its parent node unsatisfiable can be removed without the loss of the soundness. The further details are omitted here since the lack of space.

It is easy to implement UNSEARCHMO by Prolog. The code is omitted here also because of the lack of space.

4 An Example

Example 4.1 Let ✁ be the following clause set, an extension of the benchmark problem SYN009-1 given in TPTP problem library [Sutcliffe and Suttner, 2000].

The first ✳ ✱ clause will be fully split by any of SATCHMO, SATCHMORE and ✆ -SATCHMORE. That means more than ❒ ➂ ❮ caseswill be considered. As a result, we gave up the our tests on SATCHMO, SATCHMORE and ✆ - SATCHMORE with a run of three days without termination on an Intel PentiumIII/650MHZ workstation, respectively.

Now, we see how I-SATCHMO and UNSEARCHMO work. Initially, the first ✳ ✱ clause is used for forward chaining with each substitution such that its antecedent becomes satisfiable. In this way, a branch ❈ ✰ ✱ ❉ ✓ ❙ ➅ ➆ ✡ ➆ ✡ ➆ ➈ ✓ ❙ ➅ ➆ ✡ ➆ ✡ ➑ ➈ ✓ ❙ ➅ ➆ ✡ ➆ ✡ ❐ ➈ ✓ ➼ ➼ ➼ ✓ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ is generated.

At node ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ , the second ✳ ✱ clause with the substitution ❈ ➷ ✬ ➆ , ➮ ✬ ➆ , ➱ ✬ ➆ ❉ , i.e., ❦ ➅ ➆ ➈ ✡ ❦ ➅ ➆ ➈ ✡ ❦ ➅ ➆ ➈ ✓ ✤ ➅ ➆ ✡ ➆ ✡ ➆ ➈ ✘ ✢ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , is first split. For node ✤ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , ✮ can be derived and the useful consequent atom set is established as ❈ ❙ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , ✤ ➅ ➆ ✡ ➆ ✡ ➆ ➈ ❉ . At node ✢ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , ✮ can not be derived, and the second ✳ ✱ clause with the substitution ❈ ➷ ✬ ➆ , ➮ ✬ ➆ , ➱ ✬ ➑ ❉ , i.e., ❦ ➅ ➆ ➈ ✡ ❦ ➅ ➆ ➈ ✡ ❦ ➅ ➑ ➈ ✓ ✤ ➅ ➆ ✡ ➆ ✡ ➑ ➈ ; ✢ ➅ ➆ ✡ ➆ ✡ ➑ ➈ , is split. At node ✤ ➅ ➆ ✡ ➆ ✡ ➑ ➈ , similar as node ✤ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , ✮ is derived and the useful consequent atom set is ❈ ❙ ➅ ➆ ✡ ➆ ✡ ➑ ➈ , ✤ ➅ ➆ ✡ ➆ ✡ ➑ ➈ ❉ . For node ✢ ➅ ➆ ✡ ➆ ✡ ➑ ➈ , similar as node ✢ ➅ ➆ ✡ ➆ ✡ ➆ ➈ , no refutation can be derived, then the second non-Horn clause will be split with the substitution ❈ ➷ ✬ ➆ , ➮ ✬ ➆ , ➱ ✬ ❐ ❉ , and so on.

The second non-Horn clause will be further split until ❦ ➅ ❐ ➈ ✡ ❦ ➅ ❐ ➈ ✡ ❦ ➅ ❐ ➈ ✓ ✤ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ✘ ✢ ➅ ❐ ✡ ❐ ✡ ❐ ➈ is used for forward chaining at node ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ . Then, at last a refutation can be derived from each of node ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ 's child node simultaneously. The useful consequent atom set for the refutation at node ✤ ➅ ❐ ✡ ❐ ✡ ❐ ➈ is ❈ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ✡ ✤ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ and that at node ✢ ➅ ❐ ✡ ❐ ✡ ❐ ➈ is just ❈ ✢ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ . According to the formula (1), the useful consequent atom set for node ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ is constructed as ❈ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ .

If we do not distinguish the useful consequent atoms for different branches, as I-SATCHMO does, we will find that all ❙ -facts have been marked as useful. Then, the same process made on each ❙ -fact ❙ ➅ a209 ✡ a210 ✡ a211 ➈ , where each of a209 , a210 and a211 is one of ➆ , ➑ and ❐ , would be repeated for the corresponding ✃ -fact ✃ ➅ a209 ✡ a210 ✡ a211 ➈ (also for the corresponding ❚ -fact ❚ ➅ a209 ✡ a210 ✡ a211 ➈ ). Similar to other existing strategies, no answer can be obtained within a reasonable time.

However, at node ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ , where the useful consequent atom set is ❈ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ , UNSEARCHMO finds ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ useless for the refutation, i.e., the clause ❦ ➅ ➑ ➈ ✡ ❦ ➅ ❐ ➈ ✡ ❦ ➅ ❐ ➈ ✓ ✤ ➅ ➑ ✡ ❐ ✡ ❐ ➈ ✘ ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ selected at node ✢ ➅ ➑ ✡ ❐ ✡ ❐ ➈ 's parent ✢ ➅ ➆ ✡ ❐ ✡ ❐ ➈ is not necessary. According to the formula (1), the useful consequent atom set derived at its sibling node ✤ ➅ ➑ ✡ ❐ ✡ ❐ ➈ , i.e., ❈ ❙ ➅ ➑ ✡ ❐ ✡ ❐ ➈ ✡ ✤ ➅ ➑ ✡ ❐ ✡ ❐ ➈ ❉ , is abandoned, and the useful consequent atom set for node ✢ ➅ ➆ ✡ ❐ ✡ ❐ ➈ is still ❈ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ .

Similar backtracking repeatedly continues to node ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ , where the useful consequent atom set established by UNSEARCHMO is still ❈ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ . The same process made on node ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ will be also made on its sibling node ✃ ➅ ❐ ✡ ❐ ✡ ❐ ➈ and node ❚ ➅ ❐ ✡ ❐ ✡ ❐ ➈ , and the corresponding useful consequent atom set are found to be ❈ ✃ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ and ❈ ❚ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ❉ , respectively. The violated clause ❦ ➅ ❐ ➈ ✡ ❦ ➅ ❐ ➈ ✡ ❦ ➅ ❐ ➈ ✓ ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ✘ ✃ ➅ ❐ ✡ ❐ ✡ ❐ ➈ ✘ ❚ ➅ ❐ ✡ ❐ ✡ ❐ ➈ selected at node ❙ ➅ ➑ ✡ ❐ ✡ ❐ ➈ is found to be necessary.

Now, let us see what happens when UNSEARCHMO backtracks to ❙ ➅ ❐ ✡ ❐ ✡ ❐ ➈ 's parent node ❙ ➅ ➑ ✡ ❐ ✡ ❐ ➈ , where, according to the formula (1), useful consequent atom set is surprisedly found to be empty! no other consequent atom is useful for our refutation! UNSEARCHMO simply backtracks to the root node ❈ ✰ ✱ ❉ to conclude that the given clause set is unsatisfiable.

With the help of distinguishing the useful consequent atoms for different branches, UNSEARCHMO only takes 0.002 seconds to find its solution on an Intel PentiumIII/650MHZ workstation.

5 Conclusion

In this paper, we have introduced how to eliminate redundant search space on backtracking for forward chaining theorem proving as much as possible. The redundant search branches are immediately pruned away when unnecessary ones are found on backtracking. At any reasoning point, only those necessary violated clauses are completely split for forward chaining. Repeated search by invoking unnecessary nonHorn clauses can be effectively eliminated. The experimental result has shown that our method is powerful for forward chaining theorem proving.

Since our strategy prunes away unnecessary proof branches after unnecessary non-Horn clauses are used for forward chaining, the violated non-Horn clauses for forward chaining can be used in any order decided by any advance checking strategy. That is, we can incorporate the relevancy checking proposed in SATCHMORE and the availability testing introduced in ✆ -SATCHMORE into our strategies to improve the performance further.

It is obvious that our method can be applied to disjunction logic programming (database). The principle of our method to eliminate redundant search space in forward chaining based prover can also be applied to reason about other logics whenever forward chaining strategy is used. This gives our method a wide application in automated reasoning field.

As future works, we will use our prover to test those benchmark problems provided in TPTP library [Sutcliffe and Suttner, 2000], to clear which class of problems will be helped by our approach.