A class of programs for which \(SLDNF\) resolution and \(NAF\) rule are complete (Q689290)

A logical language (syntax and declarative semantics) \(\mathcal L\) containing three logical constants (true, false, undefined) is introduced, in a Łukasiewicz classical 3-valued logic manner. A (logical) program is a finite set of program clauses. The notions of locally stratified, locally call-consistent, well-behaved and allowed programs are defined, in the mentioned context. Following \textit{K. Kunen} [Negation in logic programming, J. Logic Program. 4, 289-308 (1987; Zbl 0655.68018)] and \textit{S. Baratella} [Models of Clark's completion for some classes of logic programms, Fundam. Inf. 14/3, 323-337 (1991; Zbl 0714.68009)], a sufficient condition is presented, under which Kunen's completeness result can be used to prove a 2-valued (classical) logic completion theorem. More precisely, it is shown that SLDNF resolution under the NAF (negation as-finite-failure) rule for locally stratified, well be haved and allowed programs is sound and complete. The paper is almost self-contained and it is conjectured that the proofs may be carried on similarly for locally call-consistent programs or even by weakening the allowedness condition on programs.