---
title: "Practical Partition-Based Theorem Proving for Large Knowledge Bases"
authors:
  - "Bill MacCartney"
  - "Sheila A. McIlraith"
  - "Eyal Amir"
  - "Tomás E. Uribe"
doi: ""
url: "https://ijcai.org/proceedings/2003/13"
pdf: "https://ijcai.org/proceedings/2003/0013.pdf"
venue: "Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence"
year: 2003
pages: "89-97"
track: ""
keywords:
---

# Practical Partition-Based Theorem Proving for Large Knowledge Bases

Bill MacCartney, Sheila A. McIlraith, Eyal Amir, Tomás E. Uribe

*Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence*, pages 89-97.

## Abstract

Query answering over commonsense knowledge bases typically employs a first-order logic theorem prover. While first-order inference is intractable in genera l, 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 when this strategy is used. Finally, we augment partition-based message passing, partition-derived ordering, and MFS by combining them with the set-of-support restriction. While these combinations are incomplete, they often produce dramatic improvements in practice. This work presents promising practical techniques for query answering with large and potentially distributed commonsense KBs.