Practical Partition-Based Theorem Proving for Large Knowledge Bases

1 Introduction

Theorem proving in first-order logic (FOL) is intractable in general. Nevertheless, first-order provers are commonly used for query answering over large knowledge bases (KBs) con­ taining thousands of axioms, such as Cycorp's Cyc and the High Performance Knowledge Base (HPKB) [4]. To make headway in large KBs, theorem provers usually require KB­ specific tuning and customization.

Partition-based reasoning (PBR) [2; 12] promises to speed up reasoning, without manual tuning, by exploiting the struc­ ture implicit in such large commonsense KBs, which typi­ cally contain loosely coupled clusters of domain knowledge.

Eyal Amir

Computer Science Div. University of California Berkeley, CA eyal@cs. berkeley.edu Tomas E. Uribe AI Center SRI International Menlo Park, CA uribe@ai .sri .com

PBR uses graph-based techniques to automatically partition a logical theory into a network of subtheories minimally con­ nected by links of shared vocabulary. Theorem proving is performed locally in each subtheory, and relevant results are propagated between partitions to achieve globally sound and complete collaborative reasoning.

Previous work on PBR has presented a theoretical frame­ work and made claims about the potential for improving the efficiency of reasoning in practice. In this paper we validate these claims empirically, and introduce novel FOL resolution strategies that exploit PBR techniques to improve the effi­ ciency of reasoning.

Outline: In Section 2, we review the theoretical framework of PBR. In Section 3 we explain how a generic theorem prover may be easily augmented with PBR, and describe the experimental testbed we developed using the SNARK theo­ rem prover [18] . Using this testbed, in Section 4 we com­ pare the performance of the PBR message-passing algorithm (MP) to that of popular resolution strategies [3]. MP far out­ performs unrestricted resolution, fares comparably to ordered resolution with a default ordering, and sometimes beats set­ of-support (SOS) resolution.

In Section 5 we show how automatic partitioning [1] can induce a partition-derived ordering (PDO) for use with or­ dered resolution. Ordering can be a highly efficient resolution strategy, but its success has previously depended on hand­ crafted orderings tailored to a specific KB, often through trial and error. Our PDO is competitive with hand-crafted order­ ings and far outperforms SNARK's default ordering. This important result will let future theorem provers incorporate efficient automatic ordering.

In Section 6, we present a novel resolution strategy, MFS resolution, and show it to be sound and complete. MFS combines MP with a focused support restriction employed within partitions. Focused support is a novel resolution re­ striction that is complete for consequence-finding in a speci­ fied sublanguage. In experiments, MFS significantly reduces the number of resolution steps required to answer queries.

Finally, in Section 7 we examine combinations of each of these strategies (MP, PDO, and MFS) with SOS. While these combinations are, in general, incomplete, they perform well in experimental testing. PDO+SOS was found to outperform every other strategy and combination examined, and its theo­ retical incompleteness was never encountered in practice.

This paper introduces novel, easily implemented tech­ niques for improving the efficiency of FOL theorem proving with large structured KBs such as commonsense KBs. It is the first to report experimental results for PBR, and the first to examine combinations ofMP with other strategies in a the­ oretical or experimental setting.

2 Background: partition-based reasoning

The PBR framework has two components: graph-based algo­ rithms for automatic partitioning of a theory, and message­ passing algorithms for reasoning with the partitioned theory. For further details see [2; 12; 1].

2.1 Automatically partitioning a theory

