Theorem Proving with Structured Theories

1 Introduction

Theorem provers are becoming increasingly prevalent as query-answering machinery for reasoning over single or multiple large commonsense knowledge bases (KBs) [3]. Commonsense KBs, as exemplified by Cycorp's Cyc and the High Performance Knowledge Base (HPKB) systems developed by Stanford's Knowledge Systems Lab and by SRI often comprise tens/hundreds of thousands of logical axioms, embodying loosely coupled content in a variety of different subject domains. Unlike mathematical theories (the original domain of automated theorem provers), commonsense theories are often highly structured and with large signatures, lending themselves to graph-based techniques for improving the efficiency of reasoning.

Graph-based algorithms are commonly used as a means of exploiting structure to improve the efficiency of reasoning in Bayes Nets (e.g., [18]), Constraint Satisfaction Problems (CSPs) (e.g., [12]) and most recently in logical reasoning (e.g., [11; 3; 25]). In all cases, the basic approach is to convert a graphical representation of the problem into a treestructured representation, where each node in the tree represents a tightly-connected subproblem, and the arcs represent the loose coupling between subproblems. Inference is done locally at each node and the necessary information is propagated between nodes to provide a global solution. Inference thus proves to be linear in the tree structure, and often worstcase exponential within the individual nodes.

∗ Knowledge Systems Laboratory (KSL)

We leverage these ideas to perform more efficient sound and complete theorem proving over theories in first-order logic (FOL) and propositional logic. In this paper we assume that we are given a first-order or propositional theory that is partitioned into subtheories that are minimally coupled, sharing minimal vocabulary. Sometimes this partitioning is provided by the user because the problem requires reasoning over multiple KBs. Other times, a partitioning is induced automatically to improve the efficiency of reasoning. (Some automated techniques for performing this partitioning are discussed in [3; 2].) This partitioning can be depicted as a graph in which each node represents a particular partition or subtheory and each arc represents shared vocabulary between subtheories. Theorem proving is performed locally in each subtheory, and relevant information propagated to ensure sound and complete entailment in the global theory. To maximize the effectiveness of structure-based theorem proving we must 1) minimize the coupling between nodes of the tree to reduce information being passed, and 2) minimize local inference within each node, while, in both cases, preserving global soundness and completeness.

In this paper we present message-passing algorithms that reason over partitioned theories, minimizing the number of messages sent between partitions and the local inference within partitions. We first extend the applicability of a message-passing algorithm presented in [3] to a larger class of local reasoning procedures. In Section 3 we modify this algorithm to use first-order resolution as the local reasoning procedure. In Section 4 we exploit Lyndon's Interpolation Theorem to provide an algorithm that reduces the size of the communication languages connecting partitions by considering the polarity of literals. Finally, in Section 5 we attempt to minimize the reasoning within each partition using algorithms for focused and incremental consequence finding. We also provide an algorithm for compiling partitioned propositional theories into theories in a reduced sublanguage. We have proven the soundness and completeness of all of these algorithms with respect to reasoning procedures that are complete for consequence finding in a specified sublanguage. Proofs omitted from this paper can be found at [22].

2 Partition-Based Logical Reasoning

In this section we describe the basic framework adopted in this paper. We extend it with new soundness and completeness results that will enable us to minimize local inference.

g replacements

Following [3], we say that {Ai}i≤n is a partitioning of a logical theory A if A = ⋃i Ai. Each individual Ai is a set of axioms called a partition, L(Ai) is its signature (the set of non-logical symbols), and L(Ai) is its language (the set of formulae built with L(Ai)). The partitions may share literals and axioms. A partitioning of a theory induces a graphical representation, G = (V,E, l), which we call the theory's intersection graph. Each node of the intersection graph, i, represents an individual partition, Ai, (V = {1, ..., n}), two nodes i, j are linked by an edge if L(Ai) and L(Aj) have a non-logical symbol in common (E = {(i, j) | L(Ai) ∩ L(Aj) ̸= ∅}), and the edges are labeled with the set of symbols that the associated partitions share (l(i, j) = L(Ai) ∩ L(Aj)). We refer to l(i, j) as the communication language between partitions Ai and Aj . We ensure that the intersection graph is connected by adding a minimal number of edges to E with empty labels, l(i, j) = ∅. Figure 1 illustrates a propositional theory A in clausal form (left-hand side) and its partitioning displayed as an intersection graph (right-hand side). (Figures 1, 2 and 3 first appeared in [3].)

