Loop Checking and the Well-founded Semantics (1995)
Vladimir Lifschitz, Norman McCain, Teodor C. Przymusinski and Robert F. Staerk
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.
In Logic Programming and Non-monotonic Reasoning: Proceedings of the Third Int'l Conf., pp. 127-142 1995.

Vladimir Lifschitz Faculty vl [at] cs utexas edu
Norman McCain Ph.D. Alumni nmccain [at] sunflower com