Theorem Proving with Structed Theories (Full Report)

Citation: Sheila A. McIlraith and Eyal Amir. (2001) Theorem Proving with Structed Theories (Full Report). In KSL-01-04, April,2001.

Publication techreport ( Edit )
type	Technical Report
bibtype	techreport
Bibtex basics
author	Sheila A. McIlraith and Eyal Amir
title	Theorem Proving with Structed Theories (Full Report)
number	KSL-01-04
institution	Knowledge Systems, AI Laboratory
year	2001
month	April
Bibtex more
Access Paper
abstract	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.

KSL Technical Report ID: KSL-01-04

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 +
Bibtype	techreport +
Has author	Sheila A. McIlraith and Eyal Amir +
Has identifier	KSL-01-04 +
Has publishing details	April,2001 +
Has title	Theorem Proving with Structed Theories (Full Report) +
Has where published	KSL-01-04 +
Has year	2001 +
Institution	Knowledge Systems, AI Laboratory +
Ksl tr id	KSL-01-04 +
Month	April +
Number	KSL-01-04 +
Process note	NO +
Title	Theorem Proving with Structed Theories (Full Report) +
Year	2001 +