Bipolar Abstract Dialectical Frameworks Are Covered by Kleene’s Three-valued Logic

1 Introduction

The field of computational models of argument has become a vibrant research area in Artificial Intelligence (AI) [BenchCapon and Dunne, 2007; Atkinson et al., 2017; Baroni et al., 2018]. One main reason for the recently increased interest is the insight that broad acceptance for AI technologies can only be attained if recommended decisions are explainable to the user. That is, especially in areas with far-reaching effects like criminal justice, finance sector or healthcare, we want trustworthy systems which are able to respond why a certain option was (not) chosen and to react on counterarguments in an interactive way. Computational models of argumentation are engaged with modeling arguments and their relationships, as well as the evaluation of conflicting scenarios. Consequently, they are perfectly suited for such explanation tasks and thus might be used as an additional component for an AI system [Cocarascu and Toni, 2016].

One can distinguish two major lines of research in the field: logic-based and abstract approaches. The former takes the logical structure of arguments into account and defines notions like attack, undercut, defensibility etc. in terms of logical properties of the chosen argument structures (cf. [Besnard and Hunter, 2008] for an excellent overview). At the heart of the second approach are currently Dung's widely used abstract argumentation frameworks (AFs) and their associated semantics [Dung, 1995]. Through the years the community realized that the limited expressive capability of AFs, namely the option of single attacks only, reduces their suitability as sound target systems for more complex applications [Atkinson et al., 2017]. Therefore a number of additional functionalities were introduced encompassing preferences, values, collective attacks, attacks on attacks as well as support relations between arguments [Amgoud and Vesic, 2011; Bench-Capon and Atkinson, 2009; Nielsen and Parsons, 2006; Baroni et al., 2009; Cayrol and LagasquieSchiex, 2009]. One of the most powerful generalizations of Dung AFs, yet staying on the abstract layer, are abstract dialectical frameworks (ADFs) [Brewka and Woltran, 2010; Brewka et al., 2014]. The additional expressive power is achieved by adding acceptance conditions to the arguments which allow for the specification of more complex relationships between arguments, e.g. collective attacks as well as single and collective support.

Semantics for ADFs generalize classical semantics and coincide with them if Dung-style acceptance functions are used. They rely on different (pre-)fixpoints of the so-called Γ-operator and in general, their computational complexity is one level up in the polynomial hierarchy compared to their AF counterparts [Straß and Wallner, 2015]. Interestingly, there is the subclass of bipolar ADFs (BADFs) which are as complex as AFs while arguably offering more modeling capacities [Brewka et al., 2017b]. This property makes BADFs very attractive from a knowledge representation point of view and is the reason why this class has received much attention recently [Alviano et al., 2016; Baumann and Straß, 2017; Straß, 2018]. In this paper we make further contributions to this line of research, namely:

1. Introducing a new class of propositional formulae, socalled bipolar disjunctive normal forms (bipolar DNFs), and showing that bipolar ADFs are representable via these normal forms.
2. We then proceed with the main theorem showing that Kleene's three-valued logic K3 [Kleene, 1952] is suitable for bipolar DNFs allowing to bypass the computationally intensive procedure of the Γ-operator.
3. Extending the main result to syntactically bipolar formulae [Straß, 2015] which offer more representational freedom.
4. Implementing a solver and conducting experiments showing the computational benefit of using Kleene's K3.

2 Background

2.1 Propositional Logic and Kleene's K3

In the following we recap standard logical concepts. Both logics use the same syntax. Let A be a fixed set of atoms, then the set of formulae F (over A) is inductively defined as: 1. A ⊆ F and 2. If φ, ψ ∈ F, then φ ∧ ψ, φ ∨ ψ, ¬φ ∈ F. We consider two-valued resp. three-valued interpretations v which assign one of the truth values true (t), false (f) or unknown (u) to each atomic formula. Formally, v : A → {t, f} or v : A → {t, f, u}, respectively. We use V2 (V A 2 ) and V3 (V A 3 ) for the set of all two- resp. three-valued interpretations (over A). Kleene's K3 generalizes classical logic as it allows to assign the truth value unknown [Kleene, 1952; Fitting, 1991]. However, in the classical corner cases both logics coincide. The associated truth tables are given in Table 1. We use w(φ) and vK3 (φ) to indicate that formula φ is evaluated w.r.t. classical logic or Kleene, respectively. Consequently, we implicitly have that w ∈ V2 and v ∈ V3.

