A Model-Theoretic Counterpart of Loop Formulas

Abstract

In an important recent paper, Lin and Zhao introduced the concept of a loop formula, and showed that the answer sets for a logic program are exactly the models of Clark's completion of the program that satisfy the loop formulas. Just as sets are a model-theoretic account of completion, externally supported sets, defined in this paper, are a model-theoretic counterpart of loop formulas. This reformulation of loop formulas shows that they are related to assumption sets (Sacca and Zaniolo) and to unfounded sets (Van Gelder, Ross and Schlipf; Leone, Rullo and Scarcello), invented many years earlier. Other contributions of this paper includes a simplification of the definition of a loop, extending it to programs with classical negation and infinite programs, and a generalization of the definition of a loop formula.