Figure 2 displays FORWARD-M-P (FMP), a messagepassing algorithm for partition-based logical reasoning. It takes as input a partitioned theory, A, an associated graph structure G = (V,E, l), and a query formula Q in L(Ak), and returns YES if the query was entailed by A. The algorithm uses procedures that generate consequences (consequence finders) as the local reasoning mechanismwithin each partition or graphical node. It passes a concluded formula to an adjacent node if the formula's signature is in the communication language l of the adjacent node, and that node is on the path to the node containing the query.

Recall, consequence finding (as opposed to proof finding) was defined by Lee [19] to be the problem of finding all nontautological logical consequences of a theory or sentences that subsume them. A prime implicate generator is a popular example of a consequence finder 1 .

To determine the direction in which messages should be sent in the graph G, step 1 in FMP computes a strict partial order over nodes in the graph using the partitioning together with a query, Q.

Definition 2.1 (≺) Given partitioned theory A = ⋃i≤n Ai, associated graph G = (V,E, l) and query Q ∈ L(Ak), let dist(i, j) (i, j ∈ V ) be the length of the shortest path between nodes i, j in G. Then i ≺ j iff dist(i, k) < dist(j, k).

PROCEDURE FORWARD-M-P (FMP)({Ai}i≤n, G, Q)

{Ai}i≤n a partitioning of the theory A, G = (V, E, l) a graph describing the connections between the partitions, Q a query in L(Ak) (k ≤ n).

1. Determine ≺ as in Definition 2.1.
2. Concurrently,
3. (a) Perform consequence finding for each of the partitions Ai, i ≤ n.
4. (b) For every (i, j) ∈ E such that i ≺ j, for every consequence ϕ of Aj found (or ϕ in Aj ), if ϕ ∈ L(l(i, j)), then add ϕ to the set of axioms of Ai.
5. (c) If Q is proven a in Ak, return YES.

a Derive a subsuming formula or initially add ¬Q to Ak and derive inconsistency.

Figure 2: A forward message-passing algorithm.

Figure 3 illustrates an execution of the FMP algorithm using resolution as the consequence finder within a partition. As can be seen from the example, the partitioning reduces the number of possible inference steps by precluding the direct resolution of axioms residing in different partitions. Indeed, [3] showed that partition-based reasoning reduces the search space significantly, as a function of the size of the communication language between partitions.

FMP is sound and complete if we guarantee some properties of the graph G and the consequence finders used for each partition. The graph G is required to be a tree that is properly labeled for A.

Definition 2.2 (Proper Labeling) A tree-structured representation, G = (V,E, l), of a partitioned theory A = {Ai}i≤n is said to have a proper labeling, if for all (i, j) ∈ E and B1, B2, the two subtheories of A on the two sides of the edge (i, j) in G, it is true that l(i, j) ⊇ L(B1) ∩ L(B2).

For example, every intersection graph that is a tree is properly labeled. A simple algorithm called BREAK-CYCLES

1 Recall, an implicate is a clause entailed by a theory. It is prime if it is minimal in some way. Definitions of prime vary including the use of subsumption, syntactic minimality, or entailment.

that transforms an intersection graph that is not tree into a properly labeled tree was presented in [3]. Note that the notion of proper labeling is equivalent, in this context, to the running intersection property used in Bayes Nets.

The consequence finders applied to each partition i are required to be complete for Li-generation for a sublanguage Li ⊂ L(Ai) that depends on the graph G and the query Q.

Definition 2.3 (Completeness for L-Generation) Let A be a set of axioms, L ⊆ L(A) a language, and R a consequence finder. Let CR,L(A) be the consequences of A generated by R that are in L. R is complete for L-generation if for all ϕ ∈ L, if A |= ϕ, then CR,L(A) |= ϕ.

Theorem 2.4 (Soundness and Completeness) Let A be a partitioned theory {Ai}i≤n of arbitrary propositional or first-order formulae, G a tree that is properly labeled with respect to A, and Q ∈ L(Ak), k ≤ n, a query. For all i ≤ n, let Li = L(l(i, j)) for j such that (i, j) ∈ E and j ≺ i (there is only one such j), and let {Ri}i≤n be reasoning procedures associated with partitions {Ai}i≤n. If every Ri is complete for Li-generation then A |= Q iff FMP({Ai}i≤n, G, Q) outputs YES.

This soundness and completeness result improves upon a soundness and completeness result in [3] by allowing consequence finders that focus on consequences in the communication language between partitions. In certain cases, we can restrict consequence finding in FMP even further by using reasoners that are complete for L-consequence finding.

