Stable Model Semantics of Abstract Dialectical Frameworks Revisited: A Logic Programming Perspective

1 Introduction

Abstract argumentation frameworks (AFs; Dung 1995) are used to represent and reason about the fundamental mechanism humans use in argumentation. A well-known example is the Nixon diamond, whose arguments "Nixon is antipacifist since he is a republican" and "Nixon is a pacifist since he is a quaker" attack each other. AFs are represented by graphs whose nodes represent abstract arguments, where abstract refers to the fact that the content of these arguments is not further analyzed. What is analyzed instead is the attack relation, represented by links: an argument is accepted if it is not attacked by any accepted arguments.

Abstract dialectical frameworks (ADFs; Brewka and Woltran 2010) are extensions of AFs that essentially allow for

∗Mario Alviano was partly supported by MIUR within project "SI-LAB BA2KNOW - Business Analitycs to Know", by Regione Calabria, POR Calabria FESR 2007-2013, within project "ITravel PLUS" and project "KnowRex", by the National Group for Scientific Computation (GNCS-INDAM), and by Finanziamento Giovani Ricercatori UNICAL.

Wolfgang Faber

University of Huddersfield, UK wf@wfaber.com

more expressive acceptance conditions. In fact, each statement, or argument, of an ADF is associated with a Boolean function whose domain is the power set of the set of parent nodes of the statement. Intuitively, a set of parent nodes is mapped to true if their acceptance jointly supports the statement. Conversely, a set of parent nodes is mapped to false if their acceptance jointly attacks the statement. As an example, consider a scenario in which three lazy programmers a, b, c are asked to accomplish a specific task. Programmer a will work on the task if and only if she can take all the glory (i.e., if neither b nor c will work) or if the total amount of work is minimal (i.e., if both b and c will work as well). Programmer b will work if and only if the amount of work is reasonable, i.e., if a or c will work as well. Programmer c will work if and only if also b will work, regardless of what a will do. Boolean functions can be represented by propositional wellformed formulas, which suggests a syntactic similarity with logic programs with generalized atoms, referred to as logic programs with Boolean functions (LPBFs) in this paper.

Several semantics have been proposed for ADFs, among them stable models [Brewka et al., 2013; Strass, 2013]. Roughly, a model is considered stable if it can be reconstructed via logical entailment in the reduced ADF obtained by constraining the original acceptance conditions. Different notions of logical entailment and reduct result in different stable model semantics. Stable models are also defined for LPBFs [Pelov et al., 2007; Son and Pontelli, 2007; Shen and Wang, 2012; Gelfond and Zhang, 2014; Faber et al., 2011; Ferraris, 2005]. A natural question is thus "What relations do exist between these notions of stable models?"

This paper provides an answer to this question by introducing mappings from the two formalisms to what will be referred to as definitorial LPBFs, i.e., LPBFs in which each propositional atom is defined by exactly one rule whose body consists of exactly one Boolean function. By restating the original definitions of stable models, the paper will shed light on the similarities and differences between these semantics. In particular, stable models by Brewka et al. are equivalent to those by Pelov et al., Son and Pontelli and by Shen and Wang, while stable models by Strass are equivalent to those by Gelfond and Zhang. The new, restated definitions will also demonstrate a subset-containment relation between these semantics: every stable model of Gelfond and Zhang is a stable model of Son and Pontelli, and the inclusion is strict as the other direction does not hold in general.