2.2 Abstract Dialectial Frameworks (ADFs)

In a nutshell, ADFs are just directed graphs equipped with further acceptance information. We briefly recall some notation and refer to [Brewka et al., 2017b] for an exhaustive overview. An ADF is a triple D = (S, L, C) where S ⊆ A

is a set of statements, L ⊆ S × S is a set of links, and C = {Cs|s ∈ S} is a set of acceptance functions with Cs : 2par(s) → {t, f} where par(s) = {s′ | (s′ , s) ∈ L} denotes the set of parent nodes of s. Each Cs precisely specifies when a statement s is getting accepted. It is common to represent an acceptance function Cs as a propositional (acceptance) formula φs over the vocabulary par(s) (cf. [Straß, 2015] for more details). 1 In this case we write D = (S,Φ) with Φ = {φs | s ∈ S} and leave the links implicit. It is important to have in mind that the latter representation is not uniquely determined as syntactically different formulae may represent the same acceptance function. Let us proceed with an example.

Example 1. Suppose that Jack has gotten the offer for a new job (j). He would surely accept this offer if the new position offers a high salary (h). Alternatively Jack would take the job if it provides a meaningful activity for society (m) and he has the opportunity to work remotely. It is known that the job is meaningful and he does not have to be physically at his workplace (w). However, the salary has yet to be discussed. The associated ADF can be given as D = ({j, h,m, w}, {φj = h ∨ (m ∧ ¬w), φh = h, φm = ⊤, φw = ⊥}).

2.3 Γ-Operator and Semantics

Argumentation semantics rely on computing the so-called Γoperator. In order to present this operator we have to introduce the so-called information order <i which assigns a greater informational content of the classical truth values, i.e. u <i t and u <i f (cf. [Straß and Wallner, 2015] for more background information). We use ≤i for the reflexive closure of <i. The resulting meet-operation ⊓i on ({t, f, u},≤i) is called consensus which assigns t ⊓i t = t, f ⊓i f = f , and u otherwise. Finally, we generalize ≤i to three-valued interpretations in the following point-wise way: v1 ≤i v2 iff for all s ∈ S : v1(s) ∈ {t, f} =⇒ v1(s) = v2(s) and define for any v ∈ V3 the set of two-valued completions of it as [v]2 = {w ∈ V2 | v ≤i w}. For an ADF D = (S,Φ) we define the associated ΓD : V D 3 →V D 3 as

This means, the Γ-operator takes as an input a three-valued interpretation v and returns a new one ΓD(v). This interpretation assigns t (f) to a statement s if all two-valued completion of it assigns t (f) to φs. If two completions disagree on φs, s is rendered u.

1 If par(s) = ∅, we use the 0-ary connectives "⊤" or "⊥".

Example 2 (Example 1 cont.). Consider the three-valued interpretation v = {j ↦→ t, h ↦→ u,m ↦→ u,w ↦→ f}. In order to obtain the new interpretation ΓD(v) we have to compute the value ΓD(v)[s] for each single statement s ∈ S.

1. There are four two-valued completions v1, v2, v3, v4 of v as the statements h and m are set to u.
2. We have to evaluate all acceptance formulae φ w.r.t. each single completion (depicted in Table 2).
3. Finally, we have to build the consensus ⊓i of each column in order to obtain ΓD(v)[s]. Hence, ΓD(v) = {j ↦→ u, h ↦→ u, m ↦→ t, w ↦→ f }.

Now, we are ready to define three well-known semantics [Brewka et al., 2013], namely admissible, complete and preferred semantics (abbr. as adm, cmp and prf ).

Definition 1. Given an ADF D = (S, Φ) and v ∈ V D 3 .

1. v ∈ adm(D) iff v ≤i ΓD(v),
2. v ∈ cmp(D) iff v = ΓD(v) and
3. v ∈ prf (D) iff v is ≤i-maximal in cmp(D).

Example 3 (Example 2 cont.). Note that v ̸≤i ΓD(v) since v(j) = t ̸= u = ΓD(v)[j]. Consequently, v /∈ adm(D) and therefore, v /∈ τ(D) for τ ∈ {cmp, prf }. We leave it to the reader to verify that w = {j ↦→ t, h ↦→ u,m ↦→ t, w ↦→ f} is a complete (but not preferred) interpretation of D.

