First-Order Loop Formulas for Normal Logic Programs ∗ Abstract

In this paper we extend Lin and Zhao’s notions of loops and loop formulas to normal logic programs that may contain variables. Under our definition, a loop formula of such a logic program is a first-order sentence. We show that together with Clark’s completion, our notion of first-order loop formulas captures the answer set semantics on the instantiationbasis: for any finite set F of ground facts about the extensional relations of a program P, the answer sets of the ground program obtained by instantiating P using F are exactly the models of the propositional theory obtained by instantiating using F the first order theory consisting of the loop formulas of P and Clark’s completion of the union of P and F. We also prove a theorem about how to check whether a normal logic program with variables has only a finite number of nonequivalent first-order loops