A further advantage of the unifying framework presented in this paper is that implemented systems for LPBFs are usable for ADFs, and vice versa. For example, the answer set programming (ASP) solvers CLASP [Gebser et al., 2009] and DLV [Alviano et al., 2011] compute stable models as defined by Ferraris and Faber et al., respectively, which are known to be equivalent to the definition by Pelov et al., Son and Pontelli and Shen and Wang for a large class of Boolean functions known as convex [Alviano and Faber, 2013], and therefore also to the notion by Brewka et al. thanks to the result in this paper. Hence, for ADFs whose accepting conditions can be expressed by standard aggregates, a one-to-one mapping to the input language of CLASP is possible. On the other hand, the rewritings implemented in DIAMOND [Brewka et al., 2013; Ellmauthaler and Strass, 2014] to map ADFs to ASP can be used in ASP as well to encode convex Boolean functions other than standard aggregates. The simplicity of the new characterizations also suggests a strategy for computing stable models by Strass and by Gelfond and Zhang within an ASP solver. Moreover, the unifying framework brings several complexity results from one formalism to the other, possibly making the future complexity analysis even more attractive as new results will immediately apply to both LPBFs and ADFs. Finally, stable models by Faber et al. and Ferraris, popular in LPBFs but having no counterpart in ADFs, are also restated in terms of the unifying framework. The lazy programmers example will be used to illustrate what differences there are to the existing semantics, and why stable models by Faber et al. and by Ferraris can be considered a valid point of view also for ADFs. Proofs and a tool for computing Strass stable models by modern ASP solvers such as CLASP [Gebser et al., 2009] or WASP [Alviano et al., 2013; 2014] are available at http://alviano.net/software/adf/.

2 Background

This section introduces basic notions concerning ADFs and LPBFs.

2.1 Boolean Functions and Interpretations

Let T,U,F denote the truth values true, undefined and false, respectively. Let V be a set of propositional variables, also referred to as statements or atoms. A Boolean function f is a function f : 2D → {T, F}, where D ⊆ V defines the domain of f. For such a function f, the set D is denoted by dom(f), and f(V ) will be used as a shorthand for f(dom(f)∩V ), for all V ⊆ V.

Example 1. Simple Boolean functions are represented by conjunctions, disjunctions, and in general well-formed propositional formulas. In fact, the conjunction a ∧ (b ∨ c) defines a function f such that dom(f) = {a, b, c}, f({a, b}) = f({a, c}) = f({a, b, c}) = T, and f(∅) = f({a}) = f({b}) = f({c}) = f({b, c}) = F. Also aggregates define Boolean functions: COUNT({a, b}) = 1 defines a function f such that dom(f) = {a, b}, f({a}) = f({b}) = T, and f (∅) = f ({a, b}) = F. ■

An interpretation is a pair (L,U) such that L ⊆ V and U ⊆ V, where L,U are called lower and upper bound, respectively. This is based on a common representation of fourvalued interpretations that stores true atoms (L) and possibly true atoms (U). Intuitively, atoms in L are true, those in U \ L are undefined, those in V \ U are false, and those in L \ U are inconsistent. An interpretation (L′ ,U ′ ) extends an interpretation (L,U), denoted (L,U) ≤k (L′ ,U ′ ), if L′ ⊇ L and U ′ ⊆ U. Relation ≤k corresponds to the knowledge order, i.e., undefined atoms do not increase in an extension. An interpretation (L,U) is total or two-valued if L = U; in this case, the interpretation will be usually denoted L. Two sets S, S′ of total interpretations are equivalent with respect to a context V ⊆ V, denoted S ≡V S′ , if {I ∩ V | I ∈ S} = {I ∩ V | I ∈ S′}.

A Boolean function f is true with respect to an interpretation (L, U) if f(I) = T for all I ⊆ V such that (L, U) ≤k I. Similarly, f is false if f(I) = F for all I ⊆ V such that (L,U) ≤k I. If none of the previous cases apply then f is considered undefined. These concepts are formalized next.

Definition 1. The evaluation of a Boolean function f with respect to an interpretation (L, U) is defined as follows:

(Note that L ̸⊆ U implies [f](L,U) = T for all functions.)

2.2 Abstract Dialectical Frameworks

An abstract dialectical framework F is a triple 〈S,E,C〉, where: S is a nonempty, finite set of statements; E ⊆ S × S is a set of links; C = {Cs}s∈S is a set of Boolean functions, where dom(Cs) = par(s), with par(s) denoting the parents of s in the graph 〈S,E〉. Each Cs is referred to as the acceptance condition of s.