3 Logics for ADFs: State of the Art

As we have seen in the background section the computation of the semantics of a given ADF D = (S,Φ) heavily relies on the Γ-operator which requires the consideration of all twovalued completions of a considered three-valued interpretation v. More precisely, for a specific statement s, we have ΓD(v)[s] = ⊓i{w(ϕs) | w ∈ [v]2}. As this equality does not rely on the semantics of a certain three-valued logic L3 the question arose from the start whether there is such a logic coinciding with the consensus operator, i.e.

It turned out that the answer depends on the property of truth-functionality. 2 Requiring truth-functionality yields a general negative result [Baumann and Heinrich, 2020, Theorem 1]. Dropping this property allows to find a coinciding three-valued logic, namely the so-called possibilistic logic

2 Roughly speaking, a logic is truth-functional if the evaluation of a composed formulae depends of the truth values of its constituting subformulae only.

[Heyninck et al., 2022, Lemma 2]. Although this is a remarkable theoretical result there is still one main drawback from a conceptional as well as computational point of view, namely that the semantics of possibilistic logic is based on the socalled necessity and possibility measures which still require the consideration of two-valued completions (cf. [Heyninck et al., 2022, Definition 1] or [Dubois and Prade, 1998] for more details.).

Since we are faced with the general impossibility result regarding question Q if requiring truth-functional three-valued logics, one further natural question is to ask for positive results for (interesting) syntactical subclasses G ⊆ F. So far only little is known. For instance, AF-like acceptance formulae, i.e. formulae which are conjunctions of negated atoms are covered by K3 [Baumann and Heinrich, 2020, Theorem 2] and [Ciucci et al., 2014, Proposition 4.5]. However, the question Q is still unsolved for the prominent subclass of so-called bipolar ADFs representing a proper and quite expressive generalization of AF-like ADFs. Showing that also bipolar ADFs are covered by Kleene's K3 is the main aim of the subsequent section.

4 Bipolar ADFs - The Expressive Subclass

The class of Bipolar ADFs (BADF) has been already introduced in the first paper on ADFs [Brewka and Woltran, 2010]. It gained much attention as it was shown to be a rather expressive subclass of ADFs with attractive computational properties [Straß, 2013; 2015]. More precisely, BADFs are strictly more expressive than AFs as they provide various notions of attack and support, instead of single attacks only. Moreover, and this is the decisive point from a KR perspective, the computation with all the standard semantics is of lower computational complexity in comparison to general ADFs, but without any increase when compared to AFs [Straß and Wallner, 2015; Brewka et al., 2017b].

4.1 Semantical and Syntactical Bipolarity

Let us start with the definition of BADFs. An ADF D = (S,L,C) is bipolar if each of its acceptance functions Cs is semantically bipolar [Straß, 2015]. The latter is fulfilled if each statement is supporting, attacking or both for Cs. More precisely, given a Boolean function f : 2A → {t, f}, then

• a ∈ A is supporting iff for all M ⊆ A, f(M) = t implies f (M ∪ {a}) = t,
• a ∈ A is attacking iff for all M ⊆ A, f(M) = f implies f (M ∪ {a}) = f .

We write a ∈ sup(f ) or a ∈ att (f ), respectively. Note that in case of BADFs there is no a ∈ A, s.t. a /∈ sup(f) and a /∈ att(f). In [Straß, 2015] the concept of semantically bipolar functions has been linked with the sub-class of syntactically bipolar formulae. In order to define this subclass we have to recall the concept of polarity. An occurrence of an atom a in a formula φ has positive/negative polarity if the number of negations on the path from the root of the formula tree to the atom is even/odd. We define the polarity of a in formula φ

as: 3

Now, a propositional formula φ is called syntactically bipolar if and only if no atom occurs both positively and negatively. More formally, there is no a ∈ σ(φ), s.t. pol(a, φ) = {±}. The formulae φ = ¬((¬a∨b)∧¬¬b) and ψ = ((a∨b)∧ c) ∨ ¬¬b are examples of syntactically bipolar formulae. We further say that two formulae have the same polarity, if they agree on the polarities of their shared atoms. This means, we (slightly abuse notation and) write pol(φ) = pol(ψ) if for any a ∈ σ(φ) ∩ σ(ψ), pol(a, φ) = pol(a, ψ). Note that the above presented formulae do not possess the same polarity as pol (b, φ) = {-} ̸= {+} = pol (b, ψ).

