TY - JOUR
T1 - On elementary loops of logic programs
AU - Gebser, Martin
AU - Lee, Joohyung
AU - Lierler, Yuliya
N1 - Funding Information:
We are grateful to Selim Erdog˘an, Tomi Janhunen, Dan Lessin, Vladimir Lifschitz, Torsten Schaub, Jicheng Zhao, and the anonymous referees of Gebser et al. (2006, 2007) and this paper for their useful comments. Martin Gebser was partially supported by the German Research Foundation under Grant SCHA 550/8-1. Joohyung Lee was partially supported by the National Science Foundation under Grant IIS-0916116 and by the Office of the Director of National Intelligence (ODNI), Intelligence Advanced Research Projects Activity (IARPA), through US army. Yuliya Lierler was partially supported by the National Science Foundation under Grant IIS-0712113 and by a 2010 Computing Innovation Fellowship.
PY - 2011/11
Y1 - 2011/11
N2 - Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53-65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53-87). Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.
AB - Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53-65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53-87). Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.
KW - loop formulas
KW - stable model semantics
KW - unfounded sets
UR - http://www.scopus.com/inward/record.url?scp=80155212946&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80155212946&partnerID=8YFLogxK
U2 - 10.1017/S1471068411000019
DO - 10.1017/S1471068411000019
M3 - Article
AN - SCOPUS:80155212946
SN - 1471-0684
VL - 11
SP - 953
EP - 988
JO - Theory and Practice of Logic Programming
JF - Theory and Practice of Logic Programming
IS - 6
ER -