A Complete Axiomatization of the Three-Valued Completion of Logic Programs

We prove the completeness of extended SLDNF-resolution for the new class of "-programs with respect to the three-valued completion of a logic program. Not only the class of allowed programs but also the class of definite programs are contained in the class of "-programs. To understand better the three-valued completion of a logic program we introduce a formal system for three-valued logic in which one can derive exactly the three-valued consequences of the completion of a logic program. The system is proof theoretically interesting, since it is a fragment of Gentzen's sequent calculus LK. Keywords: Logic programming; three-valued logic; negation as failure; SLDNFresolution; sequent calculus. 1 Introduction Negation as failure does not have a simple logical explanation. Procedurally, it can easily be described by the two rules the literal :A succeeds if A fails, the literal :A fails if A succeeds with answer the identity substitution. Formally it is defined as SLDNF-resolution which i..