# axiomatization_of_aggregates_in_answer_set_programming__ac4e9314.pdf

Axiomatization of Aggregates in Answer Set Programming

Jorge Fandinno*, Zachary Hansen*, Yuliya Lierler*

University of Nebraska at Omaha {jfandinno,zachhansen,ylierler}@unomha.edu

The paper presents a characterization of logic programs with aggregates based on a many-sorted generalization of operator SM that refers neither to grounding nor to fixpoints. This characterization introduces new function symbols for aggregate operations and aggregate elements, whose meaning can be fixed by adding appropriate axioms to the result of the SM transformation. We prove that for programs without positive recursion through aggregates our semantics coincides with the semantics of the answer set solver clingo.

Introduction Answer set programming (ASP; Lifschitz 2008) is a form of declarative logic programming well-suited to solving knowledge-intensive search problems. Its success relies on the combination of a rich knowledge representation language with efficient solvers for finding solutions to problems expressed in this language (Lifschitz 2019). One of the most useful constructs of this language are aggregates: intuitively, these are functions that apply to sets. The semantics of aggregates has been extensively studied in the literature (Simons, Niemel a, and Soininen 2002; Dovier, Pontelli, and Rossi 2003; Pelov, Denecker, and Bruynooghe 2007; Son and Pontelli 2007; Ferraris 2011; Faber, Pfeifer, and Leone 2011; Gelfond and Zhang 2014, 2019; Cabalar et al. 2019). In most cases, papers rely on the idea of grounding a process in which all variables are replaced by variable-free terms. Thus, first a program with variables is transformed into a propositional one, then the semantics of the propositional program is defined. This makes reasoning about programs with variables cumbersome. For instance, it prohibits using first-order theorem provers for verifying properties of programs as advocated by Fandinno et al. (2020). To the best of our knowledge, only two approaches defined the semantics of aggregates without referring to grounding. Lee, Lifschitz, and Palla (2008) translate certain count aggregates with a ground guard into an existentially quantified first-order formula. Yet, this approach is inapplicable to more general count aggregates as well as to the common sum aggregates. Cabalar et al. (2018) introduce

*These authors contributed equally. Copyright 2022, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.

intensional sets as first-class citizens into Quantified Equilibrium Logic (Pearce and Valverde 2005) with partial functions (Cabalar 2011) and provide a formalisation of aggregates that directly corresponds to the idea that aggregates are functions that apply to sets. This approach is truly general: it covers arbitrary aggregates including nested ones. The price for the generality of this formalism is complexity. Similar to the work by Cabalar et al. (2018), our approach provides a direct formalisation of the idea that aggregates are functions that apply to sets, but it aims to exclusively use the language of classical logic (instead of adding intensional sets as a new construct in the language). To achieve this goal, we assume two restrictions. First, aggregates cannot be nested and second, there cannot exist positive recursion through aggregates. Note that, in practice, solvers cannot process nested aggregates. Regarding the second restriction, solvers may process programs with recursion through aggregates. Yet, different solvers may compute distinct answers for the same input program. For the sake of uncontroversial semantics, the ASP-Core-2 standard does not consider recursion through aggregates (Calimeri et al. 2012). In this paper, we introduce a translation from logic programs to second-order logic formulas and define the semantics of aggregates using two equivalent characterizations. The expressive power of the answer set semantics cannot be captured by first-order logic, making second-order logic the prime candidate for this task. The first characterization uses a simpler language, where we restrict the considered interpretations at the meta-logic level. The second characterization fixes the meaning of some symbols in this language by providing an axiomatization at the object-level. The first characterization is easier to understand, while the second provides greater mathematical precision. In many cases we can replace second-order formulas by first-order formulas (Ferraris, Lee, and Lifschitz 2011; Lee and Meng 2011). Here we show that for programs with aggregates that apply to finite sets, we can replace the second-order axiomatization of aggregates by a first-order one. This paves the way for using first-order theorem provers to reason about programs with aggregates; to the best of our knowledge this was not yet possible. The restriction to finite aggregates is not a practical limitation as solvers cannot deal with infinite sets. In the studied fragment, our semantics coincide with the semantics of the solver clingo (Gebser et al. 2015).

The Thirty-Sixth AAAI Conference on Artificial Intelligence (AAAI-22)

Preliminaries Syntax of programs with aggregates. We assume a (program) signature with three countably infinite sets of symbols: numerals, symbolic constants and program variables. We also assume a 1-to-1 correspondence between numerals and integers; the numeral corresponding to an integer n is denoted by n. Program terms are either numerals, symbolic constants, variables or either of the special symbols inf and sup. A program term (or any other expression) is ground if it contains no variables. We assume that a total order on ground terms is chosen such that