We say that {A h<n is a partitioning of a logical theory A if A = U; A . Each A ; is a set of axioms called a partition, L(A;) is its signature (the set of non-logical symbols), and £(A;) is its language (the set of formulae built with L(A;)). Partitions may share symbols and axioms.

To partition a theory, we first construct a symbols graph from the axioms, where each vertex represents a symbol in the theory, and two vertices are joined by an edge iff the two symbols appear together in an axiom. We then use one of sev­ eral tree decomposition algorithms [16; 1] to generate a tree where each node corresponds to a tightly connected cluster of symbols, defining a partition A; consisting of the axioms in the original theory that contain only those symbols.

The result is a partition graph G : (V, E, l), where vertices correspond to partitions, and edges correspond to communi­ cation links between partitions, labeled with their communi­ cation vocabulary: the labell(i,j) on the edge between A and A 1 is the set of symbols shared by the two partitions, that is, l(i ,j) = L(A)nL(A1) . Efficientpartition-basedreason­ ing depends on finding a tree decomposition that keeps the communication languages small.

Partitioning Algorithms

A tree decomposition is a tree of nodes, where each node is a set of symbols and the tree satisfies the following property: if a symbol appears in two different nodes, then it appears in all the nodes and edges on the path between the two nodes. The width of a tree decomposition is the size (number of sym­ bols) of its largest node (the largest set of symbols in a single node). An optimal tree decomposition is one which has the lowest width among all tree decompositions for the graph. This tree's width is the treewidth of the original graph. Tree decomposition algorithms are commonly used in a variety of AI applications, including constraint satisfaction problems and Bayes Nets.

We have performed experiments with two graph partition­ ing algorithms. The first algorithm is due to [ I6] and is based on an ordering heuristic named min jill. In this heuristic we iterate over the symbols in the symbols graph. At each step, we select a symbol in the graph, add all missing edges be­ tween the symbol's neighbors in the graph, and remove that symbol from the graph. The symbol is selected such that the number of added edges is minimal. The tree decomposition is extracted from this order. The experimental results reported here are based on this partitioning algorithm.

The second algorithm is due to [I] and uses a divide-and­ conquer approach that is guaranteed to approximate the op­ timum decomposition by a factor of at most 0 (log t), where t is the treewidth of the symbols graph. Iteratively, the algo­ rithm finds a vertex cut in the graph (a set of vertices whose removal separates the graph into two or more parts). This ver­ tex cut, W, is sent recursively to each of the separated parts, and subsequent iterations are required to find a vertex cut that separates W in a balanced fashion (here, we may use algo­ rithms such as [II; 9]). The tree decomposition is built from the final parts and the vertex-cuts' vertex sets recursively. In experiments, this algorithm generated partitions somewhat fewer in number and larger in size than the first algorithm, but yielded similar performance in answering queries.

2.2 Reasoning with message passing (MP)

Figure I displays Forward-Message-Passing (MP), a PBR al­ gorithm proposed in [2]. It takes as input a partitioned theory A, an associated partition graph G = (V, E, l), and a query formula Q in L(Ak), and returns YES if the query was en­ tailed by A. MP first directs all edges in the partition graph G toward the goal partition Ak. Since G is a tree, this means each partition (except the goal) will have exactly one "out­ bound link" (leading to the next partition on the path to the goal) and an "outbound link vocabulary" Lout· MP then per­ forms consequence finding independently in each partition, and propagates each derived formula over the outbound link toward the goal iff the formula's signature matches Lout·

This algorithm was shown sound and complete when the partition graph corresponds to a tree decomposition, and the reasoning procedure employed in each partition is sound and complete for £-consequence generation, where £ is the lan­ guage defined by the outbound link vocabulary Lout:

Definition 2.1. Given a target language£, a reasoning pro­ cedure n is complete for £-consequence generation if every formula in £ logically entailed by a set of axioms S is also entailed by the set of consequences in £ that is generated by Rfrom S .

Ordered resolution is an example of a reasoning procedure that satisfies this condition [7].

3 Experimental setup

To evaluate the performance of various PBR strategies, we built an experimental platform around SNARK, a resolution­ based FOL theorem prover developed by Mark Stickel at the SRI AI Center ([18]). Adding PBR capabilities to SNARK was straightforward. Three extensions were required:

• Associate a set of partitions with each clause.
• Restrict resolution to occur only within partitions.
• Ensure appropriate propagation of new clauses to neigh­ boring partitions.

These modifications should be easy to implement in any resolution-based prover.

3.1 Implementing PBR in SNARK

In SNARK, a row is a data structure that stores a clause along with metadata such as the inference method used to derive it. We extend this data structure to include a (non-empty) set of partition IDs indicating the partitions in which the clause resides. A separate data structure holds a description of the partition graph: the partitions, the links that connect them, and the vocabulary for each partition and link.

Resolution is restricted to occur only within partitions: two rows may be resolved only if the intersection of their partition sets is non-empty. The resolvent inherits this intersection as its own partition set, so that it appears in the same partitions as its parents. (This restriction may be superimposed on top of other resolution restrictions, such as set-of-support.)

Finally, to implement message passing between partitions, we examine the vocabulary of every new resolvent. If it matches the outbound link language L out of any partition in its partition set, the partition set is expanded to include the adjacent partition reached by that link.

To generate the initial partitioning, we first load the KB axioms into SNARK and convert them to clausal form. The clauses are passed to an external partitioning tool, which generates the partition graph and defines the vocabulary for each partition and link, according to the particular partition­ ing strategy selected (see Section 2.1 ). The partition graph is essentially static, and can be generated just once for each KB, so that the cost of partitioning is amortized over many queries. However, the links between partitions are reoriented by MP on a per-query basis, to ensure that all communication links lead toward the goal partition.

3.2 Sample KBs, evaluation metrics

The greatest problem we encountered was obtaining large KBs of FOL suitable for use as test data. Test suites for the­ orem provers such as TPTP [19] are biased toward proposi­ tionallogicJPL) or small problems in FOL, while the minor­ ity of test problems containing significant numbers of FOL axioms usually describe an abstract domain and employ only a small number of symbols, making them unsuitable for par­ titioning. The best application of partitioning will be to com­ monsense KBs that contain large numbers of both axioms and symbols. Unlike most mathematical theorem proving prob­ lems, these KBs exhibit structure that can be exploited by partitioning to improve the efficiency of reasoning. However, the few such KBs publically available tend to employ propri­ etary extensions to FOL, making their direct comparison in a common testbed problematic.