Definition 2.5 (Completeness for L-Consequence Finding) Let A be a set of axioms, L ⊆ L(A) a language, and R a consequence finder. R is complete for L-consequence finding iff for every ϕ ∈ L that is not a tautology, A |= ϕ iff there exists ψ ∈ L such that A ⊢R ψ and ψ subsumes 2ϕ.

2 For clausal theories, we say that clause ψ subsumes ϕ if there is a substitution θ such that ψθ ⊂ ϕ.

Observe that every reasoner that is complete for Lconsequence finding is also complete for L-generation, for any language L that is closed under subsumption [14]. The notion of a consequence finder restricting consequence generation to consequences in a designated sublanguage was discussed by Inoue [17], and further developed by del Val [14] and others. Most results on the completeness of consequence finding exploit resolution-based reasoners, where completeness results for L-consequence finding are generally restricted to a clausal language L. The FMP reasoners in Theorem 2.4 must be complete for Li-generation in arbitrary FOL languages, Li. Corollary 2.6 refines Theorem 2.4 by restricting Ai and Li to propositional clausal languages and requiring reasoners to be complete for Li-consequence finding rather than Li-generation.

Corollary 2.6 (Soundness and Completeness) Let A be a partitioned theory {Ai}i≤n of propositional clauses, G a tree that is properly labeled with respect to A, and Q ∈ L(Ak), k ≤ n, a query. Let Li = L(l(i, j)) for j such that (i, j) ∈ E and j ≺ i (there is only one such j), and let {Ri}i≤n be reasoning procedures associated with partitions {Ai}i≤n. If every Ri is complete for Li-consequence finding then A |= Q iff FMP({Ai}i≤n, G, Q) outputs YES.

In Section 5 we provide examples of reasoners that are complete for L-consequence finding and show how to exploit them to focus reasoning within a partition.

3 Local Inference Using Resolution

In this section, we specialize FMP to resolution-based consequence finders. Resolution [26] is one of the most widely used reasoning methods for automated deduction, and more specifically for consequence finding. It requires the input formula to be in clausal form, i.e., a conjunction of disjunctions of unquantified literals. The resolution rule is complete for consequence finding (e.g., [19; 27]) and so is linear resolution and some of its variants (e.g., [23]).

We present algorithm RESOLUTION-M-P (RES-MP), that uses resolution (or resolution strategies), in Figure 4. The rest of this section is devoted to explaining four different implementations for subroutine RES-SEND(ϕ, j, i), used by this procedure to send appropriate messages between partitions: the first implementation is for clausal propositional theories; the second is for clausal FOL theories, with associated graph G, that is a properly labeled trees and whose labels include all the function and constant symbols of the language; the third is also for clausal FOL theories, however it uses unskolemization and subsequent Skolemization to generate the messages to be passed between partitions; the fourth is a refinement of the third for the same class of theories that avoids unskolemization.

In the propositional case, subroutine RES-SEND(ϕ, j, i) (Implementation 1) simply adds ϕ to Ai, as done in FMP. If the resolution strategies being employed satisfy the conditions of Corollary 2.6, then RES-MP is sound and complete.

In the FOL case, implementing RES-SEND requires more care. To illustrate, consider the case where resolution generates the clause P(B, x) (B a constant symbol and x a variable). It also implicitly proves that ∃b P(b, x). RES-MP

PROCEDURE RESOLUTION-M-P(RES-MP)({Ai}i≤n , G, Q) {Ai}i≤n a partitioned theory, G = (V, E, l) a graph, Q a query formula in the language of L(Ak) (k ≤ n).

1. Determine ≺ as in Definition 2.1.
2. Add the clausal form of ¬Q to Ak.
3. Concurrently,
4. (a) Perform resolution for each of the partitions Ai, i ≤ n.
5. (b) For every (i, j) ∈ E such that i ≺ j, if partition Aj includes the clause ϕ (as input or resolvent) and the predicates of ϕ are in L(l(i, j)), then perform RESSEND(ϕ, j, i).
6. (c) If Q is proven in Ak, return YES.

Figure 4: A resolution forward message-passing algorithm.