inf is its least element and sup is its greatest element, for any integers m and n, m < n iff m < n, and for any integer n and any symbolic constant c, n < c.

An atom is an expression of the form p(t), where p is a symbolic constant and t is a list of program terms. A comparison is an expression of the form t t , where t and t are program terms and is one of the comparison symbols:

= = < > (1)

An atomic formula is either an atom or a comparison. A basic literal is an atomic formula possibly preceded by one or two occurrences of not. An aggregate element has the form

t1, . . . , tk : l1, . . . , lm (2)

where each ti (1 i k) is a program term and each li (1 i m) is a basic literal. An aggregate atom is of form

#op{E} u (3)

where op is an operation name, E is an aggregate element, is one of the comparison symbols in (1), and u is a program term, called guard. We consider operation names names count and sum. For example, expression #sum{K, X, Y : in(X, Y ), cost(K, X, Y )} > J is an aggregate atom. An aggregate literal is an aggregate atom possibly preceded by one or two occurrences of not. A literal is either a basic literal or an aggregate literal. A rule is an expression of the form

Head :- B1, . . . , Bn, (4)

Head is either an atom or symbol ; we often omit symbol which results in an empty head; each Bi (1 i n) is a literal.

We call the symbol :- a rule operator. We call the left hand side of the rule operator the head, the right hand side of the rule operator the body. When the head of the rule is an atom we call the rule normal. A program is a finite set of rules. We assume that aggregates do not have positive recursion. This is a less restrictive assumption than the one used in the ASP-Core-2 semantics (Calimeri et al. 2012), which requires aggregates have neither positive nor negative recursion. Formally, a predicate symbol is a pair p/n, where p is a symbolic constant and n is a nonnegative integer. About a program or another syntactic expression,

we say that a predicate symbol p/n occurs in it if it contains an atom of the form p(t1, . . . , tn). We say that an occurrence of a predicate symbol p/n in a literal is strictly positive if it is not in the scope of negation. For example, literals not r(X, Y, Z), #sum{Y, Z : not r(X, Y, Z)} and not #sum{Y, Z : r(X, Y, Z)} contain no strictly positive occurrence of r/3. For a program Π, its (directed predicate) dependency graph is defined by

1. a set of vertices containing all predicate symbols occurring in Π , 2. a set of edges containing an edge (h, b) for every normal rule (4) with h being the predicate symbol occurring in the atom Head of the rule and b being any predicate symbol that has a strictly positive occurrence in one of the literals B1, ... , Bn of the rule.

The aggregates in Π have no positive recursion if, for every normal rule R of form (4), there is no path in the program s dependency graph from any predicate symbol with a strictly positive occurrence in an aggregate element of one of the literals B1, . .. , Bn in R to the predicate symbol occurring in Head of R. For instance, a program consisting of rule r(X, Y, Z) :- q(X, Y, Z), #sum{Y, Z : not r(X, Y, Z)} has no aggregate with positive recursion; a program consisting of r(X, Y, Z) :- q(X, Y, Z), #sum{Y, Z : r(X, Y, Z)} has an aggregate with positive recursion. Each operation name op is associated with a function c op that maps every set of tuples of ground terms to a ground term. If the first member of a tuple t is a numeral n then we say that integer n is the weight of t, otherwise the weight of t is 0. For any set of tuples of ground terms,

\ count( ) is the numeral corresponding to the cardinality of , if is finite; and sup otherwise. d sum( ) is the numeral corresponding to the sum of the weights of all tuples in , if contains finitely many tuples with non-zero weights; and 0 otherwise.1 If is empty, then d sum( ) = 0.

Operator SM for many-sorted signature. Here, we recall the standard definition of many-sorted first-order logic. A signature σ consists of function and predicate constants and a set of sorts. The arity of every function or predicate constant is a tuple of sorts; the arity of function constants is a nonempty tuple. A predicate constant whose arity is the empty tuple is called a proposition. We assume that there are infinitely many variables for each sort. Atomic formulas are built similar to the standard unsorted logic with the restriction that in a term f(t1, . . . , tn) (an atom p(t1, . . . , tn), respectively), the sort of term ti must be a subsort of the ith argument of f (of p, respectively). In addition, t1 = t2 is an atomic formula if the sorts of t1 and t2 have a common supersort. A many-sorted interpretation I has a nonempty universe |I|s for each sort s. When sort s1 is a subsort of sort s2, an interpretation additionally satisfies the condition |I|s1 |I|s2. The notion of satisfaction is analogous

1The sum of a set of integers is not always defined. We could choose a special symbol to denote this case, we chose to use 0 following the description of abstract gringo (Gebser et al. 2015).

to the unsorted case with the restriction that an interpretation maps a term to an element in the universe of its associated sort. The following symbols are considered to be the logical primitives:

