# grounded_fixpoints__aad7b248.pdf

Grounded Fixpoints

Bart Bogaerts Department of Computer Science KU Leuven 3001 Heverlee, Belgium bart.bogaerts@cs.kuleuven.be

Joost Vennekens Department of Computer Science Campus De Nayer, KU Leuven 2860 Sint-Katelijne-Waver, Belgium joost.vennekens@cs.kuleuven.be

Marc Denecker Department of Computer Science KU Leuven 3001 Heverlee, Belgium marc.denecker@cs.kuleuven.be

Algebraical ﬁxpoint theory is an invaluable instrument for studying semantics of logics. For example, all major semantics of logic programming, autoepistemic logic, default logic and more recently, abstract argumentation have been shown to be induced by the different types of ﬁxpoints deﬁned in approximation ﬁxpoint theory (AFT). In this paper, we add a new type of ﬁxpoint to AFT: a grounded ﬁxpoint of lattice operator O : L L is deﬁned as a lattice element x L such that O(x) = x and for all v L such that O(v x) v, it holds that x v. On the algebraical level, we show that all grounded ﬁxpoints are minimal ﬁxpoints approximated by the well-founded ﬁxpoint and that all stable ﬁxpoints are grounded. On the logical level, grounded ﬁxpoints provide a new mathematically simple and compact type of semantics for any logic with a (possibly non-monotone) semantic operator. We explain the intuition underlying this semantics in the context of logic programming by pointing out that grounded ﬁxpoints of the immediate consequence operator are interpretations that have no non-trivial unfounded sets. We also analyse the complexity of the induced semantics. Summarised, grounded ﬁxpoint semantics is a new, probably the simplest and most compact, element in the family of semantics that capture basic intuitions and principles of various non-monotonic logics.

1 Introduction Motivated by structural analogies in the semantics of several non-monotonic logics, Denecker, Marek, and Truszczy nski (2000) developed an algebraic theory that deﬁnes different types of ﬁxpoints for a so-called approximating bilattice operator, called supported, Kripke-Kleene, stable and wellfounded ﬁxpoints. In the context of logic programming, they found that Fitting s immediate consequence operator is an approximating operator of the two-valued immediate consequence operator and that its four different types of ﬁxpoints correspond exactly with the four major, equally named semantics of logic programs. They also identiﬁed approximating operators for default logic (DL) and autoepistemic logic (AEL) and showed that the ﬁxpoint theory induces all main

Copyright c 2015, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

and some new semantics in these ﬁelds (Denecker, Marek, and Truszczy nski 2003). By showing that Konolige s mapping from DL to AEL preserves the approximating operator, they resolved an old research question regarding the nature of these two logics: AEL and DL are just two different dialects of autoepistemic reasoning (Denecker, Marek, and Truszczy nski 2011). The study of these approximating operators is called approximation ﬁxpoint theory (AFT). It is now commonly used to deﬁne semantics of extensions of logic programs, such as logic programs with aggregates (Pelov, Denecker, and Bruynooghe 2007) and HEX logic programs (Antic, Eiter, and Fink 2013). Vennekens, Gilis, and Denecker (2006) used AFT in an algebraic modularity study for logic programming, AEL and DL. Recently, Strass (2013) showed that many semantics from Dung s argumentation frameworks (AFs) and abstract dialectical frameworks (ADFs) can be obtained by direct applications of AFT and Bogaerts et al. (2014) deﬁned the causal logic FO(C) as an instantiation of AFT. This work suggests that ﬁxpoint theory, despite its high level of abstraction, captures certain fundamental intuitions and cognitive principles in a range of logics and sorts of human knowledge. It is this observation that provides the basic motivation for the present study. In Section 3, we extend AFT with a new type of ﬁxpoint: a point x in a lattice L is a grounded ﬁxpoint of operator O : L L if O(x) = x and for all v L such that O(x v) v, it holds that x v. In Section 4, we discuss the relation between grounded ﬁxpoints and the other ﬁxpoints deﬁned by AFT. In particular, we show that all (ultimate) stable ﬁxpoints are grounded and that all grounded ﬁxpoints are minimal ﬁxpoints approximated by the (ultimate) well-founded ﬁxpoint in the bilattice. In general there are minimal ﬁxpoints that are not grounded, and grounded ﬁxpoints that are not stable. If the well-founded ﬁxpoint is exact , the well-founded ﬁxpoint is the unique grounded and stable ﬁxpoint of O. Grounded ﬁxpoints have several appealing properties. First of all, a grounded ﬁxpoint is a purely algebraical concept. As such, it can be used in all ﬁelds where AFT is applied. Secondly, a ﬁrst step in the application of AFT for a lattice operator O is to choose a bilattice operator that approximates O. In contrast, grounded ﬁxpoints are deﬁned directly in terms of the original operator O. Thirdly, their

Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence

