* Yin Chen, Fangzhen Lin, Yisong Wang, Mingyi Zhang*

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 instantiation-basis: 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 non-equivalent first-order loops.

*Subjects: *11. Knowledge Representation; 3.3 Nonmonotonic Reasoning

*Submitted: *Mar 6, 2006

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.