Negation, truth and equivalence are assumed to be abbreviations: F stands for F, stands for , and (F G) (G F) stands for F G. The definition of the operator SM for a many-sorted signature is a straightforward generalization of the unsorted case (Ferraris, Lee, and Lifschitz 2011). If p and u are predicate constants or variables of the same arity (note that while the original definition does not account for sort information, here arity refers to both number and sort of the arguments), then u p stands for the formula

W(u(W) p(W)),

where W is a tuple of distinct object variables matching the arity of p and u. If p and u are tuples p1, . . . , pn and u1, . . . , un of predicate constants or variables such that each pi and ui have the same arity, then u p stands for the conjunction

(u1 p1) (un pn),

and u < p stands for (u p) (p u). For any manysorted first-order formula F and a list p of predicate constants, by SMp[F] we denote the second-order formula

F u (u < p) F (u)

where u is a list of distinct predicate variables u1, . . . , un of the same length as p, such that the arity of each ui is the same as the arity of pi, and F (u) is defined recursively:

F = F for any atomic formula F that does not contain members of p, pi(t) = ui(t) for any predicate symbol pi belonging to p and any list t of terms, (F G) = F G

(F G) = F G

(F G) = (F G ) (F G) ( x F) = x F

( x F) = x F

If the list p is empty, then we understand SMp[F] as F. For a finite theory Γ, we write SMp[Γ] to represent SMp[F], where F is the conjunction of all formulas in Γ.

Programs With Aggregates as Many-Sorted First-Order Sentences In this section we present the translation τ that turns a program Π (whose aggregates lack positive recursion) into a first-order sentence with equality over a signature σΠ of two sorts. We start by defining this signature. To do so, we must first introduce the concepts of a global variable and an aggregate symbol. A variable is said to be global in a rule if

1. it occurs in any non-aggregate literal, or 2. it occurs in a guard of any aggregate literal. For instance, in rule

p(X) :- q(X), #sum{Y, Z : r(X, Y, Z)} 1. (5) the only global variable is X. An aggregate symbol is a pair E/X, where E is an aggregate element and X is a list of variables occurring in E. We say that E/X occurs in rule R if this rule contains an aggregate literal with the aggregate element E and X is the list of all variables in E that are global in R. For instance, Y, Z : r(X, Y, Z)/X is the only aggregate symbol occurring in rule (5). We say that E/X occurs in a program if E/X occurs in some rule of the program. For the sake of readability we associate each aggregate symbol E/X with a different name |E/X|. As stated earlier, the signature σΠ is defined over two sorts. The first sort is called the program sort; all program terms are of this sort. The second sort is called the set sort; it contains entities that are sets (of tuples of object constants of the program sort). We denote the two sorts in an intuitive manner: sprg and sset. For a program Π, signature σΠ contains: 1. all ground terms as object constants of the program sort; 2. all predicate symbols occurring in Π as predicate constants with all arguments of sort program; 3. the comparison symbols other than equality and inequality as predicate constants of arity sprg sprg; 4. function constants count and sum of arity sset sprg; 5. for each aggregate symbol E/X occurring in Π, a function constant set|E/X| of arity sprg sprg sset. This function symbol takes as many arguments of the program sort as there are variables in X. If X is the empty list, then set|E/X| is an object constant. Intuitively, the result of count is the cardinality of the set passed as an argument; the result of sum is the sum of all elements of the set passed as an argument; and set|E/X|(t1, . . . , tk) represents the set of elements corresponding to the aggregate element E once all global variables in X = X1, . . . , Xk are replaced by ground terms t1, . . . , tk. We formalize these claims below. As customary in arithmetic we use infix notation in constructing atoms that utilize predicate symbols >, , <, . Expression t1 = t2 is considered an abbreviation for the formula (t1 = t2). In the following, we use letters X, Y, Z and their variants to denote variables of sort sprg and letter S and its variants to denote variables of sort sset. We use their bold face variants to denote lists of variables of that sort. We now describe a translation τ that converts a program into a finite set of first-order sentences. Given a list Z of global variables in some rule R, we define τ Z for all elements of R as follows: 1. for every atomic formula A occurring outside of an aggregate literal, its translation τ ZA is A itself; τ Z is ; 2. for an aggregate atom A of form #count{E} u or #sum{E} u, its translation τ Z is the atom count(set|E/X|(X)) u or sum(set|E/X|(X)) u

respectively, where X is the list of variables in Z occurring in E; 3. for every (basic or aggregate) literal of the form not A its translation τ Z(not A) is τ ZA; for every literal of the form not not A its translation τ Z(not not A) is τ ZA.

We now define the translation τ as follows:

