Using a calculus of goals, we define the success and failure of a goal for propositional programs in the presence of loop checking. The calculus is sound with respect to the well-founded semantics; for finite programs, it is also complete. A Prolog-style proof search strategy for a modification of this calculus provides a query evaluation algorithm for finite propositional programs under the well-founded semantics. This algorithm is implemented as a meta-interpreter.

PS

In Logic Programming and Non-monotonic Reasoning: Proceedings of the Third Int'l Conf., pp. 127-142 1995.

@INPROCEEDINGS{lif95a, title={Loop Checking and the Well-founded Semantics}, author={Vladimir Lifschitz and Norman McCain and Teodor C. Przymusinski and Robert F. Staerk}, booktitle={Logic Programming and Non-monotonic Reasoning: Proceedings of the Third Int'l Conf.}, pages={127-142}, url="http://www.cs.utexas.edu/users/ai-lab?lif95a", year={1995} }