4.2 Representing BADFs - ANormal Form

In this section we introduce a new normal form, so-called bipolar disjunctive normal form (for short, bipolar DNF), and show that it is expressive enough to cover semantically bipolar functions. As the name suggests we want to consider formulae which are in disjunctive normal form and are also bipolar. In order to prove our main result we provide an inductive definition enabling structural induction. As building blocks we use the set C containing cubes over A which does not allow multiple occurrences of atoms. Remember that a cube is a conjunction of literals. This means, φ = a ∧ b ∧ ¬c is in C whereas neither ψ = (a∧b)∨c (no cube), nor ξ = a∧b∧¬a (multiple occurrences of a) possess this property. Now we are ready to define formulae in bipolar DNF inductively.

Definition 2. The set Fb of bipolar DNFs is defined as:

Note that the condition pol (φ) = pol (ψ) enforces that different occurrences of an atom agree on their polarity. This means, the formula (a ∧ b ∧ ¬c) ∨ (b ∧ ¬d) is a bipolar DNF and (a ∧ b ∧ ¬c) ∨ (¬b ∧ ¬d) is not. We now formally prove that bipolar disjunctive normal forms are indeed syntactically bipolar as their name suggests.

Proposition 1. Bipolar DNFs are syntactically bipolar.

Proof. We prove the assertion by structural induction.

• (base case) Let ϕ ∈ C. By definition, we have that any atom occurs at most once in ϕ. Hence, there is no a ∈ σ(φ), s.t. pol (a, φ) = {±}.
• (induction step) Given φ, ψ ∈ Fb with pol(φ) = pol(ψ) and φ as well as ψ are syntactically bipolar. Consider φ ∨ ψ. Towards a contradiction assume that φ ∨ ψ is not syntactically bipolar. This means, there is an a ∈ σ(φ∨ψ), s.t. pol (a, φ∨ψ) = {±}. Note that σ(φ∨ψ) = σ(φ) ∪ σ(ψ). Case distinction:
• a ∈ σ(φ) \ σ(ψ). Impossible as φ is assumed to be syntactically bipolar.

3 The set σ(φ) contains all atoms occurring in φ.

1. a ∈ σ(φ) ∩ σ(ψ). Impossible as pol(φ) = pol(ψ) guarantees that for any a ∈ σ(φ) ∩ σ(ψ), pol (a, φ) = pol (a, ψ).
2. a ∈ σ(ψ) \σ(φ). Impossible as ψ is assumed to be syntactically bipolar.

We now turn to the main result of this section allowing us to link the class of bipolar ADFs with bipolar DNFs. More precisely, we show that semantically bipolar functions can be represented as bipolar DNFs. Moreover, any bipolar DNF canonically induces a semantically bipolar function. The result is a strengthening of a former correspondence result [Straß, 2015, Theorem 1] and will be the decisive ingredient to show that BADFs are covered by Kleene's K3.

Theorem 1.

1. For each formula φ in bipolar DNF we have that

is semantically bipolar. The interpretation vM is obtained from M via: For each a ∈ σ(φ), vM(a) = t iff a ∈ M.

1. For each semantically bipolar function f : 2A → {t, f}, a bipolar DNF ψf with fψf = f is given by:

Proof.

1. Given a formula φ in bipolar DNF. In Proposition 1 we have shown that formulae in bipolar DNF are syntactically bipolar. Hence, we me apply [Straß, 2015, Item 1 of Theorem 1] and obtain the semantical bipolarity of the presented function.
2. The construction of ψf was already given in [Straß, 2015, Item 2 of Theorem 1]. It remains to check that this formula is indeed in bipolar disjunctive normal form. First, for each set M, the associated formula ψM is a cube without multiple occurrences of atoms as a ∈ M and a ∈ A \ M is impossible. This means, for each M, ψM ∈ C. Moreover, since by definition a semantically bipolar function possesses arguments which are supporting, attacking or both, i.e. a /∈ sup(f) and a /∈ att(f) is impossible, we deduce the impossibility of having pol(a, ψM) = {+} and pol(a, ψM′) = {-} for two cubes ψM and ψM′ . Hence, ψf meets any criteria of a bipolar DNF.

To get an idea of the constructions used in Theorem 1 we present the following example.

