© 1991 by Oxford University Press
Original Articles |
A Complete Axiomatization of the Three valued Completion of Logic Programs
Institut für Informatik und angewandte Mathematik, Universität Bern Längassstrasse 51, CH-3012 Bern, Switzerland
We prove the completeness of extended SLDNF-resolution for the new class of e-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; SLDNF-resolution; sequent calculus