First-Order Loop Formulas for Normal Logic Programs

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.

Authors

• Fangzhen Lin Hong Kong University of Science and Technology
• Yin Chen South China Normal University
• Yisong Wang
• Mingyi Zhang Guizhou Academy of Sciences

Keywords

No keywords are indexed for this paper.