Introduction

Norms are indispensable in many aspects of society, ranging from law, ethics, to business protocols and AI. They motivate, guide, and regulate agents, whether they are human or artificial. Often, agents affected by norms do not only need to know that they are bound by obligations or that they may appeal to rights: they need to understand why. Such understanding may enhance compliance and collaboration and is especially pressing when conflicts between norms arise. For instance, I may want to know why I may take over on the left, despite being obliged to drive on the right. Here, a good explanation not only explains that I am permitted, but also why the obligation to the contrary does not currently apply: the permission is an exception to the obligation. Answers to this type of why-question are called deontic explanations.

Deontic logic is the well-established field exploring formal methods to model normative reasoning. However, the focus has been nearly exclusively on formal systems that determine which obligations and permissions can be inferred from a normative system, rather than to explain why. This gap is remarkable, especially given the increasingly vital role that normative systems play in alignment and compliance requirements for AI. This paper investigates how knowledge representation methods can be used to generate explanatory deontic dialogues.

The demand for explanatory models in AI is increasing [1] and formal argumentation provides a promising method in this respect. First of all, formal argumentation has proven to be a unifying framework for nonmonotonic reasoning [2]. In particular, two central paradigms of defeasible reasoning, constrained Input/Output (I/O) logic [3] and default logic [4], can be argumentatively characterized [5,6]. Second, a wide variety of methods has been proposed in Argumentation for Explainable AI (ArgXAI, [7]). Finally, dialogue models and argumentation games [8,9,10], offer dynamic characterizations of formal argumentation, that have the potential to yield interactive (or even tailor-made) explanatory episodes through dialogues.

Once a given nonmonotonic logic is represented in logical argumentation, such as I/O-or default logic, dialogical methods can be leveraged for explanatory purposes. However, a first obstacle, in this respect, is that most characterization results are shown with respect to stable semantics (including [5,6]; also see [2]), whereas other semantics such as preferred, admissible, and grounded are more suitable for dialogical generalization. In brief, the problem with stable extensions is that they reference the entire set of arguments (each argument is either 'in' or 'out'), while we expect explanatory dialogues to focus on reasons relevant to the explanatory purpose. Furthermore, defining dialogue models and argumentation games for skeptical reasoning is challenging (in the context of multi-extension semantics such as preferred; cf. [10]).

Contributions. We provide dialogue models for one of the central defeasible normative reasoning formalisms in the literature: Input/Output logic [3,11]. Unfortunately, the original formalism does not naturally lend itself to explanatory reasoning. Recently, a highly modular rule-based proof system -the Deontic Argumentation Calculus (DAC) -was developed with the aim of making I/O suitable for explanatory purposes and it was shown that DAC-induced argumentation frameworks are sound and complete for a large class of constrained I/O logics [5] and default logic [6]. Despite these promising results, the correspondences were only obtained for stable semantics, making them seemingly unsuitable for dialogical deontic explanations.

In this article, we extend these results by a model of dialogue episodes for deontic explanations:

(1) As a preparatory step, we first prove that for DAC-induced argumentation frameworks the stable and the preferred semantics coincide. This allows us to use well-developed preferred dialogue models in the context of I/O reasoning. (2) Furthermore, we lift recent results [12] that show that the 'free consequences' of skeptical entailment under stable semantics is identical to entailment under the grounded semantics.

In other words, we may also use grounded dialogue models for I/O reasoning. (3) Using (1) and (2), we enhance dialogue models and define contrastive deontic explanations that explain certain obligations in contrast to seeming obligations to the contrary.

Outline. Section 2 introduces the DAC formalism. In Section 3, we define DAC-induced argumentation frameworks and prove that stable equals preferred and the free consequences correspond to grounded entailment. We harness these results to specify contrastive dialogue models in Section 4. This paper lays the foundations for a more extensive study of dialogue models of deontic explanation and, for this reason, we discuss five key challenges in Section 5.

Preliminaries: A Deontic Argumentation Calculus (DAC)