4. for every rule R of form (4), its translation τ R is the universal closure of the implication

τ ZB1 τ ZBn τ Z Head,

where Z is the list of the global variables of R. 5. for every program Π, its translation τ Π is the first-order theory containing τ R for each rule R in Π. For example, the result of applying τ to a program consisting of rule (5) and the rules

s(X) :- q(X), #sum{Y : r(X, Y, Z)} 1. (6) t :- #sum{Y, Z : r(X, Y, Z)} 1. (7) q(a). q(b). q(c). (8) r(a, 1, a). r(b, 1, a). r(b, 1, a). r(b, 1, b). r(c, 0, a). (9)

is the first-order theory composed of the universal closure of the following formulas:

q(X) sum(sete1(X)) 1 p(X) (10) q(X) sum(sete2(X)) 1 s(X) (11) sum(sete3) 1 t (12) q(a) q(b) q(c) (13) r(a, 1, a) r(b, 1, a) r(b, 1, a) r(b, 1, b) r(c, 0, a) (14)

where e1 and e2 are the names for aggregate symbols Y, Z : r(X, Y, Z)/X and Y : r(X, Y, Z)/X, respectively; e3 is the name for an aggregate symbol Y, Z : r(X, Y, Z). Note that the aggregate symbols corresponding to names e1 and e2 have a global variable X. Consequently, function symbols sete1 and sete2 have arity sprg sset. The aggregate symbol corresponding to e3 has no global variables. Consequently, sete3 is an object constant of sort sset.

Semantics of programs with aggregates. For the sake of clarity, we describe the semantics of programs with aggregates in two steps. We start by assuming some restrictions on the form of interpretations of interest. These interpretations have fixed meanings for the symbols of signature σΠ introduced in conditions 3-5. In the next section, we remove these restrictions on symbols count, sum and set|E/X| and fix their meaning by providing appropriate axioms. In both cases, we assume that the interpretation of the symbolic constants is the identity. Consider additional notation. For a tuple X of distinct variables, a tuple x of ground terms of the same length as X, and an expression α that contains variables from X, αX x denotes the expression obtained from α by substituting x for X. An agg-interpretation I is a many-sorted interpretation that satisfies the following conditions:

1. the domain |I|sprg is the set containing all ground terms of program sort (or ground program terms, for short);

2. I interprets each ground program term as itself;

3. I interprets predicate symbols >, , <, according to the total order chosen earlier;

4. universe |I|sset is the set of all sets of non-empty tuples that can be formed with elements from |I|sprg;

5. if E/X is an aggregate symbol, where E is an aggregate element of form (2), Y is the list of all variables occurring in E that are not in X, and x and y are lists of ground program terms of the same length as X and Y respectively, then set|E/X|(x)I is the set of all tuples of form (t1)XY xy , . . . , (tk)XY xy such that I satisfies (l1)XY xy (lm)XY xy ;

6. for term tset of sort sset, count(tset)I is \ count(t I set);

7. for term tset of sort sset, sum(tset)I is d sum(t I set);

An agg-interpretation satisfies the standard name assumption for object constants of the program sort, but not for object constants and function constants of the set sort. We say that an agg-interpretation I is a stable model of program Π if it satisfies the second-order sentence SMp[τ Π] with p being the list of all predicate symbols occurring in Π (note that this excludes predicate constants for the comparisons >, , <, ). In general, ASP solvers do not provide a complete first-order interpretation corresponding to a computed stable model. Rather, they list the set of ground atoms corresponding to it. Formally, for an agg-interpretation I, by Ans(I), we denote the set of ground atoms that are satisfied by I and whose predicate symbol is of sort program. If I is a stable model of Π, we say that Ans(I) is an answer set of Π. For example, take Π1 to denote a program composed of rules (5-9). Let I be an agg-interpretation over σΠ1 such that

q I = {a, b, c}

r I = {(a, 1, a), (b, 1, a), (b, 1, a), (b, 1, b), (c, 0, a)}. (15)

Conditions 5 and 7 imply that this agg-interpretation also satisfies the following statements

sete1(a)I = {(1, a)}

sete1(b)I = {( 1, a), (1, a), (1, b)}

sete1(c)I = {(0, a)}

sete2(a)I = {(1)}

sete2(b)I = {( 1), (1)}

sete2(c)I = {(0)}

set I e3 = {(1, a),( 1, a),(1, b),(0, a)}

sum(sete1(a))I = 1

sum(sete1(b))I = 1

sum(sete1(c))I = 0

sum(sete2(a))I = 1

sum(sete2(b))I = 0

sum(sete2(c))I = 0

sum(sete3)I = 1

Such an agg-interpretation I is a stable model of program Π1 when p I = {a, b}, s I = {a}, and t I = true. It turns out, this program has a unique answer set

