Infinitary Formulas in Answer Set Programming
By
Amelia Harrison,
Vladimir Lifschitz, and
Miroslaw Truszczynski
Abstract:
The original definition of a stable model [Gelfond and Lifschitz1988] has been generalized in several ways (a survey by Lifschitz [Lifschitz2010] provides a comprehensive overview). In particular, it was extended to arbitrary propositional formulas [Pearce1997,Ferraris2005]. More recently it was extended to propositional formulas with infinite conjunctions and disjunctions [Truszczynski2012], and this generalization has been used to define the semantics of aggregates in the input language of the answer set grounder GRINGO [Harrison et al.2014,Gebser et al.2015].
Infinitary propositional formulas of rank r, where r is a nonnegative integer, are defined recursively. Propositional atoms are formulas of rank 0. If H is a set of formulas, and r is the smallest integer that is greater than the ranks of all elements of H, then both the conjunction over all elements of H and the disjunction over all elements of H are formulas of rank r. If r is the smallest integer that is greater than the ranks of F and G then F →G is a formula of rank r. The expression ¬F stands for the formula
where ⊥ is the disjunction over the empty set of formulas and so, is a formula of rank 0. For instance, if Q and P(α), for every α from a non-empty (possibly infinite) set A are atoms then
is a formula of rank 1,
is a formula of rank 2, and
is a formula of rank 3.
The definition of a stable model for a set of infinitary formulas [Truszczynski2012] is a straightforward generalization of the definition proposed by Ferraris [Ferraris2005]. For example, the stable models of (1) are the singletons {P(α)} for all α from A.
Rules involving aggregates can be viewed as abbreviations for infinitary propositional formulas. For example, the rule
(“q holds if the set p is non-empty”) can be thought of as shorthand for (2), where A is the set of all ground terms. The rule
(“q holds if the set p is empty”) can be thought of as shorthand for (3). Gebser et al. [Gebser et al.2015] use this idea to define the semantics of a large subset of the input language of GRINGO. The translation τ, introduced in that paper, transforms programs in that language into infinitary propositional formulas. This translation is modular: it applies to the program rule by rule. In this sense, it is similar to the process of grounding used in the original definition of a stable model, and differs from the process of “intelligent instantiation”, which is limited to safe programs and is used in the design of answer set solvers.
The stable models of a program Π are then defined as the stable models of the infinitary propositional formula τΠ.
The functionality of Version 4.5 of GRINGO, which was released in May of 2015, fully conforms to the semantics defined by Gebser et al. [Gebser et al.2015], and this semantics will serve as a specification for future versions. Proofs of correctness of programs with respect to this semantics rely on the theory of stable models of infinitary formulas. In particular, the study of equivalent transformations of programs uses the extension of the theory of strong equivalence [Lifschitz et al.2001] to infinitary formulas, described by Harrison et al. [Harrison et al.2015b]. For example, according to the definition from that paper, the implication (2) is strongly equivalent to the infinite conjunction
Strong equivalence of infinitary propositional formulas can be sometimes justified using the concept of an “infinitary instance” of a first-order formula [Harrison et al.2015a]. For example, (2) is the instance of
if A is the set of object constants of the underlying signature, and (4) is the instance of
From the fact that these first-order formulas are intuitionistically equivalent to each other, we can conclude that (2) is indeed strongly equivalent to (4).
Bibliography
- Ferraris2005
- Paolo Ferraris.Answer sets for propositional theories.In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pages 119-131, 2005.
- Gebser et al.2015
- Martin Gebser, Amelia Harrison, Roland Kaminski, Vladimir Lifschitz, and
Torsten Schaub.Abstract Gringo.In Proceedings of International Conference on Logic Programming (ICLP), 2015.http://www.cs.utexas.edu/users/vl/papers/AG.pdf; to appear. - Gelfond and Lifschitz1988
- Michael Gelfond and Vladimir Lifschitz.The stable model semantics for logic programming.In Robert Kowalski and Kenneth Bowen, editors, Proceedings of
International Logic Programming Conference and Symposium, pages 1070-1080.
MIT Press, 1988. - Harrison et al.2014
- Amelia Harrison, Vladimir Lifschitz, and Fangkai Yang.The semantics of Gringo and infinitary propositional formulas.In Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), 2014.
- Harrison et al.2015a
- Amelia Harrison, Vladimir Lifschitz, and Julian Michael.Finite proofs for infinitary formulas.http://www.cs.utexas.edu/users /vl/papers/fpfif.pdf; submitted,
2015. - Harrison et al.2015b
- Amelia Harrison, Vladimir Lifschitz, David Pearce, and Agustin Valverde.Infinitary equilibrium logic and strong equivalence.In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 2015.http://www.cs.utexas.edu/users /vl/papers/iel_lpnmr.pdf; to
appear. - Lifschitz et al.2001
- Vladimir Lifschitz, David Pearce, and Agustin Valverde.Strongly equivalent logic programs.ACM Transactions on Computational Logic, 2:526-541, 2001.
- Lifschitz2010
- Vladimir Lifschitz.Thirteen definitions of a stable model.In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of his 70th Birthday, pages 488-503. Springer, 2010.
- Pearce1997
- David Pearce.A new logical characterization of stable models and answer sets.In Jürgen Dix, Luis Pereira, and Teodor Przymusinski, editors, Non-Monotonic Extensions of Logic Programming (Lecture Notes in Artificial Intelligence 1216), pages 57-70. Springer, 1997.
- Truszczynski2012
- Miroslaw Truszczynski.Connecting first-order ASP and the logic FO(ID) through reducts.In Esra Erdem, Joohyung Lee, Yuliya Lierler, and David Pearce, editors, Correct Reasoning: Essays on Logic-Based AI in Honor of Vladimir Lifschitz, pages 543-559. Springer, 2012.