We recall the basics of the Deontic Argumentation Calculus (DAC). Although the results in this paper hold for a range of languages, base logics, and DAC systems, for readability we assume a propositional language ℒ and classical logic L, and illustrate our approach for one DAC system from [5]. To enhance explainability, ℒ is labeled and augmented with a language of norms: Labeled propositional languages: ℒ 𝑖 = {𝜙 𝑖 | 𝜙 ∈ ℒ} where 𝑖 ∈ {𝑓, 𝑜, 𝑐}.

Norm languages: ℒ𝑛 = {(𝜙, 𝜓) | 𝜙, 𝜓 ∈ ℒ} and ℒ 𝑛 = {¬Δ | ∅ ⊂ Δ ⊆ ℒ 𝑛 , Δ is finite}.

Normative systems: 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ is a normative system, where ℱ ⊆ ℒ 𝑓 is a factual context, 𝒩 ⊆ ℒ 𝑛 a normative code, and 𝒞 ⊆ ℒ 𝑐 a set of constraints (and ℱ and 𝒞 are L-consistent).

Labels explicate the roles that propositional formulas adopt in the reasoning process: 𝜙 𝑓 denotes that 𝜙 is a fact, 𝜙 𝑜 that 𝜙 is obligatory, and 𝜙 𝑐 that obligations must be consistent with 𝜙. We take (𝜙, 𝜓) ∈ ℒ 𝑛 to expresses the norm "given 𝜙, it is obligatory that 𝜓" and ¬Δ ∈ ℒ 𝑛 is read as "the norms in Δ are jointly inapplicable. " For ¬{(𝜙, 𝜓)}, we simply write ¬(𝜙, 𝜓). The latter type of expression plays an essential role in defeasible reasoning with norms. The entire enhanced I/O language is defined as the union

ℒ 𝑖𝑜 = ℒ 𝑓 ∪ ℒ 𝑜 ∪ ℒ 𝑐 ∪ ℒ 𝑛 ∪ ℒ 𝑛 .

We write Γ 𝑖 , Δ 𝑖 , . . . for finite sets of 𝑖-labeled formulas, where 𝑖 ∈ {𝑓, 𝑜, 𝑐}. We write Γ, Δ, . . . for any finite subset of ℒ 𝑖𝑜 and Δ ↓ for a set Δ ⊆ ℒ 𝑖 stripped from its label 𝑖 ∈ {𝑓, 𝑜, 𝑐}.

Defeasible normative reasoning occurs with respect to a normative system 𝒦. The basic idea of I/O reasoning [3] and DAC is that facts (input) trigger norms from which obligations (output) are detached where the constraints filter the output to ensure consistency. Our aim is to construct arguments from 𝒦. Our approach belongs to logical argumentation (a subfield of structured argumentation [2]). We write arguments as sequents: 𝑎 = Γ ⇒ 𝜙, where prem(𝑎) = Γ is a (possibly empty) set of premises, and conc(𝑎) = 𝜙 is the conclusion of the argument. An explanatory argument is an argument stating reasons for a conclusion. We take facts, constraints, and norms as reasons and differentiate two types of argument:

𝜙 𝑓 , (𝜙, 𝜓) ⇒ 𝜓 𝑜 and 𝜙 𝑓 , ¬𝜓 𝑐 ⇒ ¬(𝜙, 𝜓)

The first type (left) contains arguments providing reasons for obligations, where the fact 𝜙 𝑓 and norm (𝜙, 𝜓) provide reasons for the obligation 𝜓 𝑜 . The second type (right) contains arguments that attack reasons, expressing which norms are inapplicable in the given context, where given 𝜙 𝑓 , the norm (𝜙, 𝜓) is inapplicable since its detachable obligation is inconsistent with the constraint ¬𝜓 𝑐 . The latter type attacks all arguments using (𝜙, 𝜓) as a reason.

A DAC is a sequent-style, that is, rule-based proof system for deriving these two types of argument [5]. We assume that LC is the sound and complete sequent calculus for L.

