In some approaches to the declarative semantics of logic programming, a program Pi is treated as shorthand for the propositional program Ground(Pi) whose rules are the ground instances of the rules of Pi. We relate the success and failure of a program Pi with a goal G under SLDNF with constructive negation to the success and failure of Ground(Pi) with ground instances of G under propositional SLDNF. As a corollary, we get a soundness theorem for SLDNF with constructive negation relative to the answer set semantics. Since this semantics is closely related to default logic and autoepistemic logic, proofs of such theorems help us understand why the computational mechanisms developed in logic programming provide partial implementations of these nonmonotonic formalisms.

PS

In Proceedings ICLP-95, pp. 581-595 1995.

@InProceedings{lif95, title={SLDNF, Constructive Negation and Grounding}, author={Vladimir Lifschitz}, booktitle={Proceedings ICLP-95}, pages={581-595}, url="http://www.cs.utexas.edu/users/ai-lab?lif95", year={1995} }