Recently, it was shown how to translate logic programs with aggregates into first-order formulas. In combination with the SM operator, this translation can be used to describe the ASP-Core-2 semantics for this class of programs without relying on grounding. In this paper we prove that this same translation can be used to describe the semantics used by the answer set solver clingo when we interpret functions in an intensional way. We also state a similar conjecture regarding the semantics used by the answer set solver dlv. Recall that these solvers extend the ASP-Core-2 semantics to programs that contain recursive aggregates. If this last conjecture is correct, the interpretation of aggregates used by clingo and dlv are exactly the same and the diference in their behaviour arises only from the diferent interpretations of implication (and negation).
Answer set programming (ASP) is a form of declarative logic programming well-suited to solving knowledge-intensive search and optimization problems [1]. Its success relies on the combination of a rich knowledge representation language with eficient solvers. Some of the most useful constructs of this language are aggregates: intuitively, these are functions that apply to sets. The semantics of aggregates have been extensively studied in the literature [2, 3, 4, 5, 6, 7, 8, 9, 10]. 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 program, then the semantics of the propositional program are 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. [11].
Though there are several approaches to describe the semantics of aggregates that bypass the need for grounding, most of these approaches only allow a restricted class of aggregates [12, 13] or use some extension of the logical language [14, 15, 16, 17]. Recently, Fandinno et al. [18] showed how to translate logic programs with aggregates into first-formulas, which, after the application of the SM operator [19] to the result, captures the ASP-Core-2 semantics. Recall that the ASP-Core-2 semantics do not allow recursion through aggregates. Despite the fact that most practical problems can be represented within the restrictions of the ASP-Core-2 semantics, there are some notable execptions that are more naturally represented using recursive aggregates. One of these examples is the Company Control problem, which consists of finding companies that control other companies by (directly or indirectly) owning a majority of its shares. This problem has been encoded in the literature using the following logic program [4, 7, 20, 21, 22]: ctrStk(C1,C1,C2,P) :- ownsStk(C1,C2,P). ctrStk(C1,C2,C3,P) :- controls(C1,C2), ownsStk(C2,C3,P).
controls(C1,C3) :- company(C1), company(C3),
#sum{P,C2 : ctrStk(C1,C2,C3,P)} > 50.
(
In this paper, we show that the translation introduced by Fandinno et al. [18] can also be used for programs with recursive aggregates if we interpret functions in an intensional way [25, 26, 27, 28]. In particular, we focus on the Abstract Gringo [29] generalization of the semantics by Ferraris [6], which is used in the answer set solver clingo, and the semantics by Faber et al. [7], which is used in the answer set solver dlv. More precisely, we prove that the translation introduced by Fandinno et al. [18] coincides with the Abstract Gringo semantics when we interpret the function symbols representing sets according to the semantics for intensional functions by Bartholomew and Lee [28]. For the semantics used by dlv, we introduce a variation of these semantics for intensional functions based on the FLPT semantics [14] and state a similar conjecture, which is matter of ongoing study.
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 is denoted by . 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 and , < if < , and • for any integer and any symbolic constant , < .
An atom is an expression of the form (t), where is a symbolic constant and t is a list of
program terms. A comparison is an expression of the form ≺ ′, where and ′ are program
terms and ≺ is one of the comparison symbols:
= ̸= <
> ≤ ≥
(
#op{} ≺
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
where op is an operation name, is an aggregate element, ≺ is one of the comparison symbols
in (
#sum{P,C2 : ctrStk(C1,C2,C3,P)} > 50
in the body of rule (
A rule is an expression of the form
Head :- 1, . . . , ,
(
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.
Each operation name op is associated with a function 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 then we say that integer is the weight of t, otherwise the weight of t is 0. For any set Δ of tuples of ground terms, • cˆou︂nt(Δ) is the numeral corresponding to the cardinality of Δ, if Δ is finite; and sup otherwise. • ŝu︂m(Δ) 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 ŝu︂m(Δ) = 0. 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 [30].
Many-sorted formulas A many-sorted signature consists of symbols of three kinds—sorts, function constants, and predicate constants. A reflexive and transitive subsort relation is defined on the set of sorts. A tuple 1, . . . , ( ≥ 0) of argument sorts is assigned to every function constant and to every predicate constant; in addition, a value sort is assigned to every function constant. Function constants with = 0 are called object constants.
We assume that for every sort, an infinite sequence of object variables of that sort is chosen. Terms over a (many-sorted) signature are defined recursively: • object constants and object variables of a sort are terms of sort ; • if is a function constant with argument sorts 1, . . . , ( > 0) and value sort , and 1, . . . , are terms such that the sort of is a subsort of ( = 1, . . . , ), then (1, . . . , ) is a term of sort .
Atomic formulas over are • expressions of the form (1, . . . , ), where is a predicate constant and 1, . . . , are terms such that their sorts are subsorts of the argument sorts 1, . . . , of , and • expressions of the form 1 = 2, where 1 and 2 are terms such that their sorts have a common supersort. (First-order) formulas over are formed from atomic formulas and the 0-place connective ⊥ (falsity) using the binary connectives ∧, ∨, → and the quantifiers ∀, ∃. The other connectives are treated as abbreviations: ¬ stands for → ⊥ and ↔ stands for ( → ) ∧ ( → ).
An interpretation of a signature assigns • a non-empty domain || to every sort of , so that ||1 ⊆ | |2 whenever 1 is a subsort of 2, • a function from ||1 × · · · × | | to || to every function constant with argument sorts 1, . . . , and value sort , and • a Boolean-valued function on ||1 × · · · × | | to every predicate constant with argument sorts 1, . . . , .
by adding, for every element of a domain ||, its name * as an object constant of sort . The interpretation is extended to by defining (* ) = . The value assigned by an interpretation of to a ground term over and the satisfaction relation between an interpretation of and a sentence over are defined recursively, in the usual way.
If d is a tuple 1, . . . , of elements of domains of then d* stands for the tuple *1, . . . , * of their names. If t is a tuple 1, . . . , of ground terms then t stands for the tuple 1 , . . . , of values assigned to them by .
In this section, we present translation * that turns a program Π into a first-order sentence
with equality over a signature * (, ) of three sorts where and respectively are sets of
predicate and set symbols. An set symbol is a pair /X, where is an aggregate element and X
is a list of variables occurring in . In the sake of brevity, each set symbol /X is assigned a
short name |/X|. The first sort is called the program sort (denoted prg ); all program terms
are of this sort. The second sort is called the tuple sort (denoted tuple ); it contains entities that
are tuples of objects of the program sort. The second sort is called the set sort (denoted set );
it contains entities that are sets of elements of the second sort, that is, tuples of objects of the
program sort. Signature * (, ) contains:
1. all ground terms as object constants of the program sort;
2. all predicate symbols in with all arguments of program sort;
3. the comparison symbols other than equality as binary predicate constants whose
arguments are of the program sort;
4. predicate constant ∈/2 with the first argument of the sort tuple and the second argument
of the sort set;
5. function constant tuple / with arguments of the program sort and value of the tuple
sort for each set symbol /X in with of the form of (
the program sort and its value is of the set sort and where is the number of variables in X; We use infix notation in constructing atoms that utilize predicate symbols >, ≥ , <, ≤ , ̸= and ∈.
Intuitively, tuple (1, . . . , ) is a constructor for the -tuple containing program terms 1, . . . , .
set of tuples represented2 by xX. The result of count is the cardinality of the set passed as
an argument; the result of sum is the sum of the weights of all elements in the set passed as
an argument. These claims are formalized below. Note also that in contrast to other work
on the theory of stable models that do not consider aggregates (or intensional functions),
expression 1 ̸= 2 is not equivalent to ¬(1 = 2). This is necessary because according to the
Abstract Gringo semantics inequality and the negation of equality are not equivalent when
used in aggregate atoms. For instance, the program consisting of rule
(
p(a) :- #count{X : p(X)} ̸= 0. has the empty set as its unique answer set. On the other hand, this replacement is correct under the dlv semantics and, in fact, both programs have only the empty set as their unique answer set. 2For a tuple X of distinct variables, a tuple x of ground terms of the same length as X, and an expression , by xX we denote the expression obtained from by substituting x for X.
About a predicate symbol /, we say that is occurs in a program Π if there is an atom of the form (1, . . . , ) in Π. For set symbols, we need to introduce first the concepts of a global variable and an set 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.
We say that set symbol /X occurs in rule if this rule contains an aggregate literal with the
aggregate element and X is the list of all variables in that are global in . We say that /X
occurs in a program Π if /X occurs in some rule of the program. For instance, in rule (
In the following, when discussing some program Π, we assume a signature * (, ) such that is a set that contains all predicate symbols occurring in Π and contains all set symbols occurring in Π. When no confusion arises we will simply write * instead of * (, ). In the following, we also assume that is the set of intensional symbols and that the set of intensional functions ℱ is the set of all function symbols corresponding to the set symbols in . Translation * We now describe a translation * that converts a program into a finite set of ifrst-order sentences.
Given a list Z of global variables in some rule , we define Z* for all elements of as follows: 1. for every atomic formula occurring outside of an aggregate literal, its translation Z* is itself; Z*⊥ is ⊥; 2. for an aggregate atom of form #count{} ≺ or #sum{} ≺ , its translation Z* is the atom
count (set |/X|(X)) ≺ or sum(set |/X|(X)) ≺
respectively, where X is the list of variables in Z occurring in ;
3. for every (basic or aggregate) literal of the form not its translation Z*(not ) is ¬ Z*;
for every literal of the form not not its translation Z*(not not ) is ¬¬ Z*.
We now define the translation * as follows:
4. for every rule of form (
For instance, rule (
company (1) ∧ company (3) ∧ sum(set (1, 3)) > 50 → controls(1, 3)
(
To complete the first-order characterization of the Abstract Gringo semantics, we introduce
a set axiom as follows. For each set symbol /X of the form of (
Proposition 1. A standard interpretation of * satisfies (
For instance, the program representing the Company Control problem has a unique set
symbol that is associated with the function symbol set /2. For this function symbol, we have
the first-order sentence
∀13 (︀ ∈ set (1, 3) ↔ ∃ 2( = tuple (, 2) ∧ ctrStk (1, 2, 3, )))︀
(
In this section, we establish the correspondence between the semantics of programs with aggregates introduced in the previous section and the Abstract Gringo [29]. These semantics are stated in terms of infinitary formulas.
Background on Infinitary Formulas We recall some definitions of infinitary logic [ 31]. We denote a propositional signature (a set of propositional atoms) as . For every nonnegative integer , (infinitary propositional) formulas of rank are defined recursively: • every ground atom in is a formula of rank 0, • if Γ is a set of formulas, and is the smallest nonnegative integer that is greater than the ranks of all elements of Γ, then Γ∧ and Γ∨ are formulas of rank , • if and are formulas, and is the smallest nonnegative integer that is greater than the ranks of and , then → is a formula of rank .
We write {, }∧ as ∧ , {, }∨ as ∨ , and ∅∨ as ⊥.
Subsets of a propositional signature will be called interpretations. The satisfaction relation between an interpretation and an infinitary formula is defined recursively: • for every ground atom from , |= if belongs to , • |= Γ∧ if for every formula in Γ, |= , • |= Γ∨ if there is a formula in Γ such that |= , • |= → if ̸|= or |= .
An interpretation satisfies a set Γ of formulas if it satisfies every formula in Γ. We say that a set of atoms is a ⊆ -minimal model of an infinitary formula , if |= and there is no ℬ that satisfies both ℬ |= and ℬ ⊂ .
Stable Models The FT-reduct of an infinitary formula with respect to a set of atoms is defined recursively. If ̸|= then is ⊥; otherwise, • for every ground atom , is • (Γ∧) = { | ∈ Γ}∧, • (Γ∨) = { | ∈ Γ}∨, • ( → ) is → .
We say that a set of ground atoms is a FT-stable model of an infinitary formula if it is a ⊆ -minimal model of . We say that a set of ground atoms is a gringo answer set of a program Π if a FT-stable model of Π where is the translation from logic programs to infinitary formulas defined by Gebser et al. [29].
The first-order characterization of the Abstract Gringo Semantics proposed here relies on the stable model semantics with intensional functions [28]. Our presentation follows the definition in terms of of equilibrium logic [32] described by Bartholomew and Lee [33, Section 3.3]. Stable Model Semantics with Intensional Functions. Let and be two interpretations of a signature and and ℱ respectively be sets of predicate and function constants of . We write ≤ ℱ if • and have the same universe for all sorts; • ⊆ for every predicate constant in and = for every predicate constant not in ; • ̸= for every function constant in and = for every function constant not in ; We write <ℱ if ≤ ℱ and ̸= .
Let and ℱ be sets of predicate and function constant of , that we consider intensional. An ht-interpretation of is a pair ⟨, ⟩, where and are interpretation of such that ≤ ℱ . (In terms of Kripke models with two sorts, is the there-world, and is the here-world of a non-total interpretation). The satisfaction relation |=ℎ between HT-interpretation ⟨, ⟩ of and a sentence over is defined recursively as follows: • ⟨, ⟩ |=ℎ (t), if |= (t) and |= (t); • ⟨, ⟩ |=ℎ 1 = 2 if 1 = 2 and 1 = 2 ; • ⟨, ⟩ ̸|=ℎ ⊥; • ⟨, ⟩ |=ℎ ∧ if ⟨, ⟩ |=ℎ and ⟨, ⟩ |=ℎ ; • ⟨, ⟩ |=ℎ ∨ if ⟨, ⟩ |=ℎ or ⟨, ⟩ |=ℎ ; • ⟨, ⟩ |=ℎ → if (i) |= → , and (ii) ⟨, ⟩ ̸|=ℎ or ⟨, ⟩ |=ℎ , • ⟨, ⟩ |=ℎ ∀ () if ⟨, ⟩ |=ℎ (* ) for each ∈ ||, where is the sort of ; • ⟨, ⟩ |=ℎ ∃ () if ⟨, ⟩ |=ℎ (* ) for some ∈ ||, where is the sort of . If ⟨, ⟩ |=ℎ holds, we say that ⟨, ⟩ satisfies and that ⟨, ⟩ is an ht-model of . If two formulas have the same ht-models then we say that they are ht-equivalent.
An ht-interpretation ⟨, ⟩ is said to be standard if both and are standard.
Proposition 2. A standard ht-interpretation ⟨, ⟩ of * satisfies (
About a model of a set Γ of sentences over we say it is ht-stable if every ht-interpretation ⟨, ⟩ with <ℱ does not satisfy Γ.
Now we define the first-order counterpart of gringo answer sets defined in the previous section. For an interpretation of * , by Ans(), we denote the set of ground atoms that are satisfied by and whose predicate symbol is not a comparison. If is a standard ht-stable model of SCA ∪ * Π, we say that Ans() is a fo-gringo answer set of Π.
Theorem 1. The fo-gringo answer sets of any program coincide with its gringo answer sets.
Similarly to the Abstract Gringo semantics, the dlv semantics can be stated in terms of a the same translation to infinitary formulas, but using a diferent reduct [34].
FLP-stable models are defined for sets of implications rather than arbitrary formulas. Let Γ be a set of infinitary formulas of the form → , where is a disjunction of propositional atoms from . The FLP-reduct (Γ, ) of Γ w.r.t. an interpretation is the set of all formulas → from Γ such that satisfies . A set of ground atoms is an FLP-stable model of Γ if it is a ⊆ -minimal model of (Γ, ). We say that a set of ground atoms is a dlv answer set of a program Π if a FLP-stable model of Π.
First-order characterization of the dlv semantics. For the dlv semantics we introduce a
new entailment relation |=, which is variation of the here-and-there entailment relation |=ℎ
defined above. This relation is defined recursively, analogously to the relation |=ℎ, with the
only diference being the implication case:
• ⟨, ⟩ |= → if
(i) |= → , and
(ii) ̸|= or ̸|= or both |= and |= ;
If ⟨, ⟩ |=ℎ holds, we say that ⟨, ⟩ dlv-staisfies and that ⟨, ⟩ is an dlv-model of .
Proposition 3. A standard ht-interpretation ⟨, ⟩ of * dlv-staisfies (
()xXyY set |/X|(x) is the set of all tuples of form ⟨(1)xXyY, . . . , ()xXyY⟩ such that where x and y are lists of ground program terms of the same length as X and Y respectively.
About a model of a set Γ of sentences, we say it is dlv-stable if there is no ht-interpretation ⟨, ⟩ with <ℱ and ⟨, ⟩ |= Γ. If is a dlv-stable model of SCA ∪ * Π, we say that Ans ( ) is a fo-dlv answer set of Π.
The following conjecture about the relation between dlv answer sets and fo-dlv answer sets is a matter of ongoing work: Conjecture 1. The fo-dlv answer sets of any program coincide with its dlv answer sets.
This work presents a characterization of recursive aggregates that does not rely on grounding. For this, we use the same translation from logic programs to first-order formulas described by Fandinno et al. [35], but we rely on semantics that treat function symbols corresponding to set symbols as intensional. Recall that these functions map ground terms to sets of tuples of ground terms - each of these tuples must satisfy the associated conditions present in the aggregate element. Interestingly, for the semantics of the solver clingo, this particular class of function symbols behaves in a truly analogous way to intensional predicate symbols; namely, the constructed set in the here-world is a subset of the constructed set in the there-world, for any arguments to the function. This is not ordinarily the case for intensional functions nor does it seem to be the case for the semantics of the solver dlv.
Another interesting outcome of this work is Conjecture 1. The implication of this conjecture (if proven) is that the diferences between recursive aggregates in clingo and dlv are not actually rooted in aggregates themselves. In both solvers, aggregates are the same intensional functions on sets of tuples, but which tuples belong to these sets varies between solvers due to diferences in their treatment of implication and negation. The proof of this conjecture is a matter of ongoing work.
The results presented in this paper bring us closer to a long-term goal of using first-order reasoning tools to automatically verify properties of programs with aggregates. The next step is to prove Conjecture 1 and explore its implications. Subsequent future work will include extending results on strong equivalence to the class of programs studied here. [13] V. Lifschitz, Strong equivalence of logic programs with counting, Theory and Practice of
Logic Programming 22 (2022) 573–588. [14] M. Bartholomew, J. Lee, Y. Meng, First-order extension of the flp stable model semantics via modified circumscription., in: T. Walsh (Ed.), Proceedings of the Twenty-second International Joint Conference on Artificial Intelligence (IJCAI’11), IJCAI/AAAI Press, 2011, pp. 724–730. [15] J. Lee, Y. Meng, Stable models of formulas with generalized quantifiers (preliminary report), in: A. Dovier, V. Santos Costa (Eds.), Technical Communications of the Twentyeighth International Conference on Logic Programming (ICLP’12), volume 17, Leibniz International Proceedings in Informatics (LIPIcs), 2012, pp. 61–71. [16] V. Asuncion, Y. Chen, Y. Zhang, Y. Zhou, Ordered completion for logic programs with aggregates, Artificial Intelligence 224 (2015) 72–102. [17] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, D. Pearce, Functional ASP with intensional sets: Application to Gelfond-Zhang aggregates, Theory and Practice of Logic Programming 18 (2018) 390–405. [18] J. Fandinno, Z. Hansen, Y. Lierler, Axiomatization of aggregates in answer set programming, in: Proceedings of the Thirty-sixth National Conference on Artificial Intelligence (AAAI’22), AAAI Press, 2022, pp. 5634–5641. [19] P. Ferraris, J. Lee, V. Lifschitz, Stable models and circumscription, Artificial Intelligence 175 (2011) 236–263. [20] I. Mumick, H. Pirahesh, R. Ramakrishnan, The magic of duplicates and aggregates, in: D. McLeod, R. Sacks-Davis, H. Schek (Eds.), Proceedings of the Sixteenth International Conference on Very Large Data Bases (VLDB’90), Morgan Kaufmann Publishers, 1990, pp. 264–277. [21] D. Kemp, P. Stuckey, Semantics of logic programs with aggregates, in: V. Saraswat, K. Ueda (Eds.), Proceedings of the 1991 International Symposium on Logic Programming (ISLP’91), MIT Press, 1991, pp. 387–401. [22] K. Ross, Y. Sagiv, Monotonic aggregation in deductive databases, Journal of Computer and System Sciences 54 (1997) 79–97. [23] V. Lifschitz, D. Pearce, A. Valverde, Strongly equivalent logic programs, ACM Transactions on Computational Logic 2 (2001) 526–541. [24] V. Lifschitz, D. Pearce, A. Valverde, A characterization of strong equivalence for logic programs with variables, in: C. Baral, G. Brewka, J. Schlipf (Eds.), Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’07), volume 4483 of Lecture Notes in Artificial Intelligence , Springer-Verlag, 2007, pp. 188–200. [25] F. Lin, Y. Wang, Answer set programming with functions, in: G. Brewka, J. Lang (Eds.), Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR’08), AAAI Press, 2008, pp. 454–465. [26] P. Cabalar, Functional answer set programming, Theory and Practice of Logic Programming 11 (2011) 203–233. [27] M. Balduccini, ASP with non-herbrand partial functions: A language and system for practical use, Theory and Practice of Logic Programming 13 (2013) 547–561. [28] M. Bartholomew, J. Lee, First-order stable model semantics with intensional functions,
Lemma 1. Let be an aggregate element of the form (
Proof. satisfies (13) if condition 1 is equivalent to: satisfies ∃Y ( = tuple (′1, . . . , ′) ∧ 1′ ∧ · · · ∧ Furthemore, the latter holds if there is a list c of domain elements of sort prg such that tuple = tuple (′1′, . . . , ′′) = tuple (′1′, . . . , ′′) = ⟨(′1′) , . . . , (′′) ⟩ and satisfies 1′′ ∧ · · · ∧
′′ with y = c* if condition 2 holds.
Lemma 2. Let be an aggregate element of the form (
Right-to-left. Assume that set ||(x) is the set of all tuples of the form ⟨(′1′) , . . . , (′′) ⟩ such that satisfies 1′′ ∧ · · · ∧ ′′ for some list y of ground terms of sort prg of the same length as Y. Pick any domain element tuple of sort tuple . By Lemma 1, satisfies (13) and, thus, satisfies (14).
Proof of Proposition 1. Pick any list c of domain elements of sort prg and let x = c* . Then, the result follows directly by Lemma 2.
Lemma 3. ⟨, ⟩ |=ℎ ↔ if • |= ↔ , and • ⟨, ⟩ |=ℎ if ⟨, ⟩ |=ℎ .
Proof. ⟨, ⟩ |=ℎ ↔ if ⟨, ⟩ |=ℎ → and ⟨, ⟩ |=ℎ → if both • |= → and either ⟨, ⟩ ̸|=ℎ or ⟨, ⟩ |=ℎ , and • |= → and either ⟨, ⟩ ̸|=ℎ or ⟨, ⟩ |=ℎ if if • |= → and |= → , and • either ⟨, ⟩ ̸|=ℎ or ⟨, ⟩ |=ℎ , and • either ⟨, ⟩ ̸|=ℎ or ⟨, ⟩ |=ℎ • |= ↔ , and • ⟨, ⟩ |=ℎ if ⟨, ⟩ |=ℎ .
Lemma 4. If ⟨, ⟩ is a standard ht-interpretation, then set |/X|(x) is a subset of set /X(x) for every set symbol /X and list x of ground terms of the same length as X.
Proof. Pick any element tuple of set |/X|(x) . Since ⟨, ⟩ is a standard ht-interpretation, it
follows that is a standard interpreation and, thus, that the pair (tuple , set |/X|(x) ) belongs
to ∈ . Hence, (tuple , set |/X|(x) ) also belongs to ∈ and, thus, tuple of set |/X|(x) .
Lemma 5. Let be an aggregate element of the form (
Proof. From Lemma 3, ⟨, ⟩ satisfies (13) if satisfies (13) and the following two conditions are equivalent: 5. ⟨, ⟩ satisfies *tuple ∈ set ||(x); 6. ⟨, ⟩ satisfies ∃Y ( = tuple (′1, . . . , ′) ∧ 1′ ∧ · · · ∧ Furthemore, by Lemma 1, satisfies (13) if Conditions 1 and 2 are equivalent. Hence, ⟨, ⟩ satisfies (13) if Conditions 1 and 2 are equivalent, and Conditions 5 and 6 are equivalent.
On the one hand, condition 6 is equivalent to conjuntion of conditions 1 and 3. On the other hand, condition 6 holds if there is a list c of domain elements of sort prg such that tuple = tuple (′1′, . . . , ′′) = tuple (′1′, . . . , ′′) = ⟨(′1′) , . . . , (′′) ⟩ and ⟨, ⟩ satisfies 1′′ ∧ · · · ∧ ifes (13) if
′′ with y = c* if condition 4 holds. Therefore, ⟨, ⟩ satis• Conditions 1 and 2 are equivalent, and • Condition 4 is equivalent to the conjunction of conditions 1 and 3.
Finally, note that by Lemma 4 condition 3 implies 1 and the result holds.
Lemma 6. Let be an aggregate element of the form (
Proof. Left-to-right. Assume that ⟨, ⟩ satisfies (14) and pick any domain element tuple of sort tuple . Then, ⟨, ⟩ satisfies (13) and the result follows immediately by Lemma 5. Right-to-left. Pick any domain element tuple of sort tuple. The conditions of Lemma 5 are satisfied and the result follows by this lemma.
Proof of Proposition 2. Pick any list c of domain elements of sort prg and let x = c* . Then, the result follows directly by Lemma 2.
A.1. Proof of Theorem 1 First-order interpretations and infinitary formulas. We can extend the satisfaction relation for ht-interpretations can be extended to infinitary formulas by adding the following two conditions to the definition for first-order formulas: • ⟨, ⟩ |=ℎ Γ∧ if for every formula in Γ, ⟨, ⟩ |=ℎ , • ⟨, ⟩ |=ℎ Γ∨ if there is a formula in Γ such that ⟨, ⟩ |=ℎ , We write |= if ⟨ , ⟩ |=ℎ .
In the following, if is an interpretation, then ℐ denotes the set of ground atomic formulas satisfied by .
Proposition 4. Let be a propositional signature consisting of all the ground atomic formulas of first-order signature . Let be a an infinitary formula of . Then,
|= ⟨, ⟩ |=ℎ if if ℐ |= ℋ |= ℐ Proof. We proceed by induction on the rank of . For a formula of rank + 1, assume that, for all formulas of lesser rank than occurring in , ⟨, ⟩ |=ℎ if ℋ |= ℐ . Base Case: = 0, is a ground atomic formula. Then, ⟨, ⟩ |=ℎ if |= and |= if |= and ℐ = if ℋ |= ℐ Induction Step:
Case 1: Formula of rank + 1 has form Γ∧. Then, ⟨, ⟩ |=ℎ if ⟨, ⟩ |=ℎ for every formula in Γ if ℋ |= ℐ for every formula in Γ if ℋ |= {ℐ | ∈ Γ}∧ if ℋ |= ℐ
Case 2: Formula of rank + 1 has form Γ∨. Then, ⟨, ⟩ |=ℎ if ⟨, ⟩ |=ℎ for some formula in Γ if ℋ |= ℐ for this certain formula in Γ if ℋ |= {ℐ | ∈ Γ}∨ if ℋ |= ℐ (by definition) (by induction hypothesis)
(by definition) (by induction hypothesis)
Case 3: Formula of rank + 1 has form 1 → 2. Then, ⟨, ⟩ |=ℎ if |= 1 → 2 and ⟨, ⟩ ̸|=ℎ 1 or ⟨, ⟩ |=ℎ 2 if ⟨, ⟩ |=ℎ 1 → 2 and ⟨, ⟩ ̸|=ℎ 1 or ⟨, ⟩ |=ℎ 2 if ℐ |= 1ℐ → 2ℐ and ℋ ̸|= 1ℐ or ℋ |= 2ℐ if ℐ |= 1 → 2 and ℋ ̸|= 1ℐ or ℋ |= 2ℐ if ℐ |= 1 → 2 and ℋ |= 1ℐ → 2ℐ if ℐ = 1ℐ → 2ℐ and ℋ |= 1ℐ → 2ℐ if ℋ |= ℐ (by definition) (by definition) (by induction hypothesis)
An interpretation that satisfies the condition of Proposition 1 for every set symbol /X in is called an agg-interpretation. Similarly, a ht-interpretation that satisfies the condition of Proposition 2 for every set symbol /X in is called an agg-ht-interpretation. A model that is an agg-interpretation is called an agg-model and a ht-model that is an agg-ht-interpretation is called an agg-ht-model.
Lemma 7. Let ⟨, ⟩ be an agg-ht-interpretation. Then, <ℱ if <∅ . Proof. Right-to-left. <∅ means that there is a predicate symbol such that ⊂ and, thus, <ℱ also holds. Lert-to-right. <ℱ means that on of the following holds • ⊂ for some intensional predicate symbol ; or • ̸= for some intensional function symbol .
The first immediately implies that <∅ also holds. For the latter, must be of the form set |/X| for some aggregate element . Therefore, the set of the set of all tuples of form ⟨(1)xXyY, . . . , ()xXyY⟩ such that satisfies (1)xXyY ∧ · · · ∧ ()xXyY and the set of all tuples of form ⟨(1)xXyY, . . . , ()xXyY⟩ such that ⟨, ⟩ satisfies (1)xXyY ∧· · ·∧ ()xXyY must be diferent. This means that ̸= for some predicate symbols and, thus, ⊂ and <∅ follow.
We say that an agg-model of an infinitary formula is an FT-agg-stable model of if there is no agg-ht-interpretation ⟨, ⟩ with <ℱ such that ⟨, ⟩ satisfies .
In the following two Lemmas, is an agg-interpretationand ℐ is the set of ground atomic formulas satisfied by .
Lemma 8. If ℐ is a FT-stable model of , then is a FT-agg-stable model of . Proof. Since is a FT-stable model of , we get that satisfies and, thus, is an agg-model of . Suppose, for the sake of contradiction, that there is an agg-ht-interpretation ⟨, ⟩ with <ℱ such that ⟨, ⟩ satisfies . Then, by Proposition 4, it follows that ℋ |= ℐ . Furthermore, by Proposition 7, it follows that <∅ and, thus, ℋ ⊂ ℐ . This is a contradiction with the assumption that ℐ is a FT-stable model of .
Lemma 9. Let be a an infinitary formula that does not contain function symbols corresponding to set symbols. Then, ℐ is a FT-stable model of if is FT-agg-stable model of Proof. The left-to-right direction follows by Lemma 8. For the right-to-left direction, assume that is an FT-agg-stable model of . Then, satisfies and, by Proposition 4, it follows that ℐ is a model of . Suppose, for the sake of contradiction, that ℐ is a FT-stable model of . Then, there is some model of ℐ such that ⊂ ℐ . Let be an agg-interpretation such that • has the same domain as , • for every ground atomic formula (t) that does not function symbols corresponding to set symbols, (t) is true if (t) belongs to .
Then, <∅ and, from Proposition 7, we get that <ℱ . Since is an FT-agg-stable model of , it follows that ⟨, ⟩ ̸|=ℎ . From Proposition 4, this implies that ℋ ̸|= ℐ where ℋ is the set of ground atomic formulas satisfied by . However, and ℋ agree on all atoms occurring in , so this is a contradiction with the fact that is a model of ℐ . Infinitary grounding The grounding of a first order sentence with respect to an interpretation and sets and ℱ of intensional predicate and function symbols is defined as follows: • gr ℱ (⊥) = ⊥; • gr ℱ ((t)) = ((t )* ) if (t) contains intensional symbols; • gr ℱ ((t)) = ⊤ if (t) does not contain intensional symbols and |= (t); and gr ℱ ((t)) = ⊥ otherwise; • gr ℱ (1 = 2) = (1 = 2) if 1 or 2 contain intensional symbols; • gr ℱ (1 = 2) = ⊤ if 1 and 2 do not contain intensional symbols and 1 = 2 and ⊥ otherwise; • gr ℱ ( ⊗ ) = gr ℱ ( ) ⊗ gr ℱ () if ⊗ is ∧, ∨, or →; • gr ℱ (∃ ()) = {gr ℱ ( ()) | ∈ ||}∨ if is a variable of sort ; • gr ℱ (∀ ()) = {gr ℱ ( ()) | ∈ ||}∧ if is a variable of sort ; For a first order theory Γ, we define gr ℱ (Γ) = {gr ℱ ( ) | ∈ Γ}∧.
In the following, we write gr ( ) instead of gr ℱ ( ) when clear by the context. Lemma 10. An interpretation satisfies a sentence over if satisfies gr ( ). Proof. By induction on .
Case 1: is an atomic sentence. Then, gr ( ) = and the result is trivial.
Case 2: is ∀() with a variable of sort . Then, gr ( ) = {gr ((* )) | * ∈ ||}∧ and
⟨, ⟩ |=ℎ if ⟨, ⟩ |=ℎ (* ) for each ∈ || if ⟨, ⟩ |=ℎ gr ((* )) for each ∈ || (induction) if ⟨, ⟩ |=ℎ gr ( ).
The case where is ∃() is analogous to Case 2. The remaining cases where is 1 ∧ 2, 1 ∨ 2 or 1 → 2 follow immediately by induction.
Lemma 11. An ht-interpretation ⟨, ⟩ satisfies a sentence over if ⟨, ⟩ satisfies gr ( ). Lemma 12. Let Γ be a set of first-order sentences. Then, is a agg-stable model of Γ if is an FT-agg-stable model of gr (Γ).
Proof. First, note that by Lemma 10, it follows that is agg-model of Γ if is an agg-interpretation and |= Γ if is agg-modelof gr (Γ). Then, is a agg-stable model of Γ if there is no ⟨, ⟩ with <ℱ that satisfies Γ if there is no ⟨, ⟩ with <ℱ that satisfies gr (Γ) (Lemma 11) if is a FT-agg-stable model of gr (Γ).
Lemma 13. Let be an agg-interpretation and op be an operation name.
Then, satisfies op(set |/X|(x)) ≺ if satisfies
⎛ ⋀︁ ⎜ ⋀︁ lxXyY →
⎝ Δ∈ y∈Δ
⋁︁
⎞ lxXyY⎟⎠ (15) where is the set of subsets Δ of ΨxX that do not justify aggregate atom op{xX} ≺ . Proof. Let Y be the list of variables occurring in that do not occur in X. Let Δ = { y ∈ ΨxX | |= lxXyY } and be the formula Then, ̸|= and Consequently, we have ⋀︁ lxXyY → y∈Δ
⋁︁ y∈Ψ∖Δ
lxXyY set |/X|(x) = {txXyY | y ∈ Δ } = [Δ ]. |= (15) if is not a conjunctive term of (15) if Δ justifies op(set |/X|(x)) ≺ if |= op|([Δ ]* ) ≺ if |= op(set |/X|(x)) ≺ Lemma 14. Let ⟨, ⟩ be an agg-ht-interpretation and op be an operation name. Then, ⟨, ⟩ satisfies op(set |/X|(x)) ≺ if ⟨, ⟩ satisfies
⎛ Δ∈
y∈Δ ⋀︁ ⎜ ⋀︁ lxXyY → ⎝
⋁︁ where is the set of subsets Δ of ΨxX that do not justify aggregate atom op{xX} ≺ .
Case 1: ̸|= . By Lemma 13, it follows that ̸|= (16). Therefore, ⟨, ⟩ ̸|=ℎ and ⟨, ⟩ ̸|=ℎ (16). Case 2: |= . By Lemma 13, it follows that |= (16). Let and ⟨,⟩ be the formula Then, ⟨, ⟩ ̸|= ⟨,⟩ and Consequently, we have Δ⟨,⟩ = { y ∈ ΨxX | ⟨, ⟩ |=ℎ lxXyY }
⋀︁ y∈Δ⟨,⟩ lxXyY →
⋁︁ y∈Ψ∖Δ⟨,⟩
lxXyY set |/X|(x) = {txXyY | y ∈ Δ⟨,⟩} = [Δ⟨,⟩]. ⟨, ⟩ |= (16) if |= (16) and
⟨,⟩ is not a conjunctive term of (16) if ⟨,⟩ is not a conjunctive term of (16) if Δ⟨,⟩ justifies op(set |/X|(x)) ≺ if |= op|([Δ⟨,⟩]* ) ≺ if |= op(set |/X|(x)) ≺ if |= if ⟨, ⟩ |= Lemma 15. Let Π be a program, be the set of all predicate symbols in * other than comparisons, ℱ be the set of all function symbols corresponding set symbols. Then, ⟨, ⟩ |=ℎ Π if
⟨, ⟩ |=ℎ gr ℱ ( * Π) for every agg-ht-interpretation ⟨, ⟩.
Proof. Recall that comparisons are not intensional in the definition of the stable models of a program, that is, they do not belong to . Then, it is easy to see that Π can be obtained from gr ℱ ( * Π) by replacing each occurrence of op(set |/X|(x)) ≺ , where op is an operation name, by its corresponding formula of the form of (15): Here is the set of subsets Δ of ΨxX that do not justify op(set |/X|(x)). Hence, it is enough to show that ⟨, ⟩ |=ℎ op(set |/X|(x) ≺ ) if ⟨, ⟩ |=ℎ (15) This follows from Lemma 15.
In the following two Lemmas, Π is a program, is the set of all predicate symbols in * other than comparisons, ℱ is the set of all function symbols corresponding set symbols, and let be an agg-interpretation.
Lemma 16. is an FT-agg-stablemodel of Π if it is an FT-agg-stablemodel of gr ( * Π). Proof. By Lemma 15, Π and gr ( * Π) have the same agg-ht-models.
Lemma 17. ℐ is an FT-stable model of Π if is an agg-stable model of * Π.
Proof. ℐ is an FT-stable model of Π if is an FT-agg-stable model of Π if is an FT-agg-stable model of gr ( * Π) if is an agg-stable model of * Π.
(Lemma 9) (Lemma 16) (Lemma 12) Lemma 18. A set of ground atoms is an FT-stable model of Π if there is some agg-stable model of * Π such that = Ans().
Proof. The right-to-left direction follows directly from Lemma 17 by taking noting that there are no comparison symbols in Π. For the left-to-right direction let be an agg-interpretation such that (t) is true if (t) belongs to . Then, is the set of all ground atoms in ℐ that do not contain comparison symbols and, since Π does not contain comparison symbols, it follows that ℐ is a FT-stable model of Π too. The result follows now by Lemma 17.
Lemma 19. is a stable model of SCA ∪ Γ if is a agg-stable model of Γ.
Proof. By definition, is a agg-stable model of Γ if is an agg-model of Γ and there is no agg-ht-interpretation ⟨, ⟩ with <ℱ such that ⟨, ⟩ satisfies Γ if (Propositions 1 and 2) if is a model of SCA ∪ Γ and there is no agg-ht-interpretation ⟨, ⟩ with <ℱ such that ⟨, ⟩ satisfies SCA ∪ Γ if is a stable model of SCA ∪ Γ.
Proof of Theorem 1. Let Π be a program. Then,
is a gringo answer set of Π. if is an FT-stable model of Π if (Lemma 18) there is an agg-stable model of * Π such that Ans() = if (Lemma 19) there is an stable model of SCA ∪ * Π such that Ans() = if is a fo-gringo answer set of Π Lemma 20. ⟨, ⟩ |= ↔ if
Proof. ⟨, ⟩ |= ↔ if ⟨, ⟩ |= → and ⟨, ⟩ |= → if both • |= → and either ̸|= or ̸|= or both |= and |= , and • |= → and either ̸|= or ̸|= or both |= and |= ; • |= → and |= → , and • either ̸|= or ̸|= or both |= and |= , and • either ̸|= or ̸|= or both |= and |= ; • |= ↔ , and • |= and |= implies |= and |= , and • |= and |= implies |= and |= ; • |= ↔ , and • |= implies |= , and • |= implies |= ; • |= ↔ , and • |= ↔ .
Lemma 21. Let be an aggregate element of the form (
Proof. From Lemma 20, ⟨, ⟩ dlv-staisfies (13) if both and satisfy (13). The result follows now by Lemma 1.
Proof of Proposition 3. Pick any list c of domain elements of sort prg and let x = c* . Then, the result follows directly by Lemma 21.