Completeness of the negation as failure rule
Joxan Jaffar, Jean-Louis Lassez, John Wylie Lloyd · 1983
Let P be a Horn clause logic program and comp(p) be its completion in the sense of Clark. Clark gave a justification for the negation as failure rule by showing that if a ground atom A is in the finite failure set of P, then ~A is a logical consequence of comp(P), that is, the negation as failure rule is sound. We prove here that the converse also holds, that is, the negation as failure rule is complete. I