Complete Pruning Methods and a Practical Search Strategy for SOL Hidetomo Nabeshima Koji Iwanuma University of Yamanashi, Japan University of Yamanashi, Japan Katsumi Inoue National Institute of Informatics, Japan Abstract The ability to find non-trivial consequences of an axiom set is useful in many applications of AI such as theorem proving, query answering and nonmonotonic reasoning. SOL (Skip Ordered Linear) calculus is one of the most significant calculi for consequence finding, which is complete for finding the non-subsumed consequences of a clausal theory. In this paper, we propose new complete pruning methods and a practical search strategy for SOL tableaux. These methods are indispensable for practical use in many application areas. The experimental results show that these techniques improve the performance of consequence finding process greatly. 1 Introduction The task of consequence finding [8] is to discover hidden theorems of a given axiom set. These theorems to be found are not given in an explicit way, but are only characterized by some desired properties. Thus, consequence finding is clearly distinguished from proof finding or theorem proving. One of the most significant calculi for consequence finding is the SOL (Skip Ordered Linear) calculus[1], which is com- plete for finding the non-subsumed consequences of a clausal theory. There are many application areas of SOL calculus such as nonmonotonic reasoning, abduction [1, 2], induction [3], default reasoning [4] and query answering [7, 6]. The original SOL-resolution calculus can be viewed as extending Love- land’s model-elimination calculus [11] with a so-called Skip operation. Iwanuma et al. [5] subsequently reformulated SOL-resolution within the framework of connection tableaux [9, 10] and proposed several pruning methods [5, 6]. In this paper, we propose two kinds of new complete pruning methods for SOL tableau calculus, local failure caching for length condition and skip-minimality. The former is an extension of local failure caching [9, 10, 5] which is an excellent pruning technique for connection tableau calculus. The extension ensures the completeness of the calculus in case we are only interested in consequences up to a given maximal length. A user usually prefers short and simple consequences rather than long and complicated ones. Moreover, limiting the length of consequences has the effect of reducing the search space vastly. In such a situation, our proposed method accelerates the performance of the consequence finding process significantly. The latter method, Skip-minimality, restrains the use of the Skip operation and prunes many redundant SOL derivations. In addition, we describe a new practical search strategy, called consequence iterative lengthening (CIL), which has the effect of finding short and simple consequences preferentially in a limited time. We demonstrate the effectiveness of these methods by the experimental evaluation. The remainder of this paper is organized as follows: Section 2 reviews the SOL tableau calculus. Section 3 and 4 introduces new pruning methods and a search strategy for consequence finding, respec- tively. Section 5 shows the experimental evaluation. Section 6 concludes with a summary and discussion of future work. Rudnicki P, Sutcliffe G., Konev B., Schmidt R., Schulz S. (eds.); Proceedings of the Combined KEAPPA - IWIL Workshops, pp. 113- 122 113 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue 2 SOL Tableaux for Consequence Finding This section reviews the SOL tableau calculus [5]. This paper assumes a first-order language (without equality). We write ⊆ms to denote the inclusion relation over multisets which is defined as usual. When C and D are clauses, C subsumes D if there is a substitution ! such that C! ⊆ms D. We say C properly subsumes D if C subsumes D but D does not subsume C. For a set " of clauses, µ " denotes the set of clauses in " not properly subsumed by any clause in ". Definition 1. A production field P is a pair "L, Cond #, where L is a set of literals closed under instanti- ation, and Cond is a certain condition to be satisfied. If Cond is not specified, P is just denoted as "L #. A clause C belongs to P = "L, Cond # if every literal in C belongs to L and C satisfies Cond. For a set of clauses ", the set of logical consequences of " belonging to P is denoted as ThP ("). A production field P is stable if, for any two clauses C and D such that C subsumes D, the clause D belongs to P only if C belongs to P. Example 1. Let L = L + ∪ L − be the set of all literals in the first-order language, where L+ and L − are the positive and negative literals in the language, respectively. The following are examples of stable production fields. (a) P1 = "L #: ThP1 (") is the set of logical consequences of ". (b) P2 = "L − , length is less than k #: ThP2 (") is the set of negative clauses implied by " consisting of less than k literals. In contrast, P3 = "L, length is greater than k # is not a stable production field. For example, if k = 2 and L = {p(a), q(b), ¬r(c)}, then C = p(a) ∨ q(b) subsumes D = p(a) ∨ q(b) ∨ ¬r(c), and D belongs to P3 while C does not. Note that the empty clause ! is the unique clause in µ ThP (") iff " is unsatisfiable. This means that proof finding is a special case of consequence finding. Stable production fields are practically important [1]. In the condition Cond, we can specify the maximum length of each clause, the maximum term depth of any literal in a clause, and so on. Definition 2. A clausal tableau T is a labeled ordered tree, where every non-root node of T is labeled with a literal. We identify a node with its label (i.e., a literal) if no confusion arises. If the immediate successors of a node are literals L1 , . . . , Ln , then L1 ∨ · · · ∨ Ln is called a tableau clause. The tableau clause below the root is called the start clause. T is a clausal tableau for a set " of clauses if every tableau clause C in T is an instance of a clause D in ". In this case, D is called an origin clause of C. A connection tableau is a clausal tableau such that, for every non-leaf node L except the root, there is an immediate successor labeled with L. A marked tableau T is a clausal tableau such that some leaves are marked with labels closed or skipped. The unmarked leaves are called subgoals. A node N in T is said to be solved if either N itself is a marked leaf node or all leaf nodes of branches through N of T are marked. T is solved if all leaves are marked. skip(T ) denotes the set of literals of nodes marked with skipped. Notice that skip(T ) is a set, not a multiset. skip(T ) is also identified with a clause. We will abbreviate a marked connection tableau as a tableau. Definition 3. A tableau T is regular if no two nodes on any branch in T are labeled with the same literal. T is tautology-free if no tableau clause in T is tautology. T is complement-free if no two non-leaf nodes on any branch in T are labeled with complementary literals. A tableau T is skip-regular if there is no node L in T such that L ∈ skip(T ). T is TCS-free (Tableau Clause Subsumption free) for a clause set " if no tableau clause C in T is subsumed by any clause in " other than the origin clauses. 114 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue Notice that the skip-regularity applies to all over a tableau, so it is effective not only for subgoals but also for non-leaf and solved nodes. Definition 4 (Selection Function [5]). A selection function # is a mapping assigning a subgoal to every tableau that is not solved. # is said to be depth-first if # selects from any tableau T a subgoal with a maximum depth. # is stable under substitution if, for any tableau T and any substitution $ , # (T ) = # (T $ ) holds. Selection functions are assumed to be stable under substitution in this paper. Definition 5 (SOL Tableau Calculus [5]). Let " be a set of clauses, C a clause, P a production field and # a selection functions. An SOL-deduction deriving a clause S from " +C and P via # consists of a sequence of tableaux T0 , T1 , . . . , Tn satisfying that: (i) T0 consists of the start clause C only. All leaf nodes of T0 are unmarked. (ii) Tn is a solved tableau, and skip(Tn ) = S. (iii) For each Ti (i = 0, . . . , n), Ti is regular, tautology-free, complement-free, skip-regular, and TCS-free for " ∪ {C}. (iv) For each Ti (i = 0, . . . , n), the clause skip(Ti ) belongs to P. (v) Ti+1 is constructed from Ti as follows. Select a subgoal K by # , then apply one of the following rules to Ti to obtain Ti+1 : (a) Skip: If skip(Ti ) ∪ {K} belongs to P, then mark K with label skipped. (b) Skip-factoring: If skip(Ti ) contains a literal L, and K and L are unifiable with mgu ! , then mark K with skipped, and apply ! to Ti . (c) Extension: Select a clause B from " ∪ {C} and obtain a variant B( = L1 ∨ · · · ∨ Lm by renaming. If there is a literal Lj such that K and L j are unifiable with mgu ! , then attach new nodes L1 , . . . , Lm to K as the immediate successors. Next, mark Lj with closed and apply ! to the extended tableau. (d) Reduction: If K has an ancestor node L, and K and L are unifiable with mgu ! , then mark K with closed, and apply ! to Ti . Theorem 1 (Soundness and Completeness of SOL [5]). (1) If there is an SOL-deduction of a clause S from " +C and P via # , then S belongs to ThP (" ∪ {C}). (2) If a clause F does not belong to ThP (") but belongs to T hP (" ∪ {C}), then there is an SOL- deduction of a clause S from " +C and P via # such that S subsumes F. Example 2. We define a start clause C, a set " of clauses and a production field P as follows. Let # be a selection function. C = p(X) ∨ s(X), " = { q(X) ∨ ¬p(X), ¬s(Y ), ¬p(Z) ∨ ¬q(Z) ∨ r(Z) }, P = "L + , length is less than 2 #. Figure 1 shows three solved tableaux that are derived by SOL-deductions from " + C and P via # . In the tableau Ta , the node p(X) is skipped since the positive literal p(X) belongs to P, and s(X) 115 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue p(X) s(X) p(X) s(X) skipped ~s(X) q(X) ~p(X) ~s(X) closed skipped closed closed Ta Tb reduction p(X) s(X) q(X) ~p(X) ~s(X) closed closed ~p(X) ~q(X) r(X) closed closed skipped Tc Figure 1: Solved tableaux of Example 2 is extended by using the unit clause ¬s(Y ). Note that s(X) cannot be skipped since the production field P limits the maximum length of consequences to one. The derived consequence is skip(Ta ) = {p(X)}. Tb shows the other derived tableau whose node p(X) is extended by q(X) ∨ ¬p(X), and the node q(X) is skipped. The consequence of Tb is skip(Tb ) = {q(X)}. In Tc , the nodes p(X) and q(X) are extended by q(X) ∨ ¬p(X) and ¬p(Z) ∨ ¬q(Z) ∨ r(Z) respectively. The bottom node ¬p(X) is closed by reduction with the ancestor p(X), and r(X) is skipped. The consequence is skip(Tc ) = {r(X)}. There are some redundant solved tableaux other than Ta , Tb and Tc . The consequences of those are subsumed by p(X), q(X) or r(X)1 . As the results, we can get three new characteristic clauses in this example: Newcarc(",C, P) = {p(X), q(X), r(X)}. 3 Pruning Methods for SOL Tableau Calculus 3.1 Local Failure Caching for Length Condition Local failure caching [9, 10] is an excellent pruning method for refutation finding which can avoid solv- ing repetitiously a subgoal with the same or a more specific substitution. Iwanuma et al. [5] reformulated the local failure caching for consequence finding. This procedure is complete if a production field does not imply a maximum length condition. We review the procedure and then show a counter example. We first define the SOL search tree to explicitly express all possible SOL-deductions. Definition 6. The SOL search tree from " +C and P via # is a tree T labeled with tableaux as follows. We identify a node with its label (i.e., a tableau) if no confusion arises. The root of T is a tableau which consists of the start clause C only. Every non-leaf node T in T has as many successor nodes as there are successful applications of a single inference step applied to the selected subgoal in T by # , and the successor nodes of T are the respective resulting tableaux. A segment of T is a subtree that contains the nodes explored by # from the root to some node. 1 The new pruning method skip-minimality proposed in Section 3.2 can prune such redundant tableaux. 116 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue Definition 7 (Solution and Failure Substitution). Given a SOL search tree T and a depth-first selection function. Let T be a tableau in T and K the selected subgoal in T . 1. If T ( in T is a descendant tableau of T such that all branches through K in T( are solved, then the composition $ = $1 · · · $k of substitutions applied to the tableau T on the way from T to T( is called a solution of K at T via T ( . 2. If T ( is an initial segment of T containing no proof at T( or below it, then the solution $ is named a failure substitution for K at T in T ( . Definition 8 (Local Failure Caching Procedure for Consequence Finding [5]). Let T ( be a finite initial segment of a tableau search tree T . Step 1: Whenever a subgoal K in a tableau T in T ( has been solved via a tableau T( , then the computed solution $ is stored at the node K. a. If T ( cannot be completed to a solved tableau in T ( and the proof procedure backtracks over T ( , then $ is turned into a failure substitution. b. If T ( once has been completed in T ( at a previous stage and the proof procedure back- tracks over T ( for searching alternative consequences, then continue the backtracking, with- out adding $ to the failure substitutions. Step 2: In any alternative solution process of the subgoal K below the search node T , if a substitution % = %1 · · · %m is computed such that one of the failure substitutions stored at the node K is more general than % , then the proof procedure immediately backtracks. Step 3: When the search node T (at which K was selected) is backtracked, then all failure substitutions at K are deleted. We show a counter example for the completeness of the above procedure. Example 3. We define a start clause C = p(X)∨q(X)∨r(X), a set of clauses " = { ¬q(X)∨s(X), ¬s(Y ) }, and a production field P = "L + , length is less than 3 #. We consider finding consequences from this problem. We can apply the Skip operation to p(X) and q(X) in the start clause since they are positive. But we cannot close r(X), because the maximum length of consequences is limited to two (see T1 in Figure 2). In this case, the local failure caching procedure stores an empty failure substitution $ = 0/ at the node q(X). Since 0/ is the most general substitution, all the other applicable operations to q(X) are pruned immediately. As the result, we cannot solve this problem and get any consequences. However, if we do not use the local failure caching, we can obtain the consequence p(X) ∨ r(X) from the solved tableau T2 in Figure 2. Hence, the local failure caching is incomplete if there exists a maximum length condition. The cause of incompleteness is that the procedure does not consider skipped nodes. We extend the definitions of solution and failure substitution, and propose a complete procedure, called local failure caching for length condition. Definition 9 (Extended Solution and Failure Substitution). Given a tableau search tree T and a depth- first selection function. Let T be a tableau in T and K the selected subgoal in T . 1. If T ( in T is a descendant tableau of T such that all branches through K in T( are solved, then the pair "$ , s#, where $ is the composition $ = $1 · · · $k of substitutions applied to the tableau T on the way from T to T ( and s = skip(T ( ), is called an extended solution of K at T via T( . 117 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue T1 T2 p(X) q(X) r(X) p(X) q(X) r(X) skipped skipped skipped skipped fail ~q(X) s(X ) closed ~s(X ) closed Figure 2: A counter example of local failure caching for consequence finding 2. If T ( is an initial segment of T containing no proof at T( or below it, then the extended solution "$ , s# is named an extended failure substitution for K at T in T ( . For two extended failure substitutions "$ , s1 # and "% , s2 #, "$ , s1 # is more general than "% , s2 # if ∃! ($ ! = % ∧ s1 ! ⊆ s2 ), that is, $ is more general than % and s1 subsumes s2 . If P does not have a maximum length condition, then we simply ignore the latter condition, that is, "$ , s1 # is more general than "% , s2 # if ∃! ($ ! = % ). Definition 10 (Local Failure Caching Procedure for Length Condition). The definition is same as Def- inition 8 except for replacing terms of “solution” and “failure substitution” with “extended solution” and “extended failure substitution” respectively. The completeness of the local failure caching for length condition is given by the following proposi- tion. Proposition 1. Let T be a tableau search tree, T a tableau in T , K the selected subgoal in T , and Ta , Tb descendant tableaux of T . Suppose that "$ , s1 # is the extended failure substitution for K at T via Ta , and "% , s2 # is the extended solution of K at T via Tb generated by an alternative process. If Tb has a solved tableau Tbs as a descendant node in T , then "$ , s1 # is not more general than "% , s2 #. Proof. We prove the completeness by a reductio-ad-absurdum. We assume that "$ , s1 # is more general than "% , s2 #, that is, ∃! ($ ! = % ∧ s1 ! ⊆ s2 ). Let Sa and Sbs be the subtableaux with root K in Ta and Tbs respectively (see Figure 3). Then, we replace Sbs in Tbs with Sa ! , and denote the resulting tableau as Tbs( , which is solved and satisfies the maximum length condition. The reason is as follows. Let N be the set of selected subgoals on the way to Tbs after Tb . We extract the set N f of nodes from N which are skipped by the Skip-factoring operation. There might exist the skipped nodes in Nf which have the factoring target in Sbs but not in Sa ! . However, the number of such nodes is at most |s2 \ s1 ! | since s1 ! ⊆ s2 . Therefore, we can apply the Skip operation instead of the Skip-factoring to such nodes. As the results, skip(Tbs( ) satisfies the maximum length condition. This means that if the subtableau Sa was solved with the substitution $ ! instead of $ , then there should exist a solved tableau in T below Ta . Hence, if Sa is solved with the more general substitution $ , then there must be a solved tableau in T below Ta . But this contradicts the assumption of "$ , s1 # being a failure substitution. We consider solving Example 3 by using local failure caching for length condition. Since we cannot close r(X) in T1 , the extended failure substitution "0, / {p(X), q(X)}# is stored to the node q(X). When the alternative process solves q(X) using two extension operations (see T2 in Figure 2), the extended solution substitution "0, / {p(X)}# is stored to q(X). Now, "0, / {p(X), q(X)}# is not more general than "0,/ {p(X)}# 118 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue Ta Tbs Tbs’ K K K failed Sa Sbs solved Saθ solved solved with <σ,s1> solved with <τ,s2> solved with <σθ,s1θ> solved solved Figure 3: Completeness of local failure caching for length condition because {p(X), q(X)} +⊆ {p(X)}. Hence, we can obtain the solved tableau T2 by skipping r(X) and get the consequence p(X) ∨ r(X). Since the Skip operation never instantiates a tableau, local failure caching is significantly effective for the SOL tableau calculus. Moreover, using the maximum length condition is important for finding simple and short consequences in practical time. In such a situation, local failure caching for length condition is an essential technique for practical use. 3.2 Skip-minimality The task of consequence finding is to find all minimal consequences with respect to subsumption. This means that even if we find a solved tableau, we have to continue searching other solved tableaux for finding all minimal consequences. In proof finding, we can halt the computational process immediately if one refutation is found. This is an important difference between consequence finding and proof finding. Of course, if a refutation is found in a consequence finding process, then we can stop the computation immediately since the refutation is the most general consequence. Skip-minimality improves the efficiency of such a consequence enumeration process. This method can prune unsolved tableaux which will generate only non-minimal consequences with respect to sub- sumption by using the consequences derived from already solved tableaux. Definition 11 (Skip-Minimality). Let & be a set of clauses. A tableau T is skip-minimal for & if the clause skip(T ) is not properly subsumed by any clause in &. Suppose that & is a set of consequences derived by some SOL-deductions in a consequence enumer- ation process. If a tableau T is not skip-minimal for &, then T and all its descendant tableaux can be pruned immediately. Skip-minimality is complete since the four kinds of operations in Definition5 never generalize skip(T ). If we find general and short consequences in early stages, then skip-minimality is very effective since it prevents generating many redundant tableaux. 4 Search Strategy Limiting the maximum length of consequences is important. When there is no limit, the branching factor of a SOL search tree increases and the size of the tree grows exponentially. However, it is difficult to know the appropriate length condition in advance. One of the solutions is to execute a search process with incrementing the maximum length limit iteratively, like DFID (depth-first iterative deepening) search strategy. 119 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue We propose the consequence iterative lengthening (CIL) strategy. Let P be a consequence enumer- ation process and l a length limit of consequences (initially l = 0). CIL strategy executes the process P with the length limit l repeatedly, incrementing l for each iteration. If l reaches a given limit or satisfies the condition s < l, then the iteration stops, where s is the maximum number of used Skip operations in every tableau. Since CIL strategy visits the same tableaux in a SOL search tree multiple times, it may seem wasteful. However, it turns out to be not so costly, because the number of tableaux in the SOL search tree increases exponentially in proportion to incrementing the length limit of consequences. We show the property of CIL strategy in Section 5 experimentally. 5 Experimental Results We have implemented skip-minimality, local failure caching for length condition and CIL strategy in SOLAR [12] which is a Java implementation of the SOL tableau calculus. Table 1 shows the experi- mental results for our proposed methods. We used some problems in the TPTP library v2.5.0 [14] as consequence finding problems, which are satisfiable instances (for example, “BOO008-3.p” is the file name of the problem). There are 1,092 satisfiable problems in the library and 24 categories contain such satisfiable instances. We selected 10 categories and chose one satisfiable problem from each category. We defined a production field in each problem as "L , length ≤ x #, where L is the set of all literals and the length condition is given as “len ≤ x” in Table 1. “dep ≤ y” means that we limited the maximum depth of tableaux to y. “sr”, “sm” and “lfc” denote skip-regularity, skip-minimality and local failure caching for length condition respectively. “#C.” and “#Steps” are the number of found consequences and the total number of derived tableaux (that is the number of nodes in a SOL search tree) respectively. The experiments were done on a Core Duo (1.66GHz) machine with 2GB memory. “t.o.” means that the problem could not solve within 600 CPU seconds. Table 1 shows that our proposed pruning methods have a great ability for reducing the search space and improving the speed. In particular, skip-minimality is very effective for solving GRP123-1.005. If we do not use skip-minimality to solve the problem, then we cannot solve the problem within 600 CPU seconds. In MSC009-1 and NLP026-1, local failure caching for length condition shows a high pruning effect. In BOO008-3 and LCL168-1, skip-minimality is not effective because the current implementation of clause-subsumption checking in SOLAR is naive. The improvement of the clause-subsumption check algorithm is one of the important future work. The rightmost row of Table 1 indicates that CIL strategy has almost no overhead. For example, in KRS005-1, CIL executes DFID five times with the maximum length limit of consequences from 0 to 4. However, the number of inferences and execution time are not so different than DFID without CIL. 6 Conclusion and Future Work We have proposed new complete pruning methods and a search strategy for SOL tableau calculus. Local failure caching for length condition and skip-minimality can avoid producing many redundant tableaux. CIL is helpful to a user for finding short and simple consequences preferentially in a limited time. The completeness of local failure caching for length condition supports CIL strategy, and the pruning power of skip-minimality is promoted by CIL since it generates short consequences in early stages. Currently, SOLAR does not have a special mechanism for handling equality. In order to solve a problem with equality efficiently, the development of the complete equality handling mechanism for consequence finding is one of the important future work. 120 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue Table 1: Experimental results Pruning DFID DFID + CIL Problem Params #C Methods #Steps Time [sec] #Steps Time [sec] none 831 308,437 2.3 355,371 2.4 dep ≤ 3 sr 831 303,424 2.3 350,358 2.5 BOO008-3.p sm 831 308,437 7.2 355,371 7.4 len ≤ 5 lfc 831 299,195 2.4 342,711 2.5 all 831 295,944 7.3 339,460 7.7 none - - t.o. - t.o. dep ≤ 5 sr - - t.o. - t.o. GRP123-1.005.p sm 65 822,283 4.5 935,057 4.9 len ≤ 1 lfc - - t.o. - t.o. all 65 784,888 4.8 897,662 5.2 none 4 7,187,849 18.3 7,409,286 18.8 dep ≤ 10 sr 4 4,392,088 11.6 4,571,153 12.1 HWV034-1.p sm 4 6,686,239 17.6 6,907,676 18.1 len ≤ 3 lfc 4 4,733,454 14.2 4,952,443 15.1 all 4 3,112,295 10.6 3,288,912 11.0 none 131 160,767,095 438.5 165,203,316 441.4 dep ≤ 4 sr 131 44,631,879 136.2 46,621,089 136.4 KRS005-1.p sm 131 46,303,085 139.3 47,444,019 141.5 len ≤ 4 lfc 131 106,297,270 319.2 110,027,318 333.5 all 131 8,730,512 36.8 9,166,063 37.9 none 2,091 39,103 33.3 40,752 33.4 dep ≤ 5 sr 2,091 38,615 33.5 40,264 33.6 LCL168-1.p sm 2,091 39,103 35.4 40,752 35.6 len ≤ 1 lfc 2,091 38,629 33.4 40,278 33.8 all 2,091 38,141 35.5 39,790 36.0 none 43 11,160,097 23.4 11,442,019 24.7 dep ≤ 4 sr 43 7,453,146 16.7 7,705,908 17.0 MSC009-1.p sm 43 8,835,505 20.1 9,117,427 20.4 len ≤ 4 lfc 43 4,786,900 12.0 4,915,009 12.2 all 43 1,992,519 6.4 2,107,194 6.7 none 15 129,692,801 301.8 130,198,526 307.0 dep ≤ 5 sr 15 72,182,022 178.0 72,667,948 176.5 NLP026-1.p sm 15 129,025,421 309.8 129,531,146 305.0 len ≤ 2 lfc 15 8,218,827 23.7 8,716,795 25.6 all 15 6,391,292 20.8 6,870,050 22.8 none 26 34,997,018 134.7 39,946,809 145.8 dep ≤ 10 sr 26 14,845,990 59.6 17,823,280 66.4 PUZ001-3.p sm 26 731,711 3.8 1,157,985 5.0 len ≤ 3 lfc 26 33,799,877 143.4 38,495,682 154.7 all 26 458,832 3.2 759,780 4.3 none 3 3,906,678 9.3 3,994,168 9.6 dep ≤ 6 sr 3 1,118,100 3.4 1,158,829 3.5 SET777-1.p sm 3 3,502,145 8.5 3,583,800 8.7 len ≤ 2 lfc 3 2,251,658 7.1 2,302,211 7.3 all 3 656,933 2.8 680,619 2.9 none 5 1,335,866 7.0 1,622,436 8.0 dep ≤ 3 sr 5 1,210,436 6.9 1,486,172 7.8 SYN084-1.p sm 5 328,239 2.5 441,974 2.7 len ≤ 4 lfc 5 1,335,866 7.3 1,621,274 8.2 all 5 285,808 2.4 395,557 2.7 121 Pruning Methods and a Search Strategy for SOL Nabeshima, Iwanuma, Inoue Ray and Inoue [13] have proposed a transformation method for unstable production fields, which converts these into stable ones. This method greatly helps to define a desired production field and to prune an unnecessary search space. References [1] K Inoue. Linear resolution for consequence finding. Artificial Intelligence, 56:301–353, 1992. [2] Katsumi Inoue. Automated abduction. In Antonis C. Kakas and Fariba Sadri, editors, Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II, volume 2408 of Lecture Notes in Computer Science, pages 311–341. Springer, 2002. [3] Katsumi Inoue. Induction as consequence finding. Machine Learning, 55(2):109–135, 2004. [4] Katsumi Inoue, Koji Iwanuma, and Hidetomo Nabeshima. Consequence finding and computing answers with defaults. Journal of Intelligent Information Systems, 26(1):41–58, 2006. [5] K Iwanuma, K Inoue, and K Satoh. Completeness of pruning methods for consequence finding procedure SOL. In Proceedings of FTP-2000, pages 89–100, 2000. [6] Koji Iwanuma and Katsumi Inoue. Conditional answer computation in SOL as speculative computation in multi-agent environments. In Proceedings of the Third International Workshop on Computational Logic in Multi-Agent Systems (CLIMA-02), pages 149–162, 2002. [7] Koji Iwanuma and Katsumi Inoue. Minimal answer computation and SOL. In Proceedings of the Eighth European Conference on Logics in Artificial Intelligence (JELIA 2002), volume 2424 of Lecture Notes in Artificial Intelligence, pages 245–257. Springer, 2002. [8] Char Tung Lee. A completeness theorem and a computer program for finding theorems derivable from given axioms. PhD thesis, Department of Electrical Engineering and Computer Science, University of California, Berkeley, CA, 1967. [9] R. Letz, C. Goller, and K. Mayr. Controlled integration of the cut rule into connection tableau calculi. Journal of Automated Reasoning, 13(3):297–338, 1994. [10] Reinhold Letz. Clausal tableaux. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction - A Basis for Applications, volume I: Foundations, pages 39–68. Kluwer, Dordrecht, 1998. [11] Donald W. Loveland. Automated Theorem Proving: a logical basis. North-Holland Publishing Company, Amsterdam, 1978. [12] Hidetomo Nabeshima, Koji Iwanuma, and Katsumi Inoue. SOLAR: A consequence finding system for ad- vanced reasoning. In Proceedings of Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2003), pages 257–263, 2003. [13] Oliver Ray and Katsumi Inoue. A consequence finding approach for full clausal abduction. In Proceedings of the 10th International Conference on Discovery Science (DS 2007), pages 173–184, 2007. [14] Geoff Sutcliffe and Christian Suttner. The TPTP problem library for automated theorem proving v2.5.0. http://www.tptp.org/, 2002. 122