KSL-01-04 + redirect page
Theorem Proving with Structed Theories (Full Report) + Has identifier
Theorem Proving with Structed Theories (Full Report) + Ksl tr id
Theorem Proving with Structed Theories (Full Report) + Number
| Theorem Proving with Structed Theories (Full Report) |
Bibtype
techreport
Has publishing details
April,2001
Has title
Theorem Proving with Structed Theories (Full Report)
Has where published
KSL-01-04
Has year
2001
Title
Theorem Proving with Structed Theories (Full Report)
Year
2001
Abstract
Motivated by the problem of query answerin … Motivated by the problem of query answering over multiple structured commonsense theories, we exploit graph-based techniques to improve the efficiency of theorem proving for structured theories. Theories are organized into subtheories that are minimally connected by the literals they share. We present message-passing algorithms that reason over these theories using consequence finding, specializing our algorithms for the case of first-order resolution, and for batch and concurrent theorem proving. We provide an algorithm that restricts the interaction between subtheories by exploiting the polarity of literals. We attempt to minimize the reasoning within each individual partition by exploiting existing algorithms for focused incremental and general consequence finding. Finally, we propose an algorithm that compiles each subtheory into one in a reduced sublanguage. We have proven the soundness and completeness of all of these algorithms. d completeness of all of these algorithms.
Author
Sheila A. McIlraith and Eyal Amir +
Has author
Sheila A. McIlraith and Eyal Amir +
Has identifier
Theorem Proving with Structed Theories (Full Report) +
Institution
Knowledge Systems, AI Laboratory +
Ksl tr id
Theorem Proving with Structed Theories (Full Report) +
Month
April +
Number
Theorem Proving with Structed Theories (Full Report) +
Process note
NO +
Categories KSL Technical Report +, Publication +, Technical Report +
|
