Extending negation as failure by abduction: A three-valued stable model semantics

In this paper, we propose a semantics for logic programs with negation as failure, the Finite Failure Stable Model semantics (FF-SM semantics), which is a three-valued extension of Gelfond and Lifschitz' Stable Model semantics. FF-SM semantics is denned in the style of Gelfond and Lifschitz Stable Model semantics, but it builds on an underlying Kripke/Kleene semantics, in which loops causing nonterminating computations are modeled by means of the truth-value undefined. It is different from the extended Stable Model (XSM) semantics defined by Przymusinski, since it does not capture infinite failure. We also introduce an abductive proof procedure which is an abductive extension of SLDNF-resolution based on the ideas underlying Eshghi and Kowalski's abductive procedure. We prove that our procedure is sound and complete with respect to FF-SM semantics. We compare the FF-SM semantics with the XSM semantics, and provide a reconstruction for it within the bilattice-based framework proposed by Fitting. In the paper, we deal with the prepositional case.