Deontic explanations answer why-questions concerning agents' obligations and permissions. Normative systems are notoriously conflict sensitive, making contrastive explanations pressing: “Why am I obliged to do , despite my (seemingly) conflicting obligation to do ?” In this paper, we develop a model of contrastive explanatory dialogues for the well-established defeasible reasoning formalism Input/Output logic. Our model distinguishes between successful, semi-successful, and unsuccessful deontic dialogues. We prove that the credulous and skeptical (under shared reasons) entailment relation of Input/Output logic, can be characterized in formal argumentation using preferred and grounded semantics. This result allows us to leverage known results for dialogue models of the latter two semantics. Since this work is the first of its kind, we discuss 5 key challenges for deontic explanations through dialogue.
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 afected 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 [
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 [
Contributions. We provide dialogue models for one of the central defeasible normative
reasoning formalisms in the literature: Input/Output logic [
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 [
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.
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 [
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 ifnite 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 [
A DAC is a sequent-style, that is, rule-based proof system for deriving these two types of
argument [
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
Ax , ∈ {, , } and Γ, Δ ⊆ ℒ , Γ ⇒ Δ , Γ ⇒ Δ
Γ ⇒ Γ, (¬ ) ⇒ ⇒ (⊤, ⊤)
Con
Taut Γ, (, ) ⇒ Γ ⇒ ¬(, ) Γ ⇒ Γ ∖ ℒ ⇒ ¬(Γ ∩ ℒ) InaC Γ ⇒
, Γ′ ⇒ Δ Γ, Γ′ ⇒ Δ
Ina
Cut
, (, ) ⇒ FDet
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 [
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 out3 here and some known results [
We use formal argumentation [
• defeats , i.e., (, ) ∈ Att ⊆ Arg × Arg if conc() = ¬Δ ∈ ℒ, and Δ ⊆ prem().
We write Arg(Σ) = {⊢DAC | prem() ⊆ Σ}.
defeats an argument ∈ Arg if there is a ∈ that defeats ; and defends if defeats
every argument that defeats . Let Defended() be the set of arguments defended by .
We recall the following semantic definitions [
We recall [5, Theorem 2] that for the system adopted in this paper, DAC-induced ℱ s are
sound and complete for the system out3 of constrained Input/Output logic [
argument ∈ Arg(ℱ ∪ )).
Our aim is to employ dialogue models for contrastive deontic explanations and for this we need
coincide and we simply write |∼ grounded. The proofs below do not reference specific
some additional results. Since the grounded extension is unique [
⋂︀ stb(ℱ ) if every defeater ∈ Arg of is -inconsistent (i.e., it is defeated by an 2. grd(ℱ ) = ⋂︀ stb(ℱ ) = 2 = Defended(Arg(ℱ ∪ )) (and so |∼ grounded = |∼ s∩tarebale).1 ∈ = Δ2 , Θ2, Γ2 ⇒ ¬(,
⋂︀ stb(ℱ ) and (, Proof. Ad 1. Let = Δ1 , Θ1, Γ1 ⇒ Σ ∈ Arg().
) of . By Proposition 1, Θ2 ∪ {(,
)} is -inconsistent in . Since ) ∈ prem(), and by Proposition 3, Θ2 is not contained in a consistent
Left-to-Right. Consider a defeater in this set do not have defeaters. So, ∈ 2 ⊆ grd(ℱ ). 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 Ω ∩ ℒ ⋂︀ stb(ℱ ). So, ⋂︀ stb(ℱ ) defends and therefore ∈ ⋂︀ stb(ℱ ). = ∅. Since has no defeaters,
Ad 2. Left-to-Right. Straightforward. We show Right-to-Left. Let ∈
Item 1, is defended by Arg(ℱ ∪ ). Clearly, Arg(ℱ ∪ ) ⊆ 1 ⊆ grd(ℱ ) since arguments
⋂︀ stb(ℱ ). By
1Recall that ⋃︀
interesting result that the fixed-point construction of the grounded extension terminates on the second iteration.
≥ 0 where 0 = ∅ and +1 = Defended(). The proposition states the computationally
Proposition 4. Let ℱ be a DAC-induced ℱ for = ⟨ℱ , , ⟩ and let ⊆ Arg: is a
stable extension if is a preferred extension (and so |∼ *preferred = |∼ *stable, for * ∈ {∪ , ∩rea}).
Proof. Left-to-Right. Lemma 15 in [
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 [
Proof. Left-to-Right. Let ′ = (Γ ∪ Δ) ∩ ℒ, and ℱ ′ = { | ∈ Γ ∪ Δ}. By Prop. 3, there is no ℳ ∈ maxfam() with ′ ⊆ ℳ . So, there is a Ω ⊆ for which ⊥ ∈ (out3( ′, ℱ ′) ∪ Ω). 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
2In the philosophical literature deontic explanations are relatively unexplored. Our account takes the
questionoriented pragmatic approach to contrastive explanation (cf. [
R: despite( )?
R: ! H: why( )despite( )?
H: argue( = Γ ⇒ ) R: argue = Σ ⇒ ¬Γ′
Γ′ ⊆ (Γ ∩ ℒ ) H: argue Π, Σ, Θ ⇒ Π ⊆prem ℰR ,
Θ ⊆ H: argue Δ, Γ, Ω ⇒ Ω ⊆
ℰcontrast (c2)
Sub-dialogue for
the acceptance of
Sub-dialogue for
the acceptance of
ℰclaim (c1)
ℰcomp (c4)
ℰcounter (c3)
possible objections the explainee may have against concluding . c2 makes explicit the contrast
between the argument for with an argument for , and c3 provides illative and dialectical
explanations for why can be successfully objected to (our terminology mirrors Johnson’s
well-known two-tier model of argument [
Although explanatory dialogues are collaborative, we assume a burden of proof for the explainer with respect to c1 and c3, and for explainee with respect to c2 and c4. For the sake of simplified reference, we call the explainee ‘human’ ( H) and the explainer ‘robot’ (R). Explanatory Dialogues Let ℱ () be a DAC-induced argumentation framework. Let R be the explainer and H the explainee. A contrastive explanatory dialogue (CED) is a sequence ℰ = ⟨1, . . . , ⟩ of tuples = ⟨pl, lo, ta⟩ called moves such that is ’s position in the dialogue, pl() ∈ {R, H} is the player making move , lo() ∈ Locutions is the locution in , and ta() ∈ {1, . . . , − 1} ∪ {∅} is the target of . Locutions = {()!, why()despite()?, despite()?, argue()} is the set of expressions that interlocutors may use, where and range over ℒ and ranges over Arg(). ℰ is a sem-CED (for sem ∈ {preferred, grounded}) whenever ℰ satisfies the protocol stipulated by P1-P5.
1 = ⟨R, !, ∅⟩ 3 = ⟨R, argue(), 2⟩ with conc() = 2 = ⟨H, why( )despite( )?, 1⟩ 4 = ⟨R, despite( )?, 2⟩ P2 General Rules for each , ∈ ℰ : i) if > 4, then lo() = argue(), and ta() = with < . ii) if ta() = , lo() = argue() and lo() = argue(), then conc() = ¬Δ ∈ ℒ for some Δ ⊆ prem(); iii) if ta() = ta() and ̸= , then lo() ̸= lo(); iv) if ta() = , then pl() ̸= pl().
P1 stipulates that (1) R starts the dialogue with a command to which, (2) H responds with a contrastive why-question. Then, (3) R must provide reasons for the command and, after that, (4) shifts the burden of proof to H requesting support for the contrastive claim. P2 stipulates rules that hold for both R and H: (i) after the start of the dialogue any player may continue making moves that target previous moves by stating arguments, where (ii) arguments moved against other arguments express undermining defeats, (iii) players may not move an argument twice against the same move, and (iv) they may not attack their own claims.
P3 Explainer Rules for each , ∈ ℰ , if ta() = 2, then = 3 or = 4. P4 Explainee Rules for each , , ∈ ℰ : i) if ta()=ta( )=ta()=4 (and, so, pl() = H), then |{, , }| ≤ 2. ii) if ta()=ta( )=4, ̸=, {lo(), lo( )} = {argue(), argue()}, lo(3) = argue(), then conc() = and = prem(), prem(), Ω ⇒ with Ω ⊆ . iii) if ta() = , ta() = , ta( ) = 4, lo( ) = argue(), with conc() ̸= ∅, and lo() = argue(), then – either lo() = argue(Σ, prem(), ⇒ ), and Σ ⊆ prem(ℰR) with ℰR = { | ∈ ℰ , pl() = R, lo() = argue()}; – or lo() = argue() for some with conc() = ¬Δ ∈ ℒ and Δ ⊆ prem().
P3 states that R must provide exactly two moves against the contrastive why-question (one of which provides reasons, and the other questioning the contrastive claim). P4 stipulates that the explainee H may (i) make at most two moves against R’s questioning of the contrastive link, (ii) one of which is an argument providing reasons for the counter-claim, one which shows the -incompatibility of the arguments for the claim and the counter-claim . Then, (iii) H may also move against the explainer’s argument opposing the reasons for the counter-claim. In case is incompatible with the other arguments ofered by R, R engages in incoherent reasoning. H may, thus, oppose by demonstrating the -incompatibility of and other R arguments.
A CED has a tree-structure since each move has exactly one predecessor (except for the root). A branch of ℰ containing is the maximal linear sequence branch() = ⟨1 , . . . , = , . . . , ⟩ such that for each and +1 , ta(+1 ) = . We say is a leaf. Each CED consists of four subdialogues (see Fig. 3), which constitute four sub-explanations: a subdialogue ℰclaim (cf. c1) that engages with the argument given in favour of the claim (generated from 3 down); a subdialogue ℰcounter (cf. c3) that engages with the argument given in favour of the counter-claim (generated from the move attacking the argument providing reasons for ); and the subdialogues ℰcontrast (cf. c2) and ℰcomp (cf. c4) each containing at most one node with an argument that shows the -incompatibility of and , respectively, joint -incompatibility of R’s explanations ℰclaim and ℰcounter. These four subdialogues determine when a given dialogues is (un/semi)successful.
Before defining success, we add P5 to the protocol to accommodate reasoning with preferred
and grounded acceptance of arguments. For sem ∈ {preferred, grounded}, (i) R may move at
most one counter-argument to each H argument. For preferred dialogues, (ii) H is not allowed to
move the same argument twice on a branch in ℰclaim or ℰcounter. For grounded dialogues, (iii) R
is not allowed to move the same argument twice on a branch. We note that (i)-(iii) follow the
protocols for admissible (and, so, preferred) and grounded argumentation games [
Successful dialogues Let ℱ () be DAC-induced. A CED ℰ satisfying P1-P5 is: ∙ successful if ℰcontrast ̸= ∅, ℰcomp = ∅, and ℰclaim and ℰcounter both contain R-leaves only; ∙ semi-successful if ℰcontrast = ∅ = ℰcomp, and ℰclaim contains R-leaves only; ∙ unsuccessful if neither of the above holds.
Then, ℰ is sem-successful when it is saturated (i.e., all movable arguments from ℱ ()
are moved in ℰ ; cf. [
In brief, a successful CED features (c1) an illative explanation that is supplemented by a dialectical explanation (ℰclaim contains only R-leaves), where (c2) the explainee is able to demonstrate the incompatibility of the contrastive claim (ℰcontrast ̸= ∅), the latter which (c3) the explainer successfully counters (ℰcounter contains only R-leaves). Furthermore, (c4) the position taken by R in ℰclaim and ℰcounter must be -compatible. A semi-successful dialogue features (c1), but H is not able to demonstrate the adequacy of the contrastive link (ℰcontrast = ∅). A dialogue can be unsuccessful for various reasons, e.g., R cannot provide an illative or dialectic explanation, or R cannot argue against H’s counter-claim.
Under saturation, it can be easily checked that the sub-dialogues in ℰclaim and ℰcounter are for
sem ∈ {preferred, grounded} instances of credulous preferred and grounded argumentation
games [
R: ¬ ! R: ! H: why(¬ )despite( )? H: why( )despite(¬ )? R: argue(a) H: argue( )
R: argue( ) ℰclaim i)
R: despite( )? ℰcomp
H: argue( ) H: ∅
R: argue
H: argue( )
ℰcontrast ℰcounter
R: argue( )
H: argue( ) ℰclaim ii)
H: ∅ ℰcomp
H: argue( )
R: despite(¬ )? R: argue H: argue ℰcounter
H: argue( ) ℰcontrast 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 .
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 ofered 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.
that are, under thorough analysis, not really incompatible with the ofered 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 diferent conceptual base than the one provided here, posing their own specific challenges (e.g., balancing reasons). Acknowledgements. This work was partially funded by the “Logical Methods of Deontic Explanations” (LoDeX) project, Deutsche Forschungsgemeinschaft, Project number 511915728.