An Intuitionistic Interpretation of Finite and Infinite Failure
L. Thorne McCarty, Ron van der Meyden · Logic Programming and Non-Monotonic Reasoning · 1993
In this paper, we propose an intuitionistic semantics for negation-as-failure in logic programs. The basic idea is to work with the completion of the program, not in classical logic, but in intuitionistic (or, more precisely, minimal) logic. Moreover, we consider two forms of completion: (1) first-order predicate completion, as defined by Clark, which is related to SLDNF resolution; and (2) second-order completion, using circumscription. Specifically, given any program R, we write a sentence in second-order intuitionistic logic, called the partial intuitionistic circumscription axiom, and we declare this sentence to be the "meaning" of R. We then show that our semantics -- called the PIC semantics -- agrees with the perfect model semantics in the case of a locally stratified program. For nonstratified programs, we show that the PIC semantics is strictly stronger than the (3-valued) wellfounded semantics. We also show a more complex relationship to the (2-valued) stable model semantics....