Deontic Argumentation Calculus (DAC):

Let DAC be a system consisting of the rules Ax, FDet, DDet, Con, Ina, InaC, Taut, and Cut (Figure 1). A DAC-derivation of Γ ⇒ Δ is a tree-like structure whose leaves are initial sequents, whose root is Γ ⇒ Δ, and whose ruleapplications are instances of the rules of DAC. We say Γ ⇒ Δ is DAC-derivable (written ⊢ DAC Γ ⇒ Δ) whenever there exists a DAC-derivation for it, Γ ⊆ ℒ 𝑖𝑜 , and Δ ⊆ ℒ 𝑖𝑜 contains at most one formula. We say

Γ ⇒ Δ is 𝒦-based whenever Γ ⊆ ℱ ∪ 𝒩 ∪ 𝒞.

There are three initial sequent rules: Ax introduces labeled versions of any classically derivable Γ ⇒ Δ to a DAC-derivation (and so LC rules are not part of DAC). Taut guarantees that all propositional tautologies are among the output. FDet expresses factual detachment and gives an initial explanatory argument stating that the fact 𝜙 𝑓 and the norm (𝜙, 𝜓) are reasons for concluding the obligation 𝜓 𝑜 . DDet corresponds to deontic detachment and makes it possible that a norm may be triggered by obligations detached from other norms (see Ex. 1). The rules Con, Ina, and InaC deal with the defeasibility of normative reasoning and yield attacking arguments. The Con rule expresses the consistency constraint that if Γ constitutes reasons for 𝜙 𝑜 , then Γ is inconsistent with the constraint ¬𝜙 𝑐 (where an empty right-hand side denotes inconsistent reasons). We also refer to Γ ⇒ as an inconsistent argument. When an argument expresses inconsistent reasons, at least one of its involved norms is inapplicable (Ina) and all involved norms are jointly inapplicable (InaC). We refer to [5] for other DAC systems.

⊢ LC Γ ⇒ Δ Ax Γ 𝑖 ⇒ Δ 𝑖 , 𝑖 ∈ {𝑓, 𝑜, 𝑐} and Γ, Δ ⊆ ℒ Taut ⇒ (⊤, ⊤) FDet 𝜙 𝑓 , (𝜙, 𝜓) ⇒ 𝜓 𝑜 𝜙 𝑓 , Γ ⇒ Δ DDet 𝑎 𝜙 𝑜 , Γ ⇒ Δ Γ ⇒ 𝜙 𝑜 Con Γ, (¬𝜙) 𝑐 ⇒ Γ, (𝜙, 𝜓) ⇒ Ina Γ ⇒ ¬(𝜙, 𝜓) Γ ⇒ InaC Γ ∖ ℒ 𝑛 ⇒ ¬(Γ ∩ ℒ 𝑛 ) Γ ⇒ 𝜙 𝜙, Γ ′ ⇒ Δ Cut 𝑏 Γ, Γ ′ ⇒ Δ

Example 1. We look at Chisholm's scenario [11], an archetype of contrary-to-duty reasoning. Billie is obligated to go and help her neighbors (⊤, ℎ) (⊤ denotes that ℎ is detached by default). If Billie goes to help, she must tell the neighbors she goes (ℎ, 𝑡), otherwise she ought not to tell them she goes (¬ℎ, ¬𝑡). Suppose that Billie does not go and help ¬ℎ 𝑓 and, so, violates the default duty in (⊤, ℎ). To know what Billie must do in light of her violation ¬ℎ 𝑓 , the constraint is imposed that the obligations must be consistent with the fact that Billie does not help ¬ℎ 𝑐 [5,11]. Let ℱ = {¬ℎ 𝑓 }, 𝒩 = {(⊤, ℎ), (ℎ, 𝑡), (¬ℎ, ¬𝑡)}, and 𝒞 = {¬ℎ 𝑐 } be the normative system 𝒦. The desired outcome is that Billie ought not to tell the neighbors she goes ¬𝑡 𝑜 given that she does not go.