deﬁnition formalises and generalises well-known intuitions. In the context of logic programming, which we discuss in Section 5, the algebraic results show that grounded ﬁxpoints induce a semantics that is slightly more liberal than stable semantics: all stable models are grounded (i.e., we identiﬁed a property all stable models have in common) but also every grounded ﬁxpoint is approximated by the well-founded model; the differences collapse in case the well-founded model is two-valued. We will see that for logic programming, this semantics is simple and intuitive: we show that the grounded ﬁxpoints can be characterised in terms of a generalised notion of unfounded set. Contrary to the more common semantics of logic programs, grounded ﬁxpoint semantics does not rely on any form of three-valued logic: It is deﬁned directly in terms of the (twovalued!) immediate consequence operator. The grounded ﬁxpoint semantics is very ﬂexible towards language extensions. Currently, much research is being conducted in order to extend stable and well-founded semantics for logic programs with new language constructs (Pelov, Denecker, and Bruynooghe 2007; Faber, Pfeifer, and Leone 2011; Marek, Niemel a, and Truszczy nski 2008; Balduccini 2013). Since the grounded ﬁxpoint semantics is completely deﬁned using the two-valued immediate consequence operator, it sufﬁces to extend this operator to obtain an extended semantics; this is often trivial. These nice properties come at a cost: we show that in general, determining whether a logic program has a grounded ﬁxpoint is ΣP 2 -complete. However, for large classes of programs, grounded ﬁxpoint semantics coincides with stable semantics. For those programs, we obtained a simple, concise, purely 2-valued and algebraical, extensible reformulation of the existing semantics. Due to space limitations, we do not elaborate on how our theory applies to AEL, DL or ADFs and refer to (Bogaerts, Vennekens, and Denecker 2014) for proofs. Summarised, the main contributions of this paper are as follows. We extend AFT with the notion of a grounded ﬁxpoint, a ﬁxpoint closely related to stable ﬁxpoints with similar properties, but that is determined by O, not by the choice of an approximator. Applied to logic programming this yields an intuitive, purely two-valued, semantics that is easily extensible and that formalises well-known intuitions.

2 Preliminaries 2.1 Lattices and Operators

A poset L, is a set L equipped with a partial order , i.e., a reﬂexive antisymmetric, transitive relation. If S is a subset of L, then x is an upper bound, respectively a lower bound of S if for every s S, it holds that s x respectively x s. An element x is a least upper bound, respectively greatest lower bound of S if it is an upper bound that is smaller than every other upper bound, respectively a lower bound that is greater than every other lower bound. If S has a least upper bound, respectively a greatest lower bound, we denote it lub(S), respectively glb(S). As is custom, we sometimes call a greatest lower bound a meet, and a least upper bound a join and use the related notations V S = glb(S), x y = glb({x, y}), W S = lub(S) and x y = lub({x, y}).

We call L, a complete lattice if every subset of L has a least upper bound and a greatest lower bound. A complete lattice has both a least element and a greatest element . An operator O : L L is monotone if x y implies that O(x) O(y). An element x L is a preﬁxpoint, a ﬁxpoint, a postﬁxpoint if O(x) x, respectively O(x) = x, x O(x). Every monotone operator O in a complete lattice has a least ﬁxpoint, denoted lfp(O), which is also O s least preﬁxpoint and the limit (the least upper bound) of the increasing sequence (xi)i 0 deﬁned by x0 = , xi+1 = O(xi), xλ = lub({xi | i < λ}), for limit ordinals λ.

2.2 Logic Programming In the following sections, we illustrate our abstract results in the context of logic programming. We recall some preliminaries. We restrict ourselves to propositional logic programs, but allow arbitrary propositional formulas in rule bodies. However, AFT has been applied in a much broader context (Denecker, Bruynooghe, and Vennekens 2012; Pelov, Denecker, and Bruynooghe 2007; Antic, Eiter, and Fink 2013) and our results can also be applied in these extensions of logic programming. Let Σ be an alphabet, i.e., a collection of symbols which are called atoms. A literal is an atom p or the negation q of an atom q. A logic program P is a set of rules r of the form h ϕ, where h is an atom called the head of r, denoted head(r), and ϕ is a propositional formula called the body of r, denoted body(r). An interpretation I of the alphabet Σ is an element of 2Σ, i.e., a subset of Σ. The set of interpretations 2Σ forms a lattice equipped with the order . The truth value (t or f) of a propositional formula ϕ in a structure I, denoted ϕI is deﬁned as usual. With a logic program P, we associate an immediate consequence operator (van Emden and Kowalski 1976) TP that maps a structure I to