A total interpretation I is a model of F, denoted I |= F, if s ∈ I whenever [Cs]I = T. A stable model semantics for ADF was proposed by Brewka et al. (2013). It is based on the following operator:

where F is an ADF, and (L, U) is an interpretation. The least fixpoint of ΓF is denoted by ΓF ⇑ (∅, S).

Definition 2 (Brewka et al.). A total interpretation I is a B-stable model of an ADF F = 〈S,E,C〉 if I |= F and I = ΓF ′ ⇑ (∅, S), where F ′ = 〈I,E ∩ (I × I), {C ′s }s∈I〉, and C ′s is a Boolean function with domain par(s) ∩ I and such that C ′s (A) = T if and only if both Cs(A) = T and (par (s) \ A) ∩ I = ∅, for all A ⊆ par (s).

A different notion of stable model was proposed by Strass (2013). In particular, the characterization in (the proof of) Proposition 3.9 in [Strass, 2013] is based on the least fixpoint GIF ⇑ ∅ of the following operator:

where F = 〈S,E,C〉 is an ADF, I is a total interpretation, and X ⊆ S.

Definition 3 (Strass). A total interpretation I is an S-stable model of an ADF F = 〈S, E, C〉 if I = GIF ⇑ (∅, S).

The two semantics are not equivalent.

Example 2. Consider an ADF F1 = 〈S, E, C〉 such that:

• S = {a, b}, and E = {(a, a), (b, a), (b, b)};
• Ca(∅) = Ca({a}) = Ca({a, b}) = T, Ca({b}) = F;
• Cb({b}) = T, and Cb(∅) = F.

F1 has one stable model, {a}, according to Brewka et al.. In fact, {a} |= F1, and ADF F ′1 is 〈{a}, {(a, a)}, {C′a}〉, where dom(C′a ) = {a} and C ′a (∅) = C ′a ({a}) = T. Hence, the least fixpoint of ΓF ′1 is {a}. On the other hand, F1 has no stable model according to Strass. In particular, {a} is not stable because the least fixpoint of G{a} F1 is ∅. ■

Example 3. Consider an ADF F2 = (S, E, C) such that:

• S = {a, b, c}, and E = {(a, b), (a, c), (b, a), (c, c)};
• Ca(∅) = T, Ca({b}) = F; Cb(∅) = T, Cb({a}) = F;
• Cc({b}) = Cc({b, c}) = T; Cc(∅) = Cc({c}) = F.

Interpretation {a} is a stable model according to both Brewka et al. and Strass, while {b, c} is a stable model only according to Brewka et al. ■

2.3 Logic Programs with Boolean Functions

A logic program with Boolean functions Π is a set of rules of the form p ← f, where p ∈ V and f is a Boolean function. The set of atoms occurring in Π is denoted by At (Π). A total interpretation I is a model of Π, denoted I |= Π, if p ∈ I whenever [f]I = T, for all p ← f ∈ Π.

Stable models by Pelov et al. (2007), Son and Pontelli (2007) and by Shen and Wang (2012) are defined by means of the least fixpoint KIΠ ⇑ ∅ of the following operator:

where Π is an LPBF, I is a total interpretation, and X ⊆ V.

Definition 4 (Pelov et al., Son and Pontelli, Shen and Wang). A total interpretation I is a stable model of an LPBP Π if I = KIΠ ⇑ ∅.

A different notion of stable model was proposed by Gelfond and Zhang (2014).

Definition 5 (Gelfond and Zhang). A total interpretation I is a stable model of an LPBP Π if I |= Π and there is no J ⊂ I such that J is a model of the following program:

The two semantics are not equivalent.

Example 4. Let Π1 = {a ← g, b ← h}, where:

• dom(g) = {a, b}, g(∅) = g({a}) = g({a, b}) = T, g({b}) = F;
• dom(h) = {b}, h({b}) = T, and h(∅) = F.

