COMPLETENESS FOR PROPOSITIONAL LOGIC PROGRAMS WITH NEGATION

Whether logic programming is declarative depends on the technical condition of soundness and completeness: answers produced by resolution should be exactly the logical consequences of an easily understandable completion of the program. For SLDNF-resolution (on which Prolog is based), and for programs with negation, this goal has not yet been achieved, even at the propositional level. In this paper we prove soundness and completeness of SLDNF-resolution for the full class of propositional programs with negation (including normal programs). This is done in several ways: in classical, intuitionistic, intermediate, and modal logics. In each version we use an intuitively natural program completion, which is different from Clark's completion. The results of the paper can be of interest for rule-based expert systems which represent knowledge in propositional logic.