@article{GerbserLeeLierler2006,
  author    = {Gerbser, Martin and Lee, Joohyung and Lierler, Yuliya},
  title     = {Elementary sets for logic programs},
  isbn      = {978-1-57735-281-5},
  year      = {2006},
  language  = {en}
}
@article{GebserLeeLierler2007,
  author    = {Gebser, Martin and Lee, Joohyung and Lierler, Yuliya},
  title     = {Head-elementary-set-free logic programs},
  isbn      = {978-3-540- 72199-4},
  year      = {2007},
  language  = {en}
}
@article{GebserLeeLierler2011,
  author    = {Gebser, Martin and Lee, Joohyung and Lierler, Yuliya},
  title     = {On elementary loops of logic programs},
  series = {Theory and practice of logic programming},
  volume    = {11},
  journal   = {Theory and practice of logic programming},
  number    = {2},
  publisher = {Cambridge Univ. Press},
  address   = {New York},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068411000019},
  pages     = {953 -- 988},
  year      = {2011},
  abstract  = {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 Ha: program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.},
  language  = {en}
}
@article{CabalarFandinnoLierler2020,
  author    = {Cabalar, Pedro and Fandinno, Jorge and Lierler, Yuliya},
  title     = {Modular Answer Set Programming as a formal specification language},
  series = {Theory and practice of logic programming},
  volume    = {20},
  journal   = {Theory and practice of logic programming},
  number    = {5},
  publisher = {Cambridge University Press},
  address   = {New York},
  issn      = {1471-0684},
  doi       = {10.1017/S1471068420000265},
  pages     = {767 -- 782},
  year      = {2020},
  abstract  = {In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining aformal proofshowing that the answer sets of a given (non-ground) logic programPcorrectly correspond to the solutions to the problem encoded byP, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order)program modulesthat may incorporate local hidden atoms at different levels. Then,verifyingthe logic programPamounts to prove some kind of equivalence betweenPand its modular specification.},
  language  = {en}
}
@misc{GebserLeeLierler2011,
  author    = {Gebser, Martin and Lee, Joohyung and Lierler, Yuliya},
  title     = {On elementary loops of logic programs},
  series = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  journal   = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe},
  number    = {566},
  issn      = {1866-8372},
  doi       = {10.25932/publishup-41309},
  url       = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-413091},
  pages     = {36},
  year      = {2011},
  abstract  = {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.},
  language  = {en}
}