A Circumscriptive Theorem Prover: Preliminary Report

We discuss the application of an assumptionbased truth maintenance system to the construction of a circumscriptive theorem prover, showing that the connection discovered by Reiter and de Kleer between assumption-based truth maintenance and prime implicants relates to the notions of minimality appearing in nonmonotonic reasoning. The ideas we present have been implemented, and the resulting system is applied to the canonical birds flying example and to the Yale shooting problem. In both cases, the implementation returns the circumscriptively correct answer.

Authors

• Matthew L. Ginsberg Andrew J. Parkes

Keywords

No keywords are indexed for this paper.