Π1 has one stable model according to Son and Pontelli, namely {a}. In fact, {a} is the least fixpoint of K{a} Π . On the other hand, Π1 has no stable model according to Gelfond and Zhang. In particular, {a} is not a stable model because program (5) is Π′1 = {a ← a}, and it is satisfied by ∅. ■

Example 5. Let Π2 = {a ← g, b ← h, c ← o}, where:

• dom(g) = {b}, g(∅) = T, g({b}) = F;
• dom(h) = {a}, h(∅) = T, h({a}) = F;
• dom(o) = {b, c}, o({b}) = o({b, c}) = T, and o(∅) = o({c}) = F.

Interpretation {a} is a stable model according to Son and Pontelli and Gelfond and Zhang, while {b, c} is a stable model only according to Son and Pontelli. ■

3 Definitorial LPBFs

A unifying framework is presented in this section to better understand similarities and differences between the several stable model semantics for ADFs and LPBFs.

A definitorial logic program with Boolean functions is an LPBF Π in which there is exactly one rule of the form p ← f for each p ∈ V. For a DLPBF Π containing p ← f, function f is denoted Πp. The immediate consequence operator is defined as follows:

where Π is a DLPBF, and (L,U) is an interpretation. The least fixpoint of T U Π is denoted by T U Π ⇑ ∅.

The new characterizations require to compute the fixpoint of the immediate consequence operator for a program reduct obtained by modifying Boolean functions of the input program. In more detail, for a total interpretation I, and a Boolean function f, the following functions are defined:

for all A ⊆ dom(f) = dom(k(f, I)), where k ∈ {keep all , keep subsets, keep equal , keep supsets}.

Definition 6 (B-stable model). A total interpretation I is a B-stable model of a DLPBF Π if I = T IB(Π,I) ⇑ ∅, where:

Definition 7 (S-stable model). A total interpretation I is an S-stable model of a DLPBF Π if I = T I S(Π,I) ⇑ ∅, where:

Definition 8 (P-stable model). A total interpretation I is a P-stable model of a DLPBF Π if I = T IP(Π,I) ⇑ ∅, where:

Definition 9 (G-stable model). A total interpretation I is a G-stable model of a DLPBF Π if I = T IG(Π,I) ⇑ ∅, where:

Example 6. ProgramΠ1fromExample 4 is definitorial. Program B(Π1, {a}) contains the following functions:

• keep subsets(g, {a}), assigning T only to ∅ and {a};
• keep subsets(h, {a}), always assigning F.

It can be checked that {a} is a B-stable model. Program S(Π1, {a}) contains the following functions:

• keep supsets(g, {a}), assigning T only to {a} and {a, b};
• keep supsets(h, {a}), always assigning F.

It can be checked that {a} is not an S-stable model. Program P(Π1, {a}) contains the following functions:

• keep all (g, {a}), assigning T only to ∅, {a} and {a, b};
• keep all(h, {a}), always assigning F.

It can be checked that {a} is a P-stable model. Program G(Π1, {a}) contains the following functions:

• keep equal (g, {a}), assigning T only to {a};
• keep equal(h, {a}), always assigning F.

It can be checked that {a} is not a G-stable model. Moreover, it can be checked that there is no other stable model. ■

Example 7. Program Π2 from Example 5 is definitorial. Interpretation {a} is a B-, S-, P- and G-stable model. Interpretation {b, c} is a B- and P-stable model. The program has no other stable model according to the previous definitions. ■

4 Equivalences

Examples 6-7 suggest that Definitions 4 and 8 are equivalent to Definitions 5 and 9, respectively.

Theorem 1. Let Π be a DLPBF, S be the set of stable models of Π according to Son and Pontelli (2007), and S′ be the set of P-stable models of Π, then S ≡At(Π) S′ .

Theorem 2. Let Π be a DLPBF, S be the set of stable models of Π according to Gelfond and Zhang (2014), and S′ be the set of G-stable models of Π, then S ≡At(Π) S′ .

