Loop checking and negation

AbstractIn this paper we extend the concept of loop checking from positive programs (as described in [1]) to locally stratified programs. Such an extension is not straightforward: the introduction of negation requires a (re)consideration of the choice of semantics, the description of a related search space, and new soundness and completeness results handling floundering in a satisfactory way. Nevertheless, an extension is achieved that allows us to generalize the loop checking mechanisms from positive programs to locally stratified programs, while preserving most soundness and completeness results. The conclusion is that negative literals cannot give rise to loops, and must be simply ignored. Note: the material presented in this paper is contained in [5, ch. 5], in which also [1, 4] can be found