In the end, we used a subset of the Cyc KB containing 730 axioms (and 150 symbols) concerning spatial relationships, along with a set of queries supplied by an outside source. We are continuing our efforts to remedy the paucity of ex­ perimental data by adding other large KBs. We are currently testing queries against the Suggested Upper Merged Ontol­ ogy (SUMO) [13] ; experimental results will be reported at the project website 1 .

We collected a variety of statistics on each KB partition­ ing task and each query trial, including runtimes and elapsed times. But we are most interested in metrics that allow us to compare one trial with another by the size of the search space explored. Processor runtime is an imperfect proxy, since it depends greatly on implementation details that are not our primary concern. Thus, in the remainder of this paper, we fo­ cus on number of resolution steps as the best measure of the quantity of work required for each trial.

4 Baseline evaluation of MP

As a starting point for evaluating the effectiveness of MP, we compare it with two common resolution restriction strategies: set-ofsupport (SOS) and ordered resolution. SOS places the negated query into a designated "set of support" and allows only resolutions involving at least one clause from the set of support, to which newly derived clauses are added. In ordered resolution, a global ordering among predicates is given (by the user), and clauses are resolved upon only on their highest literals (in the predicate ordering).

To assess the effectiveness of a resolution strategy, we ex­ amine how much work is required to answer a query using the strategy, relative to using no strategy (that is, allowing any possible resolution). As described in Section 3.2, we use the number of resolution steps as a measure of the work done in answering a query. The absolute number of resolution steps is typically in the thousands, but since this number may vary widely from one query to the next, we must normalize in or­ der to make meaningful comparisons across queries. Thus, for each query and strategy, we report the number of reso­ lution steps required to answer the query as a percent of the number of resolution steps required using no strategy.

Results for a representative selection of queries are shown in the first three histograms of Figure 2. Relative to using no strategy, MP reduces the numbers of steps required to answer most queries by one-third to two-thirds.

However, MP is significantly outperformed by SOS on many queries (though not all). Why? This "vanilla" version of MP operates only at the global level: it restricts resolution between partitions, but allows unrestricted resolution within partitions, equivalent to using no strategy at the local level. In the following sections, we show how to complement MP with smart local strategies for enhanced performance.

The trials for ordered resolution used a default (arbitrary) ordering, so the unimpressive results are no surprise. In Section 5, we introduce a mechanism for automatically inducing efficient orderings from a partition structure.

1http: / /www . ksl.stanford . edu/projects / Partitioning

5 Partition-derived ordering

A major obstacle to the effective use of ordered resolution is finding a good predicate ordering, which will minimize in­ ference. SNARK provides a default ordering, but as we saw in Section 4, it is undistinguished compared to MP and SOS, though better than using no strategy. Efficient ordered reso­ lution is usually achieved by arduous hand-crafting of a pred­ icate ordering by a theorem-proving expert.