DLPBFs can model ADFs under B- and S-stable model semantics. In fact, an ADF F = 〈S,E,C〉 can be transformed into a DLPBF def (F) comprising the following rules:

• s ←Cs, for all s ∈ S;
• p ← ⊥, where ⊥ is such that dom(⊥) = ∅ and ⊥(∅) = F, for all p ∈ V \ S.

Example 8. Consider the ADFs F1, F2 from Examples 23, and the DLPBFs Π1,Π2 from Examples 4-5. Note that def (F1) = Π1 and def (F2) = Π2 (if rules of the form p ← ⊥ are added for all p not occurring in F1, F2). ■

Equivalence of Definitions 2 and 6, and of Definitions 3 and 7, can now be established.

Theorem 3. Let F = 〈S,E,C〉 be an ADF, S be the set of stable models of F according to Brewka et al. (2013), and S′ be the set of B-stable models of def (F), then S ≡S S′ .

Theorem 4. Let F = 〈S,E,C〉 be an ADF, S be the set of stable models of F according to Strass (2013), and S′ be the set of S-stable models of def (F), then S ≡S S′ .

The unifying framework also provides a better overview of the four stable model semantics, which may also help to better understand their similarities and differences. The examples in the previous sections already gave hints to relationships between the various stable model semantics. In the following, we motivate and state the general results.

The reducts used by B- and P-stable models replace each Boolean function f with keep subsets(f, I) and keep all(f, I), respectively. The immediate consequence operator is then applied on the reducts, with the upper bound fixed to I. Hence, the image of keep all(f, I) on any V ⊃ dom(f) is irrelevant for the fixpoint computation.

Theorem 5. A total interpretation I is a B-stable model of a DLPBF Π if and only if I is a P-stable model of Π.

Similarly, the reducts used by S- and G-stable models replace each Boolean function f with keep supsets(f, I) and keep equal(f, I), respectively. Again, the image of keep supsets(f, I) on any V ⊃ dom(f) is irrelevant for the fixpoint computation.

Theorem 6. A total interpretation I is an S-stable model of a DLPBF Π if and only if I is a G-stable model of Π.

Concerning P- and G-stable models, their reducts use keep all(f, I) and keep equal(f, I), respectively. Any atom inferred by the immediate consequence operator on the reduct using keep equal (f, I) is also inferred when keep all (f, I) is used, while the converse does not hold in general.

Theorem 7. If a total interpretation I is a G-stable model of a DLPBF Π then I is a P-stable model of Π.

The following is a corollary of the previous theorems, and can also be obtained by combining results in approximation fixpoint theory [Denecker et al., 2004; Pelov et al., 2007; Strass and Wallner, 2014].

Corollary 1. If a total interpretation I is an S-stable model of a DLPBF Π then I is a B-stable model of Π.

5 Compilations

S- or G-stable models of a DLPBF Π can be obtained by means of B- or P-stable models of a rewritten DLPBF s2b(Π). In more detail, At(s2b(Π)) = {p, pF , p= | p ∈ At(Π)} ∪ {⊥}, and s2b(Π) consists of the following rules:

• p ← fp, where dom(fp) = {pF }, fp(∅) = T and fp({pF }) = F;
• pF ← gp, where dom(gp) = {p}, gp(∅) = T and gp({p}) = F;
• p= ← hp, where dom(hp) = {pF } ∪ {q= | q ∈ dom(Πp)}, and hp(I) = T if and only if either pF ∈ I, or both Πp(I) = T and {q= | q ∈ dom(Πp)} ⊆ I;

• ⊥ ← o, where dom(o) = At (s2b(Π)), and s2b(I) = T if and only if ⊥ /∈ I and there is p ← f ∈ Π such that either p= /∈ I, or both f(I) = T and pF ∈ I.

