A circumscriptive theorem prover: preliminary report
Matthew L. Ginsberg · 1988
We discuss the application of an assumption-based truth maintenance system to the construc-tion of a circumscriptive theorem prover, show-ing that the connection discovered by Reiter and de Kleer between assumption-based truth main-tenance and prime implicants relates to the no-tions 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 re-turns the circumscriptively correct answer.