Circumscribing embedded implications (without stratifications)

AbstractThis paper is a study of circumscription, not in classical logic, as usual, but in intuitionistic logic. We first review the intuitionistic circumscription of Horn clause logic programs, which was discussed in previous work, and we then consider the larger class of embedded implications. The ordinary circumscription axiom turns out to be inappropriate for this class of rules, and we analyze two alternatives: (1) prioritized circumscription, which works for stratified embedded implications; (2) partial circumscription, which is independent of the stratification. We then show that these two approaches coincide by identifying a single structure that serves as the final Kripke model for both circumscription axioms. This means that prioritized circumscription and partial circumscription entail exactly the same set of implicational queries. Several applications of these ideas are described, including (1) an interpretation of negation-as-failure, (2) a formalization of indefinite reasoning with definite rules, and (3) a methodology for analyzing inductive properties of PROLOG programs