The Partition-Based Logical Reasoning Project

KSL's Partition-Based Logical Reasoning Project is aimed at detecting and exploiting the implicit structure of knowledge to make reasoning more focused and efficient. The project is led by Dr. Sheila McIlraith (KSL) and Eyal Amir (now at UC Berkeley). Recent work has been pursued in collaboration with SRI. This project is funded by DARPA's Rapid Knowledge Formation program and ARDA's AQUAINT program.

Research Team

Knowledge Systems Lab Other
Sheila A. McIlraith
Bill MacCartney
Eyal Amir (UC Berkeley)
Tomas Uribe (SRI)

Project overview

There is growing interest in building large knowledge bases (KBs) of everyday knowledge about the world, comprising tens or hundreds of thousands of assertions. But with large KBs, general-purpose reasoners used to answer queries tend to suffer from combinatorial explosion. One promising approach to grappling with the complexity of such KBs is to structure the content into multiple domain- or task-specific partitions. But how are the partitions created, and how do we exploit them in reasoning?

Our research concerns detecting and exploiting the implicit structure of knowledge to make reasoning more focused and efficient. In particular, we investigate how two closely related questions:

Automatic partitioning of large KBs

Our goal is to improve the efficiency of theorem proving in large KBs by identifying and exploiting the implicit structure of the knowledge. Graph-based algorithms are commonly used as a means of exploiting structure to improve the efficiency of reasoning in Bayes Nets, Constraint Satisfaction Problems (CSPs) and most recently in logical reasoning. In all cases, the basic approach is to convert a graphical representation of the problem into a tree-structured representation, where each node in the tree represents a tightly-connected subproblem, and the arcs represent the loose coupling between subproblems.

A first-order or propositional theory is partitioned into tightly coupled subtheories according to the language of the axioms in the theory. This partitioning induces a graphical representation where a node represents a particular partition or subtheory and an arc represents the shared language between subtheories.

Reasoning with partitions using message-passing (MP)

We develop a family of message-passing (MP) algorithms for reasoning with partitions of axioms in propositional logic (PL) and first-order logic (FOL). We analyze the computational benefit of our algorithms and detect those parameters of a partitioning that influence the efficiency of computation.

In the MP algorithm, reasoning is performed locally in each partition, and relevant results are propagated toward the goal partition to provide a global solution. Different (possibly special-purpose) reasoning engines may be used in different partitions. Global soundness and completeness follow from the soundness and completeness of each local reasoner. Performance is shown to be linear in the tree structure, and worst-case exponential within the individual partitions.

To maximize the effectiveness of partition-based reasoning, we must (1) minimize the coupling between partitions, to reduce information being passed between nodes, and (2) minimize local inference within each partition.



Practical Partition-Based Theorem Proving for Large Knowledge Bases [ppt]
Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomas Uribe
18th International Joint Conference on Artificial Intelligence (IJCAI-03), August 2003

Partition-Based Logical Reasoning [ppt, html/ie]
Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomas Uribe
RKF Principal Investigators Meeting, Hilton Head SC, 13-15 November 2002


This work is supported by:

We are grateful for assistance from Mark Stickel and Vinay Chaudhri of SRI.

home | people | software and network services | projects | contact | technical reports | links

Copyright ©2005 Stanford University
All Rights Reserved.

Last modified: Wednesday, 20-Aug-2003 11:34:40 PDT