{ q(a), q(b), q(c), r(a, 1, a), r(b, 1, a), r(b, 1, a), r(b, 1, b), r(c, 0, a), p(a), p(b), s(a), t }.

Axiomatization of Aggregates In this section we show that conditions 5-7 characterizing agg-interpretations can be removed from the meta-logic level by adding new logical sentences to the theory representing a logic program. This provides higher mathematical rigor and allows us to build object-level proofs to reason about programs with aggregates. We introduce an extended signature σ Π that expands σΠ with new symbols and new sorts. The new sorts are sint and stuple that we refer to as integer and tuple, respectively. We also assume countably infinite sets of integer and tuple variables (variables of sorts sint and stuple). We use the letter N and its variants to denote integer variables and the letter T and its variants to denote tuple variables. Letters V, W, and their variants denote variables where the sort is explicitly mentioned. As customary in mathematics, we use infix notation for the function symbol + and the predicate symbol . Informally, tuplek(t1, . . . , tk) is a constructor for the ktuple containing program terms t1, . . . , tk; atomic formula ttuple tset holds iff tuple ttuple belongs to set tset; rem(tset, ttuple) encodes the set obtained by removing tuple ttuple from set tset; and weight(ttuple) encodes the weight of tuple ttuple (recall that the syntactic object ttuple is meant to be interpreted as an object of sort stuple). Formally, for this extended signature, we extend the set of conditions that an agg-interpretation I satisfies: 8. the domain |I|sint is the set of all numerals; 9. I interprets m + n as m + n, 10. universe |I|stuple is the set of all tuples of form d1, . . . , dm with m 1 and each di |I|sprg; 11. I interprets each tuple term of form tuplek(t1, . . . , tk) as the tuple t I 1, . . . , t I k .

12. I interprets object constant as the empty set ; 13. I satisfies t1 t2 iff tuple t I 1 belongs to set t I 2; 14. rem(tset, ttuple)I is the set obtained by removing tuple t I tuple from set t I set; and

15. weight(ttuple)I is the weight of t I tuple.

Note that |I|sset is the power set of |I|stuple. Also, each agg-interpretation is extended in a unique way: there is a one-to-one correspondence between the agg-interpretations over σΠ and σ Π. In the sequel, we identify each agg-interpretation in signature σΠ with its extension in σ Π. In the remainder of this section, we show how an agg-interpretation can be axiomatized in a theory that interprets symbols for arithmetic, tuples, sets, and program object constants in a standard way. Formally, a first-order interpretation I is called standard when it satisfies conditions 1-4 and 8-13. Such an interpretation satisfies the standard name assumption for ground program terms and tuples, the standard interpretation of arithmetic symbols, and the standard interpretation of the set theoretic membership predicate. It does not assign any special meaning to symbols count, sum, rem, weight, and any of the functions constants of form set|E/X|. It is obvious that every agg-interpretation is also a standard interpretation, but not vice-versa.

We now show that agg-interpretations can be characterized as standard interpretations that satisfy a particular class of sentences. To begin with, consider condition 5 of the agg-interpretation definition. It associates an aggregate symbol E/X, where E has the form (2), with a unique set. We characterize this set with the sentence

X T T set|E/X|(X)

Y T = tuplek(t1, . . . , tk) l1 lm , (17)

where Y is the list of all the variables occurring in E that are not in X. For instance, recall program Π1 and the aggregate symbol Y, Z : r(X, Y, Z)/X named e1 (introduced in the previous section). For this symbol, sentence (17) has the form

XT T sete1(X)

Y Z T = tuple2(Y, Z) r(X, Y, Z)

For a standard interpretation I over signature σ Π1 satisfying conditions (15) and this sentence, sete1(b)I is the set {( 1, a), (1, a), (1, b)}. This set is identical to the one stated in (16) for an agg-interpretation satisfying conditions (15). This observation hints at a general result: Proposition 1. Let I be a standard interpretation. Then, I satisfies condition 5 iff it satisfies sentence (17) for every function symbol of form set|E/X|.

Similarly, the meaning of function symbols rem and weight provided by conditions 14 and 15 of the definition of agg-interpretations can be fixed in standard interpretations using the following sentences:

STS rem(S, T) = S

T T S (T S T = T) (18)

NX2 . . . Xk weight(tuplek(N, X2, . . . , Xk)) = N (19)

X1X2 . . . Xk ( N X1 = N)

weight(tuplek(X1, X2, . . . , Xk)) = 0 . (20)