Argument 𝑑 (below left), stating that Billie ought to tell, is derived with deontic detachment. Argument 𝑒 (below right), expresses the inapplicability of ¬(⊤, ℎ) given the set constraint. Similar reasoning gives the inconsistent argument 𝑥 = ¬ℎ 𝑓 , (⊤, ℎ), (ℎ, 𝑡), (¬ℎ, ¬𝑡) ⇒ , which with Con, Cut, and InaC derives the unattackable 𝑥 ′ = ¬ℎ 𝑓 ⇒ ¬{(⊤, ℎ), (ℎ, 𝑡), (¬ℎ, ¬𝑡)}.

FDet ⊤ 𝑓 , (⊤, ℎ) ⇒ ℎ 𝑜 FDet ℎ 𝑓 , (ℎ, 𝑡) ⇒ 𝑡 𝑜 DDet ℎ 𝑜 , (ℎ, 𝑡) ⇒ 𝑡 𝑜 Cut 𝑏 = ⊤ 𝑓 , (⊤, ℎ), (ℎ, 𝑡) ⇒ 𝑡 𝑜 FDet ⊤ 𝑓 , (⊤, ℎ) ⇒ ℎ 𝑜 Con ⊤ 𝑓 , (¬ℎ) 𝑐 , (⊤, ℎ) ⇒ Ina 𝑒 = ⊤ 𝑓 , (¬ℎ) 𝑐 ⇒ ¬(⊤, ℎ)

For the sake of completion, we recall the I/O system out 3 here and some known results [5].

Proposition 1 ([5]). Let 𝒦 ↓ = ⟨ℱ, 𝒩 , 𝒞⟩ be 𝒦 stripped from its labels. Let Δ ⊆ ℒ, 𝐶𝑛(Δ) = {𝜙 | Δ ⊢ L 𝜙}, and out(𝒩 , Δ) = 𝐶𝑛({𝜙 | (𝜓, 𝜙) ∈ 𝒩 and 𝜓 ∈ 𝐶𝑛(Δ)}). Let out 3 (𝒩 , ℱ) = ⋃︀ 𝑖≥0 𝑂 𝑖 , where 𝑂 0 = out(𝒩 , ℱ) and 𝑂 𝑖+1 = 𝐶𝑛(𝑂 𝑖 ∪ out(𝒩 , 𝑂 𝑖 ∪ ℱ)). In words, out 3 is a closure of 𝒩 under successive (deontic) detachment with respect to ℱ. Then 𝒩 ⊆ ℒ 𝑛 is 𝒞-consistent in 𝒦, if ⊥ / ∈ 𝐶𝑛(out 3 (𝒩 , ℱ) ∪ 𝒞). Let Θ ⊆ 𝒩 ⊆ ℒ 𝑛 , Δ ⊆ ℱ ⊆ ℒ

and Ω ⊆ 𝒞 ⊆ ℒ, we have:

1. 𝜙 ∈ out 3 (Θ, Δ) iff ⊢ DAC Θ, Δ 𝑓 ⇒ 𝜙 𝑜 ; 2. Θ is 𝒞-inconsistent iff there are Δ ⊆ ℱ and Ω ⊆ 𝒞 for which ⊢ DAC Θ, Δ 𝑓 , Ω 𝑐 ⇒ ; 3. ⊥ ∈ 𝐶𝑛(out 3 (Θ, Δ) ∪ Ω) iff for all (𝜙, 𝜓) ∈ Θ, ⊢ DAC Θ ∖ {(𝜙, 𝜓)}, Δ 𝑓 , Ω 𝑐 ⇒ ¬(𝜙, 𝜓).

Formal Argumentation with DAC-arguments

We use formal argumentation [13] to capture the defeasibility of normative reasoning and to explicate norm conflicts [5]. An Argumentation Framework [13] contains a set of arguments and an attack relation between arguments, where semantics stipulate conditions under which sets of arguments are jointly acceptable. We instantiate such frameworks with DAC-arguments.