may need to send ∃b P(b, x) from one partition to another, but it cannot send P(B, x) if B is not in the communication language between partitions (for ground theories there is no such problem (see [27])). In the first-order case, completeness for consequence finding for a clausal first-order logic language (e.g., Lee's result for resolution) does not guarantee completeness for L-generation for the corresponding full FOL language, L. This problem is also reflected in a slightly different statement of Craig's interpolation theorem [10] that applies for resolution [27].

A simple way of addressing this problem is to add all constant and function symbols to the communication language between every connected set of partitions. This has the advantage of preserving soundness and completeness, and is simple to implement. In this case, subroutine RES-SEND(ϕ, j, i) (Implementation 2) simply adds ϕ to Ai, as done in FMP.

In large systems that consist of many partitions, the addition of so many constant and function symbols to each of the other partitions has the potential to be computationally inefficient, leading to many unnecessary and irrelevant deduction steps. Arguably, a more compelling way of addressing the problems associated with resolution for first-order theories is to infer the existential formula ∃b P (b, x) from P (B, x), send this formula to the proper partition and Skolemize it there. For example, if ϕ = P(f(g(B)), x) is the clause that RESSEND gets, replacing it with ∃b P(b, x) eliminates unnecessary work of the receiving partition.

The process of conservatively replacing function and constant symbols by existentially quantified variables is called unskolemization or reverse Skolemization and is discussed in [5; 9; 8]. [8] presents an algorithmU that is complete for our purposes and generalizes and simplifies an algorithm of [9]. (Space precludes inclusion of the algorithm.)

Theorem 3.1 ([8]) Let V be a vocabulary and ϕ, ψ be formulae such that ψ ∈ L(V ) and ϕ ⇒ ψ. There exists F ∈ L(V ) that is generated by algorithm U such that F ⇒ ψ.

Thus, for every resolution strategy that is complete for Lconsequence finding, unskolemizing ϕ using procedure U for V = l(i, j) and then Skolemizing the result gives us a combined procedure for message generation that is complete for Lj-generation. This procedure can then be used readily in RES-MP (or in FMP), upholding the soundness and completeness to that supplied by Theorem 2.4. The subroutine RES-SEND(ϕ, j, i) that implements this approach is presented in Figure 5. It replaces ϕ with a a set of formulae in L(l(i, j)) that follows from ϕ. It then Skolemizes the resulting formulae for inclusion in Ai.

PROCEDURE RES-SEND(ϕ, j, i)

(Implementation 3)

ϕ a formula, j, i ≤ n.

1. Unskolemize ϕ into a set of formulae, Φ in L(l(i, j)), treating every symbol of L(ϕ) \ l(i, j) as a Skolem symbol.
2. For every ϕ2 ∈ Φ, if ϕ2 is not subsumed by a clause that is in Ai, then add the Skolemized version of ϕ2 to the set of axioms of Ai.

Figure 5: Subroutine RES-SEND using unskolemization.

Procedure U may generate more than one formula for any given clause ϕ. For example, if ϕ = P(x, f(x), u, g(u)), for l(i, j) = {P}, then we must generate both ∀x∃y∀u∃vP (x, y, u, v) and ∀u∃v∀x∃yP (x, y, u, v) (ϕ entails both quantified formulae, and there is no one quantified formula that entails both of them). In our case we can avoid some of these quantified formulae by replacing the unskolemize and then Skolemize process of RES-SEND (Implementation 3) with a procedure that produces a set of formulae directly (Implementation 4). It is presented in Figure 6.

PROCEDURE RES-SEND(ϕ, j, i)

(Implementation 4)

ϕ a formula, j, i ≤ n.

1. Set S ←L(ϕ) \ l(i, j).
2. For every term instance, t = f(t1, ..., tk), in ϕ, if f ∈ S and t is not a subexpression of another term t′ = f ′ (t′1, ..., t′k′) of ϕ with f ′ ∈ S, then replace t with "x ← t" for some new variable, x (if k = 0, t is a constant symbol).
3. Nondeterministically a , for every pair of marked arguments "x ← α", "y ← β", in ϕ, if α, β are unifiable, then unify all occurrences of x, y (i.e., unify αi, βi for all markings x ← αi, y ← βi).
4. For every marked argument "x←α" in ϕ, do
5. (a) Collect all marked arguments with the same variable on the left-hand side of the "←" sign. Suppose these are x ← α1, ..., x ← αl .
6. (b) Let y1, ..., yr be all the variables occurring in α1, ..., αl. For every i ≤ l, replace "x ← αi" with f(y1, ..., yr) in ϕ, for a fresh function symbol f (if r = 0, f is a fresh constant symbol).
7. Add ϕ to Ai.

a Nondeterministically select the set of pairs for which to unify all occurrences of x, y.

Figure 6: Subroutine RES-SEND without unskolemization.

Steps 2-3 of procedure RES-SEND(ϕ, j, i) (Implementation 4) correspond to similar steps in procedure U presented in [8], simplifying where appropriate for our setup. Our procedure differs from unskolemizing procedures in step 4, where it stops short of replacing the Skolem functions and constants with new existentially quantified variables. Instead, it replaces them with new functions and constant symbols. The nondeterminism of step 3 is used to add all the possible combinations of unified terms, which is required to ensure completeness.

For example, if ϕ = P(f(g(B)), x) and l(i, j) = {P}, then RES-SEND adds P(A, x) to Ai, for a new constant symbol, A. If ϕ = P(x, f(x), u, g(u)), for l(i, j) = {P}, then RES-SEND adds P(x, h1(x), u, h2(u)) to Ai, for new function symbols h1, h2. Finally, if ϕ = P(x, f(x), u, f(g(u))), then RES-SEND adds P (x, f (x), u, h(u)) and P (h1(u), h2(u), u, h2(u)) to Ai, for h, h1, h2 new function symbols.

Theorem 3.2 (Soundness & Completeness of RES-MP)

Let A be the partitioned theory ⋃i≤n Ai of propositional or first-order clauses, G a tree that is properly labeled with respect to A, and Q ∈ L(Ak) k ≤ n, a sentence that is the query. A |= Q iff applying RES-MP({Ai}i≤n, G, Q) (with Implementation 4 of RES-SEND) outputs YES.

PROOF SKETCH Soundness and completeness of the algorithm follow from that of FMP, if we show that RES-SEND (Implementation 4) adds enough sentences (implying completeness) to Ai that are implied by ϕ (thus sound) in the restricted language L(l(i, j)).

If we add all sentences ϕ that are submitted to RES-SEND to Ai without any translation, then our soundness and completeness result for FMP applies (this is the case where we add all the constant and function symbols to all l(i, j)).

We use Theorem 3.1 to prove that we add enough sentences to Ai. Let ϕ2 be a quantified formula that is the result of applying algorithm U to ϕ. Then, ϕ2 results from a clause C generated in step 4 of algorithm U (respectively, Step 3 in RES-SEND). In algorithm U, for each variable x, the markings "x ← αi" in C are converted to a new variable that is existentially quantified immediately to the right of the quantification of the variables y1, ..., yr. ϕ2 is a result of ordering the quantifiers in a consistent manner to this rule (this process is done in steps 5-6 of algorithmU).

Step 4 of RES-SEND performs the same kind of replacement that algorithmU performs, but uses new function symbols instead of new quantified variables. Since each new quantified variable in ϕ2 is to the right of the variables on which it depends, and our new function uses exactly those variables as arguments, then Step 4 generates a clause C ′ from C that entails ϕ2. Thus, the clauses added to Ai by RES-SEND entail all the clauses generated by unskolemizing ϕ using U. From Theorem 3.1, these clauses entail all the sentences in L(l(i, j)) that are implied by ϕ.

To see that the result is still sound, notice that the set of clauses that we add to Ai has the same consequences as ϕ in L(l(i, j)) (i.e., if we add those clauses to Aj we get a conservative extension of Aj ).

Resolution strategies that can be readily used in RES-MP, while preserving completeness, include linear resolution [23], directional resolution [25] and lock resolution [7]. Strategies such as set-of-support and semantic resolution can be used with somewhat different treatments.

4 Minimizing Node Coupling Using Polarity

FMP and RES-MP use the communication language to determine relevant inference steps between formulae in connected partitions. This section improves the efficiency of FMP and RES-MP by exploiting the polarity of predicates in our partitions to further constrain the communication language between partitions. This leads to a reduction in the number of messages that are passed between adjacent partitions, and thus a reduction in the search space size of the global reasoning problem. Our results are predicated on Lyndon's Interpolation Theorem [20], an extension to Craig's Theorem [10].

Theorem 4.1 (Lyndon's Interpolation Theorem) Let α, β be sentences such that α ⊢ β. Then there exists a sentence γ such that α ⊢ γ and γ ⊢ β, and that every relation symbol that appears positively [negatively] in γ appears positively [negatively] in both α and β. γ is referred to as the interpolant of α and β.

This theorem guarantees that FMP need only send clauses with literals that may be used in subsequent inference steps. For example, let {A1, A2} be a partitioned theory, G = (V = {1, 2}, E={(1, 2)}, l) be a graph, and Q ∈ L(A2), be a query. If FMP concluded P from A1, and P does not show positively in A2 ⇒ Q (i.e., P does not show negatively in A2 and does not show positively in Q), then there is no need to send the message P fromA1 to A2.

Procedure POLARIZE (Figure 7) takes as input a partitioned theory, associated tree G = (V,E, l), and a query Q. It returns a new graph G′ = (V,E, l′ ) that is minimal with respect to our interpretation of Lyndon's Interpolation Theorem. The labels of the graph now include predicate/propositional symbols with associated polarities (the same symbol may appear both positively and negatively on an edge label). All function and object symbols that appeared in l also appear in l ′ for the respective edges.

Theorem 4.2 (Soundness and Completeness) Let A be a partitioned theory {Ai}i≤n of arbitrary propositional or first-order formulae, G a tree that is properly labeled with respect to A, and Q ∈ L(Ak), k ≤ n, a query. Let G′ be the result of running POLARIZE({Ai}i≤n, G, Q). Let Li = L(l(i, j)) for j such that (i, j) ∈ E and j ≺ i (there is only one such j), and let {Ri}i≤n be reasoning procedures associated with partitions {Ai}i≤n. If every Ri is complete for Li-generation then A |= ϕ iff FMP({Ai}i≤n, G′ ,Q) outputs YES.

Darwiche [11] proposed a more restricted use of polarity in graph-based algorithms for propositional SAT-search. His proposal is equivalent to first finding those propositional symbols that appear with a unique polarity throughout the theory and then assigning them the appropriate truth value. In contrast, our proposed exploitation of polarity is useful for both propositional and first-order theories, it is more effective in constraining inference steps, and is applicable to a broader class of message-passing algorithms problems. In particular,

PROCEDURE POLARIZE({Ai}i≤n, G, Q)

{Ai}i≤n a partitioning of the theory A, G = (V, E, l) a tree and Q a query formula in L(Ak) (k ≤ n).

1. For every i, j ∈ V , set l′ (i, j) to be the set of object and function symbols that appear in l(i, j), if there are any.
2. Rewrite {Ai}i≤n such that all negations appear in front of literals (i.e., in negation normal form).
3. Determine ≺ as in Definition 2.1.
4. For all (i, j) ∈ E such that i ≺ j, for every predicate symbol P ∈ l(i, j),
5. (a) Let V1, V2 be the two sets of vertices in V separated by i in G, with j ∈ V1.
6. (b) If [¬]P appears in V1 then, if [¬]P appears in Q or ¬[¬]P appears in Am, for some m ∈ V2, then add [¬]P to l′ (i, j).
7. Return G′ = (V,E, l′ ).

Figure 7: Constraining the communication language of {Ai}i≤n by exploiting polarity.

our method is useful in cases where symbols appear with different polarities in different partitions.

5 Minimizing Local Inference

To maximize the effectiveness of structure-based theorem proving, we must minimize local inference within each node of our tree-structured problem representation, while preserving global soundness and completeness. First-order and propositional consequence finding algorithms have been developed that limit deduction steps to those leading to interesting consequences, skipping deduction steps that do not.

In the propositional case, the most popular algorithms are certain L-(prime) implicate finders. (See [21] for an excellent survey.) SOL-resolution (skipping ordered linear resolution) [17] and SFK-resolution (skip-filtered, kernel resolution) [14] are two first-order resolution-based L-consequence finders. SFK-resolution is complete for first-order L-consequence finding, reducing to Directional Resolution in the propositional case [13]. In contrast, SOL-resolution is not complete for first-order L-consequence finding, but is complete for first-order incremental L-consequence finding. Given new input Φ, an incremental L-consequence finder finds the consequences of A∪Φ that were not entailed by Φ alone. Defining completeness for incremental L-consequence finding is analogous to Definition 2.5.

In the rest of this section, we propose strategies that exploit our graphical models and specialized consequence finding algorithms to improve the efficiency of reasoning. Following the results in previous sections, using SFK-resolution as a reasoner within partitions will preserve the soundness and completeness of the global problem while significantly reducing the number of inference steps. SFK-resolution can be used by all of the procedures below. Unless otherwise noted, the algorithms we describe are limited to propositional theories because first-order consequence finders may fail to terminate, even for decidable cases of FOL.

The first strategy is compilation. Figure 8 provides an algorithm, COMPILE({Ai}i≤n, G), that takes as input a partitioned theory {Ai}i≤n and associated tree G, that is properly labeled, and outputs a compiled partitioned theory {A′i}i≤n. Each new partition is composed of the logical consequences of partition Ai that are in the language Lcommi , all the communication languages associated with Ai. Prime implicate finders have commonly been used for knowledge compilation, particularly in propositional cases. SFK-resolution can be used as the sound and complete L-consequence finder in Step 2 of COMPILE.

Knowledge compilation can often create a large theory. Each partition produced by COMPILE({Ai}i≤n, G) will be of worst case size of O(2|L(Lcommi )| ) clauses. Since our assumption is that partitions are produced to minimize communication between partitions, | L(Lcommi ) | should be much smaller than | L(Ai) |. As a consequence, we might expect the compiled theory to be smaller than the original theory, though this is not guaranteed. Under the further assumption that the theories in partitions are fairly static, the cost of compilation will be amortized over many queries. We discuss further options for compilation, including the use of partial compilation, in a longer paper.

PROCEDURE COMPILE({Ai}i≤n, G)

{Ai}i≤n a partitioning of the theory A, G = (V, E, l) a tree with proper labeling for A. For each partition Ai, For i = 1, . . . , n,

1. Let Lcommi = L(⋃(i,j)∈E l(i, j))
2. Using a sound and complete L-consequence finder, perform Lcommi -consequence finding on each partition Ai , placing the output in a new partition A′i.

Figure 8: A partition-based theory compilation algorithm.

Proposition 5.1 Let A = ⋃i≤n Ai be a partitioned theory with associated tree G that is properly labeled for A. Let Lcommi = L(⋃(i,j)∈E l(i, j))). For all ϕ ∈ Li ⊆ Lcommi ⊆ L(Ai), Ai |= ϕ iff A′i |= ϕ, where {A′i}i≤n are the compiled partitions output by COMPILE({Ai}i≤n, G).

We may use our compiled theories in several different strategies for batch-style and concurrent theorem proving, as well as in our previous message-passing algorithms. Figure 9 presents an algorithm for batch-style structure-based theorem proving. BATCH-MP takes as input a (possibly compiled) partitioned theory, associated tree G that is properly labeled, and query Q. For each partition in order, it exploits focused L-consequence finding to compute all the relevant consequences of that theory. It passes the conclusions towards the partition with the query. This algorithm is very similar to the bucket elimination algorithm of [13]. BATCH-MP preserves soundness and completeness of the global problem, while exploiting focused search within each partition.

Theorem 5.2 (Soundness and Completeness) Let A be a set of clauses in propositional logic. Let {Ri}i≤n be the Li-consequence finders associated with partitions {Ai}i≤n

PROCEDURE BATCH-MP ({Ai}i≤n, G, Q)

{Ai}i≤n a (compiled) partitioning of the theory A, G = (V, E, l) a properly labeled tree describing the connections between the partitions, Q a query in L(Ak) (k ≤ n).

1. If {Ai}i≤n, is a compiled theory, replace partition Ak with the partition Ak from the uncompiled theory.
2. Determine ≺ as in Definition 2.1.
3. Let Li = L(l(i, j)) for j such that (i, j) ∈ E and j ≺ ia .
4. Following ≺ in a decreasing order, for every (i, j) ∈ E such
5. that j ≺ ia , Run the Li-consequence finder on Ai until it has exhausted its consequences, and add the consequences in Li to Aj .
6. If Q is proven b in Ak, return YES.
7. a There is only one such j.

b Derive a subsuming formula or initially add ¬Q to Ak and derive inconsistency.

Figure 9: A batch-style message-passing algorithm.

in step 4 of BATCH-MP ({Ai}i≤n,G,Q). If every Ri is complete for Li-consequence finding then A |= Q iff applying BATCH-MP({Ai}i≤n,G,Q) outputs YES.

Our final algorithm, CONCURRENT-MP, (Figure 10), takes as input a (possibly compiled) partitioned theory, associated tree G that is properly labeled, and query Q. It exploits incremental L-consequence finding in the output communication language of each partition to compute the relevant incremental consequences of that theory, and then passes them towards the partition with the query. Once again, SFK-resolution can be used as the sound and complete Lconsequence generator for the preprocessing (Step 4). In the case where the theory is compiled into propositional prime implicates, the consequences in Li may simply be picked out of the existing consequences in Ai. SOL-resolution can be used as the sound and complete incremental L-consequence finder (Step 6a). CONCURRENT-MP preserves soundness and completeness of the global problem in the propositional case, while exploiting focused search within each partition.

Theorem 5.3 (Soundness and Completeness) Let A be a set of clauses in propositional logic. Let {Ri}i≤n be the Li-consequence finders associated with partitions {Ai}i≤n in step 4 of CONCURRENT-MP({Ai}i≤n,G,Q) and let {R′i}i≤n be the incremental Li-consequence finders associated with partitions {Ai}i≤n in step 6 of CONCURRENTMP({Ai}i≤n,G,Q). If every Ri is complete for Liconsequence finding, and every R′i is complete for incremental Li-consequence finding then A |= Q iff applying CONCURRENT-MP({Ai}i≤n,G,Q) outputs YES.

6 RelatedWork

A number of AI reasoning systems exploit some type of structure to improve the efficiency of reasoning. While our exploitation of graph-based techniques is similar to that used in Bayes Nets (e.g., [18]) our work is distinguished in that we PROCEDURE CONCURRENT-MP ({Ai}i≤n, G, Q)

{Ai}i≤n a (compiled) partitioning of the theory A, G = (V, E, l) a properly labeled tree describing the connections between the partitions, Q a query in L(Ak) (k ≤ n).

1. Determine ≺ as in Definition 2.1.
2. Let Li = L(l(i, j)) for j such that (i, j) ∈ E and j ≺ ia .
3. If {Ai}i≤n, is a compiled theory, then replace partition Ak with the partition Ak from the uncompiled theory.
4. For every i ≤ n, run the Li-consequence finder on partition Ai until it has exhausted its consequences.
5. For every (i, j) ∈ E such that j ≺ ia , add the Li-prime implicates to partition Aj .
6. Concurrently,
7. (a) For every (i, j) ∈ E such that j ≺ ia , perform incremental Li-consequence finding for each of the partition Ai and add the the consequences in Li to Aj .
8. (b) If Q is proven b in Ak, return YES.
9. a There is only one such j.

b Derive a subsuming formula or initially add ¬Q to Ak and derive inconsistency.

Figure 10: A concurrent message-passing algorithm.

reason with logical rather than probabilistic theories, where notions of structure and independence take on different roles in reasoning. Our work is most significantly distinguished fromwork on CSPs (e.g., [12]) and more recently, logical reasoning (e.g., [11; 25]) in that we reason with explicitly partitioned theories using message passing algorithms and our algorithms apply to FOL as well as propositional theories.

In the area of FOL theorem proving, our work is related to research on parallel theorem proving (see surveys in [6; 15]) and on combining logical systems (e.g., [24; 4]). Most parallel theorem prover implementations are guided by lookahead and subgoals to decompose the search space dynamically or allow messages to be sent between different provers working in parallel, using heuristics to decide on which messages are relevant to each prover. These approaches typically look at decompositions into very few sub-problems. In addition, the first approach typically requires complete independence of the sub-spaces or the search is repeated on much of the space by several reasoners. In the second approach there is no clear methodology for deciding what messages should be sent and from which partition to which.

The work on combining logical systems focuses on combinations of signature-disjoint theories (allowing the queries to include symbols from all signatures) and decision procedures suitable for those theories. All approaches either nondeterministically instantiate the (newly created) variables connecting the theories or restrict the theories to be convex (disjunctions are intuitionistic) and have information flowing back and forth between the theories. In contrast, we focus on the structure of interactions between theories with signatures that share symbols and the efficiency of reasoning with consequence finders and theorem provers. We do not have any restrictions on the language besides finiteness.

Work on formalizing and reasoning with context (see [1] for a survey) can be related to theorem proving with structured theories by viewing the contextual theories as interacting sets of theories. Unfortunately, to introduce explicit contexts, a language that is more expressive than FOL is needed. Consequently, a number of researchers have focused on context for propositional logic, while much of the reasoning work has focused on proof checking (e.g., GETFOL [16]).

7 Summary

In this paper we exploited graph-based techniques to improve the efficiency of theorem proving for structured theories. Theories were organized into subtheories that were minimally connected by the literals they share. We presented message-passing algorithms that reason over these theories using consequence finding, specializing our algorithms for the case of first-order resolution, and for batch and concurrent theorem proving. We provided an algorithm that restricts the interaction between subtheories by exploiting the polarity of literals. We attempted to minimize the reasoning within each individual partition by exploiting existing algorithms for focused incremental and general consequence finding. Finally, we proposed an algorithm that compiles each subtheory into one in a reduced sublanguage. We have proven the soundness and completeness of all of these algorithms. The results presented in this paper contribute towards addressing the problem of reasoning efficiently with large or multiple structured commonsense theories.

Acknowledgements

We wish to thank the anonymous IJCAI reviewers for their thorough review of this paper, and Alvaro del Val and Pierre Marquis for helpful comments on the relationship between our work and previous work on consequence finding. This research was supported in part by DARPA grant N6600197-C-8554-P00004, NAVY grant N66001-00-C-8027, and by DARPA grant N66001-00-C-8018 (RKF program).