A Circumscriptive Theorem Prover: Preliminary Report

Matthew L. Ginsberg

We discuss the application of an assumption-based 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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.