Partial Grounded Fixpoints

1 Introduction

Approximation fixpoint theory (AFT) is an algebraical unifying study of semantics of nonmonotonic logics. Given a lattice operator and a so-called approximating bilattice operator, Denecker, Marek and Truszczy´nski (henceforth DMT) [2000] defined several types of fixpoints. They showed that all of the main semantics of logic programming are induced by AFT, using Fitting's partial immediate consequence operator as an approximator of the two-valued immediate consequence operator. They identified approximating operators for default logic (DL) [Reiter, 1980] and autoepistemic logic (AEL) [Moore, 1985] and showed that AFT induces all main and some new semantics in these fields [Denecker et al., 2003].

Recently, AFT was used in a broader context. It was used to study properties such as modularity and predicate introduction in a unifying framework by Vennekens et al. [2007; 2006]. Strass [2013] showed that many semantics for Dung's argumentation frameworks (AFs) [Dung, 1995] and abstract dialectical frameworks (ADFs) [Brewka and Woltran, 2010] can be retrieved by application of AFT. In this study, he also extends AFT with new types of fixpoints. Bi et al. [2014] extended AFT to account for inconsistencies and used this to integrate logic programs with description logics. Bogaerts et al. [2014] defined the causal logic FO(C) based on AFT.

Bogaerts et al. [2015] extended AFT with a concept called groundedness which is a surprisingly simple formalisation of intuitions that have existed in different research domains for years. They showed that grounded fixpoints are an intuitive concept, closely related to exact (two-valued) stable fixpoints. In the context of logic programming, grounded fixpoints can be characterised using a generalised notion of unfounded set.

Grounded fixpoints are lattice elements; in this work, we generalise them to points in the bilattice, while still maintaining the elegance and desirable properties of groundedness. For the case of logic programming, this generalisation boils down to extending groundedness to partial (or three-valued) interpretations. There are several reasons why it is important to generalise a notion as groundedness to a partial context.

The first, and probably most obvious one, is that sometimes partial fixpoints are a central topic of study themselves. As an example, in AFs and ADFs, most of the studied semantics are three-valued.

A second reason is that studying concepts in the bilattice (i.e., in a partial context) is more general than studying them only in the original lattice. For example, many of our results are generalisations of results from Bogaerts et al. [2015]; sometimes, these generalisations even fill holes in their theory. E.g., while Bogaerts et al. [2015] showed that exact Astable fixpoints are grounded, we show that all A-stable fixpoints are A-grounded. Also, while Bogaerts et al. [2015] showed that, if the well-founded fixpoint is exact, then it is grounded, we show that the A-well-founded fixpoint is always A-grounded. This last result illustrates that the wellfounded semantics does a great job at avoiding ungrounded models: the well-founded model is not just some grounded model, it is the least precise grounded model.

A third reason is that even in domains where we are only interested in two-valued models, partial models can be useful, e.g., as an analysis tool. For example, in answer set programming [Marek and Truszczy´nski, 1999] almost all specifications are designed for two-valued stable model semantics. Errors in such specifications may lead to logic programs without stable models; they are hard to debug. Partial stable models [Przymusinski, 1991] can help the debugging process as they can sometimes pinpoint the reason for inconsistency. As a trivial example, let Σ be a vocabulary and p a symbol not in Σ. Augmenting any logic program over Σ with the rule

yields a logic program without stable models. Debugging tools can use the observation that p is undefined in every partial stable model to identify the "mistake" in the above program, namely the extra rule. The technique of debugging knowledge bases based on partial stable models is used for example in the XNMR system [Castro and Warren, 2001]. Partial stable models are not only used for debugging. Real-life databases often contain (local) inconsistencies. The partial stable model semantics for deductive databases is more robust than the two-valued stable semantics in this case. It only assigns the value unknown to atoms in an inconsistent part of the database, hence it still facilitates inference on the rest of the database [Seipel et al., 1997; Eiter et al., 1997].

