Infinitary Formulas in Answer Set Programming
Amelia Harrison and Vladimir Lifschitz and Miroslaw Truszczynski · 2015
The concept of a stable model for infinitary propositional formulas can be used to define the semantics of answer set programming languages. A semantics of this kind serves as a specification for the latest version of the answer set grounder GRINGO. The original definition of a stable model [Gelfond and Lifschitz, 1988] has been generalized in several ways (a survey by Lifschitz [2010] provides a comprehensive overview). In particular, it was extended to arbitrary propositional formulas [Pearce, 1997; Ferraris, 2005]. More recently it was extended to propositional formulas with infinite conjunctions and disjunctions [Truszczynski, 2012], and this generalization has been used to define the semantics of aggregates in the input language of the answer set grounder GRINGO1 [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 F → ⊥ 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 ∨