{'fraction_non_alphanumeric': 0.06040671567085204, 'fraction_numerical': 0.009209736006635586, 'mean_word_length': 3.6017372992892867, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Semantics and Compilation of Answer Set Programming with Generalized Atoms

Answer Set Programming (ASP) is logic programming under the stable model or answer set semantics. During the last decade, this paradigm has seen several extensions by generalizing the notion of atom used in these programs. Among these, there are aggregate atoms, HEX atoms, generalized quantifiers, and abstract constraints. In this paper we refer to these constructs collectively as generalized atoms. The idea common to all of these constructs is that their satisfaction depends on the truth values of a set of (non-generalized) atoms, rather than the truth value of a single (non-generalized) atom. Motivated by several examples, we argue that for some of the more intricate generalized atoms, the previously suggested semantics provide unintuitive results and provide an alternative semantics, which we call supportedly stable or SFLP answer sets. We show that it is equivalent to the major previously proposed semantics for programs with convex generalized atoms, and that it in general admits more intended models than other semantics in the presence of non-convex generalized atoms. We show that the complexity of supportedly stable models is on the second level of the polynomial hierarchy, similar to previous proposals and to stable models of disjunctive logic programs. Given these complexity results, we provide a compilation method that compactly transforms programs with generalized atoms in disjunctive normal form to programs without generalized atoms. Variants are given for the new supportedly stable and the existing FLP semantics, for which a similar compilation technique has not been known so far.


Introduction
Answer Set Programming (ASP) is a widely used problemsolving framework based on logic programming under the stable model semantics. The basic language relies on Datalog with negation in rule bodies and possibly disjunction in rule heads. When actually using the language for representing practical knowledge, it became apparent that generalizations of the basic language are necessary for usability. Among the suggested extensions are aggregate atoms (similar to aggregations in database queries) (Niemelä, Simons, and Soininen 1999;Niemelä and Simons 2000;Dell'Armi et al. 2003;Faber et al. 2008) and atoms that rely on external truth valuations (Calimeri, Cozza, and Ianni 2007;Eiter et al. 2004;Eiter et al. 2005). These extensions are characterized by the fact that deciding the truth values of the new kinds of atoms depends on the truth values of a set of traditional atoms rather than a single traditional atom. We will refer to such atoms as generalized atoms, which cover also several other extensions such as abstract constraints, generalized quantifiers, and HEX atoms.
Concerning semantics for programs containing generalized atoms, there have been several different suggestions. All of these appear to coincide for programs that do not contain generalized atoms in recursive definitions. The two main semantics that emerged as standards are the PSP semantics defined in (Pelov 2004;Pelov, Denecker, and Bruynooghe 2007) and (Son and Pontelli 2007), and the FLP semantics defined in (Faber, Leone, and Pfeifer 2004;Faber, Leone, and Pfeifer 2011).
In a recent paper (Alviano and Faber 2013) the relationship between these two semantics was analyzed in detail; among other, more intricate results, it was shown that the semantics coincide up to convex generalized atoms. It was already established earlier that each PSP answer set is also an FLP answer set, but not vice versa. So for programs containing non-convex generalized atoms, some FLP answer sets are not PSP answer sets. In particular, there are programs that have FLP answer sets but no PSP answer sets.
In this paper, we argue that the FLP semantics is still too restrictive, and some programs that do not have any FLP answer set should instead have answer sets. In order to illustrate the point, consider a coordination game that is remotely inspired by the prisoners' dilemma. There are two players, each of which has the option to confess or defect. Let us also assume that both players have a fixed strategy already, which however still depends on the choice of the other player as well. In particular, each player will confess exactly if both players choose the same option, that is, if both players confess or both defect. The resulting program is P 1 in Example 2, where a means that the first player confesses and b means that the second player confesses. As will be explained later, the FLP semantics does not assign any answer set to this program, and therefore also the PSP semantics will not assign any answer sets to this program. However, this is peculiar, as the scenario in which both players confess seems like a reasonable one; indeed, even a simple inflationary operator would result in this solution.
Looking at the reason why this is not an FLP answer set, we observe that it has two countermodels that prevent it from being an answer set: One in which only the first player confesses, and another one in which only the second player confesses. Both of these countermodels are models in the classical sense, but they are weak in the sense that they are not supported, meaning that there is no rule justifying their truth. This is a situation that does not occur for aggregate-free programs, which always have supported countermodels. We argue that one needs to look at supported countermodels, instead of looking at minimal countermodels. It turns out that doing this yields the same results not only for aggregate-free programs, but also for programs containing convex aggregates, which we believe is the reason why this issue has not been noticed earlier.
In this paper, we define a new semantics along these lines and call it supportedly stable or SFLP (supportedly FLP) semantics. It provides answer sets for more programs than FLP and PSP, but is shown to be equal on convex programs. Analyzing the computational complexity of the new semantics, we show that it is in the same classes as the FLP and PSP semantics when considering polynomial-time computable generalized atoms. It should also be mentioned that the new semantics has its peculiarities, for instance adding "tautological" rules like a ← a can change the semantics of the program.
This complexity result directly leads us to the second contribution of this paper. While it has been known for quite some time that the complexity of programs with generalized atoms (even without disjunctions) is equal to the complexity of disjunctive programs, no compact transformation from programs with generalized atoms to disjunctive standard programs is known yet. We provide a contribution with this respect and show how to achieve such a compact compilation for both FLP and SFLP semantics when non-convex aggregates are in disjunctive normal form. It hinges on the use of disjunction and fresh symbols to capture satisfaction of a generalized atom.
The remainder of this paper is structured as follows. In the next section, we present the syntax and FLP semantics for programs with generalized atoms. After that, we analyze issues with the FLP semantics and define the SFLP semantics, followed by a section that proves several useful properties of the new semantics. The subsequent section then deals with compiling programs with generalized atoms into generalized-atom-free programs, followed by conclusions.

Syntax and FLP Semantics
In this section we present the syntax used in this paper and present the FLP semantics (Faber, Leone, and Pfeifer 2004;Faber, Leone, and Pfeifer 2011). To ease the presentation, we will directly describe a propositional language here. This can be easily extended to the more usual ASP notations of programs involving variables, which stand for their ground versions (that are equivalent to a propositional program).

Syntax
Let B be a countable set of propositional atoms. Definition 1. A generalized atom A on B is a mapping from 2 B to Boolean truth values. Each generalized atom A has an associated, finite 1 domain D A ⊆ B, indicating those propositional atoms that are relevant to the generalized atom. Example 1. A generalized atom A 1 modeling a conjunction a 1 , . . . , a n (n ≥ 0) of propositional atoms is such that D A 1 = {a 1 , . . . , a n } and, for every I ⊆ B, A 1 maps I to true if and only if D A 1 ⊆ I. A generalized atom A 2 modeling a conjunction a 1 , . . . , a m , ∼a m+1 , . . . , ∼a n (n ≥ m ≥ 0) of literals, where a 1 , . . . , a n are propositional atoms and ∼ denotes negation as failure, is such that D A 2 = {a 1 , . . . , a n } and, for every I ⊆ B, A 2 maps I to true if and only if {a 1 , . . . , a m } ⊆ I and {a m+1 , . . . , a n } ∩ I = ∅.
A generalized atom A 3 modeling an aggregate COUNT ({a 1 , . . . , a n }) = k (n ≥ k ≥ 0), where a 1 , . . . , a n are propositional atoms, is such that D A 3 = {a 1 , . . . , a n } and, for every I ⊆ B, A 3 maps I to true if and only if |D A 3 ∩ I| = k.
In the following, when convenient, we will represent generalized atoms as conjunctions of literals or aggregate atoms. Subsets of B mapped to true by such generalized atoms will be those satisfying the associated conjunction. Definition 2. A general rule r is of the following form: where H(r) is a disjunction a 1 ∨ · · · ∨ a n (n ≥ 0) of propositional atoms in B referred to as the head of r, and B(r) is a generalized atom on B called the body of r. For convenience, H(r) is sometimes considered a set of propositional atoms. A general program P is a set of general rules. Example 2. Consider the following rules: The following are general programs: P 1 := {r 1 ; r 2 } P 2 := {r 1 ; r 2 ; a ← b; b ← a} P 3 := {r 1 ; r 2 ; ← ∼a; ← ∼b} P 4 := {r 1 ; r 2 ; a ∨ b ←} P 5 := {r 1 ; r 2 ; a ← ∼b}

FLP Semantics
An interpretation I is a subset of B. I is a model for a generalized atom A, denoted I |= A, if A maps I to true. Otherwise, if A maps I to false, I is not a model of A, denoted I |= A. I is a model of a rule r of the form (1), denoted I |= r, if H(r) ∩ I = ∅ whenever I |= B(r). I is a model of a program P , denoted I |= P , if I |= r for every rule r ∈ P .
Generalized atoms can be partitioned into two classes according to the following definition.
Definition 3 (Convex Generalized Atoms). A generalized atom A is convex if for all triples I, J, K of interpretations such that I ⊂ J ⊂ K, I |= A and K |= A implies J |= A.
Note that convex generalized atoms are closed under conjunction (but not under disjunction or negation). A convex program is a general program whose rules have convex bodies.
We now describe a reduct-based semantics, usually referred to as FLP, which has been introduced and analyzed in (Faber, Leone, and Pfeifer 2004;Faber, Leone, and Pfeifer 2011). Definition 4 (FLP Reduct). The FLP reduct P I of a program P with respect to I is defined as the set {r ∈ P | I |= B(r)}.
Definition 5 (FLP Answer Sets). I is an FLP answer set of P if I |= P and for each J ⊂ I it holds that J |= P I . Let F LP (P ) denote the set of FLP answer sets of P . where {a} ⊂ {a, b}. We will discuss in the next section why this is a questionable situation. Concerning P 2 , it has one model, namely {a, b}, which is also its unique FLP answer set. Indeed, and hence the only model of P

SFLP Semantics
As noted in the introduction, the fact that P 1 has no FLP answer sets is striking. If we first assume that both a and b are false (interpretation ∅), and then apply a generalization of the well-known one-step derivability operator, we obtain truth of both a and b (interpretation {a, b}). Applying this operator once more again yields the same interpretation, a fix-point. {a, b} is also a supported model, that is, for all true atoms there exists a rule in which this atom is the only true head atom, and in which the body is true. It is instructive to examine why this seemingly robust model is not an FLP answer set. Its reduct is equal to the original program, P {a,b} 1 = P 1 . There are therefore two models of P 1 , {a} and {b}, that are subsets of {a, b} and therefore inhibit {a, b} from being an FLP answer set. The problem is that, contrary to {a, b}, these two models are rather weak, in the sense that they are not supported. Indeed, when considering {a}, there is no rule in P 1 such that a is the only true atom in the rule head and the body is true in {a}: The only available rule with a in the head has a false body. The situation for {b} is symmetric.
It is somewhat counter-intuitive that a model like {a, b} should be inhibited by two weak models like {a} and {b}. Indeed, this is a situation that normally does not occur in ASP. For programs that do not contain generalized atoms, whenever one finds a J ⊆ I such that J |= P I there is for sure also a K ⊆ I such that K |= P I and K is supported. Indeed, we will show in the following section that this is the case also for programs containing only convex generalized atoms. Our feeling is that since such a situation does not happen for a very wide set of programs, it has been overlooked so far.
We will now attempt to repair this kind of anomaly by stipulating that one should only consider supported models for finding inhibitors of answer sets. In other words, one does not need to worry about unsupported models of the reduct, even if they are subsets of the candidate. Let us first define supported models explicitly.
Definition 6 (Supportedness). A model I of a program P is supported if for each a ∈ I there is a rule r ∈ P such that I ∩ H(r) = {a} and I |= B(r). In this case we will write I |= s P .
Example 4. Continuing Example 3, programs P 1 , P 2 , and P 3 have one supported model, namely {a, b}. The model {a} of P 1 is not supported because the body of the the rule with a in the head has a false body with respect to {a}. For a symmetric argument, model {b} of P 1 is not supported either. The supported models of P 4 , instead, are {a}, {b}, and {a, b}, so all models of the program are supported. Note that both models {a} and {b} have the disjunctive rule as the only supporting rule for the respective single true atom, while for {a, b}, the two rules with generalized atoms serve as supporting rules for a and b. Finally, the supported models of P 5 are {a} and {a, b}.
We are now ready to formally introduce the new semantics. In this paper we will normally refer to it as SFLP answer sets or SFLP semantics, but also call it supportedly stable models occasionally. Definition 7 (SFLP Answer Sets). I is a supportedly FLP answer set (or SFLP answer set, or supportedly stable model) of P if I |= s P and for each J ⊂ I it holds that J |= s P I . Let SF LP (P ) denote the set of SFLP answer sets of P . Example 5. Consider again the programs from Example 2. Recall that P 1 has only one supported model, namely {a, b}, and P = P 1 . The programs, models, FLP answer sets, supported models, and SFLP answer sets are summarized in Table 1.
An alternative, useful characterization of SFLP answer sets can be given in terms of Clark's completion (Clark 1978). In fact, it is well-known that supported models of a program are precisely the models of its completion. We define this notion in a somewhat non-standard way, making use of the concept of generalized atom.
Next, we first define the completion of a propositional atom a with respect to a general program P as a generalized atom encoding the supportedness condition for a.
Definition 8. The completion of a propositional atom a ∈ B with respect to a general program P is a generalized atom comp(a, P ) mapping to true any interpretation I containing a and such that there is no rule r ∈ P for which I |= B(r) and I ∩ H(r) = {a}.
These generalized atoms are then used to effectively define a program whose models are the supported model of P .
Definition 9. The completion of a general program P is a general program comp(P ) extending P with a rule ← comp(a, P ) for each propositional atom a occurring in P .
Example 6. Consider again programs from Example 2. Program comp(P 1 ) extends P 1 with the following rules: Program comp(P 2 ) extends P 2 with the following rules: This characterization (which follows directly from (Clark 1978)) provides us with a means for implementation that relies only on model checks, rather than supportedness checks.
Proposition 2. Let P be a general program and I an interpretation. I is a supportedly FLP answer set of P if I |= comp(P ) and for each J ⊂ I it holds that J |= comp(P I ).

Properties
The new semantics has a number of interesting properties that we report in this section. First of all, it is an extension of the FLP semantics, in the sense that each FLP answer set is also an SFLP answer set. Theorem 1. Let P be a general program. F LP (P ) ⊆ SF LP (P ).
Proof. Let I be an FLP answer set of P . Hence, each J ⊂ I is such that J |= P I . Thus, we can conclude that J |= s P I for any J ⊂ I. Therefore, I is a SFLP answer set of P .
The inclusion is strict in general. In fact, P 1 is a simple program for which the two semantics disagree (see Examples 2-5 and Table 1). On the other hand, the two semantics are equivalent for a large class of programs, as shown below. Theorem 2. If P is a convex program then F LP (P ) = SF LP (P ).
Proof. F LP (P ) ⊆ SF LP (P ) holds by Theorem 1. For the other direction, consider an interpretation I not being an FLP answer set of P . Hence, there is J ⊂ I such that J |= P I . We also assume that J is a subset-minimal model of P I , that is, there is no K ⊂ J such that K |= P I . We shall show that J |= s P I . To this end, suppose by contradiction that there is a ∈ J such that for each r ∈ P I either J |= B(r) or J ∩ H(r) = {a}. Consider J \ {a} and a rule r ∈ P I such that J \ {a} |= B(r). Since r ∈ P I , I |= B(r), and thus J |= B(r) because B(r) is convex. Therefore, J ∩ H(r) = {a}. Moreover, J ∩ H(r) = ∅ because J |= P I by assumption. Hence, (J \ {a}) ∩ H(r) = ∅, and therefore J \ {a} |= P I . This contradicts the assumption that J is a subset-minimal model of P I .
We will now focus on computational complexity. We consider here the problem of determining whether an SFLP answer set exists. We note that the only difference to the FLP semantics is in the stability check. For FLP, subsets need to be checked for being a model, for SFLP, subsets need to be checked for being a supported model. Intuitively, one would not expect that this difference can account for a complexity jump, which is confirmed by the next result. Theorem 3. Let P be a general program whose generalized atoms are polynomial-time computable functions. Checking whether SF LP (P ) = ∅ is in Σ P 2 in general; it is Σ P 2 -hard already in the disjunction-free case if at least one form of non-convex generalized atom is permitted. The problem is N P -complete if P is disjunction-free and convex.
Proof. For the membership in Σ P 2 one can guess an interpretation I and check that there is no J ⊂ I such that J |= s P . The check can be performed by a coN P oracle.
To prove Σ P 2 -hardness we note that extending a general program P by rules a ← a for every propositional atom occurring in P is enough to guarantee that all models of any reduct of P are supported. We thus refer to the construction and proof by (Alviano and Faber 2013).
If P is disjunction-free and convex then SF LP (P ) = F LP (P ) by Theorem 2. Hence, N P -completeness follows from results in (Liu and Truszczyński 2006).
We would like to point out that the above proof also illustrates a peculiar feature of SFLP answer sets, which it shares with the supported model semantics: the semantics is sensitive to tautological rules like a ← a, as their addition can turn non-SFLP answer sets into SFLP answer sets.

Compilation
The introduction of generalized atoms in logic programs does not increase the computational complexity of checking FLP as well as SFLP answer set existence, as long as one is allowed to use disjunctive rule heads. However, so far no compilation method that compactly transforms general programs to logic programs without generalized atoms has been presented for the FLP semantics. In the following we provide such a compilation for non-convex aggregates in disjunctive normal form. The compilation is also extended for the new SFLP semantics. We point out that such compilations are not necessarily intended to provide efficient methods for computing answer sets of general programs. Their purpose is instead to provide insights that may lead to obtain such methods in the future.
In this section we only consider generalized atoms in disjunctive normal form, that is, a generalized atom A will be associated with an equivalent propositional formula of the following form: where k ≥ 1, i n ≥ i m ≥ 0 and a i1 , . . . , a in are propositional atoms for i = 1, . . . , k. We will also assume that the programs to be transformed have atomic heads. To generalize our compilations to cover disjunctive general rules is a problem to be addressed in future work. Let P be a program. In our construction we will use the following fresh propositional atoms, i.e., propositional atoms not occurring in P : A T for each generalized atom A; A Fi for each generalized atom A and integer i ≥ 0. For a generalized atom A of the form (2) and integer i = 1, . . . , k, let tr(A, i) denote the following rule: Moreover, let f ls(A, i, j) denote for j = i 1 , . . . , i m , and for j = i m+1 , . . . , i n . Abusing of notation, let f ls(A) denote the following rule: Intuitively, rule tr(A, i) forces truth of A T whenever the ith disjunct of A is true. Similarly, rule f ls(A, i, j) forces truth of A Fi whenever the i-th disjunct of A is false due to atom a ij ; if all disjuncts of A are false, rule f ls(A) forces truth of A F0 to model that A is actually false. Note that atoms occurring in negative literals of the i-th disjunct of A have been moved in the head of tr(A, i). In this way, the information encoded by tr(A, i) is preserved in the reduct with respect to an interpretation I whenever the i-th disjunct of A is true with respect to a subset of I, not necessarily I itself.
The rewriting of A, denoted rew(A), is the following set of rules: The rewriting of P , denoted rew(P ), is obtained from P by replacing each generalized atom A by A T . The FLPrewriting of P , denoted rew F LP (P ), is obtained from rew(P ) by adding rules in rew(A) for each generalized atom A occurring in P . The SFLP-rewriting of P , denoted rew SF LP (P ), is obtained from rew F LP (P ) by adding a rule supp(a) of the form for each propositional atom a occurring in P , where a ← A i (i = 1, . . . , n) are the rules of P having head a.
Example 7. Let A be the generalized atom in Example 2. Its disjunctive normal form is ∼a ∧ ∼b ∨ a ∧ b. Rules r 1 and r 2 are then a ← A and b ← A. Program rew F LP (P 1 ) is (A, 1, 1) : A F1 ← a, ∼A T f ls (A, 1, 2) : One can check that rew F LP (P 1 ) has no answer set. In particular, {a, b, A T } is not an answer set of rew F LP (P 1 ). Its FLP reduct consists of the first four rules and both {a} and {b} are minimal models of the reduct. On the other hand, neither {a} nor {b} are models of the original program, and so also not answer sets. Program rew SF LP (P 1 ) extends rew F LP (P 1 ) with the following rules: The program rew SF LP (P 1 ) has one answer set: In contrast to rew F LP (P 1 ) its FLP reduct now consists of the first four rules of rew F LP (P 1 ) plus the two additional rules: These two additional rules impede {a} and {b} to be models, and indeed only {a, b, A T } is a model of the reduct. Program rew F LP (P 2 ) is rew F LP (P 1 ) ∪ {a ← b; b ← a}. (To simplify the presentation, bodies equivalent to atomic literals are not rewritten.) In this case, is its only answer set. Different to rew F LP (P 2 ), the additional rules will be present in the reduct for {a, b, A T }: Thus the reduct models {a} and {b} are avoided. Program rew SF LP (P 2 ) extends rew F LP (P 2 ) with It is easy to see that these additional rules do not alter answer sets, so also rew SF LP (P 2 ) has a single answer set {a, b, A T }. Program rew F LP (P 3 ) is rew F LP (P 1 )∪{← ∼a; ← ∼b}. This program has no answer sets for the same reason as rew F LP (P 1 ). Indeed, the two additional rules are not in the reduct for {a, b, A T }, and so {a} and {b} are again minimal models.
Program rew SF LP (P 3 ) is rew SF LP (P 1 ) ∪ {← ∼a; ← ∼b}. For the same reason as for rew SF LP (P 1 ), this program has exactly one answer set: The two new rules disappear in the reduct, but the rules present in rew SF LP (P 1 ) but not in rew F LP (P 1 ) do not allow models {a} and {b}.
Program P 4 contains a disjunctive rule and is thus not in the domain of rew F LP and rew SF LP described here.
In the examples provided so far, it can be checked that answer sets are preserved by our transformations if auxiliary symbols are ignored. In the remainder of this section we will formalize this intuition. Definition 10. The expansion of an interpretation I for a program P , denoted exp(I), is the following interpretation: The contraction of an interpretation I to the symbols of P , denoted I| P , is the following interpretation: Below, we show that expansions and contractions define bijections between the answer sets of a program and those of the corresponding compilations. In the claim we consider only FLP answer sets of the rewritten program because it is convex, and thus its FLP and SFLP answer sets coincide by Theorem 2. Theorem 4. Let P be a program, and F ∈ {F LP, SF LP }. 1. If I ∈ F (P ) then exp(I) ∈ F LP (rew F (P )). 2. If I ∈ F LP (rew F (P )) then I| P ∈ F (P ).
Proof (item 1). Let I be an F answer set of P . Hence, I |= s P (see Definition 7 and Theorem 1). Since each generalized atom A occurring in P is replaced by A T in rew(P ), and A T ∈ exp(I) if and only if I |= A, we have I |= rew(P ). Consider rules in rew(A) for some generalized atom A of the form (2) occurring in P , and note that either A T ∈ exp(I) or A F0 , . . . , A F k ∈ exp(I).
In both cases, all rules in rew(A) are satisfied by exp(I).
Hence, exp(I) |= rew F LP (P ). Consider a rule supp(a) of the form (8) such that a ∈ I. Since I |= s P , there is i ∈ {1, . . . , n} such that I |= A i . Thus, A T i ∈ exp(I), and therefore exp(I) |= supp(a). We can conclude exp(I) |= rew SF LP (P ).
Let J ⊆ exp(I) be such that J |= rew F (P ) exp(I) . We first show that J| P = I. Consider a rule a ← A in P I such that I |= A and J| P |= A, where A is of the form (2). Hence, there is i ∈ {1, . . . , k} such that Therefore, A T ∈ J because tr(A, i) ∈ rew F (P ) exp(I) , and consequently a ∈ J because of rule a ← A T in rew F (P ) exp(I) . We thus conclude J| P |= P I . For F = F LP , this already proves J| P = I. For F = SF LP , let X ⊆ J| P be the atoms without support, i.e., X is a subsetmaximal set such that a ∈ X implies J| P \ X |= A for each rule a ← A in P I . Hence, J| P \ X |= s P I . It follows that J| P \ X = I, i.e., X = ∅ and J| P = I.
We can now show that J = exp(I). Let A be a generalized atom of the form (2). If J| P |= A there is i ∈ {1, . . . , k} such that and thus A T ∈ J because tr(A, i) ∈ rew F (P ) exp(I) and J |= rew F (P ) exp(I) . Otherwise, if J| P |= A then for all i ∈ {1, . . . , k} there is either j ∈ {1, . . . , m} such that a ij / ∈ J| P , or j ∈ {m + 1, . . . , n} such that a ij ∈ J| P . Hence, A Fi ∈ J because J |= f ls(A, i, j), and thus A F0 ∈ J because J |= f ls(A).
Proof (item 2). Let I be an FLP answer set of rew F (P ). Let A be a generalized atom A of the form (2) occurring in P . We prove the following statements: A T ∈ I if and only if I| P |= A (12) |I ∩ {A T , A Fi }| = 1 holds for i = 1, . . . , k To prove (11), define set X as a maximal subset satisfying the following requirements: if an atom a is not supported by I \X in rew F LP (P ) I then a ∈ X. We have I \ X |= rew F (P ) I , from which we conclude X = ∅.
Consider (12). If A T ∈ I then by (11) no A Fi belongs to I. Recall that FLP answer sets are supported models, i.e., I |= s rew F (P ). Thus, for F = F LP , there is i ∈ {1, . . . , k} such that I |= B(tr(A, i)) and I ∩ H(tr(A, i)) = {A T }. Therefore, I| P |= A. For F = SF LP , we just note that if A T is supported only by a rule of the form (8), then atom a is only supported by a rule a ← A T in rew F (P ). I \ {a, A T } would be a model of rew F (P ) I in this case, then contradicting I ∈ F LP (rew F (P )). Now consider the right-to-left direction. If I| P |= A then there is i ∈ {1, . . . , k} such that I| P |= a i1 ∧. . .∧a im ∧∼a im+1 ∧. . .∧∼a in , and thus A Fi / ∈ I (see Equations 4-5). Hence, A F0 / ∈ I (see Equation 6). From rule tr(A, i) (see Equation 3) we have A T ∈ I.
Concerning (13), because of (11) and (12), we have just to show that A F0 , . . . , A F k ∈ I whenever I| P |= A. In fact, in this case A T / ∈ I by (12), and for each i ∈ {1, . . . , k} there is either j ∈ {1, . . . , m} such that a ij / ∈ I| P , or j ∈ {m + 1, . . . , n} such that a ij ∈ I| P . Hence, A Fi ∈ I because of rules f ls(r, i, j) and f ls(r).
We can now prove the main claim. We start by showing that I| P |= P . Indeed, for a rule a ← A in P such that I| P |= A, rew(P ) contains a rule a ← A T . Moreover, A T ∈ I by (12), and thus a ∈ I. If F = SF LP , then for each a ∈ I we have I |= supp(a), where supp(a) is of the form (8). Hence, there is i ∈ 1, ..., n such that A T i ∈ I. Therefore, (12) implies I| P |= A i , that is, a is supported by I| P in P . We can thus conclude that I P |= s P .
To complete the proof, for F = F LP we consider X ⊆ I| P such that I| P \ X |= P I|P , while for F = SF LP we consider X ⊆ I| P such that I| P \ X |= s P I|P . Let J be the interpretation obtained from I \ X by removing all atom A T such that I| P \ X |= A. We shall show that J |= rew F (P ) I , from which we conclude X = ∅. Consider a rule of the form a ← A T in rew F (P ) I such that A T ∈ J. Hence, I| P \ X |= A by construction of J. Since a ← A is a rule in P I|P , we conclude a ∈ I| P \ X and thus a ∈ J. Consider now a rule tr(A, i) in rew F (P ) I such that J |= B(tr(A, i)) and A T / ∈ J. Hence, I| P \ X |= A by construction of J, which means that there is either j ∈ {1, . . . , m} such that a ij / ∈ I| P \ X, or j ∈ {m + 1, . . . , n} such that a ij ∈ I| P \ X. We conclude that J |= tr(A, i). Rules f ls(A, i, j) and f ls(A) are satisfied as well because no A Fi has been removed. For F = SF LP , consider a rule supp(a) of the form (8) such that a ∈ J. Since I| P \ X |= s P I|P , there is rule a ← A in P I|P such that I| P \ X |= A. Hence, by construction of J, A T ∈ J and thus J |= supp(a).

Conclusion
In this paper, we have first defined a new semantics for programs with generalized atoms, called supportedly stable models, supportedly FLP, or SFLP semantics. We have motivated its definition by an anomaly that arises for the FLP semantics in connection with non-convex generalized atoms. In particular, only unsupported models may in particular cases inhibit the stability of candidate models. The new definition overcomes this anomaly and provides a robust semantics for programs with generalized atoms. We show several properties of this new semantics, for example it coincides with the FLP semantics (and thus also the PSP semantics) on convex programs, and thus also on standard programs. Furthermore, the complexity of reasoning tasks is equal to the respective tasks using the FLP semantics. We also provide a characterization of the new semantics by a Clark-inspired completion.
We observe that other interesting semantics, such as the one by (Ferraris 2005), are also affected by the anomaly on unsupported models. In particular, the semantics by (Ferraris 2005) is presented for programs consisting of arbitrary set of propositional formulas, and it is based on a reduct in which false subformulas are replaced by ⊥. Answer sets are then defined as interpretations being subsetminimal models of their reducts. For the syntax considered in this paper, when rewriting generalized atoms to an equivalent formula, the semantics by (Ferraris 2005) coincides with FLP, which immediately shows the anomaly. In (Ferraris 2005) there is also a method for rewriting aggregates, however COU N T ({a, b}) = 1 is not explicitly supported, but should be rewritten to ¬(COU N T ({a, b}) = 1). Doing this, one can observe that for P 1 , P 2 , P 3 , and P 5 the semantics of (Ferraris 2005) behaves like SFLP (cf. Table 1), while for P 4 the semantics of (Ferraris 2005) additionally has the answer set {a, b}, which is not a supported minimal model of the FLP reduct. P 4 therefore shows that the two semantics do not coincide, even if generalized atoms are interpreted as their negated complements, and the precise re-lationship is left for further study. However, we also believe that rewriting a generalized atom into its negated complement is not always natural, and we are also not convinced that there should be a semantic difference between a generalized atom and its negated complement.
The second part of the paper concerns the question of compactly compiling generalized atoms away, to arrive at a program that contains only traditional atoms whose answer sets are in a one-to-one correspondence with the original program. Previously existing complexity results indicated that such a translation can exist, but that it has to make use of disjunction in rule heads. However, no such method is currently known. We show that similar techniques can be used for both FLP and the new SFLP semantics when non-convex aggregates are represented in disjunctive normal form.
Concerning future work, implementing a reasoner supporting the new semantics would be of interest. However, we believe that it would actually be more important to collect example programs that contain non-convex generalized atoms in recursive definitions. We have experimented with a few simple domains stemming from game theory (as outlined in the introduction), but we are not aware of many other attempts. Our intuition is that such programs would be written in several domains that describe features with feedback loops, which applies to many so-called complex systems. Also computing or checking properties of neural networks might be a possible application in this area. Another, quite different application area could be systems that loosely couple OWL ontologies with rule bases, for instance by means of HEX programs. HEX atoms interfacing to ontologies will in general not be convex, and therefore using them in recursive definitions falls into our framework, where the FLP and SFLP semantics differ.
Another area of future work arises from the fact that rules like a ← a are not irrelevant for the SFLP semantics. To us, it is not completely clear whether this is a big drawback. However, we intend to study variants of the SFLP semantics that do not exhibit this peculiarity.