Summarised, the main contributions of this paper are as follows.

1. We extend the notion of groundedness to points in the bilattice.
2. We study the relationship between partial grounded fixpoints and the other fixpoints studied in AFT. An important result in this context is that we find a new characterisation of the well-founded fixpoint based on groundedness.
3. We study how partial grounded fixpoints depend on the choice of an approximator.
4. We apply our theory to logic programming.
5. We study complexity of both credulous and sceptical reasoning of partial grounded model semantics in logic programming.

2 Preliminaries

In this section, we recall the basics of AFT. Our presentation follows the preliminaries section from Bogaerts et al. [2015].

Lattices and Operators A complete lattice 〈L,≤〉 is a set L equipped with a partial order ≤, such that every set S ⊆ L has both a least upper bound and a greatest lower bound, denoted lub(S) and glb(S) respectively. A complete lattice has a least element ⊥ and a greatest element ⊤. As custom, we also use the notations ∧ S = glb(S), x∧y = glb({x, y}), ∨ S = lub(S) and x ∨ y = lub({x, y}).

An operator O : L → L is monotone if x ≤ y implies that O(x) ≤ O(y). An element x ∈ L is a prefixpoint, a fixpoint, a postfixpoint if O(x) ≤ x, respectively O(x) = x, x ≤ O(x). Every monotone operator O in a complete lattice has a least fixpoint, denoted lfp(O), which is also O's least prefixpoint.

Approximation Fixpoint Theory Given a lattice L, AFT makes uses of the bilattice L2 . We define projections 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 order on L2 is defined as (x, y)≤p (u, v) if x ≤ u and v ≤ y. If (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 so is 〈L2 , ≤p 〉.

AFT studies fixpoints 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) ∈ [x′ , y′ ], where (x′ , y′ ) = 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. DMT [2004] showed that the consistent fixpoints of interest (supported, stable, well-founded) are uniquely determined by an approximator's restriction to Lc , hence, sometimes we only define approximators on Lc .

AFT studies fixpoints of O using fixpoints of A.

• The A-Kripke-Kleene fixpoint is the ≤p -least fixpoint of A and has the property that it approximates all fixpoints of O.
• A partial A-stable fixpoint 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 ↦→ A(x, y)1 and analogously for A(x, ·)2.
• The A-well-founded fixpoint is the least precise partial A-stable fixpoint.
• An A-stable fixpoint of O is a fixpoint x of O such that (x, x) is a partial A-stable fixpoint.

The A-Kripke-Kleene fixpoint of O can be constructed by iteratively applying A, starting from (⊥,⊤). For the A-wellfounded fixpoint, a similar constructive characterisation has been worked out by Denecker and Vennekens [2007].

Definition 2.1. An A-refinement of (x, y) is a pair (x′ , y′ ) ∈ L2 satisfying one of the following two conditions:

• (x, y)≤p (x′ , y′ )≤p A(x, y), or
• x′ = x and A(x, y′ )2 ≤ y′ ≤ y.

An A-refinement is strict if (x, y) ̸= (x′ , y′ ).

Definition 2.2. A well-founded induction of A is a sequence (xi, yi)i≤β with β an ordinal such that

• (x0, y0) = (⊥,⊤);
• (xi+1, yi+1) is an A-refinement of (xi, yi), for all i < β;
• (xλ, yλ) = lub≤p {(xi, yi) | i < λ} for each limit ordinal λ ≤ β.

A well-founded induction is terminal if its limit (xβ, yβ) has no strict A-refinements.

For an approximator A, there are many different terminal well-founded inductions of A. Denecker and Vennekens [2007] showed that they all have the same limit, which equals the A-well-founded fixpoint of O. If A is symmetric, the A-well-founded fixpoint of O (and in fact, every tuple in a well-founded induction of A) is consistent.

