A Theorem Prover for Prioritized Circumscription
Abstract
In a recent paper, Ginsberg shows how a backward-chaining atms can be used to construct a theorem prover for circumscription. Here, this work is extended to handle prioritized circumscription. The ideas to be described have been implemented, and examples are given of the system in use. 1 Introduction Of all the approaches to nonmonotonic reasoning, McCarthy 's circumscription [ McCarthy, 1980, McCarthy, 1986 ] seems to be the most popular. A great deal of work has gone into the development of new versions of circumscription designed to address various problems in commonsense reasoning. Much less work, however, has gone into the development of methods by which these formalisms might be implemented. In [ Ginsberg, 1989 ] , Ginsberg shows how a backward-chaining atms can be used to construct a theorem prover for circumscription. Here, this work is extended to handle prioritized circumscription. In [ Ginsberg, 1989 ] , the following procedure is given to determine whether a particular ...
Cite
Text
Baker and Ginsberg. "A Theorem Prover for Prioritized Circumscription." International Joint Conference on Artificial Intelligence, 1989.Markdown
[Baker and Ginsberg. "A Theorem Prover for Prioritized Circumscription." International Joint Conference on Artificial Intelligence, 1989.](https://mlanthology.org/ijcai/1989/baker1989ijcai-theorem/)BibTeX
@inproceedings{baker1989ijcai-theorem,
title = {{A Theorem Prover for Prioritized Circumscription}},
author = {Baker, Andrew B. and Ginsberg, Matthew L.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1989},
pages = {463-467},
url = {https://mlanthology.org/ijcai/1989/baker1989ijcai-theorem/}
}