Intuitively, atoms p, pF are used to guess an interpretation I ∩At(Π) for Π. Since atom⊥must be false in all B-stable models of s2b(Π), I ∩At (Π) must actually represent a model of Π if I is a B-stable model of s2b(Π). Moreover, the falsity of ⊥ also implies that all atoms of the form p= must be true. However, each p= can be derived by the immediate consequence operator only if either p /∈ I, or if all atoms q= such that q ∈ dom(Πp) are already derived in a previous application of the operator.

Theorem 8. Let Π be a DLPBF, S be the set of S- or Gstable models of Π, and S′ be the set of B- or P-stable models of s2b(Π), then S ≡At(Π) S′ .

An ASP encoding based on the rewriting s2b(·) and allowing for computing S- or G-stable models of an ADF encoded according to the DIAMOND format is available online.

Further compilations are possible. For example, for stable models by Son and Pontelli (2007), an LPBF Π can be transformed into a DLPBF def (Π) comprising the following rules:

• auxf ← f, where auxf ∈ V \ At(Π) is an auxiliary atom associated with function f , for all p ← f ∈ Π;
• p ← ∨p←f∈Π auxf , for all p ∈ At(Π).

Example 9. Let g, h, o be Boolean functions such that: dom(g) = {b}, g(∅) = T, g({b}) = F; dom(h) = {b}, h({b}) = T, h(∅) = F; dom(o) = {a}, o({a}) = T, o(∅) = F. Let Π3 = {a ← g, a ← h}. Essentially, program Π3 is {a ← not b, a ← b}, where not is the negation as failure symbol under stable model semantics [Gelfond and Lifschitz, 1988; 1991]. Program def (Π3) comprises the following rules: {a ← fa, auxg ← g, auxh ← h}, where fa is the disjunction auxg ∨ auxh, i.e., dom(fa) = {auxg, auxh} and fa assigns F only to ∅. It can be noted that {a} is the unique stable model of Π3 according to Definition 4. Similarly, {a} ∪ {auxg} is the unique stable model of def (Π3) according to Definition 8.

Consider nowΠ4 = Π3 ∪{b ← o}, i.e., {a ← not b, a ← b, b ← a}. Program def (Π4) comprises the following rules: {a ← fa, aux g ← g, aux h ← h, b ← fb, aux o ← o}, where fb is the disjunction auxo, i.e., dom(fb) = {auxo} and fo assigns F only to ∅. It can be noted that Π4 and def (Π4) have no stable model according to Definitions 6-9.

Note that a rewriting introducing rules of the form

would possibly change the semantics of the program. In fact, the rewriting of program Π4 would be {a ← g ∨ h, b ← o}, where dom(g ∨ h) = {b} and g ∨ h assigns T to both ∅ and {b}. Interpretation {a, b} is now a B- and P-stable model. ■

Theorem 1 can thus be extended to LPBFs in general.

Theorem 9. Let Π be an LPBF, S be the set of stable models of Π according to Son and Pontelli (2007), and S′ be the set of P-stable models of def (Π), then S ≡At(Π) S′ .

Concerning stable models by Gelfond and Zhang (2014), rewriting s2b(·) can be extended to LPBFs by replacing each function hp occurring in rules of the form p= ← hp as follows: dom(hp) = {pF }∪{q= | ∃p ← f ∈ Π, q ∈ dom(f)}, and hp(I) = T if and only if either pF ∈ I, or there is p ← f ∈ Π such that both f(I) = T and {q= | q ∈ dom(f)} ⊆ I.

Theorem 10. Let Π be an LPBF, S be the set of stable models of Π according to Gelfond and Zhang (2014), and S′ be the set of B- or P-stable models of s2b(Π), then S ≡At(Π) S′ .

It is also true that a DLPBF Π can be transformed into an ADF adf (Π) = 〈At(Π),E,C〉, where E = {(p, q) | q ∈ At(Π), p ∈ dom(Πq)}, and C = {Πp | p ∈ At(Π)}.

Example 10. Consider again the ADFs F1, F2 from Examples 2-3, and the DLPBFs Π1, Π2 from Examples 4-5. Note that adf (Π1) = F1 and adf (Π2) = F2. ■