In general, a lattice operator O : L → L has a family of approximators of different precision. For two approximators A and B of O, we say that A≤p B if A(x, y)≤p B(x, y)

for all (x, y) ∈ Lc . In this case, all A-stable fixpoints are Bstable fixpoints, and the B-well-founded fixpoint is more precise than the A-well-founded fixpoint. DMT [2004] showed that there exists a most precise approximator, UO, called the ultimate approximator of O. This operator is defined by UO : Lc → Lc : (x, y) ↦→ (∧ O([x, y]), ∨ O([x, y])), where O([x, y]) = {O(z) | z ∈ [x, y]}.

Bogaerts et al. [2015] called a point x ∈ L grounded for O if for each v ∈ L such that O(v ∧ x) ≤ v, it holds that x ≤ v. They explained the intuition underlying this concept under the assumption 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.

AFT and Logic Programming We restrict our attention to propositional logic programs with arbitrary propositional formulas in rule bodies. AFT has been applied in a much broader context [Denecker et al., 2012; Pelov et al., 2007; Antic et al., 2013] and our results extend there as well.

Let Σ be an alphabet, i.e., a collection of symbols which are called atoms. 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 Σ is 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 defined 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

Elements of the bilattice (2Σ)2 are four-valued interpretations, pairs I = (I1, I2) of interpretations. The pair (I1, I2) approximates all interpretations I ′ with I1 ⊆ I ′ ⊆ I2. We are mostly concerned with three-valued (or, partial) 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 Kleene's truth tables [Kleene, 1938]. We identify interpretation I with the partial interpretation (I, I). If I = (I1, I2) is a (partial) interpretation, and U ⊆ Σ, we write I[U : f] (respectively I[U : t]) for the (partial) interpretation that equals I on all elements not in U and that interprets all elements in U as f (respectively t), i.e., the interpretation (I1 \U, I2 \U) (respectively (I1 ∪ U, I2 ∪ U)).

Several approximators have been defined for logic programs. The most common is Fitting's immediate consequence operator ΨP [Fitting, 2002], a direct generalisation of TP to partial interpretations defined by

Denecker et al. [2000] showed that the ΨP-well-founded fixpoint is the well-founded model of P [Van Gelder et al., 1991] and that ΨP -stable fixpoints are exactly the stable models of P [Gelfond and Lifschitz, 1988].

In the context of logic programming, Bogaerts et al. [2015] defined that a set U ⊆ Σ is a 2-unfounded set of P with respect to interpretation I if TP(I[U : f]) ∩U = ∅. Intuitively, a 2 unfounded set is a set of atoms such that if you make them false (starting from I), they stay false (when applying TP). They showed that this definition is a slight variant of the notion of unfounded set defined by Van Gelder et al. [1991]. Furthermore, they generalised 1 this definition to partial interpretations, resulting in a definition which is equivalent with the definition by Van Gelder et al. [1991] for all interpretations used in the well-founded model construction. Bogaerts et al. [2015] showed that an interpretation I is grounded for TP if and only if I does not contain any atoms that belong to a 2-unfounded set U of P with respect to I.

3 Partial Grounded Fixpoints

We start by giving the central definition of this text, namely the notion of A-groundedness.

Definition 3.1. Let A be an approximator of O. A point (x, y) ∈ Lc is A-grounded if for every v ∈ L with A(x ∧ v, y ∧ v)2 ≤ v, also y ≤ v.