Example 4. Consider the bipolar DNF φ = a ∨ ¬b. We obtain fφ = {∅ ↦→ t, {a} ↦→ t, {b} ↦→ f, {a, b} ↦→ t}. In accordance with Item 1 fφ is semantically bipolar since a ∈ sup(fφ) and b ∈ att(fφ). Moreover, fφ induces the bipolar DNF ψfφ = ψ∅ ∨ψ{a} ∨ψ{a,b} with ψ∅ = ¬b, ψ{a} = a∧¬b and ψ{a,b} = a. Since ψfφ and φ possess the same twovalued models we verify fψfφ = fφ as claimed in Item 2.

4.3 Kleene's K3 Covers BADFs

We are now prepared for the main result of this paper. That is, we show that Kleene's three-valued logic serves for bipolar DNFs which themselves correspond to the class of bipolar ADFs. More precisely, analogously to AF-like acceptance formulae, it is possible to evaluate a bipolar DNF ϕ w.r.t. K3 instead of computing all two-valued completions and applying the consensus operator afterwards as required in the original definition.

Theorem 2. For any ϕ ∈ Fb and any v ∈ V3:

Proof. We prove the assertion by structural induction.

• (base case) Let ϕ ∈ C. This means, ϕ is of the form a1 ∧ . . . ∧ an ∧ ¬b1 ∧ . . . ∧ ¬bm with ai, bj ∈ A and some n, m ∈ N. Note that one of the two might be zero. Given v ∈ V3. Case distinction.
• Let vK3 (ϕ) = t. Hence, according to Table 1 we have that each single conjunct of φ has to be evaluated to true, i.e. vK3 (ai) = t and vK3 (¬bj) = t. The latter implies vK3 (bj) = f . Consequently, since v is already two-valued, there are no further two-valued completions, i.e. [v]2 = {v}. Since Kleene's K3 coincide with propositional logic in the two-valued case, i.e. v(ϕ) = t, we deduce ⊓i{w(ϕ) | w ∈ [v]2} = t.
• Let vK3 (ϕ) = f . Thus, according to Kleene at least one conjunct has to evaluated to false. This means, there is one ai with v(ai) = f or alternatively, one bj with v(bj) = t. Now, no matter which twovalued completion w ∈ [v]2 is considered, w and v agree on the evaluation of this atom implying that w(φ) = f even in the propositional case. Consequently, ⊓i{w(ϕ) | w ∈ [v]2} = ⊓i{f} = f .
• Let vK3 (ϕ) = u. Hence, according to Table 1 at least one conjunct has to evaluated to unknown (1) and no conjunct evaluates to false (2). Condition (1) implies vK3 (ai) = u or vK3 (¬bj) = u = vK3 (bj) for some ai or bj. This insight allows to render the conjunction false w.r.t. a two-valued completion w ∈ [v]2 via w(ai) = f or w(bj) = t, respectively. Note that the assignment for the remaining atoms does not matter as a conjunction evaluates to false, whenever at least one conjunct is false.

The second condition (2) implies that w ∈ V2 with w = {a1, . . . , an ↦→ t, b1, . . . , bn ↦→ f} is a twovalued completion of v, i.e. w ∈ [v]2. By construction w(φ) = t. Consequently, ⊓i{w(ϕ) | w ∈ [v]2} = ⊓i{t, f} = u concluding the last case.