As done before, equivalence of Definitions 2 and 6, and of Definitions 3 and 7, can be established.

Theorem 11. Let Π be a DLPBF, S be the set of B-stable models of Π, and S′ be the set of stable models of adf (Π) according to Brewka et al., then S ≡S S′ .

Theorem 12. Let Π be a DLPBF, S be the set of S-stable models of Π, and S′ be the set of stable models of adf (Π) according to Strass, then S ≡S S′ .

By combining the previous transformations, an LPBF Π can be transformed into an ADF adf (def (Π)).

Corollary 2. Let Π be an LPBF, S be the set of stable models of Π according to Brewka et al., and S′ be the set of stable models of adf (def (Π)) according to Brewka et al., then S ≡At(Π) S′ .

Corollary 3. Let Π be an LPBF, S be the set of stable models of Π according to Strass, and S′ be the set of stable models of adf (s2b(Π)) according to Brewka et al., then S ≡At(Π) S′ .

Example 11. Consider program Π4 from Example 9. The ADF adf (def (Π4)) = 〈S,E,C〉 is such that: S = {a, auxg, auxh, b, auxo}; E = {(auxg, a), (auxh, a), (b, auxg), (b, auxh), (auxo, b), (a, auxo)}; Ca = Πa, Cauxg = g, Cauxh = h, Cb = Πb, Cauxo = o. Note that adf (def (Π4)) has no stable model according to all definitions. As observed in Example 9, transforming Π4 into an ADF 〈{a, b}, {(b, a), (a, b)}, C〉 such that Ca(∅) = Ca({b}) = T, Cb({a}) = T, and Cb(∅) = F, would make {a} a stable model according to Brewka et al. ■

6 F-Stable Models

There are cases in which the previously considered semantics may be considered too restrictive.

Example 12. The lazy programmers example in the introduction can be represented by the DLPBF Π5 = {a ← g, b ← h, c ← o}, where: dom(g) = {b, c}, dom(h) = {a, c}, dom(o) = {b}; g(∅) = g({b, c}) = T, g({b}) = g({c}) = F; h({a}) = h({c}) = h({a, c}) = T, h(∅) = F; o({b}) = T, o(∅) = F. There are no stable models according to all previous definitions. As an example, consider the reducts for I = {a, b, c}: B(Π5, I) = P(Π5, I) = Π5;

S(Π5, I) = G(Π5, I) = {a ← fa, b ← fb, c ← o}, where fa and fb are equivalent to b∧c and a∧c, respectively. In all cases, the least fixpoints are equal to the empty set. ■

Other semantics for LPBFs were proposed and analyzed in the previous decade. Two of them, known as FLP [Faber et al., 2011] and Ferraris stable models [Ferraris, 2005], are implemented by current ASP solvers [Faber et al., 2008; Gebser et al., 2009]. These two semantics are equivalent for negation-free programs, and are thus equivalent for DLPBFs. The following is a restatement of the original definitions of stable models by Faber et al. and by Ferraris.

Definition 10 (F-stable model). A total interpretation I is an F-stable model of a DLPBF Π if I |= Π and there is no J ⊂ I such that J |= F(Π, I), where:

The following link follows from Theorem 5 in [Shen and Wang, 2012], Definition 3 in [Son et al., 2007] and Theorem 2 in [Son and Pontelli, 2007].

Corollary 4. Let Π be a DLPBF, and I be a total interpretation. If I is a G-, S-, P- or B-stable model then I is an F-stable model.

The other direction does not hold in general.

Example 13. Recall Π5, the lazy programmers example. As shown in Example 12, there are no B-, S-, P- or G-stable models. However, it does have an F-stable model, {a, b, c}. Indeed, the reduct F(Π5, {a, b, c}) equals Π5, and it can be checked that {a, b} and {b} do not satisfy the rule defining c, while {a, c}, {a}, {c} do not satisfy the rule defining b, and {b, c} and ∅ do not satisfy the rule defining a. ■

