Answer set programming is a logic programming paradigm that has increased in popularity over the past decade and found applications in a wide variety of elds. Even so, manuals written by the designers of answer set solvers usually described the semantics of the input languages of their systems using examples and informal comments that appeal to the users' intuition, without references to any precise semantics. We describe a precise semantics for the input language of the grounder gringo, which serves as the front end for several answer set solvers. The semantics represents gringo rules as in nitary propositional formulas. We develop methods for using this semantics to prove properties of gringo programs, such as verifying program correctness.
Answer set programming (ASP) is a powerful declarative paradigm for the design
and implementation of knowledge-intensive applications
As the number of ASP users increased, new constructs useful to programmers were added to input languages. This increase in expressivity, however, came at the expense of a fully speci ed semantics. Many of the new constructs lacked a precise mathematical formulation.
We have worked in close collaboration with the gringo system1 designers to
1 http://potassco.sourceforge.net/
bridge that gap. In
Our semantics is based on a translation from rules in the gringo input
language to in nitary propositional formulas (formulas with in nite conjunctions and
disjunctions). Previous work on the semantics of ASP used a translation to
rstorder formulas
#countfX : p(X)g = Y
where the result of applying the aggregate function is compared to a variable. In
With our semantics in place, we can ask questions regarding the correctness of ASP solvers, programs, and optimization methods, and we can develop general methods for answering such questions. The results presented in this note represent initial results on developing formal methods for approaching these kinds of questions.
Such a semantics is also a prerequisite for precisely describing the relationship between input languages of di erent ASP solvers. While this proposal deals with the input language of gringo in particular, it is worth noting that most ASP languages have very similar syntax. In this regard, formalizing a precise semantics and developing formal methods for the input language of gringo goes a long way towards doing the same for other ASP input languages.
In Section 2, we describe what we have accomplished in the direction of describing a precise semantics for the input language of gringo. In Section 3, we describe the in nitary logic which we will use to represent gringo programs, and in Section 4 we give a theoretical result which makes this logic an appealing representational choice. In Section 5, we show that the semantics can be used to establish the correctness of a gringo program. Finally, our plans for future work are documented in Section 6.
In this note we will use \Gringo" to denote the input language of gringo. In work
currently in submission
The key element of the proposed semantics is a translation function from Gringo is the formula
1 i;j n (The expression 1..n in rule (1) is an example of an interval.)
As another example, consider the aggregate expression
into the language of in nitary propositional formulas. Like grounding in the original
de nition of a stable model
(q(i; j) _ :q(i; j)) : #countfX : q(X; 1)g = 1: If the ground atom q(i; j) expresses that there is a queen at square (i; j) of a chessboard, then this aggregate expression says that there is exactly one queen in the rst column. The translation of this aggregate expression can be written as _ q(1; t) ^ ^ : ^ q(1; t); (3) t2H t2G
G H jGj=2 where H is the set of all ground terms, which may be in nite. This example illustrates the need for in nitary formulas. We will explain more precisely what is meant by \can be written as" in Section 4.
Extending the semantics proposed in
A ; not A
as proposed in
q(1..n,1..n) ; not q(1..n,1..n) has only 2 stable models.
In nitary formulas were originally introduced more than fty years ago
Let be a propositional signature, that is, a set of propositional atoms. For every nonnegative integer r, (in nitary propositional) formulas (over ) of rank r are de ned recursively, as follows: every atom from is a formula of rank 0, if H is a set of formulas, and r is the smallest nonnegative integer that is greater than the ranks of all elements of H, then H^ and H_ are formulas of rank r, if F and G are formulas, and r is the smallest nonnegative integer that is greater than the ranks of F and G, then F ! G is a formula of rank r. We will write fF; Gg^ as F ^ G, and fF; Gg_ as F _ G. The symbol ? will be understood as an abbreviation for ;_ and :F stands for F ! ?. These conventions allow us to view nite propositional formulas over as a special case of in nitary formulas.
A set or family of formulas is bounded if the ranks of its members are bounded from above. For any bounded family (F ) 2A of formulas, we denote the formula fF : 2 Ag^ by V 2A F , and similarly for disjunctions.
Subsets of a signature will be also called interpretations of . The satisfaction relation between an interpretation and a formula is de ned recursively, as follows: For every atom p from , I j= p if p 2 I.
I j= H^ if for every formula F in H, I j= F .
I j= H_ if there is a formula F in H such that I j= F .
I j= F ! G if I 6j= F or I j= G.
The reduct F I of a formula F w.r.t. an interpretation I is de ned recursively, as follows:
For every atom p from , pI is p if p 2 I, and ? otherwise. (H^)I = fGI j G 2 Hg^. (H_)I = fGI j G 2 Hg_.
(G ! H)I is GI ! HI if I j= G ! H, and ? otherwise.
An interpretation I is a stable model of a set H of formulas if it is minimal w.r.t. set inclusion among the interpretations satisfying the reducts F I of all formulas F from H.
About sets H1, H2 of in nitary formulas we say that they are strongly equivalent to each other if, for every set H of in nitary formulas, the sets H1 [ H and H2 [ H have the same stable models. About formulas F and G we say that they are strongly equivalent if the singleton sets fF g and fGg are strongly equivalent. Strong equivalence is an important property because if the translations of two rules are strongly equivalent, then we can replace one rule with the other within a Gringo program without changing the meaning of that program. Strong equivalence is also important because it allows us to simplify in nitary formulas that may be di cult to reason about. For example, recall aggregate expression (2) from Section 2. Applying our translation to that aggregate expression yields a formula that is syntactically complicated; however, that formula is strongly equivalent to (3).
It is well-known that nite propositional formulas are strongly equivalent if and
and
and
only if their equivalence is provable in a 3-valued logic called the logic of
here-andthere
) H where H is a possibly in nite set of in nitary formulas and is a nite set of innitary formulas, serve as in nitary analogs to the conjunction introduction and elimination rules of a nite system of natural deduction. It also includes the following axiom schemas:
F ) F;
F _ (F ! G) _ :G; ^ _ F ! _ ^ F (4) (5) 2A F 2H (F ) 2A 2A for every non-empty family (H ) 2A of sets of formulas such that its union is bounded; the disjunction in the consequent of (5) extends over all elements (F ) 2A of the Cartesian product of the family (H ) 2A.
In this section, we present a theorem, proved in
Table 1 shows an ASP encoding of the n-queens problem. It is similar to the
most optimized of the solutions in the language of gringo Version 3 presented in
The n-queens problem involves placing n queens on an n n chess board such that no two queens threaten each other. We will represent squares by pairs of integers (i; j) where 1 i; j n. Two squares (i1; j1) and (i2; j2) are said to be in the same row if i1 = i2; in the same column if j1 = j2; and in the same diagonal if ji1 i2j = jj1 j2j. A set Q of n squares is a solution to the n-queens problem if no two elements of Q are in the same row, in the same column, or in the same diagonal.
Let K denote the result of applying the translation de ned in our semantics to the program K. For any stable model I of K, by QI we denote the set of pairs (i; j) such that q(i; j) 2 I. % place queens on the chess board f q(1..n,1..n) g. % exactly 1 queen per row/column :- X = 1..n, not #countf Y : q(X,Y) g = 1. :- Y = 1..n, not #countf X : q(X,Y) g = 1. % pre-calculate the diagonals d1(X,Y,X-Y+n) :- X = 1..n, Y = 1..n. d2(X,Y,X+Y-1) :- X = 1..n, Y = 1..n. % at most one queen per diagonal :- D = 1..n*2-1, 2 f q(X,Y) : d1(X,Y,D) g.
:- D = 1..n*2-1, 2 f q(X,Y) : d2(X,Y,D) g.
Theorem 1 For each stable model I of K, QI is a solution to the n-queens problem. Furthermore, for each solution Q to the n-queens problem there is exactly one stable model I of K such that QI = Q.
The proof of the theorem uses as lemmas some facts regarding how we may
simplify the result of applying our translation to aggregate expressions involving the
count aggregate function
Another application of this work would be to prove the correctness of the
computational methods used in gringo and in the ASP solvers that use this grounder
as their front end. Currently, those solvers employ a number of \intelligent
instantiation" algorithms which allow the grounder to function e ciently
As previously mentioned, a semantics for Gringo takes us a long way in the
direction of a semantics for most ASP languages. Exploring how these languages
compare and contrast is yet another direction of future work. An example of one
such language is the ASP Core language
Finally, there are a number of theoretical questions regarding the in nitary
system from
My sincere thanks to my friend and mentor Vladimir Lifschitz. Thanks also to the anonymous reviewers. This research was partially supported by the National Science Foundation under Grant IIS-1422455.