The definition of this concept is a direct generalisation of groundedness for points x ∈ L. It is based on the same intuitions, but applied in a more general context. We again explain the intuitions under the assumption that the elements of L are sets of "facts" and the ≤ relation is the subset relation between such sets. In this case, a point (x, y) ∈ Lc represents a partial set of "facts": the elements of x are the facts that certainly belong to the partial set, the elements in y are those that possibly belong to the set. Thus, y \ x are the unknown elements and the complement of y are those that do not belong to the set. In this case, a point (x, y) is A-grounded if all its possible facts (those in y) are sanctioned by the operator A, in the sense that if we remove some elements from the partial set, then A will make at least one of them possible again. The above definition captures this idea, by using a set v ∈ L to remove all elements not in v from (x, y): the point (x ∧ v, y ∧ v) does not contain facts in the complement of v; on all other facts, (x ∧ v, y ∧ v) equals (x, y). In an A-grounded point (x, y) removing elements must result in a state where at least one of them is re-derived to be possible: it must hold that A(x ∧ v, y ∧ v)2 ̸≤ v. Stated differently, if the removal of elements from (x, y) is not contradicted by A, i.e., applying A results in a state where these elements are still false, then these elements cannot be part of the grounded point (y ≤ v). In what follows, we study properties of A-grounded (fix)points, including their relation to other fixpoints studied in AFT. A first observation is that for exact points, i.e., bilattice points of the form (x, x), the choice of the approximator A does not matter and our notion of groundedness coincides with the previously defined.

1 We come back to this in Section 4 and show that there are in fact many ways to extend this definition to partial interpretations.

Proposition 3.2. If A is a symmetric approximator of O, then x is grounded for O if and only if (x, x) is A-grounded.

Proof. Trivial. Follows immediately from the fact that A(x, x)2 = O(x) for all x ∈ L if A is symmetric.

A second observation is that all partial A-stable fixpoints are A-grounded. This is a generalisation of Corollary 4.5 from Bogaerts et al. [2015] which showed that all exact stable fixpoints are grounded.

Proposition 3.3. All consistent (partial) A-stable fixpoints are A-grounded.

Proof. Suppose (x, y) ∈ Lc is an A-stable fixpoint, i.e., x = lfp(A(·, y)1) and y = lfp(A(x, ·)2). Also assume that for some v, A(x ∧ v, y ∧ v)2 ≤ v. We show that y ≤ v. Since A is ≤p -monotone and y ∧ v ≤ y, it holds that

Analogously, since A is ≤p -monotone and x ∧ v ≤ x, it holds that

Combining these two observations, we find that

i.e., that y ∧ v is a prefixpoint of the monotone operator A(x, ·)2. Since y is the least prefixpoint of this operator, it must hold that y ≤ y ∧ v, thus also that y ≤ v, which we needed to show.

Example 3.4. The converse of Proposition 3.3 does not hold. Consider the logic programP

We claim that every bilattice point is ΨP-grounded in this case. Indeed, if (x, y) ∈ L2 , then for v = {p}, y ≤ v is trivially true, for v = ∅, it holds that

Hence, all points in the bilattice are ΨP-grounded. Thus, ({p}, {p}) is a ΨP -grounded fixpoint which is not ΨP -stable.

A third observation is that the A-well-founded fixpoint is less precise than any A-grounded fixpoint. This property generalises both the fact that the A-well-founded fixpoint approximates all exact grounded fixpoints of O (Theorem 4.6 from Bogaerts et al. [2015]) and the fact that the A-well-founded fixpoint is less precise than any partial A-stable fixpoint (Theorem 23 (2) from DMT [2000]).

Theorem 3.5. The well-founded fixpoint (u, v) of a symmetric approximator A of O is less precise than any A-grounded fixpoint.

Before we prove this theorem, we show that the second type of refinements in a well-founded induction eliminates only non-grounded bilattice points.

Lemma 3.6. Let (a, b) and (a, b′ ) be elements of Lc such that A(a, b′ )2 ≤ b′ ≤ b. Then for every b′′ with b′ ⪇ b′′ ≤ b, (a, b′′ ) is ungrounded.

Proof. For every such b′′ it holds that A(a ∧ b′ , b′′ ∧ b′ )2 = A(a, b′ )2 ≤ b′ while b′′ ̸≤ b′ .

