Complete logic programs with domain-closure axiom

AbstractComplete logic programs augmented with the domain-closure axiom are proposed as the reference theory for logic programming with negation as failure. An inference rule corresponding to “proof by case analysis” is proved correct within this framework. As a major consequence, the completeness results for SLD resolution and negation as failure still hold. An interesting outcome is that some novel operational properties of SLD resolution can be proved