DAC-induced Argumentation Frameworks

Let 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ be a normative system. A DAC-induced argumentation framework 𝒜ℱ(𝒦) = ⟨Arg, Att⟩ is defined as follows: • 𝒜ℱ |∼ ∩rea sem 𝜙 iff there is an 𝑎 contained in every sem-extension that concludes 𝜙; • 𝒜ℱ |∼ ∪ sem 𝜙 iff there is a sem-extension ℰ for which there is an 𝑎 ∈ ℰ concluding 𝜙.

• Δ ⇒ Γ ∈ Arg iff Δ ⇒ Γ is DAC-

|∼ ∩rea sem captures the shared arguments (shared reasons) by all sem-extensions. The resulting conclusions are called the free consequences of 𝒦, which are obligations from unproblematic norms compatible with any sem-extension. Credulous entailment |∼ ∪ sem captures the existence of reasons in favor of a conclusion for some sem-extension, expressing a defensible stance.

Example 2. The partial 𝒜ℱ in Figure 2 captures the scenario from Ex. 1. There is only one stable extension {𝑎, 𝑏, 𝑔, 𝑥 ′ } (the arrows from 𝑏, 𝑒, 𝑓, and 𝑔 to 𝑥 are implicit), which is also the grounded extension (cf. Prop. 3-2 below). We may, thus, conclude 𝒜ℱ |∼(¬𝑡) 𝑜 (where |∼ ∈ {|∼ ⋆ sem | ⋆ ∈ {∩rea, ∪} and sem ∈ {stable, grounded}}). As desired, since Billie does not go to help her neighbors, she ought not to tell them she is coming. Billie may now ask "Why am I obliged to not tell my neighbors, despite my seeming duty to tell them I am coming to help?" To this we turn next.

We recall [5, Theorem 2] that for the system adopted in this paper, DAC-induced 𝒜ℱs are sound and complete for the system out 3 of constrained Input/Output logic [3].

Proposition 2. Let 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ and let maxfam(𝒦) = {𝒩 ′ ⊆ 𝒩 | ⊥ ̸ ∈ 𝐶𝑛(out 3 (𝒩 ′ , ℱ ↓ ) ∪ 𝒞 ↓

) and for each 𝒩 ′ ⊂ 𝒩 ′′ , ⊥ ∈ 𝐶𝑛(out 3 (𝒩 ′′ , ℱ ↓ ) ∪ 𝒞 ↓ )} be the set of maximal consistent sets of norms over 𝒦. Let 𝒜ℱ be induced by DAC and 𝒦 with the set of stable extensions stable(𝒜ℱ): Our aim is to employ dialogue models for contrastive deontic explanations and for this we need some additional results. Since the grounded extension is unique [13], |∼ ∩rea grounded and |∼ ∪ grounded coincide and we simply write |∼ grounded . The proofs below do not reference specific DAC-rules (outside the base system [5,12]), and thus generalize to all DAC systems in [5] (augmented with InaC). Proposition 3 tells us that for reasoning about the free consequences under the stable semantics, it suffices to reason with the grounded semantics. Proposition 4 shows that the preferred and stable semantics coincide for DAC. Consequently, these propositions allow us to apply well-developed dialogue techniques to DAC for skeptical (in terms of free consequences) and credulous reasoning under the grounded, respectively the preferred semantics.

