A sound and complete procedure for a general logic program in non-floundering derivations with respect to the 3-valued stable model semantics

AbstractThis paper presents a sound and complete procedure with respect to the 3-valued stable model semantics. The procedure is regarded as an extension of Eshghi and Kowalski abductive proof procedure, involving finite or countably infinite SLD resolution, as well as finite or countably infinite negative recursion caused by negation as failure. The procedure makes use of the set of negative literals (the set of abducibles) for the negation as failure to be implemented. The set of abducibles is not only applicable to the extraction of explanations for abduction as in Kakas et al. (J. Logic Comput. 2 (1992) 719–770) but also specified for what stable model is now computed in the procedure, because a 3-valued stable model is not always the least (that is, the well-founded model). The procedure also contains nondeterminism in the choices of what ground negative literals are used for negation as failure. By the assumptions of some adequate choices, the procedure is well-defined inductively