We present a dialogical proof theory for credulous acceptance in abstract dialectical frameworks under the preferred semantics. Our approach is motivated by the need to explain why an argument is accepted. The proof theory defines a set of rules for a dialogue between a proponent and opponent exchanging propositional formulas. The proponent takes on the role of trying to prove that the argument in question is acceptable, and the opponent takes on the role of exhaustively challenges the proponent's moves, with a dialogue where the proponent wins represents a proof that the argument in question is accepted.
between an imaginary proponent and opponent. The rules defined by these methods determine
the permitted dialogue moves and ensure soundness and completeness, meaning that there exists
a dialogue in which the proponent wins if and only if the argument of interest is acceptable under
the preferred or grounded semantics. The idea to use dialogues of this kind for the purpose of
explaining decisions to users, often in an interactive fashion, has appeared in a number of recent
works [
For some applications, Dung’s model of abstract argumentation is not sufficiently expressive.
This has led to a number of extensions of Dung’s model. Examples are bipolar argumentation
which allow both support and attack relations between arguments [
Our proposal is related to the dialogical proof theory for ADFs under the preferred semantics
due to Zafarghandi et al. [
A dialogue that is won by the proponent is a dialogue in which the proponent has satisfied all of the challenges put forward by the opponent. Such a dialogue can be read as an explanation of the form φ1 because φ2 because . . . because φn, where φ1 is the initial claim that the argument of interest is accepted, and φn is a tautology. We believe that this approach is simpler, easier to interpret and therefore better suited to explain argument acceptance in ADFs.
Our proposal is based on a novel result relating the semantics of ADFs with the notion of
prime implicant. Prime implicants are an important concept in applications such as model-based
diagnosis [
The overview of this paper is as follows. In Section 2 we recall the necessary basics concerning ADFs. We introduce the concept of prime implicant, and establish its connection with the semantics of ADFs in Section 3. In Section 4 we present our proof theory for credulous acceptance under the preferred semantics of ADFs. In the remaining sections we discuss our findings, make a comparison with related work and discuss future work.
In this section we recall the necessary basics concerning ADFs and their semantics [
Definition 1. An abstract dialectical framework (in short, ADF) is a tuple D = (At, L,C) where • At is a finite set of atoms (also referred to as arguments) • L ⊆ At × At is a set of links • C = {φx}x∈At is a set of acceptance conditions (elements of L (At)), such that an atom y ∈ At appears in φx only if (y, x) ∈ L.
Given an ADF D = (At, L,C) and argument x ∈ At we denote by parD(x) = {y ∈ At|(y, x) ∈ L} the set of parents of x. As is common, if we omit the set L from the definition of an ADF then we assume L to be determined by the condition that (x, y) ∈ L if and only if the atom x appears in φy.
An interpretation for L (At) is a function v : At → {t, f, u}. We denote by V 3(At) the set of interpretations for L (At). Given an interpretation v ∈ V 3(At) and a set B ⊆ At, we use v|B to denote the restriction of v to B. Given a set V ⊆ V 3(At) we denote by V |B the set {v|B|v ∈ V }.
An interpretation v is two-valued if v(x) ∈ {t, f} for all x ∈ At. We denote by V (At) the set
of two-valued interpretations for L (At). We extend an interpretation v to assign truth values to
elements of L (At) using Kleene semantics [
The information order ≤ i is the reflexive closure of the strict partial order <i over {t, f, u} defined by u <i t and u <i f. Intuitively, ≤ i orders truth values according to their information content. We extend ≤ i to an order over interpretations by setting v ≤ i u if and only if v(x) ≤ i u(x) for all x ∈ At.
We denote by ⊓ the meet operation of the complete meet-semilattice ({t, f, u}, ≤ i). Intuitively, ⊓ represents a consensus that assigns t ⊓ t = t, f ⊓ f = f and assigns u in all other cases. The meet ⊓ of two interpretations v, u of At is defined by (v ⊓ u)(x) = v(x) ⊓ u(x) for all x ∈ At. The set of interpretations of a set At of atoms forms a complete meet-semilattice with respect to ≤ i.
A two-valued interpretation u extends a three-valued interpretation v iff v ≤ i u. We denote by [v]2 the set of two-valued interpretations that extend v. Given an ADF D and three-valuedinterpretation v, ΓD(v) denotes the three-valued interpretation defined by
ΓD(v)(x) = ⊓{u(φx)|u ∈ [v]2}.
The admissible, complete and preferred semantics are defined as follows.
Definition 2.
A three-valued interpretation v of an ADF D is: • admissible iff v ≤ i ΓD(v) • complete iff v = ΓD(v) • preferred iff it is ≤ i-maximal admissible.
We denote by ad(D), co(D) and pr(D) the set of admissible, complete and preferred interpretations of D.
Given an ADF D = (At,C) and argument x ∈ At we say that x is skeptically accepted under the preferred semantics if v(x) = t for every preferred interpretation v of D, and that x is credulously accepted under the preferred semantics if v(x) = t for some preferred interpretation v of D. Note that, in what follows, we focus on explaining credulous acceptance under the preferred semantics, making use of the following fact: Since preferred interpretations are ≤ i-maximal admissible, proving credulous acceptance of an argument x under the preferred semantics amounts to checking whether there exists an admissible interpretation in which x is true.
In this section we introduce the notion of prime implicant [
The following lemma establishes a characterisation of admissible interpretations in terms of prime implicants. This lemma forms the basis for the method presented in the next section. It states that the admissible interpretations are exactly those interpretations that satisfy the condition that an argument x is true only if a prime implicant of φx is true, and false only if a prime implicant of ¬φx is true.
Lemma 1. An interpretation v of an ADF D = (At,C) is admissible if and only if, for all x ∈ At: (1) If v(x) = t then v(τ ) = t for some prime implicant τ of φx.
(2) If v(x) = f then v(τ ) = t for some prime implicant τ of ¬φx.
Proof. Let D = (At, L,C) be an ADF.
For the only-if direction, suppose v is an admissible interpretation of D and let x ∈ At. For the case v(x) = t, let τ be the conjunction of literals contained in the sets {y | y ∈ parD(x), v(y) = t} and {¬y | y ∈ parD(x), v(y) = f}. We will show that τ is an implicant of φx by showing that w(τ ) = t implies w(φx) = t for every two-valued interpretation w of L (parD(x)). Let w be a two-valued interpretation of L (parD(x)) such that w(τ) = t. Then w ∈ [v]2|parD(x). Since v is admissible we have v(x) ≤ i ⊓{u(φx)|u ∈ [v]2}, which implies that u(φx) = t for every u ∈ [v]2|parD(x). It thus follows that w(φx) = t. Hence, τ is an implicant of φx which in turn implies that v(τ′) = t for some prime implicant τ′ ⊆ τ of ϕx. Hence, condition (1) in Lemma 1 is satisfied. For the case v(x) = f it similarly follows that condition (2) in Lemma 1 is satisfied.
For the if direction, let v be an interpretation that, for all x ∈ At, satisfies conditions (1) and (2) in Lemma 1. We will prove that v is admissible. Let x ∈ At. We will prove that v(x) ≤ i ΓD(v)(x). There are two cases: v(x) = t and v(x) = f. For the case v(x) = t, let τ be the prime implicant of φx such that v(τ) = t whose existence follows from condition (1) in Lemma 1. We will prove that for all u ∈ [v]2, u(φx) = t. Let u ∈ [v]2. Then v ≤ i u and, since v(τ) = t, it follows that u(τ) = t and hence u(φx) = t. It follows that ΓD(v)(x) = t and hence v(x) ≤ i ΓD(v)(x). The case v(x) = f similarly implies, using condition (2) in Lemma 1, that v(x) ≤ i ΓD(v)(x). It thus follows that v ≤ i ΓD(v) and hence that v is admissible.
Example 1. Let D be an ADF with argument a. We consider three examples of acceptance conditions for a, along with the conditions that an admissible interpretation of D must satisfy for a to be accepted or rejected.
1. φa = ¬b ∧ ¬c. Then φa has one prime implicant, namely φa itself. Accepting a therefore requires both b and c to be rejected. The prime implicants of ¬φa are b and c. Rejecting a therefore requires b or c to be accepted. 2. φa = b ∧ (c ∨ d). Then the prime implicants of φa are b ∧ c and b ∧ d. Accepting a thus requires b to be accepted as well as c or d. The prime implicants of ¬φa are ¬b and ¬c ∧ ¬d. Rejecting a thus requires b to be rejected or both c and d to be rejected. 3. φa = b ∨ ¬b. Then the only prime implicant of φa is ⊤. We can therefore accept a regardless of the status of b. Rejecting a is impossible since ¬φa does not have a prime implicant.
Note that case three in the example above demonstrates that Lemma 1 is not equivalent to the condition that x is true only if φx is true, and x is false only if ¬φx is true. To see why, note that we have φa = b ∨ ¬b with φa having one prime implicant ⊤. Then, if v(b) = u, we have that v satisfies a prime implicant of φa but it does not satisfy φa itself. Furthermore, note that we can adapt Lemma 1 to characterise complete interpretations by turning these only-if conditions into if-and-only-if conditions. 4. Dialogical Proofs for Credulous Acceptance under the
Preferred Semantics
We now present a method to prove, given an ADF D and argument x, whether x is credulously
accepted under the preferred semantics. We build on ideas behind the so called preferred game for
abstract argumentation, a dialogical procedure that similarly determines whether an argument of
an abstract argumentation framework is credulously accepted under the preferred semantics [
Definition 3. Let D = (At, L,C) be an ADF and x ∈ At be an argument. A dialogical proof for x is a sequence (p1, o1, . . . , pn, on) of formulas (with pi called the i-th proponent move and oi the i-th opponent move) such that: 1. p1 = x 2. For i ≥ 1, oi = ΘD(pi \ p1 ∪ . . . ∪ pi− 1), where ΘD(φ ) denotes the result of replacing every atom in φ with its acceptance condition. 3. For i > 1, pi is a prime implicant of oi− 1 4. p1 ∧ . . . ∧ pn is satisfiable.
We say that the dialogical proof is successful if on ≡ ⊤ .
Explanation: the initial formula put forward by the proponent is the argument x whose acceptance is being proven (condition 1). The opponent replies to every proponent move by putting forward a challenge in the form of a formula that must hold for the proponent’s claim to be hold (condition 2). This formula is constructed by taking the preceding proponent move (which is a conjunction of literals) and then removing the literals that have already been challenged in previous moves, and then replacing every atom with its acceptance condition. Subsequent proponent moves represent reasons for why these conditions are true, in the form of prime implicants (condition 3). The proponent’s moves must furthermore be jointly consistent (condition 4). Credulous acceptance is proven if the dialogue is successful, meaning that the opponent has no other challenge left but a vacuous one represented by a tautology. We can think of this as the opponent “conceding” and the proponent “winning the discussion”.
Note that the opponent’s moves are fully determined by the preceding proponent moves, whereas the proponent may need to make a choice among possible prime implicants, where some choices may lead to a successful dialogical proof and others may not. Checking whether a successful dialogical proof exists thus amounts to finding a sequence of prime implicants leading to a dialogical proof that is successful. Furthermore, whereas the moves of the opponent are arbitrary formulas, the moves of the proponent, being either the initial argument or a prime implicant of the preceding opponent move, are conjunctions of literals. This means that the consistency requirement (condition 4) amounts to checking for the presence of contradictory literals.
The following theorem establishes soundness and completeness of our method. Theorem 1. Let D = (At, L,C) be an ADF and x ∈ A be an argument. There exists a successful dialogical proof for x if and only if there exists a preferred interpretation v of D such that v(x) = t. Proof. Let D = (At, L,C) be an ADF and x ∈ At an argument.
¬b a ¬a b ¬b∧¬e c
ONLY IF: Let (p1, o1, . . . , pn, on) be a successful dialogical proof for x. Let v be the interpretation of D defined by
⎪⎧t v(x) = ⎨f ⎪⎩u if x ∈ p1 ∪ . . . ∪ pn if ¬x ∈ p1 ∪ . . . ∪ pn otherwise We will prove that v is admissible. Let y ∈ At. If v(y) = t then the construction of v implies that there is an i such that y ∈ pi. It then follows that oi |= φy. Because pi+1 is a prime implicant of oi, it follows that pi+1 |= φy. Then there must be a term τ ⊆ pi+1 that is a prime implicant of φy. We furthermore have that v(pi+1) = t and hence v(τ) = t. Thus, condition (1) in Lemma 1 is satisfied. If v(y) = f it follows similarly that condition (2) in Lemma 1 is satisfied. Using Lemma 1 it follows that v is an admissible interpretation of D such that v(x) = t. This implies that there is a preferred interpretation w of D such that v ≤ i w and hence w(x) = t.
IF: Let v be a preferred interpretation of D such that v(x) = t. We say that a sequence (p1, o1, . . . , pn, on) is v-valid if for all i in [1, . . . , n], v(pi) = v(oi) = t. We inductively and nondeterministically define a v-valid sequence A(n) for any positive integer n as follows: • A(1) = (x, ΘD(x)). • If A(n) = (p1, o1, . . . , pn, on) then A(n + 1) = (p1, o1, . . . , pn, on, pn+1, on+1) where 1. pn+1 is a prime implicant of on such that v(pi+1) = t.
2. on+1 = ΘD(pn+1 \ p1 ∪ . . . ∪ pn).
Note that A(1) is clearly v-valid. Furthermore, if A(n) = (p1, o1, . . . , pn, on) is v-valid then v(on) = t which implies, using Lemma 1 and the fact that v is admissible, that a prime implicant pn+1 such that v(pi+1) = t as mentioned in line 1 above exists, and hence that A(n + 1) exists. Furthermore, if v(pi+1) = t it follows that v(oi+1) = t and therefore A(n + 1) is also v-valid. Finiteness of At implies that there is a k such that A(k) = A(k + 1). It then follows that A(k) is a successful dialogical proof for x.
Example 2. Consider the ADF shown in Figure 1 on the left. Note that the acceptance conditions of this ADF correspond to the acceptance conditions of an abstract argumentation framework. The ADF therefore represents the abstract argumentation framework with edges interpreted as attacks. The ADF has two preferred interpretations: v1 = {a = t, b = f, c = u, d = u, e = u} and v2 = {a = f, b = t, c = f, d = t, e = f}. Thus, two arguments that are credulously accepted are a (interpretation v1) and d (interpretation v2). The successful dialogical proof for a is (1) (2) (3) (4) (5) (6) The successful dialogical proof for d is v1 = {a = f, b = f, c = f, d = f, e = t, f = f} v2 = {a = t, b = t, c = t, d = f, e = t, f = f} v3 = {a = t, b = t, c = t, d = t, e = t, f = f} v4 = {a = f, b = f, c = f, d = t, e = f, f = t} Thus, two arguments that are credulously accepted are e and f . There are two successful dialogical proofs for e. They correspond to the two ways to satisfy the acceptance condition for e namely by making d false (preferred interpretations v1 and v2) or making c true (preferred interpretations v2 and v3):
We now have a sound and complete dialogical proof method for credulous acceptance in ADFs under the preferred semantics. The approach we took is motivated by the need to explain argument acceptance in ADFs. An important question is therefore whether dialogical proofs can indeed be used for this purpose and, if not, whether they can be transformed into adequate explanations. We plan to address this question more thoroughly in future work and will suffice here with some brief remarks. Firstly, we would like to interpret a dialogical proof as a sequence of statements connected by a because relationship. One issue is that of circular justifications. Take dialogical proof (5) as an example. This proof ends with the moves ¬b, ¬b, ¬a, ¬a and ⊤. What happens here is that ¬b is justified by ¬a which is in turn, in a circular fashion, justified by ¬b. This circular justification is not made explicit in the proof, however, and finding a way to do so may be necessary to obtain adequate explanations.
Let us now consider another issue, namely that of redundancy due to repetition of formulas. The problem is that we do not want to explain a formula φ by stating that “φ because φ ”. Take again proof (5) as an example. Here we see that every proponent move apart from p4 is logically equivalent to the preceding opponent move. The reason for this is that these opponent moves are formulas with only one prime implicant, namely the formula itself. Let us refer to such formulas as deterministic. Let us furthermore refer to a dialogical proof in which all deterministic proponent moves are removed, as type 1 explanations. The type 1 explanation corresponding to the dialogical proof (5) is the following sequence (we use =⇒ to denote the “because” relationship).
f =⇒ ¬e =⇒ ¬(c ∨ ¬d) =⇒ ¬(a ∧ b) ∧ d =⇒ ¬a ∧ d =⇒ ¬b =⇒ ¬a =⇒ ⊤ Another possibility is to simply remove all opponent moves. Let us refer to this as a type 2 explanation. For the dialogical proof (5) we get the following type 2 explanation: f =⇒ ¬e =⇒ ¬c ∧ d =⇒ ¬a ∧ d =⇒ ¬b =⇒ ¬a We invite the reader to reflect on whether these two explanations adequately explain acceptance of f in the ADF shown in Figure 1 on the right.
Zafarghandi et al. [
Our proof method can be seen as a generalisation of Socratic discussion games for credulous
acceptance under the preferred semantics of abstract argumentation frameworks due to Caminada
et al. [
• PRO: IN(d)
“I have an admissible labelling in which d is labelled IN.” • OPP: OUT(c) “But then in your labelling it must also be the case that d’s attacker c is labelled OUT. Based on which grounds?” • PRO: IN(b)
“c is labelled OUT because b is labelled IN.” • OPP: OUT(a) “But then in your labelling it must also be the case that b’s attacker a is labelled OUT. Based on which grounds?” • PRO: IN(b)
“a is labelled OUT because b is labelled IN.” If we translate IN(x) to x and OUT(x) to ¬x, then this dialogue consists of the following moves.
PRO d
OPP PRO ¬c b
OPP PRO ¬a b Three observations: Firstly, this sequence is equivalent to the type 2 explanation (i.e., the sequence resulting from removing all opponent moves) corresponding to the dialogical proof (2) for d, and we see the same equivalence in proofs for other ADFs that represent argumentation frameworks. This means that the roles of the proponent and opponent in a Socratic dialogue are merged into one role, which is in our setting played by the proponent. Secondly, in a Socratic dialogue, there is no analogue of the role played by the opponent in our setting. Consider again dialogical proof (2) as an example. When the proponent moves ¬c, the opponent replies with the exact condition that must be satisfied for ¬c to be justified, which is b ∨ c (i.e., either b or c must be IN). This condition is not made explicit in the Socratic discussion shown above. Third, in a Socratic discussion game, the proponent may only claim that arguments are accepted, and the opponent may only claim that arguments are rejected. Such a restriction does not exist in our setting, where the proponent may claim that arguments are accepted as well as rejected.
In future work we plan to further investigate the use of dialogical proofs for the purpose of explanation. We will also consider ways to present explanations to users in an interactive way. An interesting question in this context is how to incorporate user feedback in such an interactive setting in case of disagreement with an outcome or its explanation, which would lead to an update of the ADF. We also plan to define variants of our method for other semantics, such as the grounded semantics, which amounts to skeptical acceptance under the complete semantics. Finally, we plan to analyse the complexity of our method and to compare its runtime with existing ADF solvers.