Proposition 2. Let I be a standard interpretation. Then, I satisfies condition 14 iff it satisfies sentence (18); and I satisfies condition 15 iff it satisfies all sentences of form (19-20). Formalizing condition 6 requires determining when a set is finite or not, that is, we need a formula Finite(tset) that holds if and only if the set represented by tset is finite. We can formalize this idea using a second-order formula, which states that there is a natural number n and an injective function from tset into the set {i N | i n}. Before formalizing this statement, let us introduce some auxiliary definitions. Given a term tset of sort sset and a function symbol f, we define Injective(f, tset) as the formula

T1T2 (T1 tset T2 tset f(T1) = f(T2) T1 = T2.)

Intuitively, formula Injective(f, tset) represents the fact that the restriction of function f, whose domain is the set corresponding to tset, is injective. If the image of f is of sort sprg and t1 and t2 are also terms of sort sprg, we define Image(f, tset, t1, t2) as the formula:

T (T tset t1 f(T) f(T) t2)

Formula Image(f, tset, t1, t2) holds when the image of the restriction of function f, whose domain is the set corresponding to tset, is between t1 and t2. Expression Finite(tset) stands for the second-order formula

f (Injective(f, tset) N Image(f, tset, 0, N)) where f is a function variable of arity stuple sint. For a term tset of the set sort, we define formula Finite Count(tset) as

T T tset N count(rem(tset, T)) = N count(tset) = N + 1

Using these formulas we can formalize condition 6 with the help of the following three sentences:

count( ) = 0 (21) S (Finite(S) Finite Count(S)) (22) S ( Finite(S) count(S) = sup) (23)

Proposition 3. Let I be an interpretation that satisfies all conditions for being an agg-interpretation except conditions 6 and 7. Then, I satisfies condition 6 iff it satisfies sentences (21-23). The axiomatization of aggregates with the operation sum is similar, but requires characterizing that the set of tuples with non-zero weight is finite (instead of the set of arbitrary tuples). Given a term tset of sort sset and a function symbol f, we define Injective Weight(f, tset) as the formula

T1T2 T1 tset T2 tset weight(T1) = 0

weight(T2) = 0 f(T1) = f(T2) T1 = T2

If the image of f is of sort sprg and t1 and t2 are also terms of sort sprg, we define Image Weight(f, tset, t1, t2) as formula

T T tset weight(T) = 0 t1 f(T) f(T) t2 .

Expression Finite Weight(tset) stands for the second-order formula

f Injective Weight(f, tset) N Image Weight(f, tset, 0, N)

where f is a function variable of arity stuple sint. For a term tset of the set sort, we define formula Finite Sum(tset) as T T tset N(sum(rem(tset, T)) = N sum(tset) = N + weight(T))

We can define sum to have arity sset sint and simplify the formula that stands for Finite Sum(tset) as follows:

T T tset sum(tset) = sum(rem(tset, T)) + weight(T)

Note that a similar simplification cannot be made for count because sometimes it returns sup, which is not of sort int. We also define Zero Weight(tset) as

T (T tset weight(T) = 0) which holds when all members of tset have zero-weight. Using these formulas we can formalize condition 7 with the help of the following three sentences:

S Zero Weight(S) sum(S) = 0 (24)

S (Finite Weight(S) Finite Sum(S)) (25)

S Finite Weight(S) sum(S) = 0 (26)

In particular, note that (24) entails sum( ) = 0.

Proposition 4. Let I be an interpretation that satisfies all conditions for being an agg-interpretation except conditions 6 and 7. Then, I satisfies condition 7 iff it satisfies sentences (24-26). The theorem below follows directly from Propositions 1-4. Symbol p refers to the list of all predicate symbols occurring in Π. Theorem 1. A set of ground atoms M is an answer set of a program Π iff there exists some standard model I of SMp[τ Π] that satisfies all sentences of form (17-26) and M = Ans(I).

First-Order Characterization There is a wide class of programs without aggregates for which the second-order SM operator can be replaced by a first-order formalization. This includes completion in the case of tight programs (Ferraris, Lee, and Lifschitz 2011) or, more generally, loop formulas (Lee and Meng 2011). The same replacement also works for our translation for programs with aggregates. Yet the resulting formula, when we consider the axiomatization approach, is not a first-order formula due to the quantification over function symbols in formulas Finite(tset) and Finite Weight(tset). These formulas are necessary to distinguish between finite and infinite sets. However, in practice, ASP solvers impose restrictions on programs that ensure that programs have finite answer sets and finite aggregates. Formally, we say that an interpretation I has finite aggregates if the set set|E/X|(x)I is finite for every aggregate symbol E/X and any list x of ground program terms of the same length as X. A program Π has finite aggregates if all standard models of SM[τ Π] have finite aggregates. In the rest of this section, we focus on programs with finite aggregates and we disregard how this property is obtained. Given two terms tset, t set of the set sort, we define the formula Subset(tset, t set) as

