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 non-separable circumscription [9], and to the Yale shooting problem. In all of these cases, the implementation returns the circumscriptively correct answer.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
W. F. Clocksin and C. S. Mellish. Programming in Prolog. Springer-Verlag, Berlin, 1981.
J. de Kleer. An assumption-based truth maintenance system. Artificial Intelligence, 28:127–162, 1986.
M. Gelfond and V. Lifschitz. Compiling circumscriptive theories into logic programs. In Proceedings of the Seventh National Conference on Artificial Intelligence, 1988.
M. Gelfond, H. Przymusinska, and T. Przymusinski. The extended closed world assumption and its relationship to parallel circumscription. In Proceedings of ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, pages 133–139, 1986.
M. R. Genesereth. An overview of meta-level architecture. In Proceedings of the Third National Conference on Artificial Intelligence, pages 119–124, 1983.
M. L. Ginsberg. Multivalued logics: A uniform approach to reasoning in artificial intelligence. Computational Intelligence, 4, 1988.
M. L. Ginsberg. A New Approach to Implicit Quantification. Technical Report 87-7, Logic Group, Stanford University, 1987.
S. Hanks and D. McDermott. Nonmonotonic logics and temporal projection. Artificial Intelligence, 33:379–412, 1987.
V. Lifschitz. Computing circumscription. In Proceedings of the Ninth International Joint Conference on Artificial Intelligence, pages 121–127, 1985.
J. McCarthy. Applications of circumscription to formalizing common sense knowledge. Artificial Intelligence, 28:89–116, 1986.
J. McCarthy. Circumscription — a form of non-monotonic reasoning. Artificial Intelligence, 13:27–39, 1980.
T. C. Przymusinski. Query-answering in circumscriptive and closed-world theories. In Proceedings of the Fifth National Conference on Artificial Intelligence, pages 186–190, 1986.
R. Reiter. On closed world data bases. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 119–140, Plenum, New York, 1978.
R. Reiter and G. Criscuolo. On interacting defaults. In Proceedings of the Seventh International Joint Conference on Artificial Intelligence, pages 270–276, 1981.
R. Reiter and J. de Kleer. Foundations of assumption-based truth maintenance systems: Preliminary report. In Proceedings of the Sixth National Conference on Artificial Intelligence, pages 183–188, 1987.
S. Russell. The Compleat Guide to MRS. Technical Report STAN-CS-85-1080, Stanford University, June 1985.
Y. Shoham. A semantical approach to nonmonotonic logics. In Proceedings of the Tenth International Joint Conference on Artificial Intelligence, pages 388–393, 1987.
D. E. Smith and M. R. Genesereth. Ordering conjunctive queries. Artificial Intelligence, 26(2):171–215, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ginsberg, M.L. (1988). A circumscriptive theorem prover. In: Reinfrank, M., de Kleer, J., Ginsberg, M.L., Sandewall, E. (eds) Non-Monotonic Reasoning. NMR 1988. Lecture Notes in Computer Science, vol 346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50701-9_22
Download citation
DOI: https://doi.org/10.1007/3-540-50701-9_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50701-7
Online ISBN: 978-3-540-46073-2
eBook Packages: Springer Book Archive