A Circumscriptive Theorem Prover
Abstract
Abstract In [6], a generalization of first-order logic was introduced that led to the development of an effective theorem prover for some simple sorts of default reasoning. In this paper, we show that these ideas can also be used to construct a theorem prover for a wide class of circumscriptive theories. The ideas to be discussed have been implemented, and the resulting system has been applied to the canonical birds flying example, to a nonseparable circumscription [9], and to the Yale shooting problem. In all of these cases, the implementation returns the circumscriptively correct answer.
Cite
Text
Ginsberg. "A Circumscriptive Theorem Prover." AAAI Conference on Artificial Intelligence, 1988.Markdown
[Ginsberg. "A Circumscriptive Theorem Prover." AAAI Conference on Artificial Intelligence, 1988.](https://mlanthology.org/aaai/1988/ginsberg1988aaai-circumscriptive/)BibTeX
@inproceedings{ginsberg1988aaai-circumscriptive,
title = {{A Circumscriptive Theorem Prover}},
author = {Ginsberg, Matthew L.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {1988},
pages = {470-474},
url = {https://mlanthology.org/aaai/1988/ginsberg1988aaai-circumscriptive/}
}