Partition-Based Logical Reasoning

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:

How can we automatically decompose a large KB into a network of tightly-focused, minimally-connected partitions?
Given a network of (possibly heterogeneous) knowledge systems, how can we achieve efficient global reasoning?

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.

Papers

Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomas Uribe, Practical Partition-Based Theorem Proving for Large Knowledge Bases. Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI-03), August 2003.
Amir, E. and McIlraith, S., Partition-Based Logical Reasoning for First-Order and Propositional Theories, accepted for publication in Artificial Intelligence.
S. McIlraith and E. Amir, Theorem proving with structured theories, 17th Intl' Joint Conference on Artificial Intelligence, 2001 (IJCAI '01). Preliminary versions appeared in LICS Workshop on Theory and Applications of Satisfiability Testing (SAT 2001) and Fifth Symposium on the Logical Formalization of Commonsense Reasoning.
E. Amir and S. McIlraith, Solving Satisfiability using Decomposition and the Most Constrained Subproblem, LICS workshop on Theory and Applications of Satisfiability Testing (SAT 2001), 2001. Proceedings of SAT 2001 appear in Electronic Notes in Discrete Mathematics (Elsevier Science). Also in IJCAI'01 workshop on Distributed Constraint Reasoning
E. Amir, Efficient Approximation for Triangulation of Minimum Treewidth, 17th Conference on Uncertainty in Artificial Intelligence (UAI '01), 2001.
E. Amir and S. McIlraith, Improving the Efficiency of Reasoning Through Structure-Based Reformulation, Proceedings of the 4th Intl' Symposium on Abstraction, Reformulation and Approximation (SARA'00), B.Y. Choueiry and T. Walsh Eds., Lecture Notes in Artificial Intelligence 1864. Springer.
E. Amir and S. McIlraith, Partition-Based Logical Reasoning, 7th International Conference on Principles of Knowledge Representation and Reasoning (KR'2000), 2000.

Presentations

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

Acknowledgements

This work is supported by:

DARPA grant N66001-97-C-8554-P00004 (Richard Fikes PI),
NAVY grant N66001-00-C-8027 (Richard Fikes PI),
AFOSR grant AFF49620-97-1-0207 (John McCarthy PI), and by
DARPA grant N66001-00-C-8018 (RKF program) (John McCarthy PI), through a subcontract to SRI.

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

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