|
Abstract : |
The three-valued Fitting/Kunen semantics is one of the best declarative semantics for negation as failure in logic programming. We show that the three-valued consequences of the completion of a logic program are exactly the four-valued consequences of the completion. Since a four-valued relation can be represented by two two-valued relations, the four-valued completion semantics, and hence the threevalued Fitting/Kunen semantics, can be expressed in terms of classical consequences of an appropriate theory, which we call the partial completion of a logic program. We prove that SLDNF-resolution is sound and complete with respect to the partial completion for a large class of normal logic programs, covering most programs of practical interest. This result can even be extended to SLDNF-resolution with built-in predicates. The partial completion, which is always consistent, leads in a natural way to formal theories of inductive definitions. We argue that such theories are appropriate for verification and termination proofs of logic programs. 1, |