T T tset T t set

stating that tset is a subset of t set. In the case of programs that have finite aggregates, we can replace sentences (22,23;25,26) by the sentences of the form

X S Subset(S, set|E/X|(X)) Finite Count(S) (27)

X S Subset(S, set|E/X|(X)) Finite Sum(S) (28)

where E/X is an aggregate symbol. Intuitively, sentences (27) and (28) have the same meaning as the pairs of sentences (22,23) and (25,26), respectively, but with some restrictions. First, this formalization is appropriate only if the interpretation of set|E/X|(x) results in a finite set. Furthermore, the interpretation of count and sum is only fixed for subsets of sets corresponding to terms of the form set|E/X|(x). Hence, there may be non standard interpretations that satisfy these sentences, which interpret those symbols differently than their intended meaning when applied to other sets. Interestingly, those sets do not correspond to any term in the theory we are interested in. The reason to include all subsets in these sentences is that Finite Count(S) and Finite Sum(S) recursively refer

to some of their subsets. The following result shows that in the case of programs with finite aggregates we can use the introduced first-order axiomatization. Theorem 2. A set of ground atoms M is an answer set of some program Π with finite aggregates iff there is some standard model I of SMp[τ Π] that satisfies all sentences of form (17-21,24,27,28) and M = Ans(I).

Relation With Abstract Gringo The abstract gringo semantics of logic programs use a translation which turns a program into a set of infinitary propositional formulas (Gebser et al. 2015). These semantics capture the behavior of the answer set solver clingo when it evaluates a program with aggregates. For space reasons, we refer to this work for formal definitions of infinitary propositional formulas and stable models of these formulas. We now present a simplified version of the abstract gringo translation which is equivalent to the original in the studied fragment. A rule or an aggregate (in a rule) is called closed if it has no global variables. An instance of a rule R is any rule that can be obtained from R by substituting ground terms for all global variables. For a closed aggregate element E of form (2) with Y being the list of non-global variables occurring in it, ΨE denotes the set of tuples y of ground program terms of the same length as Y. Let E be an aggregate atom of form (3), be a subset of ΨE and [ ] = {t Y y | y } with t being the tuple t1, . . . , tk . Then, justifies an aggregate atom if relation holds between \ count([ ]) (resp. d sum([ ])) and u. For example, if E is aggregate element 3, X, Y : p(X, Y ), then ΨE is the set of all tuples of ground program terms of length 2. If is { a, b , 5, b }, then [ ] = { 3, a, b , 3, 5, b }. Thus, justifies aggregate atom #sum{3, X, Y :p(X, Y )} 5, but not #sum{3, X, Y :p(X, Y )} 7. The abstract gringo translation τ is defined as follows: 1. for every ground atom A, its translation τA is A itself; τ is , 2. for every ground comparison t1 t2, its translation τ(t1 t2) is if the relation holds between terms t1 and t2 according to the total order selected above and otherwise; 3. for aggregate atom A of form (3), τA is formula

y ΨE\ l Y y

where χ is the set of subsets of ΨE that do not justify A, and l stands for the conjunction τl1 τlm; 4. for every (basic or aggregate) literal L of form not A, its translation τL is τA; if L is of form not not A, its translation τL is τA; 5. for every closed rule R of form (4), its translation τR is the implication

τB1 τBn τHead;

6. for every non-closed rule R, its translation τR is the conjunction of the result of applying τ to all its instances;

7. for every program Π, its translation τΠ is the infinitary theory containing τR for each rule R in Π.

A set of ground atoms A is a gringo answer set of a program Π if A is a stable model of τΠ in infinitary propositional logic.

Theorem 3. The answer sets of any program (whose aggregates have no positive recursion) coincide with its gringo answer sets.

Conclusions and Future Work

In this paper, we have provided a characterization of the semantics of programs with aggregates that bypasses grounding. This is achieved by introducing a translation from logic programs to many-sorted first-order sentences together with an axiomatization in second-order logic. Interestingly, in the studied fragment (programs whose aggregates have no positive recursion), our semantics coincides with the semantics of the widely used solver clingo (Gebser et al. 2015). Furthermore, for many practical programs the second-order axiomatization can be replaced by first-order sentences. This paves the way for the use of first-order theorem provers for reasoning about this class of programs, something that, to the best of our knowledge, was not possible before our characterization. The potential utility of this contribution is best showcased by anthem: a proof assistant that relies on the theorem prover vampire (Kov acs and Voronkov 2013) to check the correctness of clingo programs. Currently, this tool can only be applied to programs without aggregates. This paper opens the door to extend this tool to programs that contain aggregates without positive recursion. This is one of the directions for our future research. Another future line of work is to extend our characterization to programs with positive recursion through aggregates. This is something that requires further study as there are several competing semantics. In addition, we plan to investigate how the methodology for constructing formal arguments about the correctness of logic programs as advocated in (Cabalar, Fandinno, and Lierler 2020) can be extended to programs with aggregates.