• (induction step) Given φ, ψ ∈ Fb with pol(φ) = pol(ψ) as well as vK3 (ϕ) = ⊓i{w(ϕ) | w ∈ [v]2} and vK3 (ψ) = ⊓i{w(ψ) | w ∈ [v]2} for any three-valued interpretation v. We have to show that this conveys to the disjunction, i.e. vK3 (ϕ∨ψ) = ⊓i{w(ϕ∨ψ) | w ∈ [v]2} for any three-valued interpretation v. Case distinction.
• Let vK3 (ϕ) = t or vK3 (ψ) = t. (at least one t) Hence, according to Table 1 we obtain vK3 (ϕ ∨ ψ) = t. Without loss of generality assume vK3 (ϕ) = t. By induction hypothesis we obtain t = ⊓i{w(ϕ) | w ∈ [v]2} yielding w(ϕ) = t for any w ∈ [v]2. Consequently, w(ϕ∨ψ) = t for any w ∈ [v]2 proving t = ⊓i{w(ϕ ∨ ψ) | w ∈ [v]2}.
• Let vK3 (ϕ) = vK3 (ψ) = f . (both f ) Hence, vK3 (ϕ ∨ ψ) = f according to Table 1. By induction hypothesis we obtain ⊓i{w(ϕ) | w ∈ [v]2} = f = ⊓i{w(ψ) | w ∈ [v]2} yielding w(ϕ) = f for any w ∈ [v]2. Consequently, w(ϕ ∨ ψ) = f for any w ∈ [v]2 proving f = ⊓i{w(ϕ∨ψ) | w ∈ [v]2}.
• Let vK3 (ϕ) = vK3 (ψ) = u. (both u) Consequently, vK3 (ϕ ∨ ψ) = u according to Table 1. Applying induction hypothesis justifies ⊓i{w(ϕ) | w ∈ [v]2} = u = ⊓i{w(ψ) | w ∈ [v]2}. This means, there are at least two completions wφ t ,wφ f ∈ [v]2, s.t. wφ t (ϕ) = t and wφ f (ϕ) = f . The same applies to ψ. This means, there are two completions wψ t ,wψ f ∈ [v]2, s.t. wψ t (ψ) = t and wψ f (ψ) = f . Now, we have to show that there are two completions wφ∨ψ t ,wφ∨ψ f ∈ [v]2, s.t. wφ∨ψ t (φ ∨ ψ) = t (1) and wφ∨ψ f (φ ∨ ψ) = f (2). This existence guarantees u = ⊓i{w(ϕ ∨ ψ) | w ∈ [v]2} as required.
• Consider wφ∨ψ t = wψ t . Since wφ t (ϕ) = t is assumed, we immediately obtain wφ t (ϕ ∨ ψ) = t and we are done.
• Since φ, ψ ∈ Fb we may deduce that

Since wφ f (ϕ) = f we infer wφ f (Pi) = f for any 1 ≤ i ≤ n. Since any Pi is a conjunction of literals, there has to be at least one atom pi ∈ σ(Pi), s.t. wφ f (pi) = f if pol (pi, Pi) = {+} and wφ f (pi) = t if pol(pi, Pi) = {-}. For convenience, let us call such an atom pi falsifier of Pi. Since pol(φ) = pol(ψ) is assumed we have that any falsifier pi of a certain Pi is also a falsifier of Qi, whenever pi ∈ σ(Qi). Let us pick one single falsifier pi for each Pi regarding wφ f . This returns a set P = {p1, . . . , pn}. Now, choose for the remaining Qi which are not already falsified by some p ∈ P under wφ f a single falsifier qi regarding wψ f . Let us denote this set with Q = {q1, ..., qs}. Note that s = 0, i.e. Q = ∅ is possible. Moreover, P and Q are disjoint by definition. Now we are ready to define a falsifying interpretation wφ∨ψ f , namely

Consequently, wφ∨ψ f (φ∨ψ) = f by construction.

1. Let vK3 (ϕ) = u and vK3 (ψ) = f . (one u, one f) Consequently, vK3 (ϕ ∨ ψ) = u. By induction hypothesis, there are at least two completions wφ t ,wφ f ∈ [v]2, s.t. wφ t (ϕ) = t and wφ f (ϕ) = f . Moreover, w(ψ) = f for any w ∈ [v]2. Hence, we have already found two witnessing completions since wφ t (ϕ ∨ ψ) = t and wφ f (ϕ ∨ ψ) = f according to Table 1. Thus, we have shown ⊓i{w(ϕ∨ψ) | w ∈ [v]2} = ⊓i{t, f} = u.

Example 5 (Revisiting Example 2). Consider again the three-valued interpretation v = {j ↦→ t, h ↦→ u, m ↦→ u,w ↦→ f}. We observe that any non-trivial acceptance condition is in bipolar DNF. More precisely, φj = h ∨ (m ∧ ¬w) and φh = h are bipolar DNFs. Now, according to the main theorem we may simply apply Kleene's K3 instead of computing two-valued completions. More precisely, ΓD(v)[j] = vK3 (φj ) = vK3 ((h ∨ m) ∧ ¬w) = u coinciding with ⊓i{w(φj) | w ∈ [v]2}. The latter was calculated with enormous effort in Example 2.

4.4 Beyond Bipolar DNFs and Representational Issues