TP(I) = {p | r P : head(r) = p body(r)I = t}.

3 Grounded Fixpoints Let L, be a complete lattice and O : L L a lattice operator, ﬁxed throughout this entire section. We start by giving the most central deﬁnition of this text, namely the notion of groundedness. Deﬁnition 3.1 (Grounded). We call x L grounded for O if for each v L such that O(v x) v, it holds that x v. The intuition behind this concept is easiest to explain if we assume that the elements of L are sets of facts of some kind and the relation is the subset relation between such sets. In this case, a point x is grounded if it contains only facts that are sanctioned by the operator O, in the sense that if we remove them from x, then the operator will add at least one of them again. The above deﬁnition captures this idea, by using a set v L to remove all elements not in v from x. If their removal is not contradicted by O, i.e., O does not re-derive any removed element (O(x v) v), then these elements cannot be part of the grounded point (x v).

Proposition 3.2. If O is a monotone operator and x is grounded for O then x is a postﬁxpoint of O that is less than or equal to lfp(O), i.e., x O(x) and x lfp(O).

Example 3.3. The converse of Proposition 3.2 does not hold. Consider the following logic program P: ( p. q p q.

Its immediate consequence operator TP is represented by the following graph, where full edges express the order relation (to be precise, the relation is the reﬂexive transitive closure of these edges) and the dotted edges represent the operator:

6n n n n n n n n

6m m m m m m m m

TP is a monotone operator with least ﬁxpoint . Also, {q} is a postﬁxpoint of TP since TP({q}) = {q}. However, {q} is not grounded since TP({q} {p}) = TP( ) = {p} {p}, while {q} {p}.

Proposition 3.4. All grounded ﬁxpoints of O are minimal ﬁxpoints of O.

Example 3.5. The converse of Proposition 3.4 does not hold. Consider the logic program P: ( p p. q p q.

This logic program corresponds has as immediate consequence operator TP:

6n n n n n n n n

6m m m m m m m m

In this case, {p} is a minimal ﬁxpoint of TP, but {p} is not grounded since TP({p} {q}) = TP( ) = {q}.

Proposition 3.6. A monotone operator has exactly one grounded ﬁxpoint, namely its least ﬁxpoint.

4 Grounded Fixpoints and AFT 4.1 Preliminaries: AFT Given a lattice L, approximation ﬁxpoint theory makes uses of the bilattice L2. We deﬁne two projection functions for pairs as usual: (x, y)1 = x and (x, y)2 = y. Pairs (x, y) L2 are used to approximate all elements in the interval [x, y] = {z | x z z y}. We call (x, y) L2 consistent if x y, that is, if [x, y] is non-empty. We use Lc to

denote the set of consistent elements. Elements (x, x) Lc are called exact. We sometimes abuse notation and use the tuple (x, y) and the interval [x, y] interchangeably. The precision ordering on L2 is deﬁned as (x, y) p (u, v) if x u and v y. In case (u, v) is consistent, this means that (x, y) approximates all elements approximated by (u, v), or in other words that [u, v] [x, y]. If L is a complete lattice, then L2, p is also a complete lattice. AFT studies ﬁxpoints of lattice operators O : L L through operators approximating O. An operator A : L2 L2 is an approximator of O if it is p -monotone, and has the property that for all x, O(x) A(x, x). Approximators are internal in Lc (i.e., map Lc into Lc). As usual, we restrict our attention to symmetric approximators: approximators A such that for all x and y, A(x, y)1 = A(y, x)2. Denecker, Marek, and Truszczy nski (2004) showed that the consistent ﬁxpoints of interest (supported, stable, well-founded) are uniquely determined by an approximator s restriction to Lc, hence, sometimes we only deﬁne approximators on Lc. AFT studies ﬁxpoints of O using ﬁxpoints of A. The AKripke-Kleene ﬁxpoint is the p -least ﬁxpoint of A and has the property that it approximates all ﬁxpoints of O. A partial A-stable ﬁxpoint is a pair (x, y) such that x = lfp(A( , y)1) and y = lfp(A(x, )2), where A( , y)1 denotes the operator L L : x 7 A(x, y)1 and analogously for A(x, )2. The A-well-founded ﬁxpoint is the least precise partial Astable ﬁxpoint. An A-stable ﬁxpoint of O is a ﬁxpoint x of O such that (x, x) is a partial A-stable ﬁxpoint. This is equivalent with the condition that x = lfp(A( , x)1). The A-Kripke-Kleene ﬁxpoint of O can be constructed by iteratively applying A, starting from ( , ). For the A-wellfounded ﬁxpoint, a similar constructive characterisation has been worked out by Denecker and Vennekens (2007). In general, a lattice operator O : L L has a family of approximators of different precision. Denecker, Marek, and Truszczy nski (2004) showed that there exists a most precise approximator, UO, called the ultimate approximator of O. This operator is deﬁned by UO : Lc Lc : (x, y) 7 (V O([x, y]), W O([x, y])). Semantics deﬁned using the ultimate approximator have as advantage that they only depend on O since the approximator can be derived from O. It was shown that for any approximator A, all A-stable ﬁxpoints are UO-stable ﬁxpoints, and the UO-well-founded ﬁxpoint is always more precise than the A-well-founded ﬁxpoint. We refer to UO-stable ﬁxpoints as ultimate stable ﬁxpoints of O and to the UO-well-founded ﬁxpoint as the ultimate well-founded ﬁxpoint of O.

AFT and Logic Programming In the context of logic programming, elements of the bilattice 2Σ 2 are partial interpretations, pairs I = (I1, I2) of interpretations. The pair (I1, I2) approximates all interpretations I with I1 I I2. We are mostly concerned with consistent (or, threevalued) interpretations: tuples I = (I1, I2) with I1 I2. For such an interpretation, the atoms in I1 are true (t) in I, the atoms in I2\I1 are unknown (u) in I and the other atoms are false (f) in I. If I is a three-valued interpretation, and ϕ a formula, we write ϕI for the standard three-valued valuation based on the Kleene truth tables (Kleene 1938). An in-

terpretation I corresponds to the partial interpretation (I, I). If I = (I1, I2) is a (partial) interpretation, and U Σ, we write I[U : f] for the (partial) interpretation that equals I on all elements not in U and that interprets all elements in U as f, i.e., the interpretation (I1 \ U, I2 \ U). Several approximators have been deﬁned for logic programs. The most common is Fitting s immediate consequence operator ΨP (Fitting 2002), a direct generalisation of TP to partial interpretations. Denecker, Marek, and Truszczy nski (2000) showed that the well-founded ﬁxpoint of ΨP is the well-founded model of P (Van Gelder, Ross, and Schlipf 1991) and that ΨP-stable ﬁxpoints are exactly the stable models of P (Gelfond and Lifschitz 1988). Contrary to classical stable and well-founded semantics, their ultimate counterparts have the nice property that they are insensitive to equivalence preserving rewritings of the bodies of rules. If two logic programs P and P have the same immediate consequence operator, then their ultimate stable (respectively ultimate well-founded) models are the same. For example consider programs P = {p p p} and P = {p.}. Even though the body of the rule deﬁning p in P is a tautology, {p} is not a stable model of P (while it is a stable model of P ). However, the ultimate stable semantics treats these two programs identically. However, this property comes at a cost. Denecker, Marek, and Truszczy nski (2004) showed that deciding whether P has an ultimate stable model is Σ2 P -complete, while that same task is only NP-complete for classical stable models.

4.2 Grounded Fixpoints and AFT In this section, we discuss how groundedness relates to AFT. More concretely, we show that all (ultimate) stable ﬁxpoints are grounded and that all grounded ﬁxpoints are approximated by the (ultimate) well-founded ﬁxpoint. Proposition 4.1. All ultimate stable ﬁxpoints of O are grounded.

Example 4.2. The converse of Proposition 4.1 does not always hold. Consider the logic program P: ( p p q. q q p.

This logic program has as immediate consequence operator TP: = {p, q}

6n n n n n n n n 2 {q}

6m m m m m m m m

is grounded for TP, since the only v with TP( v) = TP(v) v is itself. However, since TP([ , ]) = L \ { } and {p} {q} = , it follows that V(TP[ , ]) = . Thus, lfp(V TP([ , ])) = . Therefore, is not an ultimate stable ﬁxpoint of TP.

The fact that all A-stable ﬁxpoints are ultimate stable ﬁxpoints (Denecker, Marek, and Truszczy nski 2004) yields:

Corollary 4.3. If A is an approximator of O, then all Astable ﬁxpoints are grounded ﬁxpoints of O. Theorem 4.4. The well-founded ﬁxpoint (u, v) of a symmetric approximator A of O approximates all grounded ﬁxpoints of O. Corollary 4.5. If the well-founded ﬁxpoint of a symmetric approximator A of O is exact, then this point is the unique grounded ﬁxpoint of O.

5 Grounded Fixpoints of Logic Programs In this section, we discuss grounded ﬁxpoints in the context of logic programming. It follows immediately from the algebraical results (Corollary 4.3 and Theorem 4.4) that stable models are grounded ﬁxpoints of the immediate consequence operator and that grounded ﬁxpoints are minimal ﬁxpoints approximated by the well-founded model. Grounded ﬁxpoints can be explained in terms of unfounded sets. Intuitively, an unfounded set is a set of atoms that might circularly support themselves, but have no support from outside. Stated differently, an unfounded set of a logic program P with respect to an interpretation I is a set U of atoms such that P provides no support for the truth of any atom in U, except possibly support based on the truth of other atoms in U. Since TP maps an interpretation I to the set of atoms supported by P in I, the above intuitions are directly formalised as follows. Deﬁnition 5.1 (2-Unfounded set). Let P be a logic program, TP the corresponding direct consequence operator and I 2Σ an interpretation. A set U Σ is a 2-unfounded set of P with respect to I if TP(I[U : f]) U = . Thus, U is a 2-unfounded set of P with respect to I if removing all elements of U from I results in a state I[U : f] where no atom in U is supported, i.e., TP(I[U : f]) contains no atoms from U. Deﬁnition 5.1 slightly differs from the original deﬁnition of unfounded set by Van Gelder, Ross, and Schlipf (1991) but it formalises the same intuitions. The most important difference is that we work in a two-valued setting, while van Gelder et al. deﬁned unfounded sets in a three-valued setting. For clarity, we refer to our unfounded sets as 2-unfounded sets and to the original deﬁnition as GRS-unfounded sets . Our theory does not require any form of three-valued logic. In Section 6, we extend our definition to a three-valued context and show that the different notions of unfounded set are equivalent in the context of the well-founded model construction.

Example 5.2. Let P be the following program:

p q r. q p. t s r.

Let I be the interpretation {p, q, s, t}. Then U1 = {p, q} is an unfounded set of P with respect to I since I[U1 : f] = {s, t} and in this structure, the bodies of rules deﬁning p and q are false. More formally, TP(I[U1 : f]) U1 = U1 = . U2 = {s, t} is not a 2-unfounded set of P with respect to I since TP(I[U2 : f]) U2 = {p, q, t} U2 = {t} = .

In what follows, we use U c for the set complement of U, i.e., U c = Σ \ U. Proposition 5.3. Let P be a logic program, TP the corresponding direct consequence operator and I 2Σ an interpretation. A set U Σ is a 2-unfounded set of P with respect to I if and only if TP(I U c) U c. Proposition 5.3 shows that U is a 2-unfounded set if and only if its complement satisﬁes the condition on v in Deﬁnition 3.1! This allows us to reformulate the condition that I is grounded as follows. Proposition 5.4. A structure I is grounded for TP if and only if I does not contain any atoms that belong to a 2unfounded set U of P with respect to I. If I is a ﬁxpoint of TP, then all sets U Ic are 2unfounded sets. We call these 2-unfounded sets trivial. With this terminology, we ﬁnd: Corollary 5.5. A structure I is a grounded ﬁxpoint of TP if and only if it is a ﬁxpoint of TP and P has no non-trivial 2-unfounded sets with respect to I. Similarly to ultimate semantics, grounded ﬁxpoints are insensitive to equivalence-preserving rewritings in the bodies of rules: if P and P are such that TP = TP , then the grounded ﬁxpoints of P and P coincide. Also similar to ultimate semantics, the above property comes at a cost. Theorem 5.6. The problem given a ﬁnite propositional logic program P, decide whether P has a grounded ﬁxpoint is ΣP 2 -complete. Let us brieﬂy compare grounded ﬁxpoint semantics with the two most frequently used semantics of logic programming: well-founded and stable semantics. Firstly, it deserves to be stressed that the three semantics provide different formalisations of a similar intuition: a certain minimality criterion for ﬁxpoints (which we called groundedness). Consequently it is to be expected that they often coincide. We established that for programs with a two-valued wellfounded model, the three semantics coincide. This sort of programs is common in applications for deductive databases (Datalog and extensions (Abiteboul and Vianu 1991)) and for representing inductive deﬁnitions (Denecker and Vennekens 2014). In contrast, well-founded semantics coincides only seldom with stable semantics in the context of answer set programming (ASP). We illustrated in Example 4.2 that in this case, also stable and grounded ﬁxpoint semantics may disagree. This example is quite unwieldy, as are all such programs that we found. It led us to expect that for large classes of ASP programs, both semantics still coincide. For those programs, we have deﬁned a an elegant, intuitive and concise reformulation of the existing semantics. It is a topic for future research to search for characteristics of ASP programs that guarantee that both semantics agree or disagree. Grounded ﬁxpoint semantics is, to the best of our knowledge, the ﬁrst purely two-valued and algebraical semantics. The well-founded semantics explicitly uses three-valued interpretations in the well-founded model construction. Stable semantics uses three-valued logic implicitly: the Gelfond Lifschitz reduct corresponds to an evaluation in a partial interpretation. The ultimate versions of these semantics are

purely algebraical but still refer to three-valued interpretations (replacing Kleene valuation by supervaluation). Due to this, ultimate stable and well-founded models are relatively complex to understand.

Logic Programs with Abstract Constraint Atoms. The fact that grounded ﬁxpoints semantics is two-valued and algebraical makes it not only easier to understand, but also to extend the semantics. To illustrate this, we consider logic programs with abstract constraint atoms as deﬁned by Marek, Niemel a, and Truszczy nski (2008). An abstract constraint is a collection C 2Σ. A constraint atom is an expression of the form C(X), where X Σ and C is an abstract constraint. The goal of such an atom is to model constraints on subsets of X. The truth value of C(X) in interpretation I is t if I X C and f otherwise. Abstract constraints are a generalisation of pseudo-Boolean constraints, cardinality constraints, and much more. A deterministic logic program is a set of rules of the form1

p a1 an b1 bm,

where p is an atom and the ai and bi are constraint atoms. The intuition behind such a rule is that p is justiﬁed if the constraints ai are satisﬁed while the bi are not. This intuition is captured in an extended immediate consequence operator:

TP(I) = {p | r P : head(r) = p body(r)I = t}.

Grounded ﬁxpoints of this operator still represent the same intuitions: an interpretation I is grounded if it contains no unfounded sets, or said differently, no atoms without external support. Thus, if it contains no set U of atoms such that TP(I[U : f]) U = .

Example 5.7. Let Σ be the alphabet {a, b, c, d} For every i, let C i be the cardinality constraint {X Σ | |X| i}.. Consider the following logic program P over Σ: a. b C 1(Σ). c C 4(Σ). d C 4(Σ).

Any interpretation in which d holds is not grounded since for every I, C 4(Σ)I[d:f] = f and thus d TP(I[d : f]). It can easily be veriﬁed that {a, b, c} is the only grounded ﬁxpoint of P.

This example illustrates that even for complex, abstract extensions of logic programs, groundedness is an intuitive property: for any extension, a point is grounded if it contains no self-supporting atoms. Also, it often possible to derive common properties of all grounded ﬁxpoints such as the fact that d cannot be contained in any of them. Lastly, groundedness easily extends to these rich formalisms (deﬁning grounded ﬁxpoints takes one line given the immediate consequence operator). This is in sharp contrast with more common semantics of logic programming (such as stable

1Here, we limit ourselves to deterministic programs. In general, Marek, Niemel a, and Truszczy nski also described nondeterministic programs. We come back to this issue in Section 6.

and well-founded semantics) which are often hard(er) to extend to richer formalisms, as can be observed by the many different versions of those semantics that exist for logic programs with aggregates (Ferraris 2005; Son, Pontelli, and Elkabani 2006; Pelov, Denecker, and Bruynooghe 2007; Faber, Pfeifer, and Leone 2011; Gelfond and Zhang 2014).

6 Discussion Unfounded Sets. Unfounded sets were ﬁrst deﬁned by Van Gelder, Ross, and Schlipf (1991) in their seminal paper introducing the well-founded semantics. Their deﬁnition slightly differs from Deﬁnition 5.1.

Deﬁnition 6.1 (GRS-Unfounded set). Let P be a logic program and I a three-valued interpretation. A set U Σ is a GRS-unfounded set of P with respect to I, if for each rule r with head(r) U, body(r)I = f or body(r)I[U:f] = f.

The ﬁrst difference between 2-unfounded sets and GRSunfounded sets is that GRS-unfounded sets are deﬁned for three-valued interpretations, while we restricted our attention to (total) interpretations. Our deﬁnition easily generalises to three-valued interpretations using Fitting s operator:

Deﬁnition 6.2 (3-Unfounded set). Let P be a logic program, ΨP Fitting s immediate consequence operator and I a three-valued interpretation. A set U Σ is a 3-unfounded set of P with respect to I if ΨP(I[U : f])2 U = .

This deﬁnition formalises the same intuitions as Deﬁnition 5.1: U is a 3-unfounded set if making all atoms in U false results in a state where none of them can be derived. The following proposition relates the two notions of unfounded sets.

Proposition 6.3. Let P be a logic program, I a three-valued interpretation and U Σ. The following hold.

If U is a 3-unfounded set, then U is a GRS-unfounded set. If I[U : f] is more precise than I, then U is a GRSunfounded set if and only if U is a 3-unfounded set.

We showed that for a certain class of interpretations, the two notions of unfounded sets coincide. Furthermore, Van Gelder et al. only use unfounded sets to deﬁne the wellfounded model construction. It follows immediately from Lemma 3.4 in (Van Gelder, Ross, and Schlipf 1991) that every partial interpretation I in that construction with GRSunfounded set U satisﬁes the condition in the second claim in Proposition 6.3. This means that 3-unfounded sets and GRS-unfounded sets are equivalent for all interpretations that are relevant in the original work! Essentially, we provided a new formalisation of unfounded sets that correctly formalises the underlying intuitions, and that coincides with the old deﬁnition on all interpretations used in the original work. Furthermore, our deﬁnition is simpler and translates easily to algebra. Corollary 5.5, which states that grounded ﬁxpoints are ﬁxpoints of TP that permit no non-trivial 2-unfounded sets, might sound familiar. Indeed, it has been shown that an interpretation is a stable model of a logic program if and only if it is a ﬁxpoint of TP and it permits no non-trivial

GRS-unfounded sets (Lifschitz 2008). This again shows that many of the intuitions used in Answer Set Programming are also closely related to the notion of groundedness.

Groundedness and Nondeterminism. In Section 5, we restricted ourselves to logic programs with abstract constraint atoms in the bodies of rules. As argued by Marek, Niemel a, and Truszczy nski (2008), allowing them as well in heads gives rise to a nondeterministic generalisation of the immediate consequence operator. A consistent nondeterministic operator maps every point x L to a non-empty set O(x) L. The deﬁnition of groundedness can straightforwardly be extended to this nondeterministic setting: a point x L is grounded for nondeterministic operator O, if x v for all v such that O(x v) v, where we deﬁne for a set X L that X v if x v for every x X. A thorough study of groundedness for nondeterministic operators is out of the scope of this paper.

Other Deﬁnitions of Groundedness. The terminology grounded is heavily overloaded in the literature. This is not a coincidence since this term often represents similar intuitions. For example Denecker, Marek, and Truszczy nski (2002) argued that ultimate stable models satisfy some groundedness condition without deﬁning this condition. We formally deﬁned groundedness and showed in Proposition 4.1 that with this deﬁnition, their claim indeed holds. In 1988, Konolige deﬁned notions of weak, moderate and strong groundedness in order to formalise some of his intuitions regarding good models of autoepistemic theories. However, as he mentions himself, the closest he got to formalising these intuitions was strong groundedness, a syntactical criterion that depends on how a theory is rewritten to a normal form. We now claim2 that our notion of groundedness formalises his intuitions, or at least, that it works for all examples he gave! In Dung s argumentation frameworks, the grounded semantics is also deﬁned. Since this is deﬁned as the least ﬁxpoint of the (monotone) characteristic operator, in this case this is the unique grounded ﬁxpoint. However, Strass (2013) showed that this does not generalise to abstract dialectical frameworks, where the grounded extension corresponds to the (ultimate) Kripke-Kleene ﬁxpoint.

7 Conclusion In this paper, we deﬁned a new algebraical concept, namely groundedness. We showed that grounded ﬁxpoints behave well with respect to other ﬁxpoints studied in approximation ﬁxpoint theory: given an operator O and an approximator A of O, all A-stable ﬁxpoints are grounded for O and all grounded ﬁxpoints of O are approximated by the A-wellfounded ﬁxpoint. Moreover, grounded ﬁxpoints free us from the need of choosing such an approximator: they are deﬁned directly in terms of the original lattice operator.

2The journal version of this paper will formally describe the application of our theory to various ﬁelds, including a more detailed discussion about the different notions of groundedness, Konolige s intuitions and the relation to grounded ﬁxpoints.

Grounded ﬁxpoint semantics is the ﬁrst purely two-valued and algebraical semantics for logic programming. Moreover, this semantics is compact, intuitive (directly based on the notion of unfounded sets) and easily extensible: as long as the (two-valued) immediate consequence operator is deﬁned, the grounded ﬁxpoint semantics is obtained for free. Our theory can also be applied to AEL, DL, Dung s argumentation frameworks and ADFs where it also results in a semantics with attractive properties.2

Acknowledgements This work was supported by the KU Leuven under project GOA 13/010 and by the Research Foundation - Flanders (FWO-Vlaanderen).

Abiteboul, S., and Vianu, V. 1991. Datalog extensions for database queries and updates. J. Comput. Syst. Sci. 43(1):62 124. Antic, C.; Eiter, T.; and Fink, M. 2013. Hex semantics via approximation ﬁxpoint theory. In Cabalar, P., and Son, T. C., eds., LPNMR, volume 8148 of LNCS, 102 115. Springer. Balduccini, M. 2013. ASP with non-herbrand partial functions: A language and system for practical use. TPLP 13(45):547 561. Bogaerts, B.; Vennekens, J.; Denecker, M.; and Van den Bussche, J. 2014. FO(C): A knowledge representation language of causality. TPLP 14(4-5-Online-Supplement):60 69. Bogaerts, B.; Vennekens, J.; and Denecker, M. 2014. Grounded ﬁxpoints. Technical Report CW 677, Departement of Computer Science, Katholieke Universiteit Leuven. Denecker, M., and Vennekens, J. 2007. Well-founded semantics and the algebraic theory of non-monotone inductive deﬁnitions. In Baral, C.; Brewka, G.; and Schlipf, J. S., eds., LPNMR, volume 4483 of LNCS, 84 96. Springer. Denecker, M., and Vennekens, J. 2014. The well-founded semantics is the principle of inductive deﬁnition, revisited. In Baral, C.; De Giacomo, G.; and Eiter, T., eds., KR, 22 31. AAAI Press. Denecker, M.; Bruynooghe, M.; and Vennekens, J. 2012. Approximation ﬁxpoint theory and the semantics of logic and answers set programs. In Erdem, E.; Lee, J.; Lierler, Y.; and Pearce, D., eds., Correct Reasoning, volume 7265 of LNCS. Springer. 178 194. Denecker, M.; Marek, V.; and Truszczy nski, M. 2000. Approximations, stable operators, well-founded ﬁxpoints and applications in nonmonotonic reasoning. In Minker, J., ed., Logic-Based Artiﬁcial Intelligence, volume 597 of The Springer International Series in Engineering and Computer Science. Springer US. 127 144. Denecker, M.; Marek, V. W.; and Truszczy nski, M. 2002. Ultimate approximations in nonmonotonic knowledge representation systems. In Fensel, D.; Giunchiglia, F.; Mc Guinness, D. L.; and Williams, M.-A., eds., KR, 177 190. Morgan Kaufmann.

Denecker, M.; Marek, V. W.; and Truszczy nski, M. 2003. Uniform semantic treatment of default and autoepistemic logics. Artif. Intell. 143(1):79 122. Denecker, M.; Marek, V. W.; and Truszczy nski, M. 2004. Ultimate approximation and its application in nonmonotonic knowledge representation systems. Information and Computation 192(1):84 121. Denecker, M.; Marek, V. W.; and Truszczy nski, M. 2011. Reiter s default logic is a logic of autoepistemic reasoning and a good one, too. In Brewka, G.; Marek, V.; and Truszczy nski, M., eds., Nonmonotonic Reasoning Essays Celebrating Its 30th Anniversary. College Publications. 111 144. Faber, W.; Pfeifer, G.; and Leone, N. 2011. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell. 175(1):278 298. Ferraris, P. 2005. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 119 131. Fitting, M. 2002. Fixpoint semantics for logic programming a survey. Theoretical Computer Science 278(1-2):25 51. Gelfond, M., and Lifschitz, V. 1988. The stable model semantics for logic programming. In Kowalski, R. A., and Bowen, K. A., eds., ICLP/SLP, 1070 1080. MIT Press. Gelfond, M., and Zhang, Y. 2014. Vicious circle principle and logic programs with aggregates. TPLP 14(4-5):587 601. Kleene, S. C. 1938. On notation for ordinal numbers. The Journal of Symbolic Logic 3(4):pp. 150 155. Konolige, K. 1988. On the relation between default and autoepistemic logic. Artif. Intell. 35:343 382. Lifschitz, V. 2008. Twelve deﬁnitions of a stable model. In Garc ıa de la Banda, M., and Pontelli, E., eds., ICLP, volume 5366 of LNCS, 37 51. Springer. Marek, V. W.; Niemel a, I.; and Truszczy nski, M. 2008. Logic programs with monotone abstract constraint atoms. TPLP 8(2):167 199. Pelov, N.; Denecker, M.; and Bruynooghe, M. 2007. Wellfounded and stable semantics of logic programs with aggregates. TPLP 7(3):301 353. Son, T. C.; Pontelli, E.; and Elkabani, I. 2006. An unfoldingbased semantics for logic programming with aggregates. Co RR abs/cs/0605038. Strass, H. 2013. Approximating operators and semantics for abstract dialectical frameworks. Artif. Intell. 205:39 70. van Emden, M. H., and Kowalski, R. A. 1976. The semantics of predicate logic as a programming language. J. ACM 23(4):733 742. Van Gelder, A.; Ross, K. A.; and Schlipf, J. S. 1991. The well-founded semantics for general logic programs. J. ACM 38(3):620 650. Vennekens, J.; Gilis, D.; and Denecker, M. 2006. Splitting an operator: Algebraic modularity results for logics with ﬁxpoint semantics. ACM Trans. Comput. Log. 7(4):765 797.