1. If 𝒩 ′ ∈ maxfam(𝒦), then Arg(ℱ ∪ 𝒩 ′ ∪ 𝒞) ∈ stable(𝒜ℱ); 2. If 𝒜 ∈ stable(𝒜ℱ), then there is a 𝒩 ′ ∈ maxfam(𝒦) for which 𝒜 = Arg(ℱ ∪ 𝒩 ′ ∪ 𝒞). 29-40 𝑎 = [︂ (¬ℎ) 𝑓 , (¬ℎ, ¬𝑡) ⇒ (¬𝑡) 𝑜 ]︂ 𝑏 = [︂ (¬ℎ) 𝑐 ⇒ ¬(⊤, ℎ) ]︂ 𝑑 = [︂ (⊤, ℎ), (ℎ, 𝑡) ⇒ 𝑡 𝑜 ]︂ 𝑐 = [︂ (⊤, ℎ) ⇒ ℎ 𝑜 ]︂ 𝑒 = [︂ (¬ℎ) 𝑓 , (⊤, ℎ), (ℎ, 𝑡) ⇒ ¬(¬ℎ, ¬𝑡) ]︂ 𝑓 = [︂ (¬ℎ) 𝑓 , (⊤, ℎ), (¬ℎ, ¬𝑡) ⇒ ¬(ℎ, 𝑡) ]︂ 𝑔 = [︂ (¬ℎ) 𝑓 , (ℎ, 𝑡), (¬ℎ, ¬𝑡) ⇒ ¬(⊤, ℎ) ]︂ 𝑥 ′ 𝑥

Proposition 3. Let 𝒜ℱ be a DAC-induced 𝒜ℱ for 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ and let stb(𝒜ℱ) and grd(𝒜ℱ) be the set of stable extensions, respectively the grounded extension of 𝒜ℱ:

1. 𝑎 ∈ ⋂︀ stb(𝒜ℱ) iff every defeater 𝑏 ∈ Arg of 𝑎 is 𝒞-inconsistent (i.e., it is defeated by an argument 𝑐 ∈ Arg(ℱ ∪ 𝒞)).

grd(𝒜ℱ) =

⋂︀ stb(𝒜ℱ) = 𝒢 2 = Defended(Arg(ℱ ∪ 𝒞)) (and so |∼ grounded = |∼ ∩rea stable ). 1 Proof. Ad 1.

Let 𝑎 = Δ 𝑓 1 , Θ 1 , Γ 𝑐 1 ⇒ Σ ∈ Arg(𝒦). Left-to-Right. Consider a defeater 𝑏 = Δ 𝑓 2 , Θ 2 , Γ 𝑐 2 ⇒ ¬(𝜙, 𝜓) of 𝑎. By Proposition 1, Θ 2 ∪ {(𝜙, 𝜓)} is 𝒞-inconsistent in 𝒦. Since 𝑎 ∈

⋂︀ stb(𝒜ℱ) and (𝜙, 𝜓) ∈ prem(𝑎), and by Proposition 3, Θ 2 is not contained in a consistent set of norms in 𝒦 and it is therefore inconsistent. By Proposition 1, there are

Δ 𝑓 3 ∪ Γ 𝑐 3 ⊆ ℱ ∪ 𝒞 such that Δ 𝑓 3 , Γ 𝑐 3 ⇒ ¬Θ 2 defeats 𝑏. Right-to-Left.

It is easy to see that ⋂︀ stb(𝒜ℱ) contains every argument it defends. Suppose now that 𝑏 = Γ ⇒ Δ is 𝒞-inconsistent. By Proposition 1, there is a 𝑐 = Ω ⇒ ¬(Γ ∩ ℒ 𝑛 ) that defeats 𝑏 and for which Ω ∩ ℒ 𝑛 = ∅. Since 𝑐 has no defeaters, 𝑐 ∈ ⋂︀ stb(𝒜ℱ). So, ⋂︀ stb(𝒜ℱ) defends 𝑎 and therefore 𝑎 ∈ ⋂︀ stb(𝒜ℱ). Ad 2. Left-to-Right. Straightforward. We show Right-to-Left. Let 𝑎 ∈ ⋂︀ stb(𝒜ℱ). By Item 1, 𝑎 is defended by Arg(ℱ ∪ 𝒞). Clearly, Arg(ℱ ∪ 𝒞) ⊆ 𝒢 1 ⊆ grd(𝒜ℱ) since arguments in this set do not have defeaters. So, 𝑎 ∈ 𝒢 2 ⊆ grd(𝒜ℱ). 1 Recall that ⋃︀ 𝑖≥0 𝒢𝑖 where 𝒢0 = ∅ and 𝒢𝑖+1 = Defended(𝒢𝑖). The proposition states the computationally interesting result that the fixed-point construction of the grounded extension terminates on the second iteration. Proposition 4. Let 𝒜ℱ be a DAC-induced 𝒜ℱ for 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ and let 𝒜 ⊆ Arg: 𝒜 is a stable extension iff 𝒜 is a preferred extension (and so |∼ * preferred = |∼ * stable , for * ∈ {∪, ∩rea}).