Before closing the main section and turning to experimental results we want to comment on semantically equivalent replacements. Remember that two formulae are said to be semantically equivalent if and only if both have same truth value under all interpretations. Regarding replacements, one has to be aware of the fact that semantical equivalence w.r.t. Kleene's K3 (for short, ≡K3 ) and propositional logic differ. More precisely, the former implies the latter but not necessarily vice versa. For instance, consider φ = a and ψ = a ∨ (b ∧ ¬b). Both are considered as semantically equivalent in propositional logic, i.e. w(φ) = w(ψ) for each w ∈ V2. However, the three-valued interpretation v = {a ↦→ f , b ↦→ u} witnesses their non-equivalence w.r.t. K3 as vK 3 (φ) = f ̸= u = vK 3 (ψ). This means, applying semantically equivalent replacements to an acceptance formula in bipolar DNF does not guarantee the applicability of Theorem 2 if done w.r.t. propositional logic. In contrast replacing bipolar DNFs with formulae semantically equivalent w.r.t. Kleene yields a class beyond bipolar DNFs also covered by the main result. For instance, although ξ = ¬(a ∧ b) is obviously not in bipolar DNF it is covered by Theorem 2 as vK 3 (ξ) = vK 3 (¬a ∨ ¬b) for each v ∈ V3.

The following result shows that any syntactically bipolar formula (like ξ) is semantically equivalent in terms of K3 to a bipolar DNF. This result justifies the name bipolar disjunctive normal form even in the realm of Kleene's three-valued logic.

Proposition 2. For any syntactically bipolar formula φ, there exists a formula ψ in bipolar DNF, s.t. φ ≡K3 ψ.

Proof (sketch). The following semantical equivalences are known from classical logic, but also hold for Kleene's K3 (cf. [H¨olldobler and Kencana Ramli, 2009, Table 2]).

1. Use Double Negation and De Morgan to reach the socalled negation normal form, i.e. negations are only in front of atoms.
2. Use Distributivity, Commutativity and Associativity to obtain a classical DNF.
3. Apply Idempotency to guarantee that each disjunct is in C, i.e. a cube without multiple occurrences of atoms.

It remains to argue that the obtained DNF is indeed bipolar. This property follows from the fact that each single replacement does not change the polarity of the atoms.

The former representation result allows us to extend the main theorem to the whole class of syntactically bipolar formulae. This result frees us from the strict syntactic corset of bipolar DNFs.

Theorem 3. For any syntactically bipolar formula φ and any three-valued interpretation v ∈ V3:

Proof. Combine Proposition 2 and Theorem 2.

5 Complexity and Experimental Results

The complexity of the standard decision problems like Verification, Credulous Acceptance or Sceptical Acceptance highly depend on the complexity of the Γ-operator [Straß and Wallner, 2015; Dvor´ak and Dunne, 2017]. For instance, verifying that a given three-valued interpretation v is admissible in an ADF D requires to check whether v ≤i ΓD(v). This means, we have to examine v(s) ≤i ΓD(v)[s] = ⊓i{w(ϕs) | w ∈ [v]2} for each single statement s. Consequently, if for instance v(s) = t, we have to verify that ΓD(v)[s] = t. This means, ϕs has to evaluate to true for each single w ∈ [v]2. Clearly, this reminds of the validity problem in propositional logic. And indeed, it was shown that verifying admissibility for general ADFs is coNP-complete [Wallner, 2014]. Let us now assume that we are faced with a syntactically bipolar acceptance formula φs. In this case verifying v(s) ≤i ΓD(v)[s] becomes tractable as it suffices to evaluate ϕs w.r.t. K3 and to check whether v(s) ≤i vK3 (ϕs). This means, applying Theorem 3 yields a P algorithm for verifying admissibility in case of BADFs. Again, this membership result is not new [Straß and Wallner, 2015], but the way to achieve it is. In the following we will show how we may computationally benefit from applying the main theorem.

For this very first experiment, we considered bipolar ADFs with a number of statements between 1 and 12. For each number, we generated at least 100 test instances, i.e. 100 ADFs with different bipolar acceptance formulae. The tests were run on an Ubuntu desktop with an Intel i5-6400 CPU and 32 GiB RAM. The implemented Python script systematically generates and checks all three-valued interpretations v according to the specific semantical requirements, e.g. v ≤i ΓD(v) in the case of admissible semantics. For a particular statement s, the script calculates ΓD(v)[s] in two different ways: via the classical consensus, i.e. with the help of two-valued completions, and via applying Kleene's threevalued logic. We measured the time required for each type of calculation, considering a 30 minute limit.