Acknowledgements

We would like to thank Vladimir Lifschitz for his valuable feedback on multiple iterations of this project. We also gratefully acknowledge the anonymous reviewers whose comments have improved the quality of this paper.

References Cabalar, P. 2011. Functional answer set programming. Theory and Practice of Logic Programming, 11(2-3): 203 233. Cabalar, P.; Fandinno, J.; Fari nas del Cerro, L.; and Pearce, D. 2018. Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates. Theory and Practice of Logic Programming, 18(3-4): 390 405. Cabalar, P.; Fandinno, J.; and Lierler, Y. 2020. Modular Answer Set Programming as a Formal Specification Language. Theory and Practice of Logic Programming, 20: 767 782.

Cabalar, P.; Fandinno, J.; Schaub, T.; and Schellhorn, S. 2019. Gelfond-Zhang aggregates as propositional formulas. Artificial Intelligence, 274: 26 43. Calimeri, F.; Faber, W.; Gebser, M.; Ianni, G.; Kaminski, R.; Krennwallner, T.; Leone, N.; Ricca, F.; and Schaub, T. 2012. ASP-Core-2: Input language format. Dovier, A.; Pontelli, E.; and Rossi, G. 2003. Intensional Sets in CLP. In Palamidessi, C., ed., Logic Programming, 19th International Conference, ICLP 2003, Mumbai, India, December 9-13, 2003, Proceedings, volume 2916 of Lecture Notes in Computer Science, 284 299. Springer. Faber, W.; Pfeifer, G.; and Leone, N. 2011. Semantics and Complexity of Recursive Aggregates in Answer Set Programming. Artificial Intelligence, 175(1): 278 298. Fandinno, J.; Lifschitz, V.; L uhne, P.; and Schaub, T. 2020. Verifying Tight Logic Programs with anthem and vampire. Theory and Practice of Logic Programming, 5(20): 735 750. Ferraris, P. 2011. Logic programs with propositional connectives and aggregates. ACM Transactions on Computational Logic, 12(4): 25. Ferraris, P.; Lee, J.; and Lifschitz, V. 2011. Stable models and circumscription. Artificial Intelligence, 175(1): 236 263. Fox, D.; and Gomes, C., eds. 2008. Proceedings of the Twenty-third National Conference on Artificial Intelligence (AAAI 08). AAAI Press. Gebser, M.; Harrison, A.; Kaminski, R.; Lifschitz, V.; and Schaub, T. 2015. Abstract Gringo. Theory and Practice of Logic Programming, 15(4-5): 449 463. Gelfond, M.; and Zhang, Y. 2014. Vicious Circle Principle and Logic Programs with Aggregates. Theory and Practice of Logic Programming, 14(4-5): 587 601. Gelfond, M.; and Zhang, Y. 2019. Vicious Circle Principle, Aggregates, and Formation of Sets in ASP Based Languages. Artificial Intelligence, 275: 28 77. Kov acs, L.; and Voronkov, A. 2013. First-Order Theorem Proving and Vampire. In Sharygina, N.; and Veith, H., eds., Proceedings of the Twenty-fifth International Conference on Computer Aided Verification (CAV 13), volume 8044 of Lecture Notes in Computer Science, 1 35. Springer-Verlag. Lee, J.; Lifschitz, V.; and Palla, R. 2008. A Reductive Semantics for Counting and Choice in Answer Set Programming. In (Fox and Gomes 2008), 472 479. Lee, J.; and Meng, Y. 2011. First-Order Stable Model Semantics and First-Order Loop Formulas. J. Artif. Intell. Res., 42: 125 180. Lifschitz, V. 2008. What Is Answer Set Programming? In (Fox and Gomes 2008), 1594 1597. Lifschitz, V. 2019. Answer Set Programming. Springer Publishing Company, Incorporated, 1st edition. ISBN 3030246574. Pearce, D.; and Valverde, A. 2005. A First Order Nonmonotonic Extension of Constructive Logic. Studia Logica, 30(23): 321 346.

Pelov, N.; Denecker, M.; and Bruynooghe, M. 2007. Wellfounded and stable semantics of logic programs with aggregates. Theory and Practice of Logic Programming, 7(3): 301 353. Simons, P.; Niemel a, I.; and Soininen, T. 2002. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2): 181 234. Son, T.; and Pontelli, E. 2007. A Constructive Semantic Characterization of Aggregates in Answer Set Programming. Theory and Practice of Logic Programming, 7(3): 355 375.