Proof. Left-to-Right. Lemma 15 in [13]. Right-to-Left. Suppose not, then there is an 𝑎 ∈ Arg(𝒦) ∖ 𝒜 but no 𝑏 ∈ 𝒜 for which (𝑏, 𝑎) ∈ Att. Since 𝒜 is preferred it is conflict-free. By Proposition 2, 𝒩 ′ = {(𝜙, 𝜓) | (𝜙, 𝜓) ∈ Δ ∩ ℒ 𝑛 and Δ ⇒ Γ ∈ 𝒜} is 𝒞-consistent and so 𝒩 ′ ⊆ 𝒩 ′′ for some 𝒩 ′′ ∈ maxfam(𝒦) and there is a stable extension 𝒜 ′ = Arg(ℱ ∪ 𝒩 ′′ ∪ 𝒞). Clearly, Arg(ℱ ∪ 𝒩 ′ ∪ 𝒞) ⊆ Arg(ℱ ∪ 𝒩 ′′ ∪ 𝒞) and so, 𝒜 is not maximally admissible. Contradiction.

Dialogues and Contrastive Explanations

We now provide dialogue models for contrastive deontic explanations. A contrastive explanatory dialogue starts with a command "𝜙 𝑜 !" issued by the explainer, immediately followed by the explainee asking a question of the form: "Why 𝜙 𝑜 , despite 𝜓 𝑜 ?" Due to the conflict sensitivity of norm systems [3,11], we consider contrastive why-questions as the starting point of explanatory episodes [14]. We refer in what follows to 𝜙 𝑜 as the claim and to 𝜓 𝑜 as the counter-claim. 2 We do not assume that 𝜙 𝑜 and 𝜓 𝑜 are derivable from the given normative system 𝒦, nor do we assume that there is a dialectical relation between 𝜙 𝑜 and 𝜓 𝑜 , referred to as the contrastive link. Both must become explicit (if existent) through the dialogue itself. We say there exists a contrastive link when two arguments 𝑎 and 𝑏 exist concluding 𝜙 𝑜 , respectively 𝜓 𝑜 , which are incompatible, meaning that there is no stable extension containing both. In such a case, an incompatibility argument can be provided using the premises in 𝑎 and 𝑏: Proposition 5. Let 𝒦 = ⟨ℱ, 𝒩 , 𝒞⟩ and 𝒜ℱ(𝒦) = ⟨Arg, Att⟩. For any two arguments 𝑎 = Δ ⇒ 𝜙 𝑜 , 𝑏 = Γ ⇒ 𝜓 𝑜 ∈ Arg: there is no stable extension 𝒮 with 𝑎, 𝑏 ∈ 𝒮 iff there is a DAC-derivable argument Δ, Γ, Ω ⇒ with Ω ⊆ 𝒞 (we call 𝑎 and 𝑏 𝒞-incompatible).

Proof. Left-to-Right. Let 𝒩 ′ = (Γ ∪ Δ) ∩ ℒ 𝑛 , and ℱ ′ = {𝜙 | 𝜙 𝑓 ∈ Γ ∪ Δ}. By Prop. 3, there is no ℳ ∈ maxfam(𝒦) with 𝒩 ′ ⊆ ℳ. So, there is a Ω ⊆ 𝒞 for which ⊥ ∈ 𝐶𝑛(out 3 (𝒩 ′ , ℱ ′ )∪Ω). By Prop. 1 and a Cut application, ⊢ DAC 𝒩 ′ , ℱ ′ , Ω ⇒ . Right-to-Left. Straightforward.