The results for admissible, complete and preferred semantics are depicted in Table 3. The table is structured as follows: First, column "n" indicates the number of statements. Secondly, "σ-two" and "σ-tri" announce how σ-interpretations are obtained, i.e. via two-valued completions or three-valued logic, respectively. Finally, the factor in column "speed" indicates how much faster the three-valued approach is compared to the two-valued one. Results are rounded to four digits after the decimal point, enabling runtimes like 0.0 as well as matching entries. The entry "time out" indicates that the calculation was stopped as the 30 minute limit was reached. We mention that even for the Kleene method, statement numbers over 12 timed out.

The main aim was to show that the use of Kleene's threevalued logic is significantly faster than the classical approach using two-valued completions. Indeed, the runtimes depicted in Table 3 show this impressively. However, both methods show exponential runtime growth, yielding a linear function on a logarithmic scale (cf. Figure 2). This is not surprising since the number of interpretations to be tested also depends exponentially on the number of statements. It can be observed that there are no significant differences in the runtimes among the considered semantics. According to the solver design the computation of complete/preferred interpretations should be slightly slower than that of admissible/complete interpretations as the former require the latter. Since the number of admissible/complete interpretations used to filter out complete/preferred interpretations is rather low, the additional time for comparing these interpretation is negligibly small and not visible in the results. In order to see these differences more clearly, a larger number of statements, test instances, and measurements are required. To ensure reproducability, we provide access to our repository 4 , containing the solver, test cases, and other relevant technical details.

6 Discussion and Conclusion

The topic of finding underlying logics for ADFs is not new. To the best of our knowledge the first result was given by Bochman who showed that there is a uniform and modular translation from ADFs into causal reasoning. For each acceptance function φs two causal rules are introduced, namely φs ⇒ s and ¬φs ⇒ ¬s. It is then shown that the obtained causal theory, or more precisely, its induced causal operator relates semantically to the Γ-operator in a way which allows to show a broad correspondence between the two formalisms [Bochman, 2016]. A correspondence result without translations was later given by Heyninck and colleagues. They showed that the three-valued possibilistic logic coincides with the results of the Γ-operator [Heyninck et al., 2022]. This logic is not truth-functional which is indeed unavoidable due to an impossibility result in [Baumann and Heinrich, 2020].

4 https://github.com/kmax-tech/IJCAI-23

In this paper we proved that in case of BADFs we may use Kleene's K3 as an underlying truth-functional logic. This logic allows to bypass the computationally intensive procedure of considering all two-valued completions which was still implicit in possibilistic logic. To prove the main correspondence theorem, we introduced the so-called bipolar DNFs inspired by previous results in [Straß, 2015]. The decisive point of the proof was to construct a verifying or falsifying interpretation for a compound formula given verifying or falsifying interpretations of its subformulae. Bipolar DNFs proved to be extremely helpful in this regard as their structure give us sufficient control over the considered interpretations. Finally, we free us from the syntactic restrictions of bipolar DNFs and extended the correspondence result to syntactically bipolar formulae in general.

The achieved correspondence result is in the first place a theoretical one, which clarifies the open question whether some and which three-valued logic underlies BADFs. In the future, this main result can be used for both, further theoretical issues like (re)considering complexity questions as well as practical applications such as developing new algorithms relying on Kleene's K3. One promising idea is to combine these newly developed computing methods with already existing procedures. For instance, one may think of a preprocessing step checking which acceptance formulae are syntactically bipolar. For the identified statements we may use the faster Kleene-procedure. We indicated the computational benefit of using Kleene with some first experiments. However, it will be interesting to see how combined methods may improve more sophisticated ADF solvers like k++ADF implemented in C++ programming language [Linsbichler et al., 2022], goDIAMOND [Ellmauthaler and Strass, 2016] and YADF [Brewka et al., 2017a] both based on answer set programming or Tweety using Java [Thimm, 2014; 2017].

Ethical Statement

There are no ethical issues.

Acknowledgments

This work was supported by the German Research Foundation (DFG, BA 6170/2-1 and BA 6170/3-1) and the German Federal Ministry of Education and Research (BMBF, 01/S18026A-F) by funding the competence center for Big Data and AI "ScaDS.AI" Dresden/Leipzig.