It is instructive to examine Π5 a bit more closely. It illustrates the different underlying principles of F-stable and the other notions of stable models. F-stable models also allow for "jumping over gaps," while the immediate consequence operator is not allowed to make an inference if any interpretation between the fixed upper bound and the current lower bound evaluates to false. This is the case in Π5, as there are total interpretations between ∅ and {a, b, c} for which g evaluates to false (these are {b}, {c}, {a, b}, and {a, c}). However, it is not clear why the presence of these interpretations should inhibit {a, b, c} to be a stable model, as they are never reached during the computation of the fixpoint. Brewka et al. (2013) argue for a similar example that the justification is cyclic. This depends on the point of view: in terms of Π5, the cyclic justification claimed by Brewka et al. would be as follows: a is true because b and c are true, while b is true because a is true, and c is true because b is true. However, one can argue as well that a does have also another, non-circular justification that grounds the cycle, namely ∅. Indeed, in terms of the lazy programmer example, one could imagine a dynamic process as follows: if initially nobody works, programmer a will decide to work, which makes programmer b decide to work, causing also programmer c to work. While the original reason for programmer a has been invalidated by this, she still finds herself in a situation that supports the initial decision.

7 RelatedWork

For ADFs, S-stable models [Strass, 2013] and B-stable models [Strass and Wallner, 2014] were characterized using approximation fixpoint theory [Denecker et al., 2004]. Approximation fixpoint theory was also used to characterize some stable model semantics for LPBFs [Pelov et al., 2007]. The containment relation between stable models by Strass and by Brewka et al., i.e., Corollary 1 in Section 4, can be obtained from these results. However, the formalization given in this paper is different, and closer to the original definition of stable models [Gelfond and Lifschitz, 1991], thus allowing to cover stability conditions based on subset-minimality rather than operator fixpoints. This is the case of F-stable models [Faber et al., 2011; Ferraris, 2005], for which a characterization using approximation fixpoint theory appears to be difficult.

This work is also related to ASP systems [Gebser et al., 2009; Leone et al., 2006], where rule bodies clearly define Boolean functions. Common constructs in ASP are negation as failure and aggregate atoms. Other semantically similar constructs are DL [Eiter et al., 2008] and HEX atoms [Eiter et al., 2014], which extend ASP by allowing to interact with external knowledge bases, possibly expressed in different languages. All of these constructs fit in the framework considered in this paper. For example, the interpretation of negated literals in program reducts is fixed by many semantics [Pelov et al., 2007; Son and Pontelli, 2007; Shen and Wang, 2012; Gelfond and Zhang, 2014; Ferraris, 2005] but not in [Faber et al., 2011]. Negation as failure must be also taken into account in the definition of stable models by Gelfond and Zhang, whose program reducts directly refer Boolean function domains, and therefore do not allow to consider each rule body as a unique Boolean function. By constraining rule bodies of LPBFs to comprise exactly one, indivisible Boolean function, all these technical differences disappear, and properties relating to the interpretation of Boolean functions emerge. Indeed, Definitions 6-9 provide a uniform point of view of four different notions of stable models introduced in the literature, and clarify that they differ only minimally on program reducts.

8 Conclusion

Abstract dialectical frameworks and logic programs with Boolean functions are linked here by means of definitorial logic programs with Boolean functions, a framework on which several notions of stable models can be restated uniformly. Similarities and differences of the considered stable model semantics easily emerge from the new characterizations, which are focused on Boolean functions and are not distracted by other common constructs such as negation as failure. This work can mark the beginning of a potentially very fruitful research field that crosses over two research areas. Undoubtedly many more properties can be taken over from either field to the other, and also differences might surface. And, pragmatically perhaps most important, implemented systems can be used profitably for both ADFs and LPBFs. As an example, the ASP encoding mentioned in Section 4 for computing S-stable models of ADFs can be adapted to compute G-stable models of LPBFs.