Practical partition-based theorem proving for large knowledge bases

摘要: Query answering over commonsense knowledge bases typically employs a first-order logic theorem prover. While inference is intractable in general, provers can often be hand-tuned to answer queries with reasonable performance practice. Appealing previous theoretical work on partition-based reasoning, we propose resolution-based proving strategies that exploit the structure of KB improve efficiency reasoning. We analyze and experimentally evaluate these testbed based SNARK Exploiting graph-based partitioning algorithms, show how compute partition-derived ordering for ordered resolution, good experimental results, offering an automatic alternative hand-crafted orderings. further new resolution strategy, MFS combines message passing focused sublanguage resolution. Our experiments significant reduction number steps when this strategy used. Finally, augment passing, ordering, by combining them set-of-support restriction. combinations are incomplete, they produce dramatic improvements This presents promising practical techniques query large potentially distributed KBs.