Proof of Theorem 3.5. Let (ai, bi)i≤β be a well-founded induction of A and let (x, y) be an A-grounded fixpoint. We show by induction that for every i ≤ β, ai ≤ x and y ≤ bi. The results trivially holds for i = 0 since (a0, b0) = (⊥,⊤). It is also clear that the property is preserved in limit ordinals. Hence, all we need to show is that the property is preserved by A-refinements. Suppose (a′ , b′ ) is an A-refinement of (a, b) and that (a, b)≤p (x, y). We show that (a′ , b′ )≤p (x, y). We distinguish two cases. If (a, b)≤p (a′ , b′ )≤p A(a, b), then since A is ≤p -monotone and (a, b)≤p (x, y), it holds that A(a, b)≤p A(x, y) = (x, y), hence also (a′ , b′ )≤p (x, y). For the second type of refinements, it follows from Lemma 3.6 that only ungrounded bilattice points are removed.

It is well-known that the A-well-founded fixpoint is characterised as the least precise A-stable fixpoint. The previous theorem provides us with a similar characterisation of the well-founded fixpoints in terms of groundedness. This is an important result, as it again supports the claim that many of the existing semantics are designed with the intuitions of groundedness in mind: we establish a very tight link between the well-founded fixpoints and grounded fixpoints.

Corollary 3.7. The well-founded fixpoint of a symmetric approximator A of O is the least precise A-grounded fixpoint.

Proof. The well-founded fixpoint of A is consistent and Astable, hence Proposition 3.3 shows that it is A-grounded as well. Theorem 3.5 shows that it is less precise than any Agrounded fixpoint, hence the result follows.

An operator can have multiple approximators. In Proposition 3.2, we already showed that the choice of approximator A does not affect exact A-grounded fixpoints: these are exactly the fixpoints that are grounded for O. The question still remains how groundedness of other points in the bilattice is influenced by such a choice. The next proposition answers this question.

Proposition 3.8. If A and B are approximators of O and A≤p B, then all consistent B-grounded points are also Agrounded.

Proof. Suppose (x, y) ∈ Lc is B-grounded; we show that it is also A grounded. Assume that for some v it holds that A(x ∧ v, y ∧ v)2 ≤ v. Since A≤p B, it holds that

Since (x, y) is B-grounded, we find that y ≤ v.

Example 3.9. The choice of an approximator can really make a difference for the notion of A-groundedness, i.e., not all Agrounded points are B-grounded in Proposition 3.8. Consider the logic program P

Then ({q}, {p, q}) is not ΨP-grounded since

while {p, q} ̸≤ {p}.

However, let A be the trivial approximator of TP, i.e., the approximator such that A(x, x) = (TP(x), TP(x)) for every x ∈ L and A(x, y) = (⊥,⊤) for (x, y) ∈ Lc with x ̸= y. We claim that ({q}, {p, q}) is A-grounded. We prove this claim by showing that all v ∈ L satisfy the condition from Definition 3.1. For v = ⊤ the condition y ≤ ⊤ is trivially satisfied. For v = {q}, we find

For v = {p}, we find

since ({q} ∧ {p}, {p, q} ∧ {p}) is not exact. For v = ∅, we find that

This indeed proves our claim.

4 Partial Grounded Fixpoints in Logic Programming

In this section, we apply our theory to logic programming. More concretely we extend the observation that in logic programming, groundedness is closely related to unfounded sets [Bogaerts et al., 2015]. We define several variants of unfounded sets (one for each approximator of TP) and show that A-groundedness is directly characterised by means of Aunfounded sets. When taking for A Fitting's (partial) immediate consequence operator, our definition coincides with the notion of "3-unfounded set" [Bogaerts et al., 2015].

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 a partial interpretation I is a set U of atoms such that P provides no support for any atom in U if the atoms in U are assumed false. Each approximator A of the immediate consequence operator TP defines its own notion of support: it maps a partial interpretation I to A(I), where A(I)1 are the atoms that are supported by P, and A(I)2 are the atoms that are possibly supported by P, depending on the values of atoms unknown in I. Thus, the atoms for which A provides no support are those not in A(I)2 and the above intuitions are formalised directly as follows.

