A Theorem Prover for Prioritized Circumscription

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. T h e ideas to be described have been i m p l e m e n t e d , and examples are given of the system in use. 1 I n t r o d u c t i o n Of all the approaches to nonmonotonic reasoning, McCarthy's circumscription [ M c C a r t h y , 1980, M c C a r t h y , 1986] seems to be the most popular. A great deal of work has gone i n t o the development of new versions of circumscription designed to address various problems in commonsense reasoning. M u c h less work, however, has gone i n t o the development of methods by which these formalisms m i g h t be implemented. In [Ginsberg, 1989], Ginsberg shows how a backward-chaining ATMS can be used to construct a theorem prover for circumscription. Here, this w o r k is extended to handle prioritized circumscription. In [Ginsberg, 1989], the following pro...

• Type: Conference
• Year: 1989
• Where: IJCAI
• Authors: Andrew B. Baker, Matthew L. Ginsberg
• Keywords: Backward-chaining Atms, IJCAI 1989, IJCAI 2007, Prioritized Circumscription, Theorem Prover