In this section, we propose to use automatic partitioning, and in particular PBR tree-decomposition algorithms, to au­ tomatically produce a predicate ordering. This is an impor­ tant contribution as it paves the way to improving theorem­ proving software for ordered resolution, providing more ef­ fective ordered resolution for the non-expert, and relieving the expert from arduous hand-coding of predicate ordering.

Figure 4 describes the P20 algorithm for inducing a sym­ bol ordering from a computed partitioning. It takes as input a partition graph G : (V, E, l) for partitioned theory A: Ui Ai, and a query Q in .C(Ak), and outputs Ord(A), a symbol or­ dering on A. We call this ordering a partition-derived or­ dering. When combined with ordered resolution, we call the strategy PDO. Recall that ordered resolution uses an ordering on predicate symbols, so PDO in fact uses Ord(A) restricted to predicate symbols and ignores the ordering imposed on constant and function symbols.

The underlying intuition is as follows: in MP, we perform resolution and message passing starting with the partitions farthest away from the goal partition. All predicates are re­ solved except those in the outbound link language, which are resolved in the next partition downstream, unless they con­ tinue to appear in subsequent outbound link languages. In this way, the ordering of partitions along paths toward the goal determines an ordering among predicates resolved.

PROCEDURE P20(G, Q)

• G : (V, E , l) is a partition graph for the partitioned theory A : {A;} i$n and Q is a query in L(Ak) (k::::; n).
• I . Define j -< i iff j is on the path between i and kin G.
• Let Lout; = L(l(i,j)) for j such that (i , j) E E andj-< i (there is at most one such j ; ifthere is none, then let Lout . = 0). Lout; is the output language of partition A ;. '
• Let Lin; = UhL(l(h,i)) for h such that (h,i) E E and i -< h (there may be none or multiple such h's). Lin; is the input language of partition A;.
• Initialize Or d(A) =empty list.
• Traverse the tree from furthest leaves to root following-<, in a decreasing order, for every i ::::; n . Ord(A) =
• append(Ord(A) , Lin; \ Lout;, L(A;) \ Lout;) . 6. Ord(A) = append(Ord(A), L(Ak) ,).

Figure 4: An algorithm to compute a predicate ordering.

Theorem 5.1. Let A = U{A}i~n be a partitioning of A based on predicates only (so all function and constant sym­ bols appear in all partitions), let G be a tree decomposition

corresponding to A, and let Q be a query. Then, ordered resolution with order Ord(A) is equivalent to MP, where in­ f erence within each partition uses ordered resolution with an order compatible with Or d(A) .

Proof For every p E L(A) , let P(p) be the -<-smallest parti­ tion, i , such that p E L( i). There is exactly one such partition; otherwise there would be two that are not connected, contra­ dicting the fact that G is a tree decomposition (it guarantees that if a symbol appears in two partitions then it appears on the edges on the path between them).

Define < 0 , an order between symbols, by p < o q iff p precedes q in Ord(A) (equivalently, P(p) -< P(q)). Define <A to be a total order that agrees with < 0 . Let {Pi h <m be an enumeration of the predicate symbols of A according to <A· Notice that if ordered resolution with <A resolved two clauses upon Pi , then Pi is the highest symbol in both clauses.

We show that ordered resolution is equivalent to MP by showing that ordered resolution step can be done by MP, and vice versa. Let C1, C2 be two clauses resolved on p by or­ dered resolution using the order <A· Let i 1 , i 2 be such that C1 is in partition i1 and C2 is in partition i2. Assume that MP cannot resolve the two clauses. That means that they are in different partitions and that at least one of the clauses, say C2 , should be sent to another partition, Aj, with j -< i 2 , in order for the two clauses to be resolved (j is the -<-largest partition such that j -< i1 and j -< i2).

Since C2 was not sent to partition j, its vocabulary is not in the label of one of the edges on the path between i 2 and pin G. Let q be a symbol that appears in C2 but is not on one of the edges in the path between partitions i 2 and j . p is the <A-largest symbol for both c l and C2, meaning that p appears on the path between i 1 , i 2 (thus it also appears on the path between i 2 , j, which is a subset of the path between i1 , i2) and that q <A p (because q does not appear on that path (thus, it is not p) and p is the <A -largest in C2) .

Since q is not in L(j) (otherwise it would be on the path between i2, j) and the path between j , i2 includes p, it must be that P(p) ::5 j, and P(p) ::5 j -< P( q) implies that p <A q. This contradicts the previous observation that q <A p. Thus, q appears on the path between i2' j and c2 must be sent to partition j . The same holds for C1 . Thus, MP will resolve the two clauses.

The other direction (every resolution in MP is a resolu­ tion in ordered resolution) is simpler, and follows from The­ orem 5.2 below. 0

It is interesting to observe that we can, conversely, generate a theory partitioning from a symbol ordering, should one be given by an expert. The algorithm is as follows: Let S be a stack containing the predicate symbols in logical theory A in the designated order Ord(S). Let Z be an empty stack. Pop a symbol s from S. Create a set of symbols that includes s, and all the symbols still in S that appear with s in some axiom in A. If this set of symbols is contained by another set on Z, discard it. Otherwise, push it onto Z. Continue until Sis empty. Then, set G : (V, E) to be an empty graph, and iteratively pop sets of symbols from Z. For a set of symbols Zi , add it to V as a neighbor (in G) to a set of symbols in V with which it shares the largest number of symbols. When Z is empty, create a partition Ai for every set of symbols Zi E V such that Ai includes all the axioms from A that are in .C(Zi)· Call the resulting set of partitions P(Ord(S)), and the graph G(Ord(S)) .

Theorem 5.2. Assume that Ord is an order on the nonlogical symbols of theory A, and that Q is a query such that .C ( Q) are the final symbols in order Or d. Then, ordered resolution with order Ord is equivalent to MP with partitions P(Ord) and graph G( Ord), where inference within each partition uses ordered resolution with an order compatible with Ord(A).

Proof Sketch. To see that MP does not perform more resolu­ tions than ordered resolution with order ~A, we only need to notice that every partition corresponds to a bucket in the ordered resolution algorithm. If MP resolves C 1 , C2 on pred­ icate p' then c 1, c2 were together in some partition j' and were resolved on their highest predicate. Thus, C1 , C2 will also be resolved by ordered resolution with order ~A· D

Proposition 5.3. PDO is sound and complete.

In our experimental evaluation, illustrated in Figure 2, PDO made a strong showing. Its performance was compa­ rable with that of SOS for most queries; for a few queries, PDO was up to two orders of magnitude more efficient than SOS. Unsurprisingly, PDO invariably outperformed ordered resolution with SNARK's default ordering. PDO also outper­ formed vanilla MP, which by itself does not focus reasoning at the local level. When MP is augmented with focused sup­ port (the MFS combination), PDO's comparative advantage largely disappears. In Section 7, we will see that the performance of PDO can be enhanced even further by combining it with other strategies.

6 A new restriction strategy: MFS resolution

MP operates at the global level to focus reasoning by restrict­ ing between-partition resolution and passing relevant results toward the goal partition. However, MP has no impact on local reasoning, that is, reasoning within partitions. In fact, this is one of the strengths of MP: individual partitions may employ heterogeneous reasoning methods, including special­ purpose reasoners optimized for particular domains. (As de­ scribed in Section 2.2, the global soundness and completeness of MP follow from the soundness and completeness of the reasoners used in each partition.) MP can thus be used to or­ chestrate collaborative reasoning between disparate systems, provided that they share a common vocabulary. Neverthe­ less, the absence of a local strategy limits gains in efficiency. In this section we exploit PBR to propose a new restriction strategy, MFS resolution, that combines global MP with a lo­ cal strategy for focused sublanguage resolution.

With vanilla MP, all possible resolutions are performed within a partition, but resolvents can be propagated to other partitions only if they are in the outbound link language. We propose a local resolution strategy,focused support, that takes inspiration from strategies described by Slagle [ 17], SOL re­ striction [8], and SFK-resolution [7].

Definition 6.1 (Focused Support Restriction). Let T be a clausal theory and let L be a designated subset of L(T). Ini­ tialize S to be the set of clauses in T that non-exhaustively include symbols from L. Two clauses may be resolved only if one of them is inS and the resolved predicate is not in L. The

resolvent is added to S.

When focused support is used as a local strategy in PBR, clausal theory T is an individual partition A from a parti­ tioned theory, and L is the output communication language of that partition Ai.

Focused support is sound and complete for generating con­ sequences in the restricted vocabulary of L. The proof relies on the following lemma:

Lemma 6.2 ([17]). If P is an ordering of the predicate sym­ bols in a finite, unsatisfiable set U of clauses and if M is a model, then there is a semantic ?-deduction of the empty clause from U.

Roughly, P-deduction resolves clauses C1 , C2 on predicate R only if C1 satisfies M, C2 does not satisfy M, and R is the largest among the predicates in c2, in some preset order.

Theorem 6.3. Focused support is sound and complete for L­ consequence generation (cj Definition 2.1).

Proof Let A be a clausal theory and D E .C( L) a clause such that A f= D. We show that focused support eventually generates D as a result of A. Assume that A is consistent. Thus, there is a model M that satisfies A. Let S be as in the definition of the focused support strategy for L.

Lemma 6.2 says that there is a ?-resolution of{} from A for the model M and for every ordering P of the predicate symbols. Since everything D resolves with is already in S, we can remove --.D from the resolution graph of this proof and yield D from the ?-deduction of A. This shows that there is a ?-deduction of D from A.

To show that there is a focused support deduction of D from A we still need to show that restricting resolution to occur only on non-L literals does not prevent proving D. Choose P to be an order such that the symbols not in L come before those in L. Sentences that are not in S have no sym­ bols from L. When we resolve sentences from S with those not in S, then clearly the focused support condition holds. We move all the clauses of S that are completely in L(LJ (i.e., have no symbols outside L) into a distinguished set, S. Now, when we resolve two sentences from S, both of them have symbols that are not in L. Those symbols take prece­ dence over the ones from L, so the focused support condition is held. If the resolvent has only literals from L, then we put it inS. Otherwise, we put it inS.

Finally, assume that S ~D. Then, Su{ --.D} is consistent. However, SUS f= D (as shown above with the ?-deduction), so SUS U { --.D} is not consistent. However, for sentences in S, S resolution with our semantic support condition is equiv­ alent to using ordered resolution with the order only specify­ ing that literals in L are resolved after literals not in L. Since this is known to be complete for L-consequence finding [20; 7], we know that Sf= D, and the proof is done. 0

MFS resolution is the combination of MP with the focused support restriction within partitions. As discussed in Section 2.2, MP is sound and complete provided that each partition uses a reasoning procedure that is sound and complete for L-consequence finding. Since focused support is such a pro­ cedure, MFS resolution is also sound and complete:

Corollary 6.4 (Soundness and Completeness of MFS). MP with the focused support restriction (MFS resolution) is sound and complete.

The relative performance of MFS, as depicted in Figure 2, is encouraging. For most queries, the performance of MFS is comparable to that of SOS; and for a minority of queries MFS is one or even two orders of magnitude more efficient.

We also examined the performance ofMFS combined with PDO (MFS+PDO), which was slightly superior to that of MFS alone. However, unlike MFS, MFS+PDO is incom­ plete. Section 7 discusses the incomplete strategy MFS+SOS, which exhibited even better performance.

Theorem 6.5 (Incompleteness of MFS+PDO). PDQ with the focused support restriction (MFS+PDO) is incomplete.

The incompleteness ofMFS+PDO can be seen by noticing that focused support is stricter than each of SOS and semantic resolution. When we add PDO to this restriction, we elim­ inate resolutions with any clause that does not share pred­ icates with the clauses in the negated query. Interestingly, MFS+PDO is very close to being complete, in the following sense. A close examination of the proof of Theorem 6.3 re­ veals that we can apply a predicate order restriction to clauses that do not contain predicates from L and still maintain com­ pleteness for £-consequence finding. Thus, a simple modifi­ cation ofMFS+PDO, allowing clauses in the focused support of a partition to resolve on any non-L literal (without consid­ erations of ordering) is complete.

7 Combinations of strategies

Preceding sections examined three reasoning strategies that are shown to be complete: MP, PDO, and MFS. In this section we examine combinations of these strategies with SOS. Though none of these combinations is complete, they have some interesting theoretical properties, and in practice showed the best performance of all strategies evaluated. Re­ sults of experimental evaluation are summarized in Figure 5.

To combine MP with SOS, we maintain a global set of sup­ port, which initially contains only the negated query, and we allow resolution between two clauses only if they are in the same partition and at least one of them is in the support. Be­ cause messages are sent only toward the goal partition in MP, never away, resolution will occur only in the goal partition unless we place the negated query in every partition whose language includes it. In either case, SOS resolution will oc­ cur in partitions in which the negated query appears.

Clearly, the MP+SOS combination is not complete. Infor­ mation crucial to proving the query may reside in partitions that do not participate in the computation. However, the algo­ rithm determines the clauses that are most relevant to proving the query, in a simple and dynamic way. This sort of infer­ ence is used extensively with large K.Bs, where the selection of the KB fragments needed to answer the query is done by hand. Our automatic selection mechanism may suffice for many applications, and our experiments bear this out.

The argument given for the incompleteness of MP+SOS also shows that PDO+SOS is incomplete. This follows from the relationship between MP and ordered resolution presented in Theorem 5.2. When the PDO predicate ordering is de­ termined by the same partitioning being used in MP, then PDO+SOS restricts resolution to only those clauses that in­ clude predicates that appear in the support. Despite its in­ completeness, PDO+SOS performed extremely well in exper­ imental evaluation. Incompleteness was never encountered in practice, and the PDO+SOS combination answered every query in fewer steps than any other strategy or combination of strategies.

The combination ofMFS with SOS (MFS+SOS) is incom­ plete as well, since MFS is a restricted form of MP, and MP+SOS is incomplete. This incompleteness was revealed in experimental testing, when the MFS+SOS combination failed to answer a few queries. However, when it did not fail, MFS+SOS was highly efficient, answering most queries in as few steps as PDO+SOS.

8 Summary and related work

We propose, analyze, and experimentally evaluate a variety of strategies that improve the efficiency of resolution-based FOL theorem provers. We also propose an algorithm to automat­ ically induce predicate orderings for ordered resolution. Ex­ perimental results confirm significant performance improve­ ments using our techniques. This work makes promising practical contributions to the theorem proving community, presented in a manner designed to facilitate replication. (For software and data, see http: I /www. ksl. stanford . edu/projects/Partitioning.) Our results are par­ ticularly significant for query answering with commonsense K.Bs, whose size, structure, and sometimes distributed nature make them well-suited to our structure-based efficiency im­ provements.

There is a diversity of related work. Our algorithm to in­ duce a predicate ordering is the first to use graphical structure, and in particular treewidth approximation algorithms, with FOL resolution. Current automated approaches to ordering predicates use properties of those predicates, such as their ar­ ity (e.g., the Knuth-Bendix method [10] when applied to a uniform weight function, as in [21 ]), or generate an arbitrary default ordering (e.g., lexical, as in [18]). Our work is most significantly distinguished from work on CSPs (e.g., [6]) and propositional reasoning (e.g., [5; 15]) in that we partition (and subsequently order) a graph that includes all the nonlogical symbols in the theory, whereas propositional methods order nodes in a graph that correspond to propositional symbols and ordering is often dynamic.

Our focused support restriction (on which MFS is based) resembles SFK resolution [7] and SOL resolution [8] in its computation of resolvents in a target language. However, in contrast to SFK resolution, our target language is not closed under subsumption. Further, in [7] there is no clear way to determine a predicate ordering. MFS resolution combines fo­ cused support with predicate ordering imposed by MP, gen­ erating a significant improvement in performance.

Finally, there has been little experimental work studying the behavior of theorem proving strategies on large KBs, and none on commonsense KBs. The success rate of leading theo­ rem provers, such as SPASS, Otter, Setheo, Protein and 3TAP, in formal verification problems with hundreds of axioms, is shown in [14] to depend strongly on how good they are at finding the few relevant axioms needed in the proofs. Our work presents a principled method to successfully elicit such a set of relevant axioms, the PDO+SOS strategy being most notably successful.

In the future, we plan to continue our experimental eval­ uation with additional KBs. We also hope to demonstrate the use of MP for collaborative theorem proving among dis­ tributed KBs and diverse (perhaps special-purpose) reasoners. Finally, we note that PBR naturally enables parallelization of the FOL theorem proving task. The benefits of partition­ driven parallelism can be evaluated with little further imple­ mentation effort.

Acknowledgements

We thank Mark Stickel, Vinay Chaudhri, Adam Pease, and Richard Waldinger for their assistance, feedback and com­ ments. This research was supported in part by DARPA grant N66001-97-C-8554-P00004, NAVY grant N66001-00C-8027, DARPA grant N66001-00-C-8018, ONR MURI Fund N00014-0l-l-0890, ONR MURI Fund N00014-00-l0637, and NSF grant ECS-9873474.