Definition 4.1 (A-Unfounded set). Let P be a logic program, A an approximator of TP and I a three-valued interpretation. A set U ⊆ Σ is an A-unfounded set of P with respect to I if A(I[U : f])2 ∩U = ∅.

When A is Fitting's immediate consequence operator, our definition coincides with the notion of 3-unfounded set defined by Bogaerts et al. [2015]. They showed that for partial interpretations I such that I[U : f] is more precise than I, ΨP-unfounded sets are exactly unfounded sets as defined by Van Gelder et al. [1991] and that all interpretations in the well-founded model construction satisfy this condition.

We now show how groundedness relates to this generalised notion of unfounded sets. This proposition generalises Proposition 5.5 from Bogaerts et al. [2015].

Proposition 4.2. Let P be a logic program, and A an approximator of the immediate consequence operator TP. A partial interpretation I is A-grounded if and only if all atoms that belong to an A-unfounded set U of P with respect to I are false in I.

Proof. First, suppose I = (I1, I2) is A-grounded and U is an A-unfounded set of P with respect to I. Let V = U c . Since U is an A-unfounded set, A(I[U : f ])2 ∩ U = ∅. This means that A(I1 ∧ V, I2 ∧ V )2 ≤ V , hence the definition of A-groundedness yields I2 ≤ V : all elements of U are false in I. This must hold for every A-unfounded set U.

The reverse direction is analogous. Suppose every Aunfounded set is disjoint from I2. Let V be such that A(I1 ∧ V, I2 ∧ V )2 ≤ V and let U = V c . Then again I[U : f ] = (I1 ∧V, I2 ∧V ) hence U is an A-unfounded set of P with respect to I. Thus, it must hold that I2 ∩U = ∅, i.e., that I2 ≤ V . We conclude that I is indeed A-grounded.

