Loop Checking and the Well-Founded Semantics

. 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. 1 Introduction A "loop check" in a logic programming system is a mechanism that allows the system to avoid some infinite loops. For instance, the execution of the program p / not q; not r; q / r; p; r / q; p (1) under Prolog would lead to an infinite loop, because Prolog would attempt to "derive" q from r and then r from q. A system with a loop check may be able to recognize this fact and to conclude that the goals q and r fail, and, accordingly, the goal p succeeds. In this paper, we make the idea of loop checking pr..