An explanatory dialogue addressing "Why 𝜙 𝑜 , despite 𝜓 𝑜 ?" is successful whenever it contains c1 an argument 𝑎 for 𝜙 𝑜 and a demonstration that all (indirect) objections to 𝑎 can be met; c2 an argument 𝑏 for 𝜓 𝑜 such that 𝑎 and 𝑏 are 𝒞-incompatible (recall Prop. 5); c3 an argument 𝑐 defeating 𝑏 and a demonstration that all (indirect) objections to 𝑐 can be met; c4 a demonstration that the demonstrations in c1 and c3 are 𝒞-compatible.

Informally, c1 provides the 'illative explanation' of "𝜙 𝑜 !" by stating 𝑎 containing the facts and norms in view of which 𝜙 𝑜 holds. It also provides the 'dialectic explanation' of 𝜙 𝑜 by refuting all Example 3. Let sem ∈ {preferred,grounded}: Figure i) provides a successful saturated sem-CED for "Why ¬𝑡 𝑜 , despite 𝑡 𝑜 ?, " notice that ℰ comp is empty since ℰ R = {𝑎, 𝑏} is 𝒞-compatible. Figure ii) contains an unsuccessful saturated sem-CED for "Why 𝑡 𝑜 , despite ¬𝑡 𝑜 ?" where H refutes the claim (with 𝑏) and defends the counter-claim (with 𝑎 and 𝑏). The arguments in i) and ii) reference those in Fig. 2 of Ex. 2 (for space reasons, we adopted an example for which grounded equals stable). ii)

An alternative successful CED for i) exists that includes R moving 𝑔 against 𝑒, followed by H moving 𝑓 , which is then defeated by R moving 𝑏. However, here we can use Proposition 3-1, giving us for sem = grounded the existence of a strategic shortcut by directly moving argument 𝑏 against 𝑒.

Challenges for Dialogical Deontic Explanations

This paper shows how to incorporate existing results in formal argumentation and refine them to yield contrastive explanatory dialogues (CEDs) in the context of defeasible normative reasoning, Input/Output logic in particular. This work is the first of its kind and, so, we end by highlighting some key challenges for deontic explanations (through formal argumentation).

Challenge 1: Conflict Types The contrastive claims offered by the explainee may give rise to various kinds of conflicts with the main claim. Two particularly interesting cases when dealing with (conditional) norms are specificity (you are not allowed to park, unless you are medical personnel) and contrary-to-duty (don't be late, but if you are, not more than 10 minutes). Good explanations should make transparent the type of conflicts involved.

Challenge 2: Cognitive Adequacy A good explainer seeks to understand the explainee in order to tailor the given explanation to precisely target the gaps in the explainee's understanding. For this the explainer may use queries and strategic argumentation, complemented by a theory of (the explainee's) mind. Moreover, the knowledge bases of the explainer and the explainee may be disjoint and incomplete. Tailored explanations must additionally keep track of commitments and shifts therein throughout a dialogue.

Challenge 3: Richer Handling of Contrastives

The explainee may offer contrastive claims that are, under thorough analysis, not really incompatible with the offered claim. A good explainer should catch such cases and provide an argument concerning the compatibility of the claims. For this, more proof-theoretic resources have to be developed. In such cases, the explainee should be able to withdraw or replace the contrast.

Challenge 4: Richer Deontic Vocabulary Often, normative codes are richer than the ones studied here, e.g., they may contain priority orderings over norms and permissive norms.

These come with challenges, for instance concerning reinstatement (e.g., permissions generally do not reinstate obligations). Dialogues ideally accommodate such complexity.

Challenge 5: Casuistry In many application contexts of ethical (e.g., in bioethics) and legal reasoning, we find case-based reasoning when reasoning towards obligations, rights, and permissions. Deontic explanations of such conclusions need a different conceptual base than the one provided here, posing their own specific challenges (e.g., balancing reasons).