Practical partition-based theorem proving for large knowledge bases
From Semantic Portal Wiki
{{#vardefine:category|Publication}}{{#vardefine:templatename|i.publication}}{{#vardefine:package|smwbp_instance_templates}}
| Edit |
Reference: {{#vardefine:pagename|practical partition-based theorem proving for large knowledge bases }}
- [[]]
bibtex
{{#vardefine:pagename|Practical partition-based theorem proving for large knowledge bases }}{{#vardefine:key| }}
abstract: Query answering over commonsense knowledge bases typically employs afirst-order logic theorem prover. While first-order inference isintractable in general, provers can often be hand-tuned to answer querieswith reasonable performance in practice. Appealing to previous theoreticalwork on partition-based reasoning, we propose resolution-based theoremproving strategies that exploit the structure of a KB to improve theefficiency of reasoning. We analyze and experimentally evaluate thesestrategies with a testbed based on the SNARK theorem prover. Exploitinggraph-based partitioning algorithms, we show how to compute apartition-derived ordering for ordered resolution, with good experimentalresults, offering an automatic alternative to hand-crafted orderings. Wefurther propose a new resolution strategy, MFS resolution, that combinespartition-based message passing with focused sublanguage resolution. Ourexperiments show a significant reduction in the number of resolution stepswhen this strategy is used. Finally, we augment partition-based messagepassing, partition-derived ordering, and MFS by combining them with theset-of-support restriction. While these combinations are incomplete, theyoften produce dramatic improvements in practice. This work presentspromising practical techniques for query answering with large andpotentially distributed commonsense KBs.
download:
- paper:
- slides:
| Abstract | Query answering over commonsense knowledge … Query answering over commonsense knowledge bases typically employs afirst-order logic theorem prover. While first-order inference isintractable in general, provers can often be hand-tuned to answer querieswith reasonable performance in practice. Appealing to previous theoreticalwork on partition-based reasoning, we propose resolution-based theoremproving strategies that exploit the structure of a KB to improve theefficiency of reasoning. We analyze and experimentally evaluate thesestrategies with a testbed based on the SNARK theorem prover. Exploitinggraph-based partitioning algorithms, we show how to compute apartition-derived ordering for ordered resolution, with good experimentalresults, offering an automatic alternative to hand-crafted orderings. Wefurther propose a new resolution strategy, MFS resolution, that combinespartition-based message passing with focused sublanguage resolution. Ourexperiments show a significant reduction in the number of resolution stepswhen this strategy is used. Finally, we augment partition-based messagepassing, partition-derived ordering, and MFS by combining them with theset-of-support restriction. While these combinations are incomplete, theyoften produce dramatic improvements in practice. This work presentspromising practical techniques for query answering with large andpotentially distributed commonsense KBs. ndpotentially distributed commonsense KBs. |
| Author | Bill MacCartney +, Sheila A. McIlraith +, Eyal Amir +, and Tomás E. Uribe + |
| Bibtype | inproceedings + |
| Booktitle | Proceedings of the Nineteenth International Conference on Artificial Intelligence (IJCAI-03) + |
| Key | KSL-03-12 + |
| Month | August + |
| Tag | Computer science + |
| Title | Practical Partition-Based Theorem Proving for Large Knowledge Bases + |
| Tr id | KSL-03-12 + |
| Year | 2003 + |
