Sciweavers

Share
IJCAI
2003

Practical Partition-Based Theorem Proving for Large Knowledge Bases

11 years 1 months ago
Practical Partition-Based Theorem Proving for Large Knowledge Bases
Query answering over commonsense knowledge bases typically employs a first-order logic theorem prover. While first-order inference is intractable in general, provers can often be hand-tuned to answer queries with reasonable performance in practice. Appealing to previous theoretical work on partition-based reasoning, we propose resolutionbased theorem proving strategies that exploit the structure of a KB to improve the efficiency of reasoning. We analyze and experimentally evaluate these strategies with a testbed based on the SNARK theorem prover. Exploiting graph-based partitioning algorithms, we show how to compute a partition-derived ordering for ordered resolution, with good experimental results, offering an automatic alternative to hand-crafted orderings. We further propose a new resolution strategy, MFS resolution, that combines partition-based message passing with focused sublanguage resolution. Our experiments show a significant reduction in the number of resolution steps w...
Bill MacCartney, Sheila A. McIlraith, Eyal Amir, T
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2003
Where IJCAI
Authors Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomás E. Uribe
Comments (0)
books