Following the analogy with the classical semantics of logic programs, we call a partial interpretation I such that I is a ΨP-grounded fixpoint of TP a partial grounded model of P. We briefly discuss complexity of partial grounded model semantics. First of all, deciding whether P has a partial grounded model is not an interesting task since the well-founded model is always grounded. We study other deterministic inference tasks, namely credulous and sceptical query answering (sometimes also called possibility inference and certainty inference, respectively) [Schlipf, 1995; Abiteboul et al., 1990; Sacc`a, 1997] under the (partial) grounded semantics. The first of these tasks consists of deciding whether a symbol p ∈ Σ holds in some grounded model, the second consists of deciding whether it holds in all grounded models.

Theorem 4.3. Given a finite propositional logic program P over Σ and an atom p ∈ Σ, the following hold.

1. The problem of deciding whether p holds in some partial grounded model of P is ΣP2 -complete.
2. The problem of deciding whether p holds in all partial grounded models of P is in P .

The first of these points is proven analogous to the proof of Theorem 5.7 by Bogaerts et al. [2015]. Our proof is heavily inspired by theirs.

Proof. This first problem is in ΣP2 ; this follows from the fact that verifying whether a partial interpretation I is a partial grounded model can be done by calculating ΨP(I[U : f ]) for all candidate ΨP-unfounded sets.

We now show ΣP2 -hardness of the problem of existence of a (partial) grounded model of a program P in which p holds. Let ϕ be propositional formula in DNF over propositional symbols x1, . . . , xm, y1, . . . , yn. For an interpretation I ⊆ {x1, . . . , xm}, we define ϕI as the formula obtained from ϕ by replacing all atoms xi ∈ I by t and all atoms xi ̸∈ I by f . Recall that the problem of deciding whether there exists an interpretation I ⊆ {x1, . . . , xm} such that ϕI is a tautology is ΣP2 -hard. We now reduce this problem to our problem. For each xi, we introduce a new variable x′i with as intended meaning the negation of xi. Let ϕ′ be the formula obtained from ϕ by replacing all literals ¬xi by x′i . Bogaerts et al. [2015] defined a program P(ϕ) consisting of the following clauses

We need to show that there is an I ⊆ {x1, . . . , xm} such that ϕI is a tautology if and only if P(ϕ) has a partial grounded model in which p holds.

Bogaerts et al. [2015] already showed that there is an I ⊆ {x1, . . . , xm} such that ϕI is a tautology if and only if P(ϕ) has an exact grounded model. Hence, all we need to show is that if P(ϕ) has a partial stable fixpoint, then there is such an I as well. We will prove a stronger claim, namely that every partial grounded model of P(ϕ) in which p holds can be extended to a two-valued grounded model in which p holds.

It is easy to see that in each partial fixpoint M of ΨP(ϕ) with pM = t the following properties hold:

1. y1, . . . , yn are true inM (since their rules have the same body as p),
2. for each i ∈ {1, . . . ,m}, either both xi and x′i are unknown in M or one of them is true and the other is false in M.

Now, suppose M is a partial grounded model of P. By the above observations, the only unknown atoms in M can be q, the xi and the x′i . Now, it is easy to see that M[{q} : f ] is also a grounded model of P. Similarly, if xi and x′i are unknown inM, thenM[{xi} : t, {x′i} : f ] is a grounded model as well. Hence, our claim follows.

The second point follows from the fact that the wellfounded model of P can be computed in polynomial time and that the well-founded model is the least precise partial grounded model (Corollary 3.7).

5 Discussion and FutureWork

Other classes of partial models In the context of logic programming and argumentation frameworks, many subclasses of partial stable models have been proposed.

• A partial stable model (X, Y ) of P is called M-stable (for maximally stable) if it is ≤p maximal, i.e., if there is no more precise partial stable model [Sacc`a and Zaniolo, 1997]. These models coincide with the preferred extensions of Dung [1995] and the regular models of You and Yuan [1990].
• A partial stable model (X, Y ) of P is called L-stable (for least undefined stable) if Y \ X is ⊆-minimal, i.e., if there exists no partial stable model (X′ , Y ′ ) of P such

that Y ′ \ X′ ⊊ Y \ X [Sacc`a and Zaniolo, 1997]. Lstable models only differ from exact stable models if a program has no two-valued stable models. This property is particularly useful in the context of debugging.

Recent work by Strass [2013] lifted these two notions to approximation fixpoint theory. 2 His definitions can be used immediately to define partial M-grounded and L-grounded fixpoints as well. Studying their properties, e.g., complexity, is a topic for future work.

Non-deterministic operators Pelov and Truszczynski [2004] characterised stable fixpoints of a disjunctive logic program using non-deterministic operators. Lots of work remains to be done in this area. Extending approximation fixpoint theory in general, and groundedness in particular to non-deterministic operators remains a topic for future work.

Applications In this paper, we only applied our theory to logic programming. However, as already indicated, our theory applies to all domains in which AFT is applied. Working out these applications is a topic for future work as well.

6 Conclusion

In this paper, we extended groundedness to points in the bilattice: for every approximating operator A, we defined a notion of A-groundedness. We showed that for exact lattice points, this coincides with groundedness for O. We related A-grounded fixpoints to other fixpoints in AFT: all A-stable fixpoints are A-grounded and the A-well-founded fixpoint is uniquely characterised as the least precise A-grounded fixpoint.

We applied our algebraical theory to logic programming, where A-groundedness is closely related to unfounded sets. Applying the theory to other research domains, such as default logic, autoepistemic logic and abstract dialectical frameworks is a topic for future work.

Acknowledgements We would like to thank the anonymous reviewers and Maurice Bruynooghe for their feedback on this work. This work was supported by the KU Leuven under project GOA 13/010 and by the Research Foundation - Flanders (FWO-Vlaanderen).