# Dialogue-based Explanations for Logical Reasoning using Structured Argumentation
**Authors**: Loan Ho, Stefan Schlobach
> Vrije University Amsterdam, The Netherlands
## Abstract
The problem of explaining inconsistency-tolerant reasoning in knowledge bases (KBs) is a prominent topic in Artificial Intelligence (AI). While there is some work on this problem, the explanations provided by existing approaches often lack critical information or fail to be expressive enough for non-binary conflicts. In this paper, we identify structural weaknesses of the state-of-the-art and propose a generic argumentation-based approach to address these problems. This approach is defined for logics involving reasoning with maximal consistent subsets and shows how any such logic can be translated to argumentation. Our work provides dialogue models as dialectic-proof procedures to compute and explain a query answer wrt inconsistency-tolerant semantics. This allows us to construct dialectical proof trees as explanations, which are more expressive and arguably more intuitive than existing explanation formalisms.
Key words and phrases: Argumentation, Inconsistency-tolerant semantics, Dialectical proof procedures, Explanation
## 1. Introduction
This paper addresses the problem of explaining logical reasoning in (inconsistent) KBs. Several approaches have been proposed by [18, 17, 22, 24], which mostly include set-based explanations and proof-based explanations. Set-based explanations, which are responsible for the derived answer, are defined as minimal sets of facts in the existential rules [18, 17] or as causes in Description Logics (DLs) [22]. Additionally, the work in [22] provides the notion of conflicts that are minimal sets of assertions responsible for a KB to be inconsistent. Set-based explanations present the necessary premises of entailment and, as such, do not articulate the (often non-obvious) reasoning that connects those premises with the conclusion nor track conflicts. Proof-based explanations provide graphical representations to allow users to understand the reasoning progress better [24]. Unfortunately, the research in this area generally focuses on reasoning in consistent KBs.
The limit of the above approaches is that they lack the tracking of contradictions, whereas argumentation can address this issue. Clearly, argumentation offers a potential solution to address inconsistencies. Those are divided into three approaches:
- Argumentation approach based on Deductive logic: Various works propose instantiations of abstract argumentation (AFs) for $\text{Datalog}^{\pm}$ [19, 35], Description Logic [14] or Classical Logic [51], focusing on the translation of KBs to argumentation without considering explanations. In [7], explanations can be viewed as dialectical trees defined abstractly, requiring a deep understanding of formal arguments and trees, making the work impractical for non-experts. In [35, 9], argumentation with collective attacks is proposed to capture non-binary conflicts in $\text{Datalog}^{\pm}$ , i.e., assuming that every conflict has more than two formulas.
- Sequent-based argumentation [69] and its extension (Hypersequent-based argumentation) [55], using Propositional Logic, provide non-monotonic extensions for Gentzen-style proof systems in terms of argumen-tation-based. Moreover, the authors conclude by wishing future work to include âthe study of more expressive formalisms, like those that are based on first-order logicsâ [69].
- Rule-based argumentation: DeLP/DeLP with collective attacks are introduced for defeasible logic programming [45, 70]. However, in [35], the authors claim that they cannot instantiate DeLP for $\text{Datalog}^{\pm}$ , since DeLP only considers ground rules. In [46, 62], ASPIC/ASPIC+ is introduced for defeasible logic. Following [61], the logical formalism in ASPIC+ is ill-defined, i.e., the contrariness relation is not general enough to consider n-ary constraints. This issue is stated in [35] for $\text{Datalog}^{\pm}$ , namely, the ASPIC+ cannot be directly instantiated with Datalog. The reasons behind this are that Datalog does not have the negation and the contrariness function of ASPIC+ is not general for this language.
Notable works include assumption-based argumentation (ABA) [44] and ABA with collective attack [53], which are applied for default logic and logic programming. However, ABAs ignore cases of the inferred assumptions conflicting, which is allowed in the existential rules, Description Logic and Logic Programming with Negation as Failure in the Head. We call the ABAs â flat ABAsâ. In [41], âflatâ ABAs link to Answer Set Programming but only consider a single conflict for each assumption. In [67, 68], â Non-flat â ABAs overcome the limits of âflatâ ABAs, which allow the inferred assumptions to conflict. However, like ASPIC+, the non-flat ABAs ignore the n-ary constraints case. Contrapositive ABAs [65] and its collective attack version [63], which use contrapositive propositional logic, propose extended forms for âflatâ and ânon-flatâ ABAs. While [63] mainly focuses on representation (which can be simulated in our setting, see Section 3.2), we extend our study to proof procedures in AFs with collective attacks.
Argumentation offers dialogue games to determine and explain the acceptance of propositions for classical logic [50], for $\text{Datalog}^{\pm}$ [33, 34, 20, 19], for logic programming/ default logic [48, 47], and for defeasible logic [42]. However, the models have limitations. In [33, 34], the dialogue models take place between a domain expert but are only applied to a specific domain (agronomy). In [20, 19, 42, 50], persuasion dialogues (dialectic proof procedures) generate the abstract dispute trees defined abstractly that include arguments and attacks and ignore the internal structure of the argument. These works lack exhaustive explanations, making them insufficient for understanding inference steps and argument structures. The works in [43, 13] provide dialectical proof procedures, while the works [47, 48] offer dialogue games (as a distributed mechanism) for âflatâ ABAs to determine sentence acceptance under (grounded/ admissible/ ideal) semantics. Although the works in [47, 48] are similar to our idea of using dialogue and tree, these approaches do not generalize to n-ary conflicts.
The existing studies are mostly restricted to (1) specific logic or have limitations in representation aspects, (2) AFs with binary conflicts, and (3) lack exhaustive explanations. This paper addresses the limitations by introducing a general framework that provides dialogue models as dialectical proof procedures for acceptance in structured argumentation. The following is a simple illustration of how our approach works in a university example.
**Example 1.1**
*Consider inconsistent knowledge about a university domain, in which we know that: lecturers $(\texttt{{Le}})$ and researchers $(\texttt{{Re}})$ are employers $(\texttt{{Em}})$ ; full professors $(\texttt{{FP}})$ are researchers; everyone who is a teaching assistant $(\texttt{{taOf}})$ of an undergraduate course $(\texttt{{UC}})$ is a teaching assistant $(\texttt{{TA}})$ ; everyone who teaches a course is a lecturer and everyone who teaches a graduate course $(\texttt{{GC}})$ is a full professor. However, teaching assistants can be neither researchers nor lecturers, which leads to inconsistency. We also know that an individual Victor apparently is or was a teaching assistant of the KD course $(\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}))$ , and the KD course is an undergraduate course $(\texttt{{UC}}(\texttt{{KD}}))$ . Additionally, Victor teaches either the KD course $(\texttt{{te}}(\texttt{{v}},\texttt{{KD}}))$ or the KR course $(\texttt{{te}}(\texttt{{v}},\texttt{{KR}}))$ , where the KR course is a graduate course $(\texttt{{GC}}(\texttt{{KR}}))$ . The KB $\mathcal{K}_{1}$ is modelled as follows:
| | $\displaystyle\mathcal{F}_{1}=$ | $\displaystyle\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\ \texttt{{te}}( \texttt{{v}},\texttt{{KD}}),\ \texttt{{UC}}(\texttt{{KD}}),\ \texttt{{te}}( \texttt{{v}},\texttt{{KR}}),\ \texttt{{GC}}(\texttt{{KR}})\}$ | |
| --- | --- | --- | --- |
When a user asks â Is Victor a researcher? â, the answer will be â Yes, but Victor is possibly a researcher â. The current method [18, 17, 22] will provide a set-based explanation consisting of (1) the cause $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}}),\ \texttt{{GC}}(\texttt{{KR}})\}$ entailing the answer (why the answer is accepted) and (2) the conflict $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\texttt{{UC}}(\texttt{{KD}})\}$ being inconsistent with every cause (why the answer cannot be accepted). The cause, though, does not show a series of reasoning steps to reach $\texttt{{Re}}(\texttt{{v}})$ from the justification $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}}),\ \texttt{{GC}}(\texttt{{KR}})\}$ . The conflict still lacks all relevant information to explain this result. Indeed, in the KB, the fact $\texttt{{te}}(\texttt{{v}},\texttt{{KD}})$ deducing $\texttt{{Le}}(\texttt{{v}})$ makes the conflict $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\texttt{{UC}}(\texttt{{KD}})\}$ deducing $\texttt{{TA}}(\texttt{{v}})$ uncertain, due to the constraint that lecturers cannot be teaching assistants. Thus, using the conflict in the explanation is insufficient to assert the non-acceptance of the answer. It remains unclear why the answer is possible. Instead, $\texttt{{te}}(\texttt{{v}},\texttt{{KD}})$ deducing $\texttt{{Le}}(\texttt{{v}})$ should be included in the explanation. Without knowing the relevant information, it is impossible for the user - especially non-experts in logic - to understand why this is the case. However, using the argumentation approach will provide a dialogical explanation that is more informative and intuitive. The idea involves a dialogue between a proponent and opponent, where they exchange logical formulas to a dispute agree. The proponent aims to prove that the argument in question is acceptable, while the opponent exhaustively challenges the proponentâs moves. The dialogue where the proponent wins represents a proof that the argument in question is accepted. The dialogue whose graphical representation is shown in Figure 4 proceeds as follows: 1. Suppose that the proponent wants to defend their claim $\texttt{{Re}}(\texttt{{v}})$ . They can do so by putting forward an argument, say $A_{1}$ , supported by facts $\texttt{{te}}(\texttt{{v}},\texttt{{KR}})$ and $\texttt{{GC}}(\texttt{{KR}})$ :
| | $\displaystyle A_{1}:\$ | $\displaystyle\texttt{{Re}}(\texttt{{v}})(\text{by }r_{3})$ | |
| --- | --- | --- | --- | 2. The opponent challenges the proponentâs argument by attacking the claim $\texttt{{Re}}(\texttt{{v}})$ with an argument $\texttt{{TA}}(\texttt{{v}})$ , say $A_{2}$ , supported by facts $\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}})$ and $\texttt{{UC}}(\texttt{{KD}})$ :
| | $\displaystyle A_{2}:\$ | $\displaystyle\texttt{{TA}}(\texttt{{v}})(\text{by }r_{4})$ | |
| --- | --- | --- | --- | 3. To argue that the opponentâs attack is not possible - and to further defend the initial claim $\texttt{{Re}}(\texttt{{v}})$ - the proponent can counter the opponentâs argument by providing additional evidence $\texttt{{Le}}(\texttt{{v}})$ supported by a fact $\texttt{{te}}(\texttt{{v}},\texttt{{KD}})$ :
| | $\displaystyle A_{3}:\$ | $\displaystyle\texttt{{Le}}(\texttt{{v}})(\text{by }r_{5})$ | |
| --- | --- | --- | --- | 4. The opponent concedes $\texttt{{Re}}(\texttt{{v}})$ since it has no argument to argue the proponent.
| | Opponent: | I concede that v is a researcher because I have no argument to argue that v is | |
| --- | --- | --- | --- |
The proponentâs belief $\texttt{{Re}}(\texttt{{v}})$ is defended successfully, namely, $\texttt{{Re}}(\texttt{{v}})$ that is justified by facts $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}})$ , $\texttt{{GC}}(\texttt{{KR}})\}$ that be extended to be the defending set $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}})$ , $\texttt{{GC}}(\texttt{{KR}})$ , $\texttt{{te}}(\texttt{{v}},\texttt{{KD}})\}$ that can counter-attack every attack. By the same line of reasoning, the opponent can similarly defend their belief in the contrary statement $\texttt{{TA}}(\texttt{{v}})$ based on the defending set $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\texttt{{UC}}(\texttt{{KD}})\}$ . Because different agents can hold contrary claims, the acceptance semantics of the answer can be considered credulous rather than sceptical. In other words, the answer is deemed possible rather than plausible. Thus, the derived system can conclude that v is possibly a researcher.*
The main contributions of this paper are the following:
- We propose a proof-oriented (logical) argumentation framework with collective attacks (P-SAF), in which we consider abstract logic to generalize monotonic and non-monotonic logics involving reasoning with maximal consistent subsets, and we show how any such logic can be translated to P-SAFs. We also conduct a detailed investigation of how existing argumentation frameworks in the literature can be instantiated as P-SAFs. Thus, we demonstrate that the P-SAF framework is sufficiently generic to encode n-ary conflicts and to enable logical reasoning with (inconsistent) KBs.
- We introduce a novel explanatory dialogue model viewed as a dialectical proof procedure to compute and explain the credulous, grounded and sceptical acceptances in P-SAFs. The dialogues, in this sense, can be regarded as explanations for the acceptances. As our main theoretical result, we prove the soundness and completeness of the dialogue model wrt argumentation semantics.
- This novel explanatory dialogue model provides dialogical explanations for the acceptance of a given query wrt inconsistency-tolerant semantics, and dialogue trees as graphical representations of the dialogical explanations. Based on these dialogical explanations, our framework assists in understanding the intermediate steps of a reasoning process and enhancing human communication on logical reasoning with inconsistencies.
## 2. Preliminaries
To motivate our work, we review argumentation approaches using Tarski abstract logic characterized by a consequence operator [71]. However, many logic in argumentation systems, like ABA or ASPIC systems, do not always impose certain axioms, such as the absurdity axiom. Defining the consequence operator by means of âmodelsâ cannot allow users to understand reasoning progresses better, as inference rule steps are implicit. These motivate a slight generalization of consequence operators in a proof-theoretic manner, inspired by [72], with minimal properties.
Most of our discussion applies to abstract logics (monotonic and non-monotonic) which slightly generalize Tarski abstract logic. Let $\mathcal{L}$ be a set of well-formed formulas, or simply formulas, and $X$ be an arbitrary set of formulas in $\mathcal{L}$ . With the help of inference rules, new formulas are derived from $X$ ; these formulas are called logical consequences of $X$ ; a consequence operator (called closure operator) returns the logical consequences of a set of formulas.
**Definition 2.1**
*We define a map $\texttt{{CN}}:2^{\mathcal{L}}\to 2^{\mathcal{L}}$ such that $\overline{\texttt{{CN}}}(X)=\bigcup_{n\geq 0}\texttt{{CN}}^{n}(X)$ satisfies the axioms:
- ( $A_{1}$ ) Expansion $X\subseteq\overline{\texttt{{CN}}}(X)$ .
- ( $A_{2}$ ) Idempotence $\overline{\texttt{{CN}}}(\overline{\texttt{{CN}}}(X))=\overline{\texttt{{CN}}} (X)$ .*
In general, a map $2^{\mathcal{L}}\to 2^{\mathcal{L}}$ satisfying these axioms $A_{1}-\ A_{2}$ is called a consequence operator. Other properties that consequence operators might have, but that we do not require in this paper, are
- ( $A_{3}$ ) Finiteness $\overline{\texttt{{CN}}}(X)\subseteq\bigcup\{\overline{\texttt{{CN}}}(Y)\mid Y \subset_{f}X\}$ where the notation $Y\subset_{f}X$ means that $Y$ is a finite proper subset of $X$ .
- ( $A_{4}$ ) Coherence $\overline{\texttt{{CN}}}(\emptyset)\neq\mathcal{L}$ .
- ( $A_{5}$ ) Absurdity $\overline{\texttt{{CN}}}(\{x\})=\mathcal{L}$ for some $x$ in the language $\mathcal{L}$ .
Note that finiteness is essential for practical reasoning and is satisfied by any logic that has a decent proof system.
An abstract logic includes a pair $\mathcal{L}$ and a consequence operator CN. Different logics have consequence operators with various properties that can satisfy certain axioms. For instance, the class of Tarskian logics, such as classical logic, is defined by a consequence operator satisfying $A_{1}-\ A_{5}$ while the one of defeasible logic satisfies $A_{1}-\ A_{3}$ .
**Example 2.2**
*An inference rule $r$ in first-order logic is of the form $\frac{p_{1},\ldots,p_{n}}{c}$ where its conclusion is $c$ and the premises are $p_{1},\ldots,p_{n}$ . $c$ is called a direct consequence of $p_{1},\ldots,p_{n}$ by virtue of $r$ . If we define $\texttt{{CN}}(X)$ as the set of direct consequences of $X\subseteq\mathcal{L}$ , then $\overline{\texttt{{CN}}}$ coincides with $\overline{\texttt{{CN}}}(X)=\{\alpha\in\mathcal{L}\mid X\vdash\alpha\}$ and satisfies the axioms $A_{1}-\ A_{5}$ .*
Fix a logic $(\mathcal{L},\texttt{{CN}})$ and a set of formulas $X\subseteq\mathcal{L}$ . We say that:
- $X$ is consistent wrt $(\mathcal{L},\texttt{{CN}})$ iff $\overline{\texttt{{CN}}}(X)\neq\mathcal{L}$ . It is inconsistent otherwise;
- $X$ is a minimal conflict of $\mathcal{K}$ if $X^{\prime}\subsetneq X$ implies $X^{\prime}$ is consistent.
- A knowledge base (KB) is any subset $\mathcal{K}$ of $\mathcal{L}$ . Formulas in a KB are called facts. A knowledge base may be inconsistent.
Reasoning in inconsistent KBs $\mathcal{K}\subseteq\mathcal{L}$ amounts to:
1. Constructing maximal consistent subsets,
1. Applying classical entailment mechanism on a choice of the maximal consistent subsets.
Motivated by this idea, we give the following definition.
**Definition 2.3**
*Let $\mathcal{K}$ be a KB and $X\subseteq\mathcal{K}$ be a set of formulas. $X$ is a maximal (for set-inclusion) consistent subsets of $\mathcal{K}$ iff
- $X$ is consistent,
- there is no $X^{\prime}$ such that $X\subset X^{\prime}$ and $X^{\prime}$ is consistent.
We denote the set of all maximal consistent subsets by $\texttt{{MCS}}(\mathcal{K})$ .*
Inconsistency-tolerant semantics allow us to determine different types of entailments.
**Definition 2.4**
*Let $\mathcal{K}$ be a KB. A formula $\phi\in\mathcal{L}$ is entailed in
- some maximal consistent subset iff for some $\Delta\in\texttt{{MCS}}(\mathcal{K})$ , $\phi\in\overline{\texttt{{CN}}}(\Delta)$ ;
- the intersection of all maximal consistent subsets iff for $\Psi=\bigcap\{\Delta\mid\Delta\in\texttt{{MCS}}(\mathcal{K})\}$ , $\phi\in\overline{\texttt{{CN}}}(\Psi)$ ;
- all maximal consistent subsets iff for all $\Delta\in\texttt{{MCS}}(\mathcal{K})$ , $\phi\in\overline{\texttt{{CN}}}(\Delta)$ .*
Informally, some maximal consistent subset semantics refers to possible answers, all maximal consistent subsets semantics to plausible answers, and the intersection of all maximal consistent subsets semantics to surest answers.
In the following subsections, we illustrate the generality of the above definition by providing instantiations for propositional logic, defeasible logic, $\text{Datalog}^{\pm}$ . Table 1 summarizes properties holding for consequence operators of the instantiations.
| $A_{1}$ $A_{2}$ $A_{3}$ | $\times$ $\times$ $\times$ | $\times$ $\times$ $\times$ | $\times$ $\times$ $\times$ | $\times$ $\times$ $\times$ | $\times$ $\times$ |
| --- | --- | --- | --- | --- | --- |
| $A_{4}$ | $\times$ | $\times$ | | | |
| $A_{5}$ | $\times$ | $\times$ | | | |
Table 1. Properties of consequence operators of the instantiations
### 2.1. Classical Logic
We assume familiarity with classical logic. A logical language for classical logic $\mathcal{L}$ is a set of well-formed formulas. Let us define $\texttt{{CN}}_{c}:2^{\mathcal{L}_{c}}\to 2^{\mathcal{L}_{c}}$ as follows: For $X\subseteq\mathcal{L}_{c}$ , a formula $x\in\mathcal{L}_{c}$ satisfies $x\in\texttt{{CN}}_{c}(X)$ iff the inference rule $\frac{y}{x}$ is applied to $X$ such that $y\in X$ . Define $\overline{\texttt{{CN}}}_{c}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{c}^{n}(X)$ . In particular, $\overline{\texttt{{CN}}}_{c}$ is a consequence operator satisfying $A_{1}-\ A_{5}$ . Examples of classical logic are propositional logic and first-order logic. Next, we will consider propositional logic as being given by our abstract notions. Since first-order logic can be similarly simulated, we do not consider here in detail.
We next present propositional logic as a special case of classical logic. Let $A$ be a set of propositional atoms. Any atoms $a\in A$ is a well-formed formula wrt. $A$ . If $\phi$ and $\alpha$ are well-formed formulas wrt. $A$ then $\neg\phi$ , $\phi\wedge\alpha$ , $\phi\vee\alpha$ are well-formulas wrt. $A$ (we also assume that the usual abbreviations $\supset$ , $\leftrightarrow$ are defined accordingly). Then $\mathcal{L}_{p}$ is the set of well-formed formulas wrt. $A$ .
Let $\texttt{{CN}}_{p}:2^{\mathcal{L}_{p}}\to 2^{\mathcal{L}_{p}}$ be defined as follows: for $X\subseteq\mathcal{L}_{p}$ , an element $x\in\mathcal{L}_{p}$ satisfies $x\in\texttt{{CN}}_{p}(X)$ iff there are $y_{1},\ldots,y_{j}\in X$ such that $x$ can be obtained from $y_{1},\ldots,y_{j}$ by the application of a single inference rule of propositional logic.
**Example 2.5**
*Consider the propositional atoms $A_{1}=\{x,y\}$ and the knowledge base $\mathcal{K}_{1}=\{x,y,x\supset\neg y\}\subseteq\mathcal{L}_{p}$ . Consider a set $\{x,x\supset\neg y\}\subseteq\mathcal{K}_{1}$ . If the inference rule (modus ponens) $\frac{A,A\supset B}{B}$ is applied to this set, then $\texttt{{CN}}_{p}(\{x,x\supset\neg y\})=\{x,x\supset\neg y,\neg y\}$ .*
Consider $\overline{\texttt{{CN}}}_{p}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{p}^{n}(X)$ . For instance, $\overline{\texttt{{CN}}}_{p}(\mathcal{K}_{1})=\{x,y,x\supset\neg y,\neg y,x \wedge y,\ldots\}$ . Since propositional logic is coherent and complete, then $x\in\overline{\texttt{{CN}}}_{p}(X)=\{x\mid X\models x\}$ where $\models$ is the entailment relation, i.e., $\phi\models\alpha$ if all models of $\phi$ are models of $\alpha$ in the propositional semantics. In particular, $\overline{\texttt{{CN}}}_{p}$ is a consequence operator satisfying $A_{1}-\ A_{5}$ . The propositional logic can be defined as $(\mathcal{L}_{p},\texttt{{CN}}_{p})$ .
It follows immediately
**Lemma 2.6**
*$(\mathcal{L}_{p},\texttt{{CN}}_{p})$ is an abstract logic.*
**Example 2.7 (Continue Example2.5)**
*Recall $\mathcal{K}_{1}$ . The KB admits a MCS: $\{x,y,x\supset\neg y\}$ .*
### 2.2. Defeasible Logic
Let $(\mathcal{L}_{d},\texttt{{CN}}_{d})$ be a defeasible logic such as used in defeasible logic programming [45], assumption-based argumentation (ABA) [44], ASPIC/ ASPIC+ systems [46, 62]. The language for defeasible logic $\mathcal{L}_{d}$ includes a set of (strict and defeasible) rules and a set of literals. The rules is the form of $x_{1},\ldots x_{i}\rightarrow_{s}x_{i+1}$ ( $x_{1},\ldots x_{i}\rightarrow_{d}x_{i+1}$ ) where $x_{1},\ldots x_{i},x_{i+1}$ are literals and $\rightarrow_{s}$ (denote strict rules) and $\rightarrow_{d}$ (denotes defeasible rules) are implication symbols.
**Definition 2.8**
*Define $\texttt{{CN}}_{d}:2^{\mathcal{L}_{d}}\to 2^{\mathcal{L}_{d}}$ as follows: for $X\subseteq\mathcal{L}_{d}$ , a formula $x\in\mathcal{L}_{d}$ satisfies $x\in\texttt{{CN}}_{d}(X)$ iff at least of the following properties is true:
1. $x$ is a literal in $X$ ,
1. there is $(y_{1},\ldots,y_{j})\rightarrow_{s}x\in X$ , or $(y_{1},\ldots,y_{j})\rightarrow_{d}x\in X$ st. $\{y_{1},\ldots,y_{j}\}\subseteq X$ .
Define $\overline{\texttt{{CN}}}_{d}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{d}^{n}(X)$ .*
**Remark 2.9**
*One can describe $\overline{\texttt{{CN}}}_{d}$ explicitly. We have $x\in\overline{\texttt{{CN}}}_{d}(X)$ iff there exists a finite sequence of literals $x_{1},\ldots,x_{n}$ such that
1. $x$ is $x_{n}$ , and
1. for each $x_{i}\in\{x_{1},\ldots,x_{n}\}$ ,
- there is $y_{1},\ldots,y_{j}\rightarrow_{s}x_{i}\in X$ , or $y_{1},\ldots,y_{j}\rightarrow_{d}x_{i}\in X$ , such that $\{y_{1},\ldots,y_{j}\}\subseteq\{x_{1},\ldots,x_{i-1}\}$ ,
- or $x_{i}$ is a literal in $X$ . Note that if $x\in\texttt{{CN}}_{d}^{n}(X)$ , the above sequence $x_{1},\ldots,x_{n}$ might have length $m\neq n$ : intuitively $n$ is the depth of the proof tree while $m$ is the number of nodes.*
**Example 2.10**
*Consider the KB $\mathcal{K}_{2}=\{x,x\rightarrow_{s}y,t\rightarrow_{d}z\}\subseteq\mathcal{L}_ {d}$ . $\overline{\texttt{{CN}}}_{d}(\mathcal{K}_{2})=\{x,y\}$ where the sequence of literals in the derivation is $x,y$ . The KB admits a MCS: $\{x,x\rightarrow_{s}y,t\rightarrow_{d}z\}$*
**Remark 2.11**
*For ASPIC/ASPIC+ systems [46, 62], Prakken claimed that strict and defeasible rules can be considered in two ways: (1) they encode information of the knowledge base, in which case they are part of the logical language $\mathcal{L}_{d}$ , (2) they represent inference rules, in which case they are part of the consequence operator. These ways can encoded by consequence operators as in [61]. Our definition of $\overline{\texttt{{CN}}}_{d}$ can align with the later interpretation as done in [61]. In particular, if we consider $X$ being a set of literals of $\mathcal{L}_{d}$ instead of being a set of literals and rules as above, the definitions of $\texttt{{CN}}_{d}$ and $\overline{\texttt{{CN}}}_{d}$ still hold for this case. Thus, the defeasible logic of ASPIC/ASPIC+ can be represented by the logic $(\mathcal{L}_{d},\texttt{{CN}}_{d})$ in our settings.*
**Proposition 2.12 ([61])**
*$\overline{\texttt{{CN}}}_{d}$ satisfies $A_{1}-\ A_{3}$ .*
It follows immediately
**Lemma 2.13**
*$(\mathcal{L}_{d},\texttt{{CN}}_{d})$ is an abstract logic.*
In [64], proposals for argumentation using defeasible logic were criticized for violating the postulates that they proposed for acceptable argumentation. One solution is to introduce contraposition into the reasoning of the underlying logic. This solution can be seen as another representation of defeasible logic. We introduce contraposition by defining a consequence operator as follows:
Consider $\mathcal{L}_{co}$ containing a set of literal and a set of (strict and defeasible) rules $\mathcal{R}_{s}$ ( $\mathcal{R}_{d})$ . For this case represent inference rules, namely, they are part of a consequence operator. For $\Delta\subseteq\mathcal{L}_{co}$ , $\texttt{Contrapositives}(\Delta)$ is the set of contrapositives formed from the rules in $\Delta$ . For instance, a strict rule $s$ is a contraposition of the rule $\phi_{1},\ldots,\phi_{n}\rightarrow_{s}\alpha\in\mathcal{R}_{s}$ iff $s=\phi_{1},\ldots,\phi_{i-1},\neg\alpha,\phi_{i+1},\ldots,\phi_{n}\rightarrow_ {s}\neg\phi_{i}$ for $1\leq i\leq n$ .
**Definition 2.14**
*Define $\texttt{{CN}}_{co}:2^{\mathcal{L}_{co}}\to 2^{\mathcal{L}_{co}}$ as follows: for a set of literals $X\subseteq\mathcal{L}_{co}$ , a formula $x\in\mathcal{L}_{co}$ satisfies $x\in\texttt{{CN}}_{co}(X)$ iff at least of the following properties is true:
1. $x$ is a literal in $X$ ,
1. there is $(y_{1},\ldots,y_{j})\rightarrow_{s}x\in\mathcal{R}_{s}\cup\texttt{ { Contrapositives}}(\mathcal{R}_{s})$ , or $(y_{1},\ldots,y_{j})\rightarrow_{d}x\in\mathcal{R}_{d}\cup\texttt{{ Contrapositives}}(\mathcal{R}_{d})$ such that $\{y_{1},\ldots,y_{j}\}\subseteq X$ .
Define $\overline{\texttt{{CN}}}_{co}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{co}^{n}(X)$ .*
**Remark 2.15**
*Similarly, one can represent $\overline{\texttt{{CN}}}_{co}$ as follows: $x\in\overline{\texttt{{CN}}}_{co}(X)$ iff there exists a sequence of literals $x_{1},\ldots,x_{n}$ such that
1. $x$ is $x_{n}$ , and
1. for each $x_{i}\in\{x_{1},\ldots,x_{n}\}$ ,
- there is $y_{1},\ldots,y_{j}\rightarrow_{s}x_{i}\in\mathcal{R}_{s}\cup\texttt{{ Contrapositives}}(\mathcal{R}_{s})$ , or $y_{1},\ldots,y_{j}\rightarrow_{d}x_{i}\in\mathcal{R}_{d}\cup\texttt{{ Contrapositives}}(\mathcal{R}_{d})$ , such that $\{y_{1},\ldots,y_{j}\}\subseteq\{x_{1},\ldots,x_{i-1}\}$ ,
- or $x_{i}$ is a literal in $X$ .*
**Proposition 2.16**
*$(\mathcal{L}_{co},\texttt{{CN}}_{co})$ is an abstract logic. $\overline{\texttt{{CN}}}_{co}$ satisfies $A_{1}-\ A_{3}$ .*
**Example 2.17**
*Consider $\mathcal{K}_{3}=\{q,\neg r,p\wedge q\rightarrow_{d}r,\neg p\rightarrow_{s}u\}$ , $\texttt{{Contrapositives}}(\mathcal{K}_{3})=\{\neg r\wedge q\rightarrow_{d} \neg p,\neg r\wedge p\rightarrow_{d}\neg q,\neg u\rightarrow_{s}p\}$ . Then $\overline{\texttt{{CN}}}_{co}(\mathcal{K}_{3})=\{q,\neg r,\neg p,u\}$ where the sequence of literals in the derivation is $q,\neg r,\neg p,u$ . The KB admits MCSs: $\{q,\neg r,\neg p\rightarrow_{s}u\}$ and $\{q,p\wedge q\rightarrow_{d}r,\neg p\rightarrow_{s}u\}$ .*
### 2.3. $\text{Datalog}^{\pm}$
We consider $\text{Datalog}^{\pm}$ [26], and shall use it to illustrate our demonstrations through the paper.
We assume a set $\mathsf{N_{t}}$ of terms which contain variables, constants and function terms. An atom is of the form $P(\vec{t})$ , with $P$ a predicate name and $\vec{t}$ a vector of terms, which is ground if it contains no variables. A database is a finite set of ground atoms (called facts). A tuple-generating dependency (TGD) $\sigma$ is a first-order formula of the form $\forall\vec{x}\forall\vec{y}\phi(\vec{x},\vec{y})\rightarrow\exists\vec{z}\psi (\vec{x},\vec{z})$ , where $\phi(\vec{x},\vec{y})$ and $\psi(\vec{x},\vec{z})$ are non-empty conjunctions of atoms. We leave out the universal quantification, and refer to $\phi(\vec{x},\vec{y})$ and $\psi(\vec{x},\vec{z})$ as the body ad head of $\sigma$ . A negative constraint (NC) $\delta$ is a rule of the form $\forall\vec{x}$ $\phi(\vec{x})\rightarrow\bot$ where $\phi(\vec{x})$ is a conjunction of atoms. We may leave out the universal restriction. A language for $\text{Datalog}^{\pm}$ $\mathcal{L}_{da}$ includes a set of facts and a set of TGDs and NCs. A knowledge base $\mathcal{K}$ of $\mathcal{L}_{da}$ is now a tuple $(\mathcal{F},\mathcal{R},\mathcal{C})$ where a database $\mathcal{F}$ , a set $\mathcal{R}$ of TGDs and a set $\mathcal{C}$ of NCs.
Define $\texttt{{CN}}_{da}:2^{\mathcal{L}_{da}}\to 2^{\mathcal{L}_{da}}$ as follows: Let $X$ be a set of facts of $\mathcal{L}_{da}$ , an element $x\in\mathcal{L}_{da}$ satisfies $x\in\texttt{{CN}}_{da}(X)$ iff there are $y_{1},\ldots,y_{j}\in X$ s.t. $x$ can be obtained from $y_{1},\ldots,y_{j}$ by the application of a single inference rule. Note that we treat such TGDs and NCs as inference rules.
Consider $\overline{\texttt{{CN}}}_{da}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{da}^{n}(X)$ . Similar to proposition logic, $x\in\overline{\texttt{{CN}}}_{da}(X)=\{x\mid X\models x\}$ where $\models$ is the entailment of first-order formulas, i.e., $X\models x$ holds iff every model of all elements in $X$ is also a model of $x$ . $\overline{\texttt{{CN}}}_{da}$ satisfies the properties $A_{1},A_{2}$ . Note that the finiteness property ( $A_{3}$ ) still holds for some fragments of $\text{Datalog}^{\pm}$ , such as guarded, weakly guarded $\text{Datalog}^{\pm}$ .
It follows immediately
**Lemma 2.18**
*$(\mathcal{L}_{da},\texttt{{CN}}_{da})$ is an abstract logic.*
**Example 2.19 (Continue Example1.1)**
*Recall $\mathcal{K}_{1}$ . The KB admits MSCs (called repairs in $\text{Datalog}^{\pm}$ ):
| | $\displaystyle\mathcal{B}_{1}=\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}), \texttt{{UC}}(\texttt{{KD}})\}\quad\mathcal{B}_{3}=\{\texttt{{taOf}}(\texttt{{ v}},\texttt{{KD}}),\texttt{{te}}(\texttt{{v}},\texttt{{KR}}),\texttt{{te}}( \texttt{{v}},\texttt{{KD}}),\texttt{{GC}}(\texttt{{KR}})\}$ | |
| --- | --- | --- |
Consider $q_{1}=\texttt{{Re}}(\texttt{{v}})$ . We have that v is a possible answer for $q_{1}$ since $q_{1}$ is entailed in some repairs, such as $\mathcal{B}_{2},\ \mathcal{B}_{3},\ \mathcal{B}_{5}$ .*
## 3. Proof-oriented (Logical) Argumentations
In this section, we present proof-oriented (logical) argumentations (P-SAFs) and their ingredients. We also provide insights into the connections between our framework and state-of-the-art argumentation frameworks. We then show the close relations of reasoning with P-SAFs to reasoning with MCSs.
### 3.1. Arguments, Collective Attacks and Proof-oriented Argumentations
Logical arguments (arguments for short) built from a KB may be defined in different ways. For instance, arguments are represented by the notion of sequents [69], proof [41, 44], a pair of $(\Gamma,\ \psi)$ where $\Gamma$ is the support, or premises, or assumptions of the argument, and $\psi$ is the claim, or conclusion, of the argument [7, 33]. To improve explanations in terms of representation and understanding, we choose the form of proof to represent arguments. The proof is in the form of a tree.
**Definition 3.1**
*A formula $\phi\in\mathcal{L}$ is tree-derivable from a set of fact-premises $H\subseteq\mathcal{K}$ if there is a tree such that
- the root holds $\phi$ ;
- $H$ is the set of formulas held by leaves;
- for every inner node $N$ , if $N$ holds the formula $\beta_{0}$ , then its successors hold $n$ formulas $\beta_{1},\ldots,\beta_{n}$ such that $\beta_{0}\in\texttt{{CN}}(\{\beta_{1},\ldots,\beta_{n}\})$ .
If such a tree exists (it might not be unique), we call $A:H\Rightarrow\phi$ an argument with the support set $\texttt{{Sup}}(A)=H$ and the conclusion $\texttt{{Con}}(A)=\phi$ . We denote the set of arguments induced from $\mathcal{K}$ by $\texttt{{Arg}}_{\mathcal{K}}$ .*
**Remark 3.2**
*By Definition 3.1 it follows that $H\Rightarrow\phi$ is an argument iff $\phi\in\overline{\texttt{{CN}}}(H)$ .*
Note that an individual argument can be represented by several different trees (with the same root and leaves). We assume these trees represent the same arguments; otherwise, we could have infinitely many arguments with the same support set and conclusion.
Intuitively, a tree represents a possible derivation of the formula at its root and the fact-premise made at its leaves. The leaves of the tree, constituting the fact-premise, belong to $H=\texttt{{CN}}^{0}(H)$ . If a node $\beta$ has children nodes $\beta_{a_{1}}\in\texttt{{CN}}^{i_{1}}(H)$ , âŠ, $\beta_{a_{k}}\in\texttt{{CN}}^{i_{k}}(H)$ , then $\beta\in\texttt{{CN}}^{i+1}(X)$ where $i=\max\{i_{1},\ldots,i_{k}\}$ because by the extension property $\texttt{{CN}}^{i_{1}}(H),\ldots,\texttt{{CN}}^{i_{k}}(H)\subseteq\texttt{{CN}} ^{i}(H)$ . The root $\phi$ , constituting the conclusion, belongs to $\texttt{{CN}}^{n}(H)$ , where $n$ is the longest path from leaf to root. Note that, by the extension property, if $\beta\in\texttt{{CN}}^{i}(H)$ , then also $\beta\in\texttt{{CN}}^{i+1}(H)$ , $\beta\in\texttt{{CN}}^{i+2}(H)$ , âŠ. The idea is to have $i$ in $\texttt{{CN}}^{i}(H)$ as small as possible (we donât want to argue longer than necessary).
Some proposals for logic-based argumentation stipulate additionally that the argumentâs support is consistent and/or that none of its subsets entails the argumentâs conclusion (see [56]). However, such restrictions, i.e., minimality and consistency, are not substantial (although required for some specific logics). In some proposals, the requirement that the support of an argument is consistent may be irrelevant for some logics, especially when consistency is defined by satisfiability. For instance, in Priestâs three-valued logic [57] or Belnapâs four-valued logic [58], every set of formulas in the language of $\{\neg,\vee,\wedge\}$ is satisfiable. In frameworks in which the supports of arguments are represented only by literals (atomic formulas or their negation), arguments like $A=\{a,b\}\Rightarrow a\vee b$ are excluded since their supports are not minimal, although one may consider $\{a,b\}$ a stronger support for $a\vee b$ than, say, $\{a\}$ , since the set $\{a,b\}$ logically implies every minimal support of $a\vee b$ . To keep our framework as general as possible, we do not consider the extra restrictions for our definition of arguments (See [56, 69] for further justifications of this choice).
We present instantiations to show the generality of Definition 3.1 for generating arguments in argumentation systems in the literature.
- We start with deductive argumentation that uses classical logic. In [59], arguments as pairs of premises and conclusions can be simulated in our settings, and for which $H\Rightarrow\phi$ is an argument (in the form of tree-derivations), where $H\subseteq\mathcal{L}_{c}$ and $\phi\in\mathcal{L}_{c}$ iff $\phi\in\overline{\texttt{{CN}}}_{c}(H)$ , $H$ is minimal (i.e., there is no $H^{\prime}\subset H$ such that $\phi\in\overline{\texttt{{CN}}}_{c}(H^{\prime})$ ) and $H$ is consistent. For example, we use the propositional logic in Example 2.5, and the following is an argument in propositional logic $A:\{x,x\supset\neg y\}\Rightarrow\neg y$ . Tree-representation of $A$ is shown in Figure 1 (left). Similarly, since most Description Logics (DLs), such as $ALC$ , DL-Lite families, Horn DL, etc., are decidable fragments of first-order logic, it is straightforward to apply Definition 3.1 to encode arguments of the framework using the DL $ALC$ in [14].
- We consider defeasible logic approaches to argumentation, such as [44, 53, 67, 68, 45]. For defeasible logic programming [45], $H\Rightarrow\phi$ is an argument (in the form of tree-derivations) iff $\phi\in\overline{\texttt{{CN}}}_{d}(H)$ and there is no $H^{\prime}\subset H$ such that $\phi\in\overline{\texttt{{CN}}}_{d}(H^{\prime})$ and it is not the case that there is $\alpha$ such that $\alpha\in\overline{\texttt{{CN}}}_{d}(H)$ and $\neg\alpha\in\overline{\texttt{{CN}}}_{d}(H)$ (i.e. $H$ is a minimal consistent set entailing $\phi$ ).
For â flat â- ABA [44, 53], assume that $\texttt{{CN}}_{d}$ ignores differences between various implication symbols in the knowledge base, and for which $H\Rightarrow\phi$ is an argument iff $\phi\in\overline{\texttt{{CN}}}_{d}(H)$ where $H\subseteq\mathcal{L}_{d}$ . In this case, the argument, from the support $H$ to the conclusion $\phi$ , can be described as tree-derivations by $\texttt{{CN}}_{d}$ . Note that the minimality and consistency requirements are dropped. Similarly, in ânon-flatâ - ABAs [67, 68], arguments as tree-derivations can be simulated in our setting.
Note, in [45] only the defeasible rules are represented in the support of the argument, and in [44, 53, 67, 68] only the literals are represented in the support of the argument, but in both cases it is a trivial change (as we do here) to represent both the rules and literals used in the derivation in the support of the argument.
**Example 3.3**
*For $\mathcal{K}_{5}=\{a,\neg b,a\rightarrow_{s}\neg c,\ \neg b\wedge\neg c \rightarrow_{d}s,\ s\rightarrow_{s}t,\ a\wedge t\rightarrow_{d}u\}$ , the following is an argument in defeasible logic programming $B:\{a,\neg b,a\rightarrow_{s}\neg c,\neg b\wedge\neg c\rightarrow_{d}s\}\Rightarrow s$ with the sequences of literals $a,\neg c,\neg b,s$ . Tree-representations of the arguments are shown in Figure 1 (middle). For $\mathcal{K}_{6}=\{p,\neg q,s,p\rightarrow\neg r,\neg q\wedge\neg r\wedge s \rightarrow t,t\wedge p\rightarrow u,v\}$ , the following is an argument in ABA $C:\{p,\neg q,s,p\rightarrow\neg r,\neg q\wedge\neg r\wedge s\rightarrow t\}\Rightarrow t$ .*
- We translate ASPIC/ ASPIC+ [46, 62] into our work as follows:
We have considered the underlying logic of ASPIC/ ASPIC+ as being given by $\overline{\texttt{{CN}}}_{d}$ (see Remark 2.11) and $\mathcal{L}_{d}$ including the set of literals and strict/ defeasible rules.
We recall argument of the form $A_{1},\ldots,A_{n}\rightarrow_{s}/\rightarrow_{d}\phi$ in these systems as follows:
1. Rules of the form $\rightarrow_{s}/\rightarrow_{d}\alpha$ , are arguments with conclusion $\alpha$ .
1. Let $r$ be a strict/defeasible rule of the form $\beta_{1},\ldots,\beta_{n}\rightarrow_{s}/\rightarrow_{d}\phi$ , $n\geq 0$ . Further suppose that $A_{1},\ldots,A_{n}$ , $n\geq 0$ , are arguments with conclusions $\beta_{1},\ldots,\beta_{n}$ respectively. Then $A_{1},\ldots,A_{n}\rightarrow_{s}/\rightarrow_{d}\phi$ is an argument with conclusion $\phi$ and last rule $r$ .
1. Every argument is constructed by applying finitely many times the above two steps.
The arguments of the form $A_{1},\ldots,A_{n}\rightarrow_{s}/\rightarrow_{d}\phi$ can be viewed as tree-derivations in the sense of Definition 3.1, in which the conclusion of the argument is $\phi$ ; the support $H$ of the argument is the set of leaves that are rules of the form $\rightarrow_{s}/\rightarrow_{d}\alpha_{i}$ such that $\alpha_{i}\in\texttt{{CN}}^{0}_{d}(H)$ . In this view, the root of the tree is labelled by $\phi$ such $\phi\in\texttt{{CN}}^{n}_{d}(H)$ ; the children $\beta_{i}$ , $i=1,\ldots,n$ , of the root are the roots of subtrees $A_{1},\ldots,A_{n}$ ; if $\phi\in\texttt{{CN}}^{n}_{d}(H)$ , then $\beta_{i}\in\texttt{{CN}}^{n-1}_{d}(H)$ . Since $\overline{\texttt{{CN}}}_{d}(H)=\bigcup_{n}\texttt{{CN}}^{n}_{d}(H)$ , it follows that $\phi\in\overline{\texttt{{CN}}}_{d}(H)$ . Note that if $n=0$ , the tree consists of just the root that is the rule of the form $\rightarrow_{s}/\rightarrow_{d}\phi$ .
- In argumentation framework for $\text{Datalog}^{\pm}$ [19, 61], arguments, viewed as pairs of the premises $H$ (i.e., the set of facts) and the conclusion $\phi$ (i.e., the derived fact), can be represented as tree-derivations in our definitions as follows: For a consistent set $H\subseteq\mathcal{F}$ and $\phi\in\mathcal{L}_{da}$ , $H\Rightarrow\phi$ is an argument in the sense of Definition 3.1 iff $\phi\in\overline{\texttt{{CN}}}_{da}(H)$ , in which $\phi$ is the root of the tree; $H$ are the leaves.
**Example 3.4**
*Let us continue Example 2.19, the following is an argument in the framework using $\text{Datalog}^{\pm}$ $A_{7}:\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\ \texttt{{UC}}(\texttt{{ KD}})\}\Rightarrow\texttt{{TA}}(\texttt{{v}})$ . By Definition 3.1, the argument can be viewed as a proof tree with the root labelled by $\texttt{{TA}}(\texttt{{v}})$ and the leaves labelled $\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\ \texttt{{UC}}(\texttt{{KD}})$ .*
<details>
<summary>x1.png Details</summary>
### Visual Description
\n
## Diagram: Set Relationship
### Overview
The image presents a diagram illustrating a set relationship using mathematical notation. It depicts a branching structure representing the relationship between different sets.
### Components/Axes
The diagram consists of three mathematical expressions connected by arrows, forming a branching structure. The expressions involve set membership notation ("â") and logical implication ("ÂŹ"). The sets are denoted as CNâ°(H), CNÂč(H), and the implication is represented as "x â ÂŹy".
### Detailed Analysis or Content Details
The diagram can be described as follows:
1. **Top Node:** ÂŹy â CNÂč(H) - This states that "not y" is an element of the set CNÂč(H).
2. **Left Branch:** x â CNâ°(H) - This states that "x" is an element of the set CNâ°(H). An arrow points from this expression to the top node.
3. **Right Branch:** x â ÂŹy â CNâ°(H) - This states that "if x then not y" is an element of the set CNâ°(H). An arrow points from this expression to the top node.
The arrow indicates a relationship where the elements in the lower branches contribute to or define the element in the top node.
### Key Observations
The diagram illustrates a logical relationship between sets and elements. The use of "ÂŹ" (not) and "â" (implication) suggests a conditional relationship. The sets CNâ°(H) and CNÂč(H) are likely defined elsewhere and represent specific mathematical spaces or collections.
### Interpretation
The diagram likely represents a condition or a proof step within a larger mathematical argument. It suggests that if 'x' is in CNâ°(H) or 'x implies not y' is in CNâ°(H), then 'not y' is in CNÂč(H). The diagram is a visual representation of a logical statement, potentially related to complex analysis or functional analysis, given the notation used. The sets CNâ°(H) and CNÂč(H) likely represent spaces of holomorphic functions, where the superscript indicates the order of the pole at a point 'H'. The diagram could be illustrating a property of these functions or a condition for their existence. Without further context, the precise meaning remains speculative, but the diagram clearly demonstrates a set-theoretic relationship involving logical implication.
</details>
<details>
<summary>x2.png Details</summary>
### Visual Description
\n
## Diagram: Logical Tree Structure
### Overview
The image depicts a tree-like diagram representing a logical structure or derivation. It shows a hierarchical breakdown of a statement 's' into its constituent parts, using logical operators and variables. The diagram appears to illustrate a proof or a logical implication.
### Components/Axes
The diagram consists of nodes connected by branches. The nodes contain logical expressions. The root node is labeled 's'. The branches represent logical dependencies or derivations. The diagram does not have traditional axes, but rather a top-down hierarchical structure.
### Detailed Analysis or Content Details
The diagram can be described as follows, starting from the root:
1. **Root Node:** 's'
2. **First Branch (Left):** From 's' branches to 'ÂŹc' (not c).
3. **Second Branch (Right):** From 's' branches to 'ÂŹb ⧠c â d' (not b and not c implies d).
4. **Sub-branch of 'ÂŹc':** From 'ÂŹc' branches to 'a'.
5. **Sub-branch of 'a':** From 'a' branches to 'a âs ÂŹc' (if a then s not c).
The expressions within the nodes are:
* s
* ÂŹc
* ÂŹb ⧠c â d
* a
* a âs ÂŹc
### Key Observations
The diagram shows a logical decomposition of 's' into two main components: 'ÂŹc' and 'ÂŹb ⧠c â d'. The 'ÂŹc' component is further broken down into 'a', which then leads to 'a âs ÂŹc'. The diagram suggests a conditional relationship between 'a' and 'ÂŹc' within the context of 's'.
### Interpretation
The diagram represents a logical argument or proof. The root 's' is the statement being proven or derived. The branches show how 's' can be broken down into simpler statements. The 'ÂŹb ⧠c â d' component suggests a conditional implication. The sub-branch involving 'a' and 'ÂŹc' indicates that 'a' is a condition for 'ÂŹc' to be true, within the larger context of 's'. The diagram is a visual representation of a logical deduction, showing the steps involved in deriving 's' from its constituent parts. It is a formal representation of a logical argument, likely used in mathematical logic or computer science. The 'âs' notation is unusual and may indicate a specific proof system or convention. It could mean "implies s" or "derived from s". Without further context, the precise meaning of 'âs' is ambiguous.
</details>
<details>
<summary>x3.png Details</summary>
### Visual Description
\n
## Diagram: Logical Decomposition
### Overview
The image presents a diagram illustrating a logical decomposition or derivation process. It appears to be a tree-like structure representing the breakdown of a logical statement into simpler components. The diagram uses logical symbols and annotations to show the relationships between these components.
### Components/Axes
The diagram consists of the following elements:
* **Top Node:** `p, p â q ~ q` (where â represents implication and ~ represents negation)
* **Left Branch:** `p ~ p, q`
* **Right Branch:** `p, q ~ q`
* **Bottom Left Node:** `p ~ p` with annotation `[Mon]`
* **Bottom Right Node:** `q ~ q` with annotation `[Mon]`
* **Connecting Label:** `[â~]` above the branches.
### Detailed Analysis or Content Details
The diagram shows a decomposition starting from the statement `p, p â q ~ q`. This statement is broken down into two branches:
1. **Left Branch:** `p ~ p, q`. This branch further decomposes into `p ~ p` annotated with `[Mon]`.
2. **Right Branch:** `p, q ~ q`. This branch decomposes into `q ~ q` annotated with `[Mon]`.
The label `[â~]` connects the top node to the two branches, indicating the rule or operation used for the decomposition. The annotations `[Mon]` at the bottom nodes likely refer to a specific logical property or rule (possibly monotonicity).
### Key Observations
* The diagram is symmetrical in its branching structure.
* The bottom nodes represent simpler statements than the top node.
* The annotations `[Mon]` suggest a focus on properties related to monotonicity in logic.
* The diagram does not contain numerical data or quantitative measurements.
### Interpretation
The diagram likely represents a proof or derivation in a formal logical system. The top node represents a starting point or hypothesis, and the branches show how this statement can be broken down into simpler, more fundamental statements. The annotations `[Mon]` and `[â~]` indicate the specific logical rules or properties being applied during the decomposition. The diagram suggests a process of simplification or reduction, where a complex statement is broken down into its constituent parts. The symmetry of the diagram might indicate a balanced or reversible process. The diagram is a visual representation of a logical argument, and its purpose is to demonstrate the validity of a particular inference or derivation.
The use of symbols like `â` (implication) and `~` (negation) indicates that the diagram is rooted in propositional logic. The annotations `[Mon]` suggest that the derivation is concerned with preserving certain properties of the logical statements, such as monotonicity (where adding premises does not remove conclusions).
Without further context, it's difficult to determine the specific logical system or the precise meaning of the annotations. However, the diagram provides a clear visual representation of a logical decomposition process.
</details>
Figure 1. Tree-representation for arguments wrt logics.
As shown in examples of [35, 61, 63], binary attacks, used in the literature [69, 19, 7, 14, 50], are not enough expressive to capture cases in which n-ary conflicts may arise. To overcome this limit, some argumentation frameworks introduced the notion of collective attacks to better capture non-binary conflicts, and so improve the decision making process in various conflicting situations. To ensure the generality of our framework, we introduce collective attacks.
**Definition 3.5 (Collective Attacks)**
*Let $A:\Gamma\Rightarrow\alpha$ be an argument and $\mathcal{X}\subseteq\texttt{{Arg}}_{\mathcal{K}}$ be a set of arguments such that $\bigcup_{X\in\mathcal{X}}\texttt{{Sup}}(X)$ is consistent. We say that
- $\mathcal{X}$ undercut-attacks $A$ iff there is $\Gamma^{\prime}\subseteq\Gamma$ s.t $\bigcup_{X\in\mathcal{X}}\{\texttt{{Con}}(X)\}\cup\Gamma^{\prime}$ is inconsistent.
- $\mathcal{X}$ rebuttal-attacks $A$ iff $\bigcup_{X\in\mathcal{X}}\{\texttt{{Con}}(X)\}\cup\{\alpha\}$ is inconsistent.
We can say that $\mathcal{X}$ attacks $A$ for short. We use $\texttt{{Att}}_{\mathcal{K}}\subseteq 2^{\texttt{{Arg}}_{\mathcal{K}}}\times \texttt{{Arg}}_{\mathcal{K}}$ to denote the set of attacks induced from $\mathcal{K}$ .*
Note that deductive argumentation can capture n-ary conflicts. However, as discussed in [35, 9], it argued that the argumentation framework using $\text{Datalog}^{\pm}$ , an instance of deductive argumentation, may generate a large number of arguments and attacks when using the definition of deductive arguments, as in [19]. To address this problem, some redundant arguments are dropped, as discussed in [9], or arguments are re-defined as those in ASPIC+, as seen in [35]. Then the attack relation must be redesigned to preserve all conflicts. In particular, n-ary attacks are allowed where arguments can jointly attack an argument. We will show this issue in the following example.
**Example 3.6**
*Consider $\mathcal{K}_{2}=(\mathcal{F}_{2},\mathcal{R}_{2},\mathcal{C}_{2})$ where
| | $\displaystyle\mathcal{R}_{2}=$ | $\displaystyle\emptyset,$ | |
| --- | --- | --- | --- |
The deductive argumentation approach [19] uses six arguments
| | $\displaystyle C_{2}:(\{B(a)\},B(a)),C_{3}:(\{C(a)\},C(a)),C_{4}:(\{A(a),B(a)\} ,A(a)\land B(a)),$ | |
| --- | --- | --- |
to obtains the preferred extensions: $\{C_{1},C_{2},C_{4}\}$ , $\{C_{1},C_{3},C_{5}\}$ , $\{C_{2},C_{3},C_{6}\}$ . In contrast, our approach uses three arguments $B_{1}:\{A(a)\}\Rightarrow A(a)$ , $B_{2}:\{B(a)\}\Rightarrow B(a)$ , $B_{3}:\{C(a)\}\Rightarrow C(a)$ with collective attacks, such as $\{B_{1},B_{2}\}$ attacks $B_{3}$ , etc., to obtain extensions $\{B_{1},B_{2}\},\{B_{1},B_{3}\},\{B_{2},B_{3}\}$ .*
**Remark 3.7**
*Similar to structured argumentation, such as deductive argumentation for propositional logic [59], DLs [14], $\text{Datalog}^{\pm}$ [19], DeLP systems [45], ASPIC systems [46] and sequent-based argumentation [65, 63], attacks in our framework are defined between individual arguments. In contrast, in ABA systems [44, 53, 67, 68], attacks are defined between sets of assumptions. However, in these ABA systems, the arguments generated from a set of assumptions are tree-derivations (both notions are used interchangeably), which can be instantiated by Definition 3.1, see above. Thus, the attacks defined on assumptions are equivalent to the attacks defined on the level of arguments.*
**Remark 3.8**
*Note that the definition of collective attacks holds if we only consider ASPIC+ without preferences [62]. We leave the case of preferences for future work.*
We introduce proof-oriented argumentation (P-SAF) as an instantiation of SAFs [25]. Our framework is comparable to the one of [52] in that both are applied to abstract logic. However, arguments in our setting differ from those in [52] in that we represent arguments in the form of a tree.
**Definition 3.9**
*Let $\mathcal{K}$ be a KB, the corresponding proof-oriented (logical) argumentation (P-SAF) $\mathcal{AF}_{\mathcal{K}}$ is the pair $(\texttt{{Arg}}_{\mathcal{K}},\texttt{{Att}}_{\mathcal{K}})$ where $\texttt{{Arg}}_{\mathcal{K}}$ is the set of arguments induced from $\mathcal{K}$ and $\texttt{{Att}}_{\mathcal{K}}$ is the set of attacks.*
In the next subsections, we show that the existing argumentation frameworks are instances of logic-associated argumentation frameworks.
### 3.2. Translating the Existing Argumentation Frameworks to P-SAFs
We have already shown that the existing frameworks (deductive argumentation [59, 14, 19], DeLP systems [45], ASPIC systems [46], ASPIC+ without preferences [62], ABA systems [44, 53, 67, 68]) can be seen as instances of our settings. Now we show how sequent-based argumentation [69, 55] and contrapositive ABAs [65, 63] fit in our framework.
- Sequent-based argumentation [69], using propositional logic, represents arguments as sequents. The construction of arguments from simpler arguments is done by the inference rules of the sequent calculus. Attack rules are represented as sequent elimination rules. The ingredients of sequent-based argumentation may be simulated in our setting:
We start with a logic $(\mathcal{L}_{s},\texttt{{CN}}_{s})$ . $\mathcal{L}_{s}$ is a propositional language having a set of atomic formulas $\texttt{{Atoms}}(\mathcal{L}_{s})$ . If $\phi$ and $\alpha$ are formulas wrt. $\texttt{{Atoms}}(\mathcal{L}_{s})$ then $\neg\phi$ , $\phi\wedge\alpha$ are formulas wrt. $\texttt{{Atoms}}(\mathcal{L}_{s})$ . We assume that the implication $\supset$ and $\leftrightarrow$ are defined accordingly. Propositional logic can be modelled by using sequents [69]. A sequent is a formula in the language $\mathcal{L}_{s}$ of propositional logic enriched by the addition of a new symbol $\leadsto$ . We call such sequent the s-formula of $\mathcal{L}_{s}$ to avoid ambiguity. In particular, for a formula $p\in\mathcal{L}_{s}$ the axiom $p\leadsto p$ are a s-formula in $\mathcal{L}_{s}$ . In general, for any set of formulas $\Psi\subseteq\mathcal{L}_{s}$ and $\phi\in\mathcal{L}_{s}$ , the sequents $\Psi\leadsto\phi$ are s-formulas of $\mathcal{L}_{s}$ .
Define $\texttt{{CN}}_{s}$ as follows: For a set of formulas $X\subseteq\mathcal{L}_{s}$ , a formula $\phi\in\mathcal{L}_{s}$ satisfies $\phi\in\texttt{{CN}}_{s}(X)$ iff an inference rule $\frac{\Psi_{1}\leadsto\phi_{1}\ldots\Psi_{n}\leadsto\phi_{n}}{\Psi\leadsto\phi}$ , where the sequents $\Psi\leadsto\phi$ and $\Psi_{i}\leadsto\phi_{i}$ ( $i=1,\ldots,n$ ) are s-formulas of $\mathcal{L}_{s}$ , is applied to $X$ such that $\Psi_{1},\ldots,\Psi_{n}$ are subsets of $X$ . We here consider the inference rules as structural rules and logical rules in [69]. Then we define $\overline{\texttt{{CN}}}_{s}(X)=\bigcup_{n\geq 0}\texttt{{CN}}_{s}^{n}(X)$ .
Let us define arguments in the sense of Definition 3.1: For a set of formulas $H\subseteq\mathcal{L}_{s}$ , $H\Rightarrow\phi$ is an argument iff $\phi\in\overline{\texttt{{CN}}}_{s}(H)$ . In this case, the argument, from the premise $H$ to the conclusion $\phi$ , can be described by a sequence of applications of inference rules. Such sequence is naturally organized in the shape of a tree by $\texttt{{CN}}_{s}$ . Each step up the tree corresponds to an application of an inference rule. The root of the tree is the final sequent (the conclusion), and the leaves are the axioms or initial sequents.
We show how the attack rules can be described in terms of corresponding attack relations in Definition 3.5. The attack rule has the form of $\frac{\Psi_{1}\leadsto\phi_{1},\ldots,\Psi_{n}\leadsto\phi_{n}}{\Psi_{n}\not \leadsto\phi_{n}}$ , in which the first sequent in the attack ruleâs prerequisites is the âattackingâ sequent, the last sequent in the attack ruleâs prerequisites is the âattackedâ sequent, and the other prerequisites are the conditions for the attack. According to the discussion above, these sequents $\Psi_{i}\leadsto\phi_{i}$ , ( $i=1,\ldots,n$ ), can be viewed as arguments $A_{i}:\Psi_{i}\Rightarrow\phi_{i}$ in the sense of Definition 3.1 where $\phi_{i}\in\overline{\texttt{{CN}}}_{s}(\Psi_{i})$ . Then, in this view, the first sequent $\Psi_{1}\leadsto\phi_{1}$ is the attacking argument $A_{1}$ , the last sequent $\Psi_{n}\leadsto\phi_{n}$ is the attacked argument $A_{n}$ , and the conclusions of the attack rule are the eliminations of the attacked arguments, meaning that $A_{n}$ is removed since $A_{1}$ attacks $A_{n}$ in the sense of Definition 3.5.
**Example 3.10 (Continue Example2.5)**
*Consider $\mathcal{K}=\{x,x\supset y,\neg y\}\subseteq\mathcal{L}_{s}$ . The following is an argument in propositional logic $A:\{x,x\supset y\}\Rightarrow y$ , $B:\{\neg y\}\Rightarrow\neg y$ . $A$ attacks $B$ since $\{x,x\supset y,\neg y\}$ is inconsistent, i.e., $\overline{\texttt{{CN}}}_{s}(\{x,x\supset y,\neg y\})=\mathcal{L}_{s}$ . Tree-representations of the arguments are shown in Figure 1 (Right), in which $[Mon]$ and $[\supset,\leadsto]$ are the names of inference rules.*
- Contrapositive ABA [65, 63] may be based on propositional logic and strict and candidate (defeasible) assumptions consists of arbitrary formulas in the language of that logic. Attacks are defined between sets of assumptions, i.e., defeasible assumptions may be attacked in the presence of a counter defeasible information. Our P-SAF framework using logic $(\mathcal{L}_{co},\texttt{{CN}}_{co})$ can simulate contrapositive ABAs as follows:
Assume that an implication connective $\supset$ is deductive (i.e., it is a $\vdash$ -implication in contrapositive ABAs) and converting such implications $\supset$ (i.e., $\phi_{1}\wedge\cdots\wedge\phi_{n}\supset\psi$ ) to rules of the form $\phi_{1},\ldots,\phi_{n}\rightarrow\psi$ in $\mathcal{L}_{co}$ . Here we ignore the distinction between defeasible and strict rules. With this assumption, the rules in $\mathcal{L}_{co}$ can be treated as $\vdash$ - implication, i.e., $\{\phi_{1},\ldots,\phi_{n}\rightarrow\psi\in\mathcal{L}_{co}\mid\phi_{1}, \ldots,\phi_{n}\vdash\psi\}$ ; their contrapositions treated as $\vdash$ - contrapositive, i.e., $\{\phi_{1},\ldots,\phi_{i-1},\neg\psi,\phi_{i+1},\dots\phi_{n}\rightarrow\neg \phi_{i}\mid\phi_{1},\ldots,\phi_{i-1},\neg\psi,\phi_{i+1},\dots\phi_{n}\vdash \neg\phi_{i}\}$ See definitions of $\vdash$ -implication and $\vdash$ -contrapositive in [65, 63]. This translation views the contrapositive ABA as a special case of the traditional definition of ABA [44]; also the traditional ABA can be simulated in our P-SAF using $(\mathcal{L}_{co},\texttt{{CN}}_{co})$ . Thus, the results and concepts of P-SAFs can apply to the contrapositive ABAs. Indeed, first, $\mathcal{L}_{co}$ includes the strict and candidate assumptions We abuse the term âstrict and candidate assumptionsâ and refer them as âliteralsâ. and the set of rules. These rules as reasoning patterns are used in $\texttt{{CN}}_{co}$ as defined in Definition 2.14. Second, by Definition 3.1, for $H\subseteq\mathcal{L}_{co}$ be a set of assumptions and $\phi\in\mathcal{L}_{co}$ , $H\Rightarrow\phi$ is an argument iff $\phi\in\overline{\texttt{{CN}}}_{co}(H)$ . Third, the attacks defined on assumptions in traditional ABA are equivalent to those in our S-PAFs (see Remark 3.7 for further explanation).
Note that contrapositive ABAs in [63] (with collective attacks) are analogous to those in [65], except they drop the requirement that any set of candidate assumptions contributing to the attacks must be close. Similarly, our P-SAF framework, which uses $\overline{\texttt{{CN}}}_{co}$ in the definition of inconsistency for our attacks, does not impose this additional requirement.
### 3.3. Acceptability of P-SAFs and Relations to Reasoning with MSCs
Semantics of P-SAFs are now defined as in the definition of semantics for SAFs [25]. These semantics consist of admissible, complete, stable, preferred and grounded semantics.
Given a P-SAF $\mathcal{AF}_{\mathcal{K}}=(\texttt{{Arg}}_{\mathcal{K}},\texttt{{Att}}_{ \mathcal{K}})$ and $\mathcal{S}\subseteq\texttt{{Arg}}_{\mathcal{K}}$ . $\mathcal{S}$ attacks $\mathcal{X}$ iff $\exists A\in\mathcal{X}$ s.t. $\mathcal{S}$ attacks $A$ . $\mathcal{S}$ defends $A$ if for each $\mathcal{X}\subseteq\texttt{{Arg}}_{\mathcal{K}}$ s.t. $\mathcal{X}$ attacks $A$ , some $\mathcal{S}^{\prime}\subseteq\mathcal{S}$ attacks $\mathcal{X}$ . An extension $\mathcal{S}$ is called
- conflict-free if it does not attack itself;
- admissible $(\texttt{{adm}})$ if it is conflict-free and defends itself.
- complete $(\texttt{{cmp}})$ if it is admissible containing all arguments it defends.
- preferred $(\texttt{{prf}})$ if it is an inclusion-maximal admissible extension.
- stable $(\texttt{{stb}})$ if it is conflict-free and attacks every argument not in it.
- grounded $(\texttt{{grd}})$ if it is an inclusion-minimal complete extension.
Note that this implies that each grounded or preferred extension of a P-SAF is an admissible one, the grounded extension is contained in all other extensions.
Let $\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ denote the set of all extensions of $\mathcal{AF}_{\mathcal{K}}$ under the semantics $\texttt{{sem}}\in\{\texttt{{adm}},\ \texttt{{stb}},\ \texttt{{prf}},\ \texttt{ {grd}}\}$ . Let us define acceptability in P-SAFs.
**Definition 3.11**
*Let $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of a KB $\mathcal{K}$ and $\texttt{{sem}}\in\{\texttt{{adm}},\texttt{{stb}},\texttt{{prf}}\}$ . A formula $\phi\in\mathcal{L}$ is
- credulously accepted under sem iff for some $\mathcal{E}\in\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi\in\texttt{{Cons}}(\mathcal{E})$ .
- groundedly accepted under grd iff for some $\mathcal{E}\in\texttt{{Exts}}_{\texttt{{grd}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi\in\texttt{{Cons}}(\mathcal{E})$ .
- sceptically accepted under sem iff for all $\mathcal{E}\in\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi\in\texttt{{Cons}}(\mathcal{E})$ .*
Next, we show the relation to reasoning with maximal consistent subsets in inconsistent KBs. Proposition 3.12 shows a relation between extensions of P-SAFs and MSCs of KBs.
**Proposition 3.12**
*Let $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of a KB $\mathcal{K}$ . Then, - the maximal consistent subset of $\mathcal{K}$ coincides with the stable/ preferred extension of $\mathcal{AF}_{\mathcal{K}}$ ;
- the intersection of the maximal consistent subsets of $\mathcal{K}$ coincides with the grounded extension of $\mathcal{AF}_{\mathcal{K}}$ .*
* Proof*
The idea of the proof is to show that every preferred extension is the set of arguments generated from a MCS, that every such set of arguments is a stable extension, and that every stable extension is preferred. The proof of the second statement follows the lemma saying that if there are no rejected arguments under preferred semantics, then the grounded extension is equal to the intersection of all preferred extensions. By the proof of the first statement, every preferred extension is a maximal consistent subset. Thus the second statement is proved. â
**Remark 3.13**
*In general, the grounded extension is contained in the intersection of all maximal consistent subsets.*
The main result of this section, Theorem 3.14, which follows from Proposition 3.12 generalises results from previous works.
**Theorem 3.14**
*Let $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of a KB $\mathcal{K}$ , $\phi\in\mathcal{L}$ a formula and $\texttt{{sem}}\in\{\texttt{{adm}},\texttt{{stb}},\texttt{{prf}}\}$ . Then, $\phi$ is entailed in
- some maximal consistent subset iff $\phi$ is credulously accepted under sem.
- all maximal consistent subsets iff $\phi$ is sceptically accepted under sem.
- the intersection of all maximal consistent subsets iff $\phi$ is groundedly accepted under grd.*
To argue the quality of P-SAF, it can be shown that it satisfies the rationality postulates introduced in [51, 40].
**Definition 3.15**
*Let $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of a KB $\mathcal{K}$ . Wrt. $\texttt{{sem}}\in\{\texttt{{adm}},\texttt{{stb}},\texttt{{prf}},\texttt{{grd}}\}$ , $\mathcal{AF}_{\mathcal{K}}$ is
1. closed under $\overline{\texttt{{CN}}}$ iff for all $\mathcal{E}\in\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\texttt{{Cons}}(\mathcal{E})=\overline{\texttt{{CN}}}(\texttt{{Cons}}(\mathcal {E}))$ ;
1. consistent iff for all $\mathcal{E}\in\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\texttt{{Cons}}(\mathcal{E})$ is consistent;*
**Proposition 3.16**
*Wrt. to any semantics in $\{\texttt{{adm}},\texttt{{stb}}$ , $\texttt{{prf}},\texttt{{grd}}\}$ , $\mathcal{AF}_{\mathcal{K}}$ satisfies consistency, closure.*
The proof of Proposition 3.16 is analogous to those of Proposition 2 in [52]. Because of this similarity, they are not included in the appendix.
**Example 3.17 (Continue Example2.19)**
*Recall $\mathcal{K}_{1}$ . Table 2 shows the supports and conclusions of all arguments induced from $\mathcal{K}$ . The corresponding P-SAF admits stb (prf) extensions: $\texttt{{Exts}}_{\texttt{{stb}}/\texttt{{prf}}}(\mathcal{AF}_{1})=\{\mathcal{E }_{1},\ldots,\mathcal{E}_{6}\}$ , where $\mathcal{E}_{1}=\texttt{{Args}}(\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}), \texttt{{UC}}(\texttt{{KD}})\})$ Fix $\mathcal{F}^{\prime}\subseteq\mathcal{F}$ , $\texttt{{Args}}(\mathcal{F}^{\prime})$ is the set of arguments generated by $\mathcal{F}^{\prime}$ $=\{A_{5},A_{6},A_{2}\}$ , and $\mathcal{E}_{2},\ldots,\mathcal{E}_{6}$ are obtained in an analogous way. It can be seen that the extensions correspond to the repairs of the KBs (by Theorem 3.14). Reconsider $q_{1}=\texttt{{Re}}(\texttt{{v}})$ . We have that $q_{1}$ is credulously accepted under stb (prf) extensions. In other words, v is a possible answer for $q_{1}$ .*
Table 2. Supports and conclusions of arguments
| $A_{0}$ $A_{9}$ $A_{7}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ $\{\texttt{{GC}}(\texttt{{KR}})\}$ $\{\texttt{{GC}}(\texttt{{KR}}),\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ | $\texttt{{te}}(\texttt{{v}},\texttt{{KR}})$ $\texttt{{GC}}(\texttt{{KR}})$ $\texttt{{FP}}(\texttt{{v}})$ |
| --- | --- | --- |
| $A_{1}$ | $\{\texttt{{GC}}(\texttt{{KR}}),\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ | $\texttt{{Re}}(\texttt{{v}})$ |
| $A_{4}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KD}})\}$ | $\texttt{{te}}(\texttt{{v}},\texttt{{KD}})$ |
| $A_{5}$ | $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}})\}$ | $\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}})$ |
| $A_{6}$ | $\{\texttt{{UC}}(\texttt{{KD}})\}$ | $\texttt{{UC}}(\texttt{{KD}})$ |
| $A_{2}$ | $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\ \texttt{{UC}}(\texttt{{KD}})\}$ | $\texttt{{TA}}(\texttt{{v}})$ |
| $A_{3}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KD}})\}$ | $\texttt{{Le}}(\texttt{{v}})$ |
| $A_{8}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ | $\texttt{{Le}}(\texttt{{v}})$ |
| $A_{10}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ | $\texttt{{Em}}(\texttt{{v}})$ |
| $A_{11}$ | $\{\texttt{{te}}(\texttt{{v}},\texttt{{KD}})\}$ | $\texttt{{Em}}(\texttt{{v}})$ |
| $A_{12}$ | $\{\texttt{{GC}}(\texttt{{KR}}),\texttt{{te}}(\texttt{{v}},\texttt{{KR}})\}$ | $\texttt{{Em}}(\texttt{{v}})$ |
In this section, we have translated from KBs into P-SAFs. Consequently, the acceptance of a formula $\phi$ of $\mathcal{L}$ corresponds to the acceptance of a set of arguments $\mathcal{A}$ for $\phi$ . When we say âa set of arguments $\mathcal{A}$ for $\phi$ â, it means simply that for each argument in $\mathcal{A}$ , its consequence is $\phi$ . We next introduce a novel notion of explanatory dialogue (â dialogue â for short) viewed as a dialectical proof procedure in Section 4. Section 5 will show how to use a dialogue model to determine and explain the acceptance of $\phi$ wrt argumentation semantics.
## 4. Explanatory Dialogue Models
Inspired by [23, 42], we develop a novel explanatory dialogue model of P-SAF by examining the dispute process involving the exchange of arguments (represented as formulas in KBs) between two agents. The novel explanatory dialogue model can show how to determine and explain the acceptance of a formula wrt argumentation semantics.
### 4.1. Basic Notions
Concepts of a novel dialogue model for P-SAFs include utterances, dialogues and concrete dialogue trees (â dialogue tree â for short). In this model, a topic language $\mathcal{L}_{t}$ is abstract logic $(\mathcal{L},\texttt{{CN}})$ ; dialogues are sequences of utterances between two agents $a_{1}$ and $a_{2}$ sharing a common language $\mathcal{L}_{c}$ . Utterances are defined as follows:
**Definition 4.1 (Utterances)**
*An utterance of agents $a_{i},\ i\in\{1,2\}$ has the form $u=(a_{i},\texttt{{TG}},\texttt{{C}},\texttt{{ID}})$ , where:
- $\texttt{{ID}}\in\mathbb{N}$ is the identifier of the utterance,
- TG is the target of the utterance and we impose that $\texttt{{TG}}<\texttt{{ID}}$ ,
- $\texttt{{C}}\in\mathcal{L}_{c}$ (the content) is one of the following forms: Fix $\phi\in\mathcal{L}$ and $\Delta\subseteq\mathcal{L}$ .
- $\texttt{{claim}}(\phi)$ : The agent asserts that $\phi$ is the case,
- $\texttt{{offer}}(\Delta,\phi)$ : The agent advances grounds $\Delta$ for $\phi$ uttered by the previously advanced utterances such that $\phi\in\texttt{{CN}}(\Delta)$ ,
- $\texttt{{contrary}}(\Delta,\ \phi)$ : The agent advances the formulas $\Delta$ that are contrary to $\phi$ uttered by the previously advanced utterance,
- $\texttt{{concede}}(\phi)$ : The agent gives up debating and admits that $\phi$ is the case,
- $\texttt{{fact}}(\phi)$ : The agent asserts that $\phi$ is a fact in $\mathcal{K}$ .
- $\kappa$ : The agent does not have or wants to contribute information at that point in the dialogue.
We denote by $\mathcal{U}$ the set of all utterances.*
To determine which utterances agents can make to construct a dialogue, we define a notion of legal move, similarly to communication protocols. For any two utterances $u_{i},\ u_{j}\in\mathcal{U}$ , $u_{i}\neq u_{j}$ , we say that:
- $u_{i}$ is the target utterance of $u_{j}$ iff the target of $u_{j}$ is the identifier of $u_{i}$ , i.e., $u_{i}=(\_,\_,\texttt{{C}}_{i},\texttt{{ID}})$ and $u_{j}=(\_,\texttt{{ID}},\texttt{{C}}_{j},\_)$ ;
- $u_{j}$ is the legal move after $u_{i}$ iff $u_{i}$ is the target utterance of $u_{j}$ and one of the following cases in Table 3 holds.
Table 3. Locutions and responses
$$
u_{i} u_{j} \texttt{{C}}_{i}=\texttt{{claim}}(\phi) \texttt{{C}}_{j}=\texttt{{offer}}(\_,\phi) \phi\in\texttt{{CN}}(\{\_\}) \texttt{{C}}_{j}=\texttt{{fact}}(\phi) \phi\in\mathcal{K} \texttt{{C}}_{j}=\texttt{{contrary}}(\_,\ \phi) \{\_,\phi\} \texttt{{C}}_{i}=\texttt{{fact}}(\phi) \texttt{{C}}_{j}=\texttt{{contrary}}(\_,\phi) \{\_,\phi\} \texttt{{C}}_{i}=\texttt{{offer}}(\Delta,\phi) \texttt{{C}}_{j}=\texttt{{contrary}}(\_,\ \phi) \{\_,\phi\} \phi\in\texttt{{CN}}(\Delta) \texttt{{C}}_{j}=\texttt{{contrary}}(\_,\ \Delta) \{\_\}\cup\Delta \texttt{{C}}_{j}=\texttt{{offer}}(\_,\beta_{i}) \beta_{i}\in\Delta \beta_{j}\in\texttt{{CN}}(\{\_\}) \texttt{{C}}_{i}=\texttt{{contrary}}(\beta,\_) \texttt{{C}}_{j}=\texttt{{contrary}}(\_,\beta) \{\_,\beta\} \texttt{{C}}_{j}=\texttt{{offer}}(\_,\beta) \beta\in\texttt{{CN}}(\{\_\}) \tag{1}
$$
An utterance is a legal move after another if any of the following cases happens: (1) it with content offer contributes to expanding an argument; (2) it with content fact identifies a fact in support of an argument; (3) it with content contrary starts the construction of a counter-argument. An utterance can be from the same agent or not.
### 4.2. Dialogue Trees, Dialogues and Focused Sub-dialogues
In essence, a dialogue is a sequence of utterances $u_{1},\ldots,u_{n}$ , each of which transforms the dialogue from one state to another. To keep track of information disclosed in dialogues for P-SAFs, we define dialogue trees constructed as the dialogue progresses. These are subsequently used to determine successful dialogues w.r.t argumentation semantics.
A dialogue tree represents a dispute progress between a proponent and an opponent who take turns exchanging arguments in the form of formulas of a KB. The proponent starts the dispute with their arguments and must defend against all of the opponentâs attacks to win. Informally, in a dialogue tree, the formula of each node represents an argumentâs conclusion or elements of the argumentâs support. A node is annotated unmarked if its formula is only mentioned in the claim, but without any further examination, marked-non-fact if its formula is the logical consequence of previous uttered formulas, and marked-fact if its formula has been explicitly uttered as a fact in $\mathcal{K}$ . A node is labelled P $(\texttt{{O}})$ if it is (directly or indirectly) for (against, respectively) the claim of the dialogue. The ID is used to identify the nodeâs corresponding utterance in the dialogue. The nodes are connected in two cases: (1) they belong to the same argument, and (2) they form collective attacks between arguments. We formally define dialogue trees and dialogues.
**Definition 4.2**
*Given a sequence of utterances $\delta=u_{1},\ldots,u_{n}$ , the dialogue tree $\mathcal{T}(\delta)$ drawn from $\delta$ is a tree whose nodes are tuples $(\texttt{{S}},\ [\texttt{{T}},\ \texttt{{L}},\ \texttt{{ID}}])$ , where:
- S is a formula in $\mathcal{L}$ ,
- T is either um (unmarked), nf (marked-non-fact), fa (marked-fact),
- L is either P or O,
- ID is the identifier of the utterance $u_{i}$ ; and $\mathcal{T}(\delta)$ is $\mathcal{T}^{n}$ in the sequence $\mathcal{T}^{1},\ldots,\mathcal{T}^{n}$ constructed inductively from $\delta$ , as follows:
1. $\mathcal{T}^{1}$ contains a single node: $(\phi,[\texttt{{um}},\ \texttt{{P}},\ \texttt{{id}}_{1}])$ where $\texttt{{id}}_{1}$ is the identifier of the utterance $u_{1}=(\_,\_,\texttt{{claim}}(\phi),\texttt{{id}}_{1})$ ;
1. Let $u_{i+1}=(\_,\ \texttt{{ta}},\ \texttt{{C}},\ \texttt{{id}})$ be the utterance in $\delta$ ; $\mathcal{T}^{i}$ be the $i$ -th tree with the utterance $(\_,\ \_,\ \texttt{{C}}_{\texttt{{ta}}},\ \texttt{{ta}})$ as the target utterance of $u_{i+1}$ . Then $\mathcal{T}^{i+1}$ is obtained from $\mathcal{T}^{i}$ by $u_{i+1}$ , if one of the following conditions holds: $(\texttt{{L}},\texttt{{L}}_{\texttt{{ta}}}\in\{\texttt{{P}},\texttt{{O}}\}, \texttt{{L}}\neq\texttt{{L}}_{\texttt{{ta}}})$ :
1. If $\texttt{{C}}=\texttt{{offer}}(\Delta,\ \alpha)$ with $\Delta=\{\beta_{1},\ldots,\beta_{m}\}$ and $\alpha\in\texttt{{CN}}(\Delta)$ , then $\mathcal{T}^{i+1}$ is obtained:
- For all $\beta_{j}\in\Delta$ , new nodes $(\beta_{j},[\texttt{{T}},\ \texttt{{L}},\ \texttt{{id}}])$ are added to the node $(\alpha,[\_,\ \texttt{{L}},\ \texttt{{ta}}])$ of $\mathcal{T}^{i}$ . Here $\texttt{{T}}=\texttt{{fa}}$ if $\beta_{j}\in\mathcal{K}$ , otherwise $\texttt{{T}}=\texttt{{nf}}$ ;
- The node $(\alpha,[\_,\ \texttt{{L}},\ \texttt{{ta}}])$ is replaced by $(\alpha,[\texttt{{nf}},\ \texttt{{L}},\ \texttt{{ta}}])$ ;
1. If $\texttt{{C}}=\texttt{{fact}}(\alpha)$ then $\mathcal{T}^{i+1}$ is $\mathcal{T}^{i}$ with the node $(\alpha,\ [\_,\ \texttt{{L}},\ \texttt{{ta}}])$ replaced by $(\alpha,\ [\texttt{{fa}},\ \texttt{{L}},\ \texttt{{id}}])$ ;
1. If $\texttt{{C}}=\texttt{{contrary}}(\Delta,\eta)$ where $\Delta=\{\beta_{1},\ldots,\beta_{m}\}$ and $\Delta\cup\{\eta\}$ is inconsistent, then $\mathcal{T}^{i+1}$ is obtained by adding new nodes $(\beta_{j},[\texttt{{T}},\ \texttt{{L}},\ \texttt{{id}}])$ , $(\texttt{{T}}=\texttt{{fa}}$ if $\beta_{j}\in\mathcal{K}$ , otherwise $\texttt{{T}}=\texttt{{nf}})$ , as children of the node $(\eta,[\texttt{{T}}_{\texttt{{ta}}},\ \texttt{{L}}_{\texttt{{ta}}},\ \texttt{{ ta}}])$ of $\mathcal{T}^{i}$ , where $\texttt{{T}}_{\texttt{{ta}}}\in\{\texttt{{fa}},\ \texttt{{nf}}\}$ . For such dialogue tree $\mathcal{T}(\delta)$ , the nodes labelled by P (resp., O) are called the proponent nodes (resp., opponent nodes). We call the sequence $u_{1},\ldots,u_{n}$ a dialogue $D(\phi)$ for $\phi$ where $\phi$ is the formula of the root in $\mathcal{T}(\delta)$ .*
This dialogue tree can be seen as a concrete representation of an abstract dialogue tree defined in [52]. Here, the nodes represent formulas and the edges display either the monotonic inference steps used to construct arguments or the attack relations between arguments. A group of nodes in a dialogue tree with the same label P (or O) corresponds to the proponent (or opponent) argument in the abstract dialogue tree.
**Definition 4.3 (Focused sub-dialogues)**
*$\delta^{\prime}$ is called a focused sub-dialogue of a dialogue $\delta$ iff it is a dialogue for $\phi$ and, for all utterances $u\in\delta^{\prime}$ , $u\in\delta$ . We say that $\delta$ is the full-dialogue of $\delta^{\prime}$ and $\mathcal{T}(\delta^{\prime})$ drawn from $\delta^{\prime}$ is the sub-tree of $\mathcal{T}(\delta)$ .*
If there are no utterances for both proponents and opponents in a dialogue tree from a dialogue $\delta$ , then $\delta$ is called terminated. Note that a dialogue can be âincompleteâ, which means that it ends before the utterances related to determining success are claimed. To prevent this from happening we assume that dialogues are complete, i.e. that there are no âunsaidâ utterances (with the content fact, offer or contrary) in such dialogue that would bring important arguments to determine success. This assumption will ease the proof of soundness result later.
**Example 4.4 (Continue Example3.17)**
*When users received the answer â $(\texttt{{v}})$ is possible researcher â, they would like to know â Why is this the case? â. The system will explain to the users through the natural language dispute agreement that the agent $a_{1}$ is persuading $a_{2}$ to agree that v is a researcher. This dispute agreement is formally modelled by an explanatory dialogue $D(\texttt{{Re}}(\texttt{{v}}))=\delta$ as in Figure 2.
<details>
<summary>x4.png Details</summary>
### Visual Description
\n
## Data Table: Dialogue Act Sequences
### Overview
The image presents a data table outlining sequences of dialogue acts between two agents, labeled 'a1' and 'a2'. Each row represents a dialogue act 'u' with its associated parameters and a numerical identifier. The table appears to be a representation of a conversation or interaction model.
### Components/Axes
The table is structured with two main columns, one for agent 'a1' and one for agent 'a2'. Each column contains several rows, each representing a dialogue act. Each row is formatted as: `u_i = (parameters), i` where 'i' is the sequence number. The parameters within the parentheses appear to be function calls or expressions involving variables like 'v', 'Re', 'FP', 'KR', 'GC', 'te', 'KD', 'Le', 'TA', 'taOf', 'UC', and 'concede'.
### Detailed Analysis / Content Details
Here's a transcription of the table's content, row by row:
* **u1 = (a1, 0, claim(Re(v)), 1)**
* **u2 = (a1, 1, offer(FP(v), Re(v)), 2)**
* **u3 = (a1, 2, offer({te(v, KR), GC(KR)}, FP(v)), 3)**
* **u4 = (a2, 2, contrary(TA(v), Re(v)), 4)**
* **u5 = (a2, 4, offer({taOf(v, KD), UC(KD)}, TA(v)), 5)**
* **u6 = (a1, 4, contrary(Le(v), TA(v)), 6)**
* **u7 = (a1, 6, offer(te(v, KD), Le(v)), 7)**
* **u8 = (a2, 0, concede(Re(v)), 8)**
### Key Observations
The table shows a back-and-forth exchange between 'a1' and 'a2'. The dialogue acts include 'claim', 'offer', 'contrary', and 'concede'. The parameters within the acts involve functions applied to a variable 'v', suggesting that 'v' represents some proposition or topic of discussion. The sequence numbers (1 through 8) indicate the order of the dialogue acts. Agent 'a1' initiates with a claim, and the conversation progresses through offers and counter-arguments before 'a2' concedes.
### Interpretation
This data table likely represents a simplified model of a negotiation or argumentation dialogue. The functions used (claim, offer, contrary, concede) are standard speech acts in dialogue modeling. The parameters within these acts likely represent the content of the dialogue, with 'v' being the core proposition being discussed. The functions like 'FP', 'KR', 'GC', 'te', 'KD', 'Le', 'TA', 'taOf', and 'UC' likely represent specific aspects or conditions related to the proposition 'v'. The sequence of acts suggests a process where 'a1' makes a claim, 'a2' counters it, 'a1' responds, and eventually 'a2' concedes. This could be a model of how arguments are constructed and resolved in a conversational setting. The table provides a formal representation of a dialogue, which could be used for computational analysis or simulation of human-computer interaction.
</details>
Figure 2. Given $\mathcal{L}_{t}$ is $\mathcal{K}_{1}$ , a dialogue $D(\texttt{{Re}}(\texttt{{v}}))$ $=u_{1},\ldots,u_{9}$ for $q_{1}=\texttt{{Re}}(\texttt{{v}})$ Figure 3 illustrates how to fully construct a dialogue tree $\mathcal{T}(\delta)$ from $D(\texttt{{Re}}(\texttt{{v}}))=\delta$ . To avoid confusing users, after the construction processing, we display the final dialogue tree $\mathcal{T}(\delta)$ with necessary labels, such as formulas, P and O, in Figure 4. The line indicates that children conflict with their parents. The dotted line indicates that children are implied from their parents by inference rules. From this tree, the system provides a dialogical explanation in natural language as shown in Example 1.1.*
<details>
<summary>x5.png Details</summary>
### Visual Description
\n
## Diagram: Flow Diagrams of Processes T1 to T7
### Overview
The image presents seven separate flow diagrams, labeled T1(ÎŽ) through T7(ÎŽ). Each diagram depicts a series of processes and transitions, represented by labeled boxes and arrows. The diagrams appear to illustrate a sequence of operations or a state machine, with each step involving specific inputs and outputs. The diagrams are arranged in a 2x3 grid, with T1 in the top-left and T7 in the bottom-right.
### Components/Axes
Each diagram shares a similar structure:
* **Boxes:** Represent processes or states, labeled with abbreviations and numerical values.
* **Arrows:** Indicate transitions between states, labeled with abbreviations.
* **Labels:** Each box and arrow is labeled with a combination of abbreviations and numbers.
* **Common Labels:** `Re(v)`, `nf`, `P`, `r3`, `FP(v)`, `te(v, KR)`, `GC(KR)`, `TA(v)`, `taOf(v, KD)`, `UC(KD)`, `Le(v)`, `r5`, `r6`, `r7`, `r4`, `c1`, `c2`.
* **Numerical Values:** The numbers associated with the labels vary between 1 and 5.
* **ÎŽ:** Appears in each diagram title, suggesting a parameter or variable.
### Detailed Analysis or Content Details
**T1(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
**T2(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 4])`
**T3(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 3])`
**T4(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 3])`
* Process 5: `TA(v), [nf, 0, 4])`
**T5(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 3])`
* Process 5: `TA(v), [nf, 0, 4])`
* Process 6: `taOf(v, KD), [fa, 0, 5])`
* Process 7: `UC(KD), [fa, 0, 5])`
**T6(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 3])`
* Process 5: `TA(v), [nf, 0, 4])`
* Process 6: `taOf(v, KD), [fa, 0, 5])`
* Process 7: `UC(KD), [fa, 0, 5])`
* Transition 3: `r4`
* Process 8: `Le(v), [nf, P, 7])`
**T7(ÎŽ)**
* Process 1: `Re(v), [nf, P, 1])`
* Transition 1: `r3`
* Process 2: `FP(v), [nf, P, 2])`
* Transition 2: `r6`
* Process 3: `te(v, KR), [fa, P, 3])`
* Process 4: `GC(KR), [fa, P, 3])`
* Process 5: `TA(v), [nf, 0, 4])`
* Process 6: `taOf(v, KD), [fa, 0, 5])`
* Process 7: `UC(KD), [fa, 0, 5])`
* Transition 3: `r4`
* Process 8: `Le(v), [nf, P, 7])`
### Key Observations
* The initial three processes (`Re(v)`, `FP(v)`, `te(v, KR)`) are consistent across all diagrams.
* The diagrams progressively add processes, with T5, T6, and T7 introducing `TA(v)`, `taOf(v, KD)`, and `UC(KD)`.
* T6 and T7 introduce a final process `Le(v)` and a transition `r4`.
* The values within the square brackets change across diagrams, suggesting different states or conditions.
* The diagrams appear to represent a branching process, where each diagram explores a different path or outcome.
### Interpretation
The diagrams likely represent a series of state transitions within a system. The parameter ÎŽ suggests that the behavior of the system is dependent on some external variable. The consistent initial processes indicate a common starting point, while the diverging paths represent different possible outcomes or responses to different inputs. The addition of processes in later diagrams suggests increasing complexity or the introduction of new functionalities. The labels `fa`, `nf`, `P`, `KD`, and `KR` likely represent specific parameters or conditions within the system. The numerical values within the brackets could represent thresholds, probabilities, or other quantitative measures. The diagrams could be used to model a complex system, such as a biological pathway, a computer program, or a control system. The diagrams are highly abstract and require domain-specific knowledge to fully interpret. The consistent structure across the diagrams suggests a systematic approach to analyzing the system's behavior under different conditions.
</details>
Figure 3. Construction of the dialogue tree $\mathcal{T}(\delta)=\mathcal{T}_{7}(\delta)$ drawn from $D(\texttt{{Re}}(\texttt{{v}}))$ .
<details>
<summary>x6.png Details</summary>
### Visual Description
\n
## Diagram: Tree Structure - T(ÎŽ)
### Overview
The image depicts a tree-like diagram labeled "T(ÎŽ)" at the top-center. The diagram represents a hierarchical structure with nodes connected by branches. Each node contains a textual label enclosed in parentheses, and branches are labeled with variables (râ, câ, câ, etc.). The diagram appears to represent a logical or computational process, potentially a derivation or transformation.
### Components/Axes
The diagram consists of nodes and branches. There are no explicit axes in the traditional sense. The structure is organized from top to bottom, with a root node at the top and branching paths leading to terminal nodes at the bottom. The labels within the nodes are the primary components. The branches are labeled as follows:
* râ
* râ
* râ
* râ
* câ
* câ
### Detailed Analysis or Content Details
The diagram can be described as follows, starting from the root and traversing down the branches:
1. **Root Node:** (Re(v), P)
2. **Branching from Root:**
* A dotted line labeled 'râ' leads to (FP(v), P)
* A line labeled 'câ' leads to (GC(KR), P)
3. **From (FP(v), P):**
* A line labeled 'râ' leads to (te(v, KR), P)
4. **From (GC(KR), P):**
* A line labeled 'câ' leads to (TA(v), 0)
5. **From (TA(v), 0):**
* A dotted line labeled 'râ' leads to (taOf(v, KD), 0)
* A dotted line labeled 'râ' leads to (UC(KD), 0)
6. **From (te(v, KR), P):**
* A line labeled 'câ' leads to (Le(v), P)
7. **From (Le(v), P):**
* A line labeled 'râ
' leads to (te(v, KD), P)
### Key Observations
The diagram shows a branching structure with a clear hierarchy. The labels within the nodes suggest a series of transformations or operations applied to variables 'v', 'KR', and 'KD'. The presence of 'P' and '0' as second elements in the node labels might indicate different states or types of values. The dotted lines (râ, râ) and solid lines (câ, câ, râ
, râ) may represent different types of relationships or transitions.
### Interpretation
The diagram likely represents a derivation or a computational process. The nodes represent intermediate states, and the branches represent transformations or operations. The variables 'v', 'KR', and 'KD' likely represent inputs or parameters to the process. The 'P' and '0' values could indicate boolean flags or numerical values associated with each state. The diagram could be a simplified representation of a formal system, a program execution flow, or a logical proof. The use of 'te', 'GC', 'TA', 'Le', 'FP', 'taOf', and 'UC' suggests specific functions or operators within the system. Without further context, it's difficult to determine the exact meaning of the diagram, but it clearly illustrates a structured process with defined steps and transformations. The diagram is a visual representation of a logical or computational process, potentially a derivation or transformation. The labels within the nodes suggest a series of transformations or operations applied to variables 'v', 'KR', and 'KD'. The presence of 'P' and '0' as second elements in the node labels might indicate different states or types of values. The dotted lines (râ, râ) and solid lines (câ, câ, râ
, râ) may represent different types of relationships or transitions.
</details>
Figure 4. A final version of the dialogue tree $\mathcal{T}(\delta)$ is displayed for users
### 4.3. Focused Dialogue Trees
To determine and explain the arguments of acceptability (wrt argumentation semantics) by using dialogues/ dialogue trees, we present a notion of focused dialogue trees that will be needed for the following sections. This concept is useful because it allows us to show a correspondence principle between dialogue trees and abstract dialogue trees defined in [52] We reproduce the notion of abstract dialogue trees and introduce the correspondence principle in Appendix A. Here we briefly describe the concept of abstract dialogue trees: an abstract dialogue tree is a tree where nodes are labeled with arguments, and edges represent attacks between arguments. . By the correspondence principle, we can utilize the results from [52] to obtain the important results in Section 5.2 and 5.3.
Observe that a dialogue $\delta$ can be seen as a collection of several (independent) focused sub-dialogues $\delta_{1},\ldots,\delta_{n}$ . The dialogue tree $\mathcal{T}(\delta_{i})$ drawn from the focused sub-dialogue $\delta_{i}$ is a subtree of $\mathcal{T}(\delta)$ and corresponds to the abstract dialogue tree (defined in [52]) (for an argument for $\phi$ ). Each such subtree of $\mathcal{T}(\delta)$ has the following properties: (1) $\phi$ is supported by a single proponent argument; (2) An opponent argument is attacked by either a single proponent argument or a set of collective proponent arguments; (3) A proponent argument can be attacked by either multiple single opponent arguments or sets of collective opponent arguments. We call a tree with these properties the focused dialogue tree.
**Definition 4.5 (Focused dialogue trees)**
*A dialogue tree $\mathcal{T}(\delta)$ is focused iff
1. all the immediate children of the root node have the same identifier (that is, are part of a single utterance);
1. all the children labelled P of each potential argument labelled O have the same identifier (that is, are part of a single utterance)*
In the above definition, we call child of a potential argument a node that is child of any of the nodes of the potential argument.
**Remark 4.6**
*Focused dialogue trees and their relation to abstract dialogue trees are crucial for proving the important results in Section 5.2 and 5.3. We refer to Appendix B for details.*
**Example 4.7**
*Consider a query $q_{3}=A(a)$ to a KB $\mathcal{K}_{3}=(\mathcal{R}_{3},\mathcal{C}_{3},\mathcal{F}_{3})$ where
| | $\displaystyle\mathcal{R}_{3}=$ | $\displaystyle\{r_{1}:C(x)\land B(x)\rightarrow A(x),\ r_{2}:D(x)\rightarrow A( x)\}$ | |
| --- | --- | --- | --- |
Figure 5 (Left) shows a non-focused dialogue tree drawn for a dialogue $D(A(a))=\delta$ . Figure 5 (Right) shows a focused dialogue tree $\mathcal{T}(\delta_{1})$ drawn for a sub-dialogue $\delta_{1}$ of $\delta$ . This tree is the sub-tree of $\mathcal{T}(\delta)$ .*
<details>
<summary>x7.png Details</summary>
### Visual Description
\n
## Diagram: Tree-like Structure
### Overview
The image depicts a tree-like diagram representing a hierarchical structure. Nodes are connected by directed edges (arrows), indicating a parent-child relationship. Each node is labeled with a function call and associated parameters enclosed in parentheses. The diagram appears to represent a call graph or a similar dependency structure.
### Components/Axes
The diagram consists of nodes and directed edges. There are no explicit axes or scales. The nodes are arranged in a hierarchical manner, with a root node at the top and branching nodes below. Each node contains a function name (A, B, C, D, E) followed by a parameter 'a' in parentheses, and then a bracketed list of parameters and a numerical value.
### Detailed Analysis or Content Details
The diagram can be described as follows, starting from the root:
1. **A(a), [um, P, 1]** - Root node.
2. **B(a), [fa, P, 2]** - Child of A, connected by a dashed arrow.
3. **C(a), [fa, P, 2]** - Child of A, connected by a dashed arrow.
4. **D(a), [fa, 0, 3]** - Child of C, connected by a solid arrow.
5. **C(a), [fa, 0, 4]** - Child of C, connected by a solid arrow.
6. **E(a), [fa, P, 5]** - Child of D, connected by a solid arrow.
7. **C(a), [fa, P, 6]** - Child of D, connected by a solid arrow.
8. **D(a), [fa, 0, 7]** - Child of C, connected by a solid arrow.
9. **E(a), [fa, P, 11]** - Child of D, connected by a solid arrow.
10. **C(a), [fa, P, 12]** - Child of D, connected by a solid arrow.
11. **C(a), [fa, P, 9]** - Child of A, connected by a dashed arrow.
The parameters within the brackets vary, but 'fa' and 'P' appear frequently. The numerical values associated with each node are: 1, 2, 3, 4, 5, 6, 7, 9, 10, 11, 12.
### Key Observations
* The diagram shows a branching structure, with A as the root.
* There are two types of connections: solid arrows and dashed arrows. The dashed arrows connect A to its immediate children (B and C), while solid arrows represent further branching.
* The parameter 'fa' appears in most of the nodes.
* The numerical values seem to increase as you move down the tree, but not consistently.
### Interpretation
The diagram likely represents a function call graph or a similar dependency structure in a software system. The nodes represent functions, and the arrows indicate which functions call other functions. The parameters within the brackets could represent input arguments or internal state variables.
The distinction between solid and dashed arrows might indicate different types of function calls (e.g., direct vs. indirect calls, synchronous vs. asynchronous calls). The numerical values could represent execution order, cost, or some other metric associated with each function call.
The frequent appearance of 'fa' suggests it might be a common parameter or a default value. The increasing numerical values could indicate a sequential execution order or a depth-first traversal of the tree.
The diagram provides a visual representation of the relationships between different functions in a system, which can be useful for understanding the system's behavior, identifying potential bottlenecks, or debugging errors.
</details>
<details>
<summary>x8.png Details</summary>
### Visual Description
\n
## Diagram: Dependency/Flow Chart
### Overview
The image presents a diagram illustrating a sequence of dependencies or a flow of information. It consists of four labeled nodes (A, C, D, and E) connected by arrows indicating directionality. Each node is associated with a tuple containing a function call and a list of values.
### Components/Axes
The diagram consists of:
* **Nodes:** Labeled A, C, D, and E. Each node represents a function call with an argument 'a'.
* **Arrows:** Solid arrows indicating the direction of dependency or flow. A dashed arrow is present between A and C.
* **Tuples:** Each node is associated with a tuple in the format `(Function(a), [value1, value2, value3])`.
### Detailed Analysis or Content Details
The diagram shows the following dependencies and associated data:
1. **E(a), [fa, P, 11]**: The function E is called with argument 'a', and the associated list contains the values "fa", "P", and 11.
2. **D(a), [fa, 0, 10]**: The function D is called with argument 'a', and the associated list contains the values "fa", 0, and 10.
3. **C(a), [fa, P, 9]**: The function C is called with argument 'a', and the associated list contains the values "fa", "P", and 9. The arrow connecting C to A is dashed.
4. **A(a), [um, P, 1]**: The function A is called with argument 'a', and the associated list contains the values "um", "P", and 1.
The arrows indicate the following flow:
* E -> D
* D -> C
* C --(dashed)--> A
### Key Observations
* The functions called are A, C, D, and E.
* The argument passed to each function is 'a'.
* The lists associated with each function contain a mix of strings ("fa", "P", "um") and numbers (0, 9, 10, 11, 1).
* The dashed arrow between C and A suggests a different type of relationship than the solid arrows, potentially indicating a less direct or conditional dependency.
### Interpretation
This diagram likely represents a simplified dependency graph or a call stack in a program. The functions A, C, D, and E are executed in a specific order, with E being the starting point and A being the final destination (with a possible feedback loop indicated by the dashed arrow). The lists associated with each function could represent parameters, return values, or internal state information. The use of "fa", "P", "um" suggests these could be symbolic representations of data types or flags. The numerical values might represent quantities, indices, or other numerical data. The dashed arrow from C to A could indicate a recursive call or a conditional dependency where A is called based on the result of C. Without further context, it's difficult to determine the exact meaning of the diagram, but it clearly illustrates a sequence of operations and their interdependencies.
</details>
Figure 5. Left: A non-focused dialogue tree. Right: A focused dialogue tree $\mathcal{T}(\delta_{1})$ .
## 5. Results of the Paper
In this section, we study how to use a novel explanatory dialogue model to determine and explain the acceptance of a formula $\phi$ wrt argumentation semantics.
Intuitively, a successful dialogue for formula $\phi$ wrt argumentation semantics is a dialectical proof procedure for $\phi$ . To argue for the usefulness of the dialogue model, we will study winning conditions (âconditionsâ for short) for a successful dialogue to be sound and complete wrt argumentation semantics. To do so, we use dialogue trees. When the agent decides what to utter or whether a terminated dialogue is successful, it needs to consider the current dialogue tree and ensure that its new utterances will keep the tree fulfilling desired properties. Thus, the dialogue tree drawn from a dialogue can be seen as commitment store [23] holding information disclosed and used in the dialogue. Successful dialogues, in this sense, can be regarded as explanations for the acceptance of a formula.
Before continuing, we present preliminary notions/results to prove the soundness and completeness results.
### 5.1. Notions for Soundness and Completeness Results
Let us introduce notions that will be useful in the next sections. These notions include: potential argument obtained from a dialogue tree, collective attacks against a potential argument in a dialogue tree, and P-SAF drawn from a dialogue tree.
A potential argument is an argument obtained from a dialogue tree.
**Definition 5.1**
*A potential argument obtained from a dialogue tree $\mathcal{T}(\delta)$ is a sub-tree $\mathcal{T}^{s}$ of $\mathcal{T}(\delta)$ such that:
- all nodes in $\mathcal{T}^{s}$ have the same label (either P or O);
- if there is an utterance $(\_,\_,\texttt{{offer}}(\Delta,\alpha),\texttt{{id}})$ and a node $(\beta_{i},[\_,\texttt{{L}},\texttt{{id}}])$ in $\mathcal{T}^{s}$ with $\beta_{i}\in\Delta$ , then all the nodes $(\beta_{1},[\_,\texttt{{L}},\texttt{{id}}]),\ldots,(\beta_{m},[\_,\texttt{{L}} ,\texttt{{id}}])$ are in $\mathcal{T}^{s}$
- for every node $(\alpha,[\texttt{{nf}},\texttt{{L}},\_])$ in $\mathcal{T}^{s}$ , all its immediate children in $\mathcal{T}^{s}$ have the same identifier (they belong to a single utterance).
The formula $\phi$ in the root of $\mathcal{T}^{s}$ is the conclusion. The set of the formulas $H$ held by the descended nodes in $\mathcal{T}^{s}$ , i.e., $H=\{\beta\mid(\beta,[\texttt{{fa}},\ \_,\ \_])\text{ is a node in }\mathcal{T} ^{s}\}$ , is the support of $\mathcal{T}^{s}$ . A potential argument obtained from a dialogue tree is a proponent (opponent) argument if its nodes are labelled P (O, respectively).*
To shorten notation, we use the term âan argument for $\phi$ â instead of the term âan argument with the conclusion $\phi$ â.
**Example 5.2 (Continue Example4.4)**
*Figure 6 shows two potential arguments obtained from $\mathcal{T}(\delta)$ .*
Potential arguments correspond to the conventional P-SAF arguments.
**Lemma 5.3**
*A potential argument $\mathcal{T}^{s}$ corresponds to an argument for $\phi$ supported by $H$ as in conventional P-SAF (in Definition 3.1).*
* Proof*
This lemma is trivially true as a node in a potential argument can be mapped to a node in a conventional P-SAF argument (in Definition 3.1) by dropping the tag T and the identifier ID. â
We introduce collective attacks against a potential argument, or a sub-tree, in a dialogue tree. This states that a potential argument is attacked when there exist nodes within the tree that are children of the argument. Formally:
**Definition 5.4**
*Let $\mathcal{T}(\delta)$ be a dialogue tree and $\mathcal{T}^{s}$ be a potential argument obtained from $\mathcal{T}(\delta)$ . $\mathcal{T}^{s}$ is attacked iff there is a node $N=(\texttt{{L}},[\texttt{{T}},\_,\_])$ in $\mathcal{T}^{s}$ , with $\texttt{{L}}\in\{\texttt{{P}},\texttt{{O}}\}$ and $\texttt{{T}}\in\{\texttt{{fa}},\texttt{{nf}}\}$ , such that $N$ has children $M_{1},\ldots,M_{k}$ labelled by $\texttt{{L}}^{\prime}\in\{\texttt{{P}},\texttt{{O}}\}\setminus\{\texttt{{L}}\}$ in $\mathcal{T}(\delta)$ and the children have the same identifier. We say that the sub-trees rooted at $M_{j}$ ( $1\leq j\leq k$ ) attacks $\mathcal{T}^{s}$ .*
**Definition 5.5**
*(A) P-SAF drawn from $\mathcal{T}(\delta)$ is $\mathcal{AF}_{\delta}=(\texttt{{Arg}}_{\delta},\texttt{{Att}}_{\delta})$ , where
- $\texttt{{Arg}}_{\delta}$ is the set of potential arguments obtained from $\mathcal{T}(\delta)$ ;
- $\texttt{{Att}}_{\delta}$ contains the attacks between the potential arguments.*
Since $\mathcal{T}(\delta)$ is drawn from $\delta$ , we can say $\mathcal{AF}_{\delta}$ drawn from $\delta$ instead.
As in [43], two useful concepts that are used for our soundness result in the next sections are the defence set and the culprits of a dialogue tree.
**Definition 5.6**
*Given a dialogue tree $\mathcal{T}(\delta)$ ,
- The defence set $\mathcal{DE}(\mathcal{T}(\delta))$ is the set of all facts $\alpha$ in proponent nodes of the form $N=(\alpha,[\texttt{{fa}},\texttt{{P}},\_])$ such that $N$ is in a potential argument;
- The culprits $\mathcal{CU}(\mathcal{T}(\delta))$ is the set of facts $\beta$ in opponent nodes $N=(\beta,[\texttt{{fa}},\texttt{{O}},\_])$ such that $N$ has the child node $N^{\prime}=(\_,[\_,\texttt{{P}},\_])$ and $N$ and $N^{\prime}$ are in potential arguments.*
**Example 5.7**
*Figure 6 (Left) gives the focused dialogue tree drawn from the dialogue $D(\texttt{{Re}}(\texttt{{v}}))$ in Example 4.4. The defence set is $\{\texttt{{te}}(\texttt{{v}},\texttt{{KR}}),\texttt{{GC}}(\texttt{{KR}}), \texttt{{te}}(\texttt{{v}},\texttt{{KD}})\}$ ; the culprits are $\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),\texttt{{UC}}(\texttt{{KD}})\}$ .*
<details>
<summary>x9.png Details</summary>
### Visual Description
\n
## Diagram: Process Flow with Function Calls
### Overview
The image depicts a directed graph representing a process flow, likely a computational or logical sequence. The nodes represent function calls or states, and the arrows indicate transitions between them. Each node is labeled with a function name and associated data, enclosed in brackets. The diagram is titled "T(ÎŽ)" at the top-center.
### Components/Axes
The diagram consists of nodes and directed edges. The nodes are labeled with function names and data in the format: `function_name(arguments), [data_type, value, identifier]`. The edges are labeled with identifiers like `r3`, `c1`, `r6`, `c2`, `r4`, `r5`. There are no explicit axes or scales.
### Detailed Analysis or Content Details
Here's a breakdown of the nodes and transitions, moving from top to bottom:
1. **Top Node:** `Re(v), [nf, P, 1]`
2. **Transition:** `r3` leads to the next node.
3. **Second Node:** `FP(v), [nf, P, 2]`
4. **Transition:** `c1` splits into two paths.
5. **Third Node (Left Branch):** `te(v, KR), [fa, P, 3]`
6. **Fourth Node (Right Branch):** `GC(KR), [fa, P, 3]`
7. **Transition:** `c2` from `te(v, KR)` leads to the next node.
8. **Fifth Node:** `Le(v), [nf, P, 6]`
9. **Transition:** `r5` leads to the next node.
10. **Sixth Node:** `te(v, KD), [fa, P, 7]`
11. **Transition:** `r4` from `GC(KR)` splits into two paths.
12. **Seventh Node (Left Branch):** `TA(v), [nf, 0, 4]`
13. **Eighth Node (Right Branch):** `UC(KD), [fa, 0, 5]`
14. **Ninth Node:** `ta0f(v, KD), [fa, 0, 5]`
The data types appear to be:
* `nf`: Likely "not found" or a similar flag.
* `fa`: Likely "false" or a similar flag.
* `P`: A parameter or value.
* Numbers: Integer values.
The identifiers (1, 2, 3, 4, 5, 6, 7) likely represent step numbers or unique identifiers for each node.
### Key Observations
The diagram shows a branching process. The initial node `Re(v)` leads to `FP(v)`, which then splits into two parallel paths. One path involves `te(v, KR)` and `Le(v)`, ultimately leading to `te(v, KD)`. The other path involves `GC(KR)` and splits into `TA(v)` and `UC(KD)`, which then leads to `ta0f(v, KD)`. The diagram suggests a decision point at `FP(v)` and `GC(KR)`.
### Interpretation
This diagram likely represents a state machine or a workflow in a software system. The function calls suggest operations on variables `v`, `KR`, and `KD`. The data types and values indicate the status or results of these operations. The branching paths suggest conditional logic based on the outcomes of the function calls. The identifiers could be used for debugging or tracing the execution flow.
The diagram demonstrates a process that begins with `Re(v)` and proceeds through a series of function calls, potentially involving error handling (indicated by `nf`) and conditional branching. The final nodes `te(v, KD)` and `ta0f(v, KD)` suggest the process concludes with operations related to `KD`. The diagram is a visual representation of a complex algorithm or system behavior. It is not possible to determine the exact purpose of the process without further context.
</details>
<details>
<summary>x10.png Details</summary>
### Visual Description
\n
## Diagram: Tree-like Structure with Labeled Nodes
### Overview
The image depicts a tree-like diagram with nodes connected by branches. Each node contains a set of information enclosed in parentheses and square brackets. The branches are labeled with symbols representing transformations. The diagram appears to represent a hierarchical process or a series of transformations applied to a variable 'v'.
### Components/Axes
The diagram consists of:
* **Nodes:** Each node contains a tuple of information. The first element is a function applied to 'v' (or KR). The second element is a label (nf, fa). The third element is 'P'. The fourth element is a number (1, 2, or 3).
* **Branches:** Branches are labeled with 'Ï3' and 'Ï6', representing transformations.
* **Root Node:** (Re(v), [nf, P, 1])
* **Intermediate Node:** (FP(v), [nf, P, 2])
* **Leaf Nodes:** (te(v, KR), [fa, P, 3]) and (GC(KR), [fa, P, 3])
### Detailed Analysis or Content Details
The diagram can be described as follows:
1. **Root Node:** (Re(v), [nf, P, 1])
2. **Branch 1:** Connected to the root node, labeled 'Ï3', leads to the intermediate node.
3. **Intermediate Node:** (FP(v), [nf, P, 2])
4. **Branch 2:** Connected to the intermediate node, labeled 'Ï6', splits into two leaf nodes.
5. **Leaf Node 1:** (te(v, KR), [fa, P, 3])
6. **Leaf Node 2:** (GC(KR), [fa, P, 3])
The labels within the nodes are consistent in structure:
* The first element is a function: Re, FP, te, GC.
* The second element is a label: nf, fa.
* The third element is always 'P'.
* The fourth element is a number: 1, 2, 3.
### Key Observations
* The diagram represents a branching process starting from 'v' and ending at 'te(v, KR)' and 'GC(KR)'.
* The labels 'nf' and 'fa' might represent different states or properties.
* The numbers 1, 2, and 3 could indicate steps or levels in the process.
* The transformation 'Ï3' leads to 'FP(v)', while 'Ï6' splits the process into two paths.
* Both leaf nodes share the same label [fa, P, 3].
### Interpretation
The diagram likely represents a computational process or a logical derivation. 'v' is the initial input, and the functions Re, FP, te, and GC represent transformations applied to it. The labels 'nf' and 'fa' could indicate whether a certain condition is met or a specific property holds. The numbers 1, 2, and 3 might represent the order of operations or the depth of the derivation. The diagram suggests that the initial variable 'v' is transformed through a series of steps, ultimately leading to two possible outcomes: 'te(v, KR)' and 'GC(KR)'. The shared label [fa, P, 3] for the leaf nodes suggests that both outcomes share a common property or state. Without further context, it's difficult to determine the specific meaning of the functions and labels, but the diagram clearly illustrates a structured process with branching possibilities. The diagram is a visual representation of a mathematical or logical transformation.
</details>
<details>
<summary>x11.png Details</summary>
### Visual Description
\n
## Diagram: Tree-like Structure
### Overview
The image depicts a tree-like diagram representing a branching structure with labeled nodes. The diagram appears to represent a hierarchical relationship between different elements, possibly in a formal system or logic.
### Components/Axes
The diagram consists of nodes connected by branches. Each node contains a label enclosed in parentheses, followed by a bracketed list of values. The branches are labeled with "r4".
### Detailed Analysis or Content Details
The diagram has three nodes:
* **Top Node:** (TA(v), [nf, 0, 4])
* **Left Node:** (taUf(v, KD), [fa, 0, 5])
* **Right Node:** (UC(KD), [fa, 0, 5])
The top node is connected to the left and right nodes via branches labeled "r4".
### Key Observations
The left and right nodes share the same bracketed values: [fa, 0, 5]. The top node has different values: [nf, 0, 4]. The labels within the parentheses appear to be function or operator names with arguments.
### Interpretation
This diagram likely represents a derivation or transformation process within a formal system. The nodes represent states or expressions, and the branches represent the application of a rule or operation (r4). The bracketed values could represent properties or attributes of each state. The shared values in the left and right nodes suggest a common outcome or property resulting from the application of the rule. The differing value in the top node indicates a unique characteristic of the initial state. Without further context, it's difficult to determine the specific meaning of the labels and values, but the structure suggests a logical or computational process.
</details>
Figure 6. Left: A focused dialogue tree $\mathcal{T}(\delta)$ drawn from $D(\texttt{{Re}}(\texttt{{v}}))$ in Table 2. Right: Some potential argument obtained from $\mathcal{T}(\delta)$ .
### 5.2. Soundness Results
#### 5.2.1. Computing credulous acceptance
We present winning conditions for a credulously successful dialogue to prove whether a formula is credulously accepted under admissible/ preferred/ stable semantics.
Let us sketch the idea of a dialectical proof procedure for computing the credulous acceptance as follows: Assume that a (dispute) dialogue between an agent $a_{1}$ and $a_{2}$ in which $a_{1}$ persuades $a_{2}$ about its belief â $\phi$ is acceptedâ. Two agents take alternating turns in exchanging their arguments in the form of formulas. When the (dispute) dialogue progresses, we are increasingly building, starting from the root $\phi$ , a dialogue tree. Each node of such tree, labelled with either P or O, corresponds to an utterance played by the agent. The credulous acceptance of $\phi$ is proven if P can win the game by ending the dialogue in its favour according to a â last-word â principle.
To facilitate our idea, we introduce the properties of a dialogue tree: patient, last-word, defensive and non-redundant.
Firstly, we restrict dialogue trees to be patient. This means that agents wait until a potential argument has been fully constructed before beginning to attack it. Formally: A dialogue tree $\mathcal{T}(\delta)$ is patient iff for all nodes $N=(\_,[\texttt{{fa}},\_,\_])$ in $\mathcal{T}(\delta)$ , $N$ is in (the support of) a potential argument obtained from $\mathcal{T}(\delta)$ . Through this paper, the term âdialogue treesâ refers to patient dialogue trees.
We now present the âlast-wordâ principle to specify a winning condition for the proponent. In a dialogue tree, P wins if either P finishes the dialogue tree with the un-attacked facts (Item 1), or any attacks used by O have been attacked with valid counter attacks (Item 2). Formally:
**Definition 5.8**
*A focused dialogue tree $\mathcal{T}(\delta)$ is last-word iff 1. for all leaf nodes $N$ in $\mathcal{T}(\delta)$ , $N$ is the form of $(\_,[\texttt{{fa}},\texttt{{P}},\_])$ , and
1. if a node $N$ is of the form $(\_,[\texttt{{T}},\texttt{{O}},\_])$ with $\texttt{{T}}\in\{\texttt{{fa}},\texttt{{nf}}\}$ , then $N$ is in a potential argument and $N$ is properly attacked.*
In the above definition, we say that a node $N$ of a potential argument is attacked, meaning that $N$ has children labelled by P with the same identifier.
The definition of âlast-wordâ incorporates the requirement that a set of potential arguments $\mathcal{S}$ (supported by the defence set) attacks every attack against $\mathcal{S}$ . However, it does not include the requirement that $\mathcal{S}$ does not attack itself. This requirement is incorporated in the definition of defensive dialogue trees.
**Definition 5.9**
*A focused dialogue tree $\mathcal{T}(\delta)$ is defensive iff it is
- last-word, and
- no formulas $\Delta$ in opponent nodes belong to $\mathcal{DE}(\mathcal{T}(\delta))$ such that $\Delta\cup\mathcal{DE}(\mathcal{T}(\delta))$ is inconsistent.*
In admissible dialogue trees, nodes labelled P and O within potential arguments can have common facts when considering potential arguments that attack or defend others. However, potential arguments with nodes sharing common facts cannot attack proponent potential arguments whose facts are in the defence set. Let us show this in the following example.
**Example 5.10**
*Consider a query $q_{4}=A(a)$ to a KB $\mathcal{K}_{4}=(\mathcal{R}_{4},\mathcal{C}_{4},\mathcal{F}_{4})$ where
| | $\displaystyle\mathcal{R}_{4}=$ | $\displaystyle\emptyset$ | |
| --- | --- | --- | --- |
Consider the focused dialogue tree $\mathcal{T}(\delta_{i})$ (see Figure 7 (Left)) drawn from the focused sub-dialogue $\delta_{i}$ of a dialogue $D(A(a))=\delta$ . The defence set $\mathcal{DE}(\mathcal{T}(\delta_{i}))=\{A(a),C(a)\}$ ; the culprits $\mathcal{CU}(\mathcal{T}(\delta_{i}))=\{B(a),C(a)\}$ . We have $\mathcal{DE}(\mathcal{T}(\delta_{i}))\cap\mathcal{CU}(\mathcal{T}(\delta_{i})) =\{C(a)\}$ . It can seen that $\{C(a)\}\cup\mathcal{DE}(\mathcal{T}(\delta_{i}))$ is inconsistent. In other words, there exists a potential argument, say $A$ , such that $\{C(a)\}$ is the support of $A$ , and $A$ cannot attack any proponent argument supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ . Clearly, $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ and $\mathcal{CU}(\mathcal{T}(\delta_{i}))$ have the common formula, but the set of arguments supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ does not attack itself.*
<details>
<summary>x12.png Details</summary>
### Visual Description
\n
## Diagram: Tree-like Structure with Labeled Nodes
### Overview
The image depicts a tree-like diagram with five nodes, each labeled with a tuple containing an identifier (A, B, or C), a variable (a), and a bracketed list of three elements. Arrows indicate the direction of the tree's branching.
### Components/Axes
The diagram consists of nodes and directed edges (arrows). There are no explicit axes or scales. The nodes are labeled as follows:
* **(A(a), [fa, P, 3])** - Bottom-left node
* **(C(a), [fa, P, 3])** - Bottom-right node
* **(B(a), [fa, 0, 2])** - Middle node
* **(C(a), [fa, 0, 2])** - Top-right node
* **(A(a), [um, P, 1])** - Top node
### Detailed Analysis or Content Details
The diagram shows a branching structure.
* The bottom layer consists of two nodes: (A(a), [fa, P, 3]) and (C(a), [fa, P, 3]).
* These two nodes converge into a single node: (B(a), [fa, 0, 2]).
* The node (B(a), [fa, 0, 2]) then branches into two nodes: (C(a), [fa, 0, 2]) and (A(a), [um, P, 1]).
The labels within the brackets vary:
* `fa` appears frequently.
* `um` appears once.
* `P` appears in all labels.
* The numbers are 3, 0, 2, and 1.
### Key Observations
The diagram represents a hierarchical relationship between the nodes. The identifiers A, B, and C seem to represent different entities or states. The bracketed lists likely represent attributes or properties associated with each entity. The variable 'a' is consistent across all nodes.
### Interpretation
This diagram likely represents a decision tree or a state transition diagram. The nodes represent states, and the arrows represent transitions between states. The labels within the brackets could represent conditions or actions that trigger the transitions.
The presence of 'fa' and 'um' suggests different types of attributes or conditions. 'P' might be a constant or a common property. The numbers could represent probabilities, costs, or other quantitative values.
Without further context, it's difficult to determine the exact meaning of the diagram. However, it clearly illustrates a hierarchical structure with labeled nodes and directed transitions. The diagram suggests a process where two initial states (A and C) lead to a combined state (B), which then branches into two final states (C and A). The change from 'fa' to 'um' in the final node A could indicate a transformation or a different outcome.
</details>
<details>
<summary>x13.png Details</summary>
### Visual Description
\n
## Diagram: Sequence of Function Calls
### Overview
The image depicts a vertical sequence of function calls, represented as pairs of function names with arguments and associated data enclosed in square brackets. Arrows point upwards, indicating the flow of execution. The sequence appears to alternate between functions `A(a)` and `B(a)`.
### Components/Axes
The diagram consists of a series of function call expressions arranged vertically. Each expression has the following structure:
`(Function Name(argument), [data1, data2, data3])`
The functions involved are `A(a)` and `B(a)`.
The data within the square brackets varies for each call.
Arrows indicate the direction of the function call sequence.
### Detailed Analysis or Content Details
The sequence, from bottom to top, is as follows:
1. `(B(a), [fa, 0, 4])`
2. `(A(a), [fa, P, 3])`
3. `(B(a), [fa, 0, 2])`
4. `(A(a), [um, P, 1])`
5. `...` (Indicates the sequence continues beyond the visible portion)
The arguments to the functions are consistently `a`. The data within the brackets consists of strings (`fa`, `um`, `P`) and numbers (0, 1, 2, 3, 4).
### Key Observations
The sequence alternates between calls to `A(a)` and `B(a)`.
The first element within the brackets is frequently `fa`, but also includes `um`.
The second element within the brackets is frequently `P`.
The third element within the brackets is a numerical value that increases and then decreases (4, 3, 2, 1).
### Interpretation
This diagram likely represents a simplified call stack or execution trace of a program. The alternating calls to `A(a)` and `B(a)` suggest a recursive or iterative process where these two functions call each other. The data within the brackets could represent state variables or parameters that are modified during each function call. The `...` at the bottom indicates that the sequence continues, potentially infinitely or until a base case is reached. The changing numerical value (4, 3, 2, 1) might represent a counter or a depth level in a recursive call. The presence of `um` suggests a change in state or a different branch of execution. Without further context, it's difficult to determine the exact purpose of these functions and the meaning of the data they manipulate. However, the diagram clearly illustrates a sequential process with alternating function calls and evolving state information.
</details>
Figure 7. Left: A focused dialogue tree $\mathcal{T}(\delta_{i})$ . Right: An infinite dialogue tree.
From the above observation, it follows immediately that.
**Lemma 5.11**
*Let $\mathcal{T}(\delta)$ be a defensive dialogue tree. The set of proponent arguments (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ ) does not attack itself in the P-SAF drawn from $\delta$ .*
Consider the following dialogue to see why the ânon-redundantâ property is necessary.
**Example 5.12**
*Consider a query $q_{5}=A(a)$ to a KB $\mathcal{K}_{5}=(\mathcal{R}_{5},\mathcal{C}_{5},\mathcal{F}_{5})$ where
| | $\displaystyle\mathcal{R}_{5}=$ | $\displaystyle\emptyset$ | |
| --- | --- | --- | --- |
Initially, an argument $A_{1}$ asserts that â $A(a)$ is acceptedâ where $A(a)$ is at the P node. $A_{1}$ is attacked by $A_{2}$ by using $B(a)$ that is at the O node. $A_{1}$ counter-attacks $A_{2}$ by using $A(a)$ , then $A_{2}$ again attacks $A_{1}$ by using $B(a)$ , ad infinitum (see Figure 7 (Right)). Hence P cannot win. Since the grounded extension is empty, $A(a)$ is not groundedly accepted in the P-SAF, thus P should not win under the grounded semantics. Since $A(a)$ is credulously accepted in the P-SAF, we expect that P can win in a terminated dialogue under the credulous semantics.*
To ensure credulous acceptance, all possible opponent nodes must be accounted for. But if such a parent node is already in the dialogue tree, then deploying it will not help the opponent win the dialogues. To avoid this, we define a dialogue tree to be non-redundant.
**Definition 5.13**
*A focused dialogue tree $\mathcal{T}(\delta)$ is non-redundant iff for any two nodes $N_{1}=(\beta,[\texttt{{fa}},\texttt{{L}},\texttt{{id}}_{1}])$ and $N_{2}=(\beta,[\texttt{{fa}},\texttt{{L}},\texttt{{id}}_{2}])$ with $\texttt{{L}}\in\{\texttt{{P}},\texttt{{O}}\}$ and $N_{1}\neq N_{2}$ , if $N_{1}$ is in a potential argument $\mathcal{T}_{1}^{s}$ and $N_{2}$ is in a potential argument $\mathcal{T}_{2}^{s}$ , then $\mathcal{T}_{1}^{s}\neq\mathcal{T}_{2}^{s}$ .*
In Definition 5.13, when comparing two arguments, we compare their respective proof trees. Here, we only consider the formula and the tag of each node in the tree, disregarding the label and identifier of the node.
The following theorem establishes credulous soundness for admissible semantics.
theorem thmcredulous Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If there is a dialogue tree $\mathcal{T}(\delta_{i})$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ such that it is defensive and non-redundant, then
- $\delta$ is admissible-successful;
- $\phi$ is credulously accepted under adm in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ .
The proof of this theorem is in Appendix B.
We can define a notion of preferred-successful dialogue with a formula accepted under prf in the P-SAF framework drawn from the dialogue. Since every admissible set (of arguments) is necessarily contained in a preferred set (see [6, 25]), and every preferred set is admissible by definition, trivially a dialogue is preferred-successful iff it is admissible-successful. The following theorem is analogous to Theorem 5.13 for prf semantics.
theorem thmpreferred Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If there is a dialogue tree $\mathcal{T}(\delta_{i})$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ such that it is defensive and non-redundant, then $\delta$ is preferred-successful and $\phi$ is credulously accepted under prf in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ .
* Sketch*
The proof of this theory follows the fact that every preferred dialogue tree is an admissible dialogue tree. Thus, the proof of this theorem is analogous to those of Theorem 5.13. â
**Remark 5.14**
*We can similarly define a notion of stable dialogue trees for a formula accepted under stb in the P-SAF. Since stable and preferred sets coincide, trivially a dialogue tree is stable iff it is defensive and non-redundant. Thus we can use the result of Theorem 5.13 for stable semantics.*
#### 5.2.2. Computing grounded acceptance
We present winning conditions for a groundedly successful dialogue to determine grounded acceptance of a given formula. The conditions require that whenever O could advance any evidence, P still wins. This requirement is incorporated in dialogue trees being defensive. Note that credulously successful dialogues for computing credulous acceptance also require dialogue trees to be defensive (see in Theorem 5.13). However, the credulously successful dialogues cannot be used for computing the grounded acceptance, as shown by Example 5.12. In Example 5.12, it would be incorrect to infer from the depicted credulously successful dialogue that $A(a)$ is groundedly accepted as the grounded extension is empty. Note that the dialogue tree for $A(a)$ is infinite. From this observation, it follows that the credulously successful dialogues are not sound for computing grounded acceptance. Since all dialogue trees of a formula that is credulously accepted but not groundedly accepted can be infinite, we could detect this situation by checking if constructed dialogue trees are infinite. This motivates us to consider â finite â dialogue trees as a winning condition.
The following theorem establishes the soundness of grounded acceptance. theorem thmground Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If there is a dialogue tree $\mathcal{T}(\delta_{i})$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ such that it is defensive and finite, then
- $\delta$ is groundedly-successful;
- $\phi$ is groundedly accepted under grounded semantics in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ .
The proof of this theorem is in Appendix B.
#### 5.2.3. Computing sceptical acceptance
Inspired by [13], to determine the sceptically acceptance of an argument for $\phi$ , we verify the following: (1) There exists an admissible set of arguments $S$ that includes the argument for $\phi$ ; (2) For each argument $A$ attacking $S$ , there exists no admissible set of arguments containing $A$ . These steps can be interpreted through the following winning conditions for a sceptical successful dialogue to compute the sceptical acceptance of $\phi$ :
1. P wins the game by ending the dialogue,
1. none of O wins by the same line of reasoning.
This perspective allows us to introduce a notion of ideal dialogue trees.
**Definition 5.15**
*A defensive and non-redundant dialogue tree $\mathcal{T}(\delta)$ is ideal iff none of the opponent arguments obtained from $\mathcal{T}(\delta)$ belongs to an admissible set of potential arguments in $\mathcal{AF}_{\delta}$ drawn from $\mathcal{T}(\delta)$ .*
The following result sanctions the soundness of sceptical acceptance.
theoremthmsceptical Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If there is a dialogue tree $\mathcal{T}(\delta)$ drawn from $\delta$ such that it is ideal, then
- $\delta$ is sceptically-successful;
- $\phi$ is sceptically accepted under sem in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ , where $\texttt{{sem}}\in\{\texttt{{adm}},\texttt{{prf}},\texttt{{stb}}\}$ .
The proof of this theorem is in Appendix B.
### 5.3. Completeness Results
We now present completeness. In this work, dialogues viewed as dialectical proof procedures are sound but not always complete in general. The reason is that the dialectical proof procedures might enter a non-terminating loop during the process of argument constructions, which leads to the incompleteness wrt the admissibility semantics. To illustrate this, we refer to Example 1 using logic programming in [4] for an explanation. We also provide another example using $\text{Datalog}^{\pm}$ .
**Example 5.16**
*Consider a query $q_{6}=P(a)$ to a $\text{Datalog}^{\pm}$ KB $\mathcal{K}_{6}=(\mathcal{R}_{6},\mathcal{C}_{6},\mathcal{F}_{6})$ where
| | $\displaystyle\mathcal{R}_{6}=$ | $\displaystyle\{r_{1}:P(x)\rightarrow Q(x),r_{2}:Q(x)\rightarrow P(x)\}$ | |
| --- | --- | --- | --- |
The semantics of the corresponding P-SAF $\mathcal{AF}_{4}$ are determined by the arguments illustrated in Figure 8. The result should state that â $P(a)$ is a possible answerâ as the argument $B_{1}$ for $P(a)$ is credulously accepted under the admissible sets $\{B_{1}\}$ and $\{B_{2}\}$ of $\mathcal{AF}_{4}$ . But the dialectical proof procedures fail to deliver the admissible set $\{B_{1}\}$ wrt $\mathcal{AF}_{4}$ as they could not overcome the non-termination of the process to construct an argument $B_{1}$ for $P(a)$ due to the âinfinite loopâ.*
<details>
<summary>x14.png Details</summary>
### Visual Description
\n
## Diagram: State Transition Diagram with Infinite Loops
### Overview
The image depicts a state transition diagram illustrating two blocks, B1 and B2, with a repeating sequence of states and transitions within B1. The diagram highlights the presence of infinite loops within the system.
### Components/Axes
The diagram consists of two labeled blocks:
* **B1:** Located on the left side of the image.
* **B2:** Located on the right side of the image.
Within B1, the following states and transitions are visible:
* **P(a)**: A state labeled "P(a)".
* **r2**: A transition labeled "r2".
* **Q(a)**: A state labeled "Q(a)".
* **r1**: A transition labeled "r1".
* The sequence P(a) -> r2 -> Q(a) -> r1 repeats infinitely.
B2 contains a single state:
* **R(a)**: A state labeled "R(a)".
A curved bracket with the text "infinite loops" points to the repeating sequence of states within B1. An ellipsis (".....") indicates the continuation of the loop.
### Detailed Analysis / Content Details
The diagram shows a clear flow within block B1:
1. The system starts in state P(a).
2. It transitions to state Q(a) via transition r2.
3. It transitions to state P(a) via transition r1.
4. This sequence repeats indefinitely, forming an infinite loop.
Block B2, containing state R(a), appears isolated and does not interact with B1. There are no transitions shown connecting B1 and B2.
### Key Observations
* The primary feature of the diagram is the infinite loop within B1.
* B2 is disconnected from the loop and appears to represent an independent state or system.
* The diagram does not provide any information about the conditions that trigger the transitions (r1 and r2) or the meaning of the functions P(a), Q(a), and R(a).
* The diagram is purely structural, showing the possible states and transitions without specifying any timing or probabilities.
### Interpretation
The diagram likely represents a system with a potential for indefinite cycling within a specific component (B1). The infinite loop suggests a lack of exit conditions or a design flaw that prevents the system from reaching a stable state. The isolated block B2 could represent a separate, unrelated part of the system or a potential destination state that is never reached due to the loop in B1.
The diagram is a simplified representation and lacks details about the underlying mechanisms. It serves as a visual warning about the possibility of infinite loops and the need for careful design to ensure system stability. The functions P(a), Q(a), and R(a) likely represent operations or processes, but their specific meanings are not revealed by the diagram. The transitions r1 and r2 could be triggered by events, conditions, or simply time. Without further information, it is difficult to determine the exact behavior of the system.
</details>
Figure 8. Arguments of $\mathcal{AF}_{4}$
Intuitively, since the dialogues as dialectical proof procedures (implicitly) incorporate the computation of arguments top-down, the process of argument construction should be finite (also known as finite tree-derivations in the sense of Definition 3.1) to achieve the completeness results. Thus, we restrict the attention to decidable logic with cycle-restricted conditions that its corresponding P-SAF framework produces arguments to be computed finitely in a top-down fashion. For example, given a $\text{Datalog}^{\pm}$ KB $\mathcal{K}=(\mathcal{R},\mathcal{C},\mathcal{F})$ , the dependency graph of the KB as defined in [73] consists of the vertices representing the atoms and the edges from an atom $u$ to $v$ iff $v$ is obtained from $u$ (possibly with other atoms) by the application of a rule in $\mathcal{R}$ . The intuition behind the use of the dependency graph is that no infinite tree-derivation exists if the dependency graph of KB is acyclic. By restricting such acyclic dependency graph condition, the process of argument construction in the corresponding P-SAF of the KB $\mathcal{K}$ will be finite, which leads to the completeness of the dialogues wrt argumentation semantics. The following theorems show the completeness of credulous acceptances wrt admissible semantics.
theoremcompadm Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If $\phi$ is credulously accepted under adm in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ ) and $\delta$ is admissible-successful, then there is a defensive and non-redundant dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ .
The proof of this theorem is in Appendix C.
The following theorem is analogous to Theorem 8 for preferred semantics. theoremcomppreferred Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If $\phi$ is credulously accepted under prf in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ ) and $\delta$ is preferred-successful, then there is a defensive and non-redundant dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ .
* Sketch*
The proof of this theory follows the fact that every preferred-successful dialogue is an admissible-successful dialogue. Thus, the proof of this theorem is analogous to those of Theorem 8. â
Theorem 8 presents the completeness of grounded acceptances. theoremcompground Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If $\phi$ is groundedly accepted under grd in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ ) and $\delta$ is groundedly-successful, then there is a defensive and finite dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ .
The proof of this theorem is in Appendix C.
Theorem 8 presents the completeness of sceptical acceptances.
theoremcompsceptical Let $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ . If $\phi$ is sceptically accepted under sem in $\mathcal{AF}_{\delta}$ drawn from $\delta$ (supported by $\mathcal{DE}(\mathcal{T}(\delta))$ ), where $\texttt{{sem}}\in\{\texttt{{adm}},\texttt{{prf}},\texttt{{stb}}\}$ , and $\delta$ is sceptically-successful, then there is an ideal dialogue tree $\mathcal{T}(\delta)$ for $\phi$ drawn from $\delta$ .
The proof of this theorem is in Appendix C.
### 5.4. Results for a Link between Inconsistency-Tolerant Reasoning and Dialogues
In Section 5.2 and 5.3, we demonstrated the use of dialogue trees to determine the acceptance of a formula in the P-SAF drawn from the dialogue tree. As a direct corollary of Theorem 3.14 - 8, we show how to determine and explain the entailment of a formula in KBs by using dialogue trees, which was the main goal of this paper.
**Corollary 5.17**
*Let $\mathcal{K}$ be a KB, $\phi$ be a formula in $\mathcal{L}$ . Then $\phi$ is entailed in
- some maximal consistent subset of $\mathcal{K}$ iff there is a defensive and non-redundant dialogue tree $\mathcal{T}(\delta)$ for $\phi$ .
- the intersection of maximal consistent subsets of $\mathcal{K}$ iff there is a defensive and finite dialogue tree $\mathcal{T}(\delta)$ for $\phi$ .
- all maximal consistent subsets of $\mathcal{K}$ iff there is an ideal dialogue tree $\mathcal{T}(\delta)$ for $\phi$ .*
## 6. Summary and Conclusion
We introduce a generic framework to provide a flexible environment for logic argumentation, and to address the challenges of explaining inconsistency-tolerant reasoning. Particularly, we studied how deductive arguments, DeLP, ASPIC/ ASPIC+ without preferences, flat or non-flat ABAs and sequent-based argumentation are instances of P-SAF frameworks. (Detailed discussions can be found after Definition 3.1 and 3.5). However, different perspectives were considered as follows.
Regarding deductive arguments and DeLP, our work extends these approaches in several ways. First, the usual conditions of minimality and consistency of supports are dropped. This offers a simpler way of producing arguments and identifying them. Second, like ABAs, the P-SAF arguments are in the form of tree derivations to show the structure of the arguments. This offer aims to (1) clarify the argument structure, and (2) enhance understanding of intermediate reasoning steps in inconsistency-tolerant reasoning in, for instance, $\text{Datalog}^{\pm}$ and DL.
Similar to ânon-flatâ ABAs, the P-SAF framework uses the notion of CN to allow the inferred assumptions being conflicting. In contrast, âflatâ ABAs ignore the case of the inferred assumptions being conflicting. Moreover, by using collective attacks, the P-SAF framework is sufficiently general to model n-ary constraints, which are not yet addressed in ânon-flatâ ABAs and ASPIC/ ASPIC+ without preferences. Like our approach, contrapositive ABAs in [65, 63] provide an abstract view for logical argumentation, in which attacks are defined on the level assumptions. However, since a substantial part of the development of the theory of contrapositive ABA is focused on contrapositive propositional logic, we have considered the logic of ABA as being given by $\overline{\texttt{{CN}}}_{s}$ and these contrapositive ABAs being simulated in our setting, see Section 3.2. In Section 3.2, we showed how sequent-based argumentation can fit in the P-SAF setting. While our work can be applied to first-order logic, sequent-based argumentation leaves the study of first-order formalisms for further research.
The work of [71] proposed the use of Tarski abstract logic in argumentation that is characterized simply by a consequence operator. However, many logics underlying argumentation systems, like ABA or ASPIC systems, do not always impose the absurdity axiom. A similar idea of using consequence operators can be found in the work of [52]. When a consequence operation is defined by means of â models â, inference rule steps are implicit within it. If arguments are defined by consequence operators, then the structure of arguments is often ignored, which makes it difficult to clearly explain the acceptability of the arguments. These observations motivate the slight generalizations of Tarskiâs abstract logic, in which we defined consequence operators in a proof-theoretic manner, inspired by the approach of [72], with minimal properties.
As we have studied here, we introduced an alternative abstract approach for logical argumentation and showed the connections between our framework and the state-of-the-art argumentation frameworks. However, we should not claim any framework as better than those, or vice versa. Rather, the choice of an argumentation framework using specific logic should depend on the needs of the application.
Finally, this paper is the first investigation of dialectical proof procedures to compute and explain the acceptance wrt argumentation semantics in the case of collective attacks. The dialectical proof procedures address the limits of the paper [52], i.e., it is not easy to understand intermediate reasoning steps in reasoning progress with (inconsistent) KBs.
The primary message of this paper is that we introduce a generic argumentation framework to address the challenge of explaining inconsistency-tolerant reasoning in KBs. This approach is defined for any logic involving reasoning with maximal consistent subsets, therefore, it provides a flexible environment for logical argumentation. To clarify and explain the acceptance of a sentence with respect to inconsistency-tolerant semantics, we present explanatory dialogue models that can be viewed as dialectic-proof procedures and connect the dialogues with argumentation semantics. The results allow us to provide dialogical explanations with graphical representations of dialectical proof trees. The dialogical explanations are more expressive and intuitive than existing explanation formalisms.
Our approach has been studied from a theoretical viewpoint. From practice, especially, from a human-computer interaction perspective, we will perform experiments with our approach in real-data applications. We then qualitatively evaluate our explanation by human evaluation. It would be interesting to analyze the complexity of computing the explanations empirically and theoretically.
## Appendix A Preliminaries
To prove the soundness and complete results, we sketch out a general strategy as follows:
1. Our proof starts with the observation that a dialogue $\delta$ for a formula $\phi$ can be seen as a collection of several (independent) focused sub-dialogues $\delta_{1},\ldots,\delta_{n}$ . The dialogue tree $\mathcal{T}(\delta_{i})$ drawn from $\delta_{i}$ is a subtree of $\mathcal{T}(\delta)$ drawn from the sub-dialogue $\delta$ , and it corresponds to the abstract dialogue tree that has root an argument with conclusion $\phi$ . (The notion of abstract dialogue tree can be found in [52]). Thus it is necessary to consider a correspondence principle that links dialogue trees to abstract dialogue trees. The materials for this step can be found in Section A.2 and A.3.
1. The correspondence principle allows to utilize the results of abstract dialogue trees in [[52], Corollary 1] to prove the soundness results. We extend Corollary 1 of [52] to prove the completeness results.
The proof of the soundness and completeness results depends on some notions and results that we describe next.
**Notation A.1**
*Let $\mathcal{K}$ be a KB, $\mathcal{X}\subseteq\mathcal{K}$ be a set of facts and $\mathcal{S}\subseteq\texttt{{Arg}}_{\mathcal{K}}$ be a set of arguments induced from $\mathcal{K}$ . Then,
- $\texttt{{Args}}(\mathcal{X})=\{A\in\texttt{{Arg}}_{\mathcal{K}}\mid\texttt{{ Sup}}(A)\subseteq\mathcal{X}\}$ are the set of arguments generated by $\mathcal{X}$ ,
- $\texttt{{Base}}(\mathcal{S})=\underset{A\in\mathcal{S}}{\bigcup}\texttt{{Sup}} (A)$ are the set of supports of arguments in $\mathcal{S}$ ,
- An argument $B$ is a subargument of argument $A$ iff $\texttt{{Sup}}(B)\subseteq\texttt{{Sup}}(A)$ . We denote the set of subarguments of $A$ as $\texttt{{Subs}}(A)$ .*
### A.1. Abstract Dialogue Trees and Abstract Dialogue Forests
We observe that a formula $\phi$ can have many arguments whose conclusion is $\phi$ . Thus a dialogue tree with root $\phi$ can correspond to one, none, or multiple abstract dialogue trees, one for each argument for $\phi$ . We call this set of abstract dialogue trees an abstract dialogue forest. The following one presents a definition of abstract dialogue forests and reproduces a definition of abstract dialogue trees (analogous to Definition 8 in [52]). Formally:
**Definition A.2 (Abstract dialogue forests)**
*Let $\mathcal{AF}_{\delta}=(\texttt{{Arg}}_{\delta},\texttt{{Att}}_{\delta})$ be the P-SAF drawn from a dialogue $D(\phi)=\delta$ . An abstract dialogue forest (obtained from $\mathcal{AF}_{\delta}$ ) for $\phi$ is a set of abstract dialogue trees, written $\mathcal{F}_{\texttt{{G}}}(\phi)=\{\mathcal{T}^{1}_{\texttt{{G}}},\ldots, \mathcal{T}^{h}_{\texttt{{G}}}\}$ , such that: For each abstract dialogue tree $\mathcal{T}^{j}_{\texttt{{G}}}$ ( $j=1,\ldots,h$ ), - the root of $\mathcal{T}^{j}_{\texttt{{G}}}$ is the proponent argument (in $\texttt{{Arg}}_{\delta}$ ) with the conclusion $\phi$ ,
- if a node $A$ in $\mathcal{T}^{j}_{\texttt{{G}}}$ is a proponent argument (in $\texttt{{Arg}}_{\delta}$ ), then all its children (possibly none) are opponent arguments (in $\texttt{{Arg}}_{\delta}$ ) that attack $A$
- if a node $A$ in $\mathcal{T}^{j}_{\texttt{{G}}}$ is an opponent argument (in $\texttt{{Arg}}_{\delta}$ ), then exactly one of the following is true: (1) $A$ has exactly one child, and this child is a proponent argument (in $\texttt{{Arg}}_{\delta}$ ) that attacks $A$ ; (2) $A$ has more than one child, and all these children are proponent argument (in $\texttt{{Arg}}_{\delta}$ ) that collectively attacks $A$ .*
**Remark A.3**
*We call the abstract dialogue tree that has root an argument with conclusion $\phi$ an abstract dialogue tree for $\phi$ .*
Fix an abstract dialogue forest $\mathcal{F}_{\texttt{{G}}}(\phi)=\{\mathcal{T}^{1}_{\texttt{{G}}},\ldots, \mathcal{T}^{h}_{\texttt{{G}}}\}$ . For such abstract dialogue tree $\mathcal{T}^{j}_{\texttt{{G}}}$ ( $i=1,\ldots,h$ ), we adopt the following conventions:
- Let $\mathcal{B}_{1}$ be the set of all proponent arguments in $\mathcal{T}^{j}_{\texttt{{G}}}$ . $\mathcal{DE}(\mathcal{T}^{j}_{\texttt{{G}}})=\{\alpha\mid\forall A\in\mathcal{ B}_{1},\alpha\in\texttt{{Sup}}(A)\}\subseteq\mathcal{F}$ is the defence set of $\mathcal{T}^{j}_{\texttt{{G}}}$ , i.e. the set of facts in the support of the arguments in $\mathcal{B}_{1}$ .
- Similarly, let $\mathcal{B}_{2}$ be the set of all opponent arguments in $\mathcal{T}^{j}_{\texttt{{G}}}$ . $\mathcal{CU}(\mathcal{T}^{j}_{\texttt{{G}}})=\{\beta\mid\forall B\in\mathcal{B }_{2},\beta\in\texttt{{Sup}}(B)\}\subseteq\mathcal{F}$ is the culprit set of $\mathcal{T}^{j}_{\texttt{{G}}}$ , i.e. the set of facts in support of the arguments in $\mathcal{B}_{2}$ .
We reproduce a definition of admissible abstract dialogue trees given in [52]. This notion will be needed for Section A.3.
**Definition A.4 (Admissible abstract dialogue trees)**
*An abstract dialogue tree for $\phi$ is said to admissible iff the proponent wins and no argument labels both a proponent and an opponent node.*
Intuitively, in an abstract dialogue tree, a proponent wins if either the tree ends with arguments labelled by proponent nodes or every argument labelling an opponent node has a child.
### A.2. Partitioning a Dialogue Tree into Focused Substrees
This section shows how to partition a dialogue tree $\mathcal{T}(\delta)$ into focused subtrees of $\mathcal{T}(\delta)$ . We will need this result to prove soundness and completeness results.
We observe that a dialogue $D(\phi)=\delta$ , from which the dialogue tree $\mathcal{T}(\delta)$ is drawn, may contain one, none, or multiple focused sub-dialogues $\delta_{i}$ of $\delta$ . Each dialogue tree $\mathcal{T}(\delta_{i})$ drawn from the focused sub-dialogue $\delta_{i}$ is a subtree of $\mathcal{T}(\delta)$ and focused. This is proven in the following lemma.
**Lemma A.5**
*Let $\mathcal{T}(\delta)$ be a dialogue tree (with root $\phi$ ) drawn from a dialogue $D(\phi)=\delta$ . Every focused subtree of $\mathcal{T}(\delta)$ with root $\phi$ is the dialogue tree drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ .*
* Proof*
All the subtrees considered in this proof are assumed to have root $\phi$ . The proof proceeds as follows:
1. First, we construct the set of focused dialogue subtrees of $\mathcal{T}(\delta)$
1. Second, we show that each focused subtree $\mathcal{T}(\delta_{i})$ of $\mathcal{T}(\delta)$ is drawn from a focused sub-dialogue $\delta_{i}$ of $\delta$ . Let $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ be all the focused subtrees contained in $\mathcal{T}(\delta)$ with root $\phi$ . Each focused subtree is obtained in the following way: First, choose a single utterance at the root and discard the subtrees corresponding to the other utterances at the root. Then proceed (depth first) and for each potential argument labelled O with children labelled P, choose a single identifier and select among them those (and only those) with that identifier; discard the other children labelled P (which have a different identifier) and the corresponding subtrees. By Definition 4.5, every focused subtree can be obtained in this way. 2. We next prove (2) by showing the construction of the focused sub-dialogue $\delta_{i}$ that draws $\mathcal{T}(\delta_{i})$ . Given $m$ dialogue trees $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ constructed from $\mathcal{T}(\delta)$ , the focused sub-dialogue $\delta_{i}$ ( $1\leq i\leq m$ ) drawing the dialogue tree $\mathcal{T}(\delta_{i})$ is constructed as follows: - $\delta_{i}$ is initialised to empty;
- for each node $\psi,[\_,\_,\texttt{{id}}])=N$ in $\mathcal{T}(\delta_{i})$ ,
- if $u_{id}=(\_,\ \texttt{{ta}},\ \_,\ \texttt{{id}})$ is in $\delta$ but not in $\delta_{i}$ , then add $u_{id}$ to $\delta_{i}$ ;
- let $u_{\texttt{{ta}}}$ be the utterance in $\delta$ ; if $u_{\texttt{{ta}}}$ is the target utterance of $u_{\texttt{{id}}}$ , then add $u_{\texttt{{ta}}}$ to $\delta_{i}$ ;
- Sort $\delta_{i}$ in the order of utterances $ID$ . It is easy to see that each $\delta_{i}$ constructed as above is a focused sub-dialogue of $\delta$ (by the definition of focused sub-dialogues in Definition 4.2), and $\mathcal{T}(\delta_{i})$ is drawn from $\delta_{i}$ . Thus (2) is proved. â
### A.3. Transformation from Dialogue Trees into Abstract Dialogue Trees
The following correspondence principle allows to translate dialogue trees into abstract dialogue trees and vice versa.
**Remark A.6**
*Recall that a dialogue tree for $\phi$ has root $\phi$ , while an abstract dialogue tree for $\phi$ has root an argument for $\phi$ .*
**Theorem A.7 (Correspondence principle)**
*Let $\phi\in\mathcal{L}$ be a formula. Then: 1. For every defensive and non-redudant dialogue tree $\mathcal{T}(\delta)$ for $\phi$ , there exists an admissible abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}})\subseteq\mathcal{DE}(\mathcal{T}( \delta))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})\subseteq\mathcal{CU}(\mathcal{T}( \delta))$ .
1. For every admisslbe abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ for $\phi$ , there exists a defensive and non-redundant dialogue tree $\mathcal{T}(\delta)$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}(\delta))\subseteq\mathcal{DE}(\mathcal{T}_{\texttt{{G }}})$ and $\mathcal{CU}(\mathcal{T}(\delta))\subseteq\mathcal{CU}(\mathcal{T}_{\texttt{{G }}})$ .*
* Proof*
We prove the theorem by transforming dialogue trees into abstract dialogue trees and vice versa. 1. The transformation from dialogue trees into abstract dialogue trees Given a defensive and non-redundant dialogue tree $\mathcal{T}(\delta)$ with root $\phi$ , its equivalent abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ for an argument for $\phi$ in $\mathcal{T}_{\texttt{{G}}}^{1},\ldots,\mathcal{T}_{\texttt{{G}}}^{h}$ is constructed inductively as follows: 1. Modify $\mathcal{T}(\delta)$ by adding a new flag ( $0 0$ or $1$ ) to nodes in $\mathcal{T}(\delta)$ and initialise $0 0$ for all nodes; a node looks like $(\_,[\_,\_,\_])-0$ . The obtained tree is $\mathcal{T}^{\prime}(\delta)$ .
1. $\mathcal{T}_{\texttt{{G}}}$ is $\mathcal{T}_{\texttt{{G}}}^{h}$ in the sequence $\mathcal{T}_{\texttt{{G}}}^{1},\ldots,\mathcal{T}_{\texttt{{G}}}^{h}$ constructed inductively as follows:
1. Let $A$ be the potential argument drawn from $\mathcal{T}(\delta)$ that contains root $\phi$ . $\mathcal{T}_{\texttt{{G}}}^{1}$ contains exactly one node that holds $A$ and is labelled by P. Set the nodes in $\mathcal{T}^{\prime}(\delta)$ that are in $A$ to $1$ . The obtained tree is $\mathcal{T}^{\prime}_{1}(\delta)$ .
1. Let $\mathcal{T}_{\texttt{{G}}}^{k}$ be the $k$ -th tree, with $1\leq k\leq h$ . $\mathcal{T}^{k+1}_{\texttt{{G}}}$ is expanded from $\mathcal{T}^{k}_{\texttt{{G}}}$ by adding nodes $(\texttt{{L}}:\ B_{j})$ with $\texttt{{L}}\in\{\texttt{{P}},\texttt{{O}}\}$ .
For each node $(\texttt{{L}}:\ B_{j})$ , $B_{j}$ is a potential argument drawn from $\mathcal{T}^{\prime}_{k}(\delta)$ , which is a child of $C$ - another potential argument drawn from $\mathcal{T}^{\prime}_{k}(\delta)$ , such that:
- there is at least one node in $B_{j}$ that is assigned $0 0$ ;
- the root of $B_{j}$ has a parent node $t$ in $\mathcal{T}^{\prime}_{k}(\delta)$ such that the flag of $t$ is $1$ and $t$ is in $C$ ;
- if the root of $B_{j}$ is labelled by P, then L is P. Otherwise, L is O.
- set all nodes in $\mathcal{T}^{\prime}_{k}(\delta)$ that are also in $B_{j}$ to 1. The obtained tree is $\mathcal{T}^{\prime}_{k+1}(\delta)$ .
1. $h$ is the smallest index s.t there is no node in $\mathcal{T}^{\prime}_{h}(\delta)$ where its flag is $0 0$ . $\mathcal{T}_{\texttt{{G}}}$ is constructed as follows: - Every node of $\mathcal{T}_{\texttt{{G}}}=\mathcal{T}_{\texttt{{G}}}^{h}$ includes a potential argument. For each potential argument, there is a unique node in $\mathcal{T}_{\texttt{{G}}}$ . Each node is labelled P or O as potential arguments drawn from $\mathcal{T}(\delta)$ are labelled either P or O.
- The root of $\mathcal{T}_{\texttt{{G}}}$ includes the potential argument for $\phi$ of the dialogue and labelled P by constructing $\mathcal{T}(\delta)$ .
- Since $\mathcal{T}(\delta)$ is defensive, by Definition 5.9, it is focused and patient. Thus there is only one way of attacking a potential argument labelled by O. Since $\mathcal{T}(\delta)$ is defensive, by Definition 5.9, it is last-word. Then there is no un-attacked (potential) argument labelled by O. From the above, it follows that every O node has exactly one P node as its child.
- Since $\mathcal{T}(\delta)$ is non-redundant, by Definition 5.13, no potential argument labels O and P. Recall that, in $\mathcal{T}_{\texttt{{G}}}$ , the potential arguments labelling P (O, respectively) are called proponent arguments (opponent arguments, respectively). It can be seen that $\mathcal{T}_{\texttt{{G}}}$ has the following properties:
- the root is the proponent argument for $\phi$ .
- the O node has either exactly one child holding one proponent argument that attacks it or children holding the proponent arguments that collectively attack it.
- all leaves are nodes labelled by P, namely P wins and there is no node labelled by both P and O. It follows immediately that $\mathcal{T}_{\texttt{{G}}}$ is an admissible abstract dialogue tree (by the definition of abstract dialogue trees in Definition A.2 and Definition A.4). Since $\mathcal{T}_{\texttt{{G}}}$ contains the same potential arguments as $\mathcal{T}(\delta)$ and the arguments have the same $\texttt{{P}}/\texttt{{O}}$ labelling in both $\mathcal{T}_{\texttt{{G}}}$ and $\mathcal{T}(\delta)$ , we have $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}})=\mathcal{DE}(\mathcal{T}(\delta))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})=\mathcal{CU}(\mathcal{T}(\delta))$ . 2. The transformation from abstract dialogue trees into dialogue trees We first need to introduce some new concepts that together constitute the dialogue tree.
**Definition A.8 (Support trees)**
*A support tree of a formula $\alpha$ is defined as follows:
1. The root is a proponent node labelled by $\alpha$ .
1. Let $N$ be a proponent node labelled by $\sigma$ . If $\sigma$ is a fact, then either $N$ has no children, or $N$ has children that are opponent nodes labelled by $\beta_{k}$ , $k=1,\ldots,n$ such that $\{\beta_{k}\}\cup\{\sigma\}$ is inconsistent. If $\sigma$ is a non-fact, then one of the following holds:
- either (1) $N$ has children that are proponent nodes labelling $\omega_{l}$ , $l=1,\dots,m$ , such that $\sigma\in\texttt{{CN}}(\{\omega_{l}\})$ ,
- or (2) $N$ has children that are opponent nodes labelling $\beta_{k}$ , $k=1,\ldots,n$ , such that $\{\beta_{k}\}\cup\{\sigma\}$ is inconsistent,
- or both (1) and (2) hold.*
**Definition A.9 (Context trees)**
*A context tree of a formula $\alpha$ is defined as follows:
1. The root is an opponent node labelled by $\alpha$ .
1. Let $N$ be an opponent node labelled by $\sigma$ . If $\sigma$ is a fact, then $N$ has children that are proponent nodes labelled by $\beta_{k}$ , with $k=1,\ldots,n$ , such that $\{\beta_{k}\}\cup\{\sigma\}$ is inconsistent and the children have the same identify The condition of âchildren having the same identifyâ ensure that a potential argument is attacked by exactly one potential argument if $k=1$ or collectively attacked by one set of potential arguments if $k>1$ .. If $\sigma$ is a non-fact, then one of the following holds:
- either (1) $N$ has children that are opponent nodes labelled by $\omega_{l}$ , with $l=1,\dots,m$ , such that $\sigma\in\texttt{{CN}}(\{\omega_{l}\})$ ,
- or (2) $N$ has children that are proponent nodes labelling $\beta_{k}$ , with $k=1,\ldots,n$ , such that $\{\beta_{k}\}\cup\{\sigma\}$ is inconsistent and the children have the same identify,
- or both (1) and (2) hold.*
Now we prove the translation from abstract dialogue trees to dialogue trees. Given an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ for $\phi$ , its equivalent focused subtree $\mathcal{T}(\delta_{i})$ of a dialogue tree $\mathcal{T}(\delta)$ for $\phi$ is constructed inductively as follows: Let $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}})$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})$ be the defence set and the set of culprits of $\mathcal{T}_{\texttt{{G}}}$ , respectively. For each $\alpha\in\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})$ , let $arg(\beta_{k})$ , with $k=1,\ldots,n$ , be a set of arguments for $\beta_{k}$ labelling nodes in $\mathcal{T}_{\texttt{{G}}}$ such that $\{\beta_{k}\}\cup\{\alpha\}$ is inconsistent. If $k=1$ , then there exists a single argument for $\beta$ that attacks an argument including $\alpha$ . We say that an argument including $\alpha$ is an argument whose conclusion or support includes $\alpha$ . If $k>1$ , then there exists a set of arguments for $\beta_{k}$ that collectively attacks an argument including $\alpha$ . For each $\alpha\in\mathcal{DE}(\mathcal{T}_{\texttt{{G}}})$ , let $B^{\alpha}_{k}$ be the set of facts in the support of arguments for $\beta_{k}$ in $\mathcal{T}_{\texttt{{G}}}$ such that the arguments for $\beta_{k}$ attack an argument including $\alpha$ . Clearly, there exists an argument for $\beta$ that attacks an argument including $\alpha$ if $k=1$ and there exist arguments for $\beta_{k}$ that attack or collectively attack an argument including $\alpha$ if $k>1$ . We construct inductively the sequence of trees $\mathcal{T}^{1}(\delta_{i}),\ldots,\mathcal{T}^{h}(\delta_{i})$ as follows:
1. $\mathcal{T}^{1}(\delta_{i})$ is a support tree of $\phi$ corresponding to the argument labelling the root of $\mathcal{T}_{\texttt{{G}}}$ .
1. Let $j=2n$ such that the non-terminal nodes in the frontier of $\mathcal{T}^{j}(\delta_{i})$ are opponent nodes labelled by a set of formulas $\beta_{k}$ where $\{\beta_{k}\}\cup\{\alpha\}$ is inconsistent and $\alpha\in\mathcal{DE}(\mathcal{T}_{\texttt{{G}}})$ . Expand each such node by a context tree of $\beta_{k}$ wrt $B^{\alpha}_{k}$ . The obtained tree is $\mathcal{T}^{j+1}(\delta_{i})$ .
1. Let $j=2n+1$ such that the non-terminal nodes in the frontier of $\mathcal{T}^{j}(\delta_{i})$ are proponent nodes labelled by a set of formula $\beta_{k}$ , where $\{\beta_{k}\}\cup\{\alpha\}$ is inconsistent and $\alpha\in\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})$ . Expand each such node by a support tree of $\beta_{k}$ corresponding to the argument for $\beta_{k}$ . The obtained tree is $\mathcal{T}^{j+1}(\delta_{i})$ .
1. Define $\mathcal{T}(\delta_{i})$ to be the limit of $\mathcal{T}^{j}(\delta_{i})$ . It follows immediately that $\mathcal{T}(\delta_{i})$ is a dialogue tree for $\phi$ whose defence set is a subset of the defence set of $\mathcal{T}_{\texttt{{G}}}$ and whose the culprit set is a subset of the culprit set of $\mathcal{T}_{\texttt{{G}}}$ . Since $\mathcal{T}_{\texttt{{G}}}$ is admissible, by Defintion A.4, the proponent wins, namely either the tree ends with arguments labelled by proponent nodes or every argument labelled by an opponent node has a child. By Definition 5.9, $\mathcal{T}(\delta_{i})$ is defensive. Since $\mathcal{T}_{\texttt{{G}}}$ is admissible, by Defintion A.4, $\mathcal{T}_{\texttt{{G}}}$ has no argument labelling both a proponent and an opponent node. By Definition 5.13, $\mathcal{T}(\delta_{i})$ is non-redundant. â
### A.4. Notions and Results of Acceptance of an Argument from Its Abstract Dialogue Trees
For readerâs convenience, we reproduce here definitions and results for abstract dialogues for $\phi$ that can also be found in [52]. We use a similar argument for focused sub-dialogues of a dialogue $\delta$ for $\phi$ . In fact, the definitions and the results we reproduce here are essentially the same with abstract dialogues replaced by focused sub-dialogues of $\delta$ for $\phi$ . This replacement is because an abstract dialogue for $\phi$ can be seen as a focused sub-dialogue of a dialogue $\delta$ for $\phi$ . This follows immediately from the results in Lemma A.5 (i.e., showing a dialogue tree drawn from a dialogue $\delta$ for $\phi$ can be divided into focused sub-trees drawn from focused sub-dialogues of $\delta$ for $\phi$ ) and in Theorem A.7 (i.e., showing each such focused subtrees corresponds with an abstract dialogue tree drawn from an abstract dialogue).
**Definition A.10 (Analogous to Definition 9 in[52])**
*Let $\mathcal{T}_{\texttt{{G}}}$ be the abstract dialogue tree drawn from a focused sub-dialogue $\delta^{\prime}$ of a dialogue for $\phi$ . The focused sub-dialogue $\delta^{\prime}$ is called
- admissible-successful iff $\mathcal{T}_{\texttt{{G}}}$ is admissible;
- preferred-successful iff it is admissible-successful;
- grounded-successful iff $\mathcal{T}_{\texttt{{G}}}$ is admissible and finite;
- sceptical-successful iff $\mathcal{T}_{\texttt{{G}}}$ is admissible and for no opponent node in it, there exists an admissible dialogue tree for the argument labelling an opponent node.*
**Corollary A.11 (Analogous to Corollary 1 in[52])**
*Let $\mathcal{K}$ be a KB, $\phi\in\mathcal{L}$ a formula and $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of $\mathcal{K}$ . Then, $\phi$ is
- credulously accepted in some admissible/preferred extension of $\mathcal{AF}_{\mathcal{K}}$ if there is a focused sub-dialogue $\delta^{\prime}$ of a dialogue for $\phi$ such that $\delta^{\prime}$ is admissible/preferred-successful;
- groundedly accepted in a grounded extension of $\mathcal{AF}_{\mathcal{K}}$ if there is a focused sub-dialogue $\delta^{\prime}$ of a dialogue for $\phi$ such that $\delta^{\prime}$ is grounded-successful;
- sceptically accepted in all preferred extensions of $\mathcal{AF}_{\mathcal{K}}$ if there is a focused sub-dialogue $\delta^{\prime}$ of a dialogue for $\phi$ such that $\delta^{\prime}$ is sceptical-successful.*
## Appendix B Proofs for Section 5.2
We follow the general strategy to prove Theorem 5.13, 5.13, 5.2.2 and 5.15. In particular, we:
1. partition a dialogue tree for $\phi$ drawn from a dialogue $\delta$ into subtrees for $\phi$ drawn from the focused sub-dialogue of $\delta$ (by Lemma A.5),
1. use the correspondence principle to transfer each subtree for $\phi$ into an abstract dialogue tree for $\phi$ (by Theorem A.7),
1. apply Definition A.10 (analogous to Definition 9 in [52] and Corollary A.11 (analogous to Corollary 1 in [52]) for abstract dialogue trees to prove the soundness results.
### B.1. Proof of Theorem 5.13
*
* Proof*
Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ . Let $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ be sub-trees (with root $\phi$ ) constructed from $\mathcal{T}(\delta)$ . By Lemma A.5, we know all sub-trees $\mathcal{T}(\delta_{i})$ of $\mathcal{T}(\delta)$ are the dialogue trees drawn from focused sub-dialogues $\delta_{i}$ , with $i=1,\ldots,m$ , of $\delta$ and each such sub-tree is focused. We assume that $\mathcal{T}(\delta_{i})$ is defensive and non-redundant. By the correspondence principle of Theorem A.7, there is an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{DE}(\mathcal{T}(\delta_{ i}))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{CU}(\mathcal{T}(\delta_{ i}))$ . For such abstract dialogue tree, let $\mathcal{B}$ be a set of proponent arguments in $\mathcal{T}_{\texttt{{G}}}^{i}$ , we prove that
1. $\mathcal{B}$ attacks every attack against it and $\mathcal{B}$ does not attack itself;
1. no argument in $\mathcal{T}_{\texttt{{G}}}^{i}$ that labels both P or O. Since $\mathcal{T}(\delta_{i})$ is defensive and non-redundant, we get the following statements: 1. By Definition 5.9, it is focused. Then the root of $\mathcal{T}_{\texttt{{G}}}^{i}$ hold a proponent argument for $\phi$ .
1. By Definition 5.9, it is last-word. Then the proponent arguments in $\mathcal{T}_{\texttt{{G}}}^{i}$ are leaf nodes, i.e., P wins. Thus, $\mathcal{B}$ attacks every attack against it.
1. By Definition 5.9, $\mathcal{T}(\delta_{i})$ has no formulas $\alpha_{h}$ in opponent nodes belong to $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ such that $\{\alpha_{h}\}\cup\mathcal{DE}(\mathcal{T}(\delta_{i}))$ is inconsistent. $h=0$ corresponds to the case that there is no potential argument, say $A$ , such that $\{\alpha\}$ is the support of $A$ and $A$ attacks any potential arguments supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ . Similarly, for $h>0$ , there are no potential arguments collectively attacking any potential arguments supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ . Thus, $\mathcal{B}$ does not attack itself.
1. By Definition 5.13 of non-redundant trees, there is no argument in $\mathcal{T}_{\texttt{{G}}}^{i}$ that labels both P or O. It can be seen that (b) and (c) prove (1), and (d) proves (2). It follows that $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible. This result directly follows from the definition of admissible abstract dialogue trees in Definition A.4 (analogous to those in [52]). By Definition A.10 (analogous to Definition 9 in [52]), $\delta_{i}$ is admissible-successful in the P-SAF framework $\mathcal{AF}_{\delta_{i}}$ drawn from $\delta_{i}$ (supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ ). Now, we need to show $\delta$ is admissible-successful. By Definition A.1, each tree in the abstract dialogue forest contains its own set of proponent arguments, namely, $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})\neq\mathcal{DE}(\mathcal{T}_{ \texttt{{G}}}^{l})$ , with $1\leq i,\ l\leq m,\ i\neq l$ . Thus, arguments in other trees do not affect arguments in $\mathcal{AF}_{\delta_{i}}$ . It follows that $\delta$ is admissible-successful. By Corollary A.11 (analogous to Corollary 1 in [52]), $\phi$ is credulously accepted under adm semantics in $\mathcal{AF}_{\delta}$ . â
### B.2. Proof of Theorem 5.2.2
The following lemma is used in the proof of Theorem 5.2.2
**Lemma B.1**
*An abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ is finite iff the set of arguments labelling P in $\mathcal{T}_{\texttt{{G}}}$ is a subset of the grounded set of arguments.*
* Proof*
Let $\mathcal{B}$ is a set of arguments labbeling P in $\mathcal{T}_{\texttt{{G}}}$ . We prove the lemma as follows: If part: The height of a finite dialogue tree $\mathcal{T}_{\texttt{{G}}}$ is $2h$ . We prove that $\mathcal{B}$ is a subset of the grounded set by induction on $h$ . Observer that (1) if $\mathcal{A}_{1}$ , $\mathcal{A}_{2}$ are an admissible subset of the grounded set, then so is $\mathcal{A}_{1}\cup\mathcal{A}_{2}$ ; (2) if an argument $A$ is accepted wrt $\mathcal{A}_{1}$ then $\mathcal{A}_{1}\cup\{A\}$ is an admissible subset of the grounded set. $h=0$ corresponds to dialogue trees containing a single node labelled by an argument that is not attacked. So $\mathcal{B}$ containing only that argument is a subset of the grounded set. Assume the assertion holds for all finite dialogue tree of height smaller than $2h$ . Let $A$ be an argument labelling P at the root of $\mathcal{T}_{\texttt{{G}}}$ . For each argument $B$ attacking a child of $A$ , let $\mathcal{T}_{B}$ be the subtree of $\mathcal{T}_{\texttt{{G}}}$ rooted at $B$ . Clearly, $\mathcal{T}_{B}$ is a finite dispute tree with height smaller than $2h$ . The union of sets of arguments labelling P of all $\mathcal{T}_{B}$ is a subset of the grounded set and defends $A$ . So $\mathcal{B}$ is a subset of the grounded set. Only if part: to construct a finite abstract dialogue tree for a groundedly accepted argument in a finite P-SAF framework, we need the following lemma: In a finite P-SAF framework, the grounded set equals $\emptyset\cup\mathcal{F}(\emptyset)\cup\mathcal{F}^{2}(\emptyset)\cup\cdots$ . This lemma follows from two facts, proven in [6], of the characteristic function $\mathcal{F}$ :
- $\mathcal{F}$ is monotonic w.r.t. set inclusion.
- if the argument framework is finite, then $\mathcal{F}$ is $\omega-$ continuous.
For each argument $A$ in the grounded set, $A$ can be ranked by a natural number $r(A)$ such that $A\in\mathcal{F}^{n(A)}(\emptyset)\setminus\mathcal{F}^{r(A)-1}(\emptyset)$ . So $r(A)=1$ , then $A$ belongs to the grounded set and is not attacked. $r(A)=2$ , the set of arguments (of the grounded set) defended by the set of arguments (of the grounded set) such that $r(A)\leq 1$ and so on. For each set of arguments $\mathcal{S}$ collectively attacking the grounded set, the rank of $\mathcal{S}$ is $\texttt{min}\{r(A)\mid A\text{ is in the grounded set and attacks some argument in }\mathcal{S}\}$ . Clearly, $\mathcal{S}$ does not attack any argument in the grounded set of rank smaller than the rank of $\mathcal{S}$ . Given any argument $A$ in the grounded set, we can build an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}$ for $A$ as follows: The root of $\mathcal{T}_{\texttt{{G}}}$ is labelled by $A$ . For each set of arguments $\mathcal{S}$ attacking $A$ , we select a set of arguments $\mathcal{C}$ to counterattacks $\mathcal{S}$ such that the rank of $\mathcal{C}$ equals the rank of $\mathcal{S}$ , then for each set of arguments $\mathcal{E}$ attacking some arguments of $\mathcal{C}$ , we select arguments $\mathcal{F}$ to counterattacks $\mathcal{E}$ such that the rank of $\mathcal{F}$ equals to the rank of $\mathcal{E}$ , and so on. So for each branch of $\mathcal{T}_{\texttt{{G}}}$ , the rank of a proponent node is equal to that of its opponent parent node, but the rank of an opponent node is smaller than that of its parent proponent node. Clearly, ranking decreases downwards. So all branches of $\mathcal{T}_{\texttt{{G}}}$ are of finite length. Since the P-SAF is finite, $\mathcal{T}_{\texttt{{G}}}$ is finite in breath. Thus $\mathcal{T}_{\texttt{{G}}}$ is finite. â
*
* Proof*
Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ and $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ (with root $\phi$ ) be subtrees of $\mathcal{T}(\delta)$ . By Lemma A.5, all sub-trees of $\mathcal{T}(\delta)$ are the dialogue trees drawn from focused sub-dialogues $\delta_{i}$ , with $i=1,\ldots,m$ , of $\delta$ and each such subtree is focused. Assume that $\mathcal{T}(\delta_{i})$ is defensive and finite. Since $\mathcal{T}(\delta_{i})$ is defensive, by the correspondence principle of Theorem A.7, there is an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{DE}(\mathcal{T}(\delta_{ i}))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{CU}(\mathcal{T}(\delta_{ i}))$ . For such abstract dialogue tree, let $\mathcal{B}$ be the set of arguments labelling P in $\mathcal{T}_{\texttt{{G}}}^{i}$ . We need to show that 1. $\mathcal{T}_{\texttt{{G}}}^{i}$ is finite;
1. $\mathcal{B}$ attacks ever attract against it, and
1. $\mathcal{B}$ does not attack itself. Similar to the proof of Theorem 5.13, (2) and (3) directly follows from the fact that $\mathcal{T}(\delta_{i})$ is admissible. Trivially, every $\mathcal{T}(\delta_{i})$ is finite, then $\mathcal{T}_{\texttt{{G}}}^{i}$ is finite. As a direct consequence of Lemma B.1, we obtain that $\mathcal{B}$ is a subset of the grounded set of arguments in $\mathcal{T}_{\texttt{{G}}}^{i}$ . By Definition A.10 (analogous to Definition 9 in [52]), $\delta_{i}$ is grounded-successful in $\mathcal{AF}_{\delta_{i}}$ (drawn from $\delta_{i}$ ). We next prove that $\delta$ is grounded-successful. Since $\delta_{i}$ is grounded-successful in $\mathcal{AF}_{\delta_{i}}$ drawn from $\delta_{i}$ , it follows that there are no arguments attacking the arguments in $\mathcal{B}$ that have not been counter-attacked in the abstract dialogue forest $\mathcal{T}_{\texttt{{G}}}^{1},\ldots,\mathcal{T}_{\texttt{{G}}}^{m}$ (obtained from the P-SAF drawn from $\delta$ ). By Definition A.1, each tree in the abstract dialogue forest contains its own set of proponent arguments, namely, $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})\neq\mathcal{DE}(\mathcal{T}_{ \texttt{{G}}}^{l})$ , with $1\leq i,\ l,\leq m,\ i\neq l$ . If the set of proponent arguments in $\mathcal{T}_{\texttt{{G}}}^{i}$ drawn from the focused sub-dialogue $\delta_{i}$ is grounded, it is also grounded in $\mathcal{AF}_{\delta}$ drawn from $\delta$ . Thus, $\delta$ is grounded successful. By Corollary A.11 (analogous to Corollary 1 in [52]), $\phi$ is groundedly accepted in $\mathcal{AF}_{\delta}$ (supported by $\mathcal{DE}(\mathcal{T}(\delta_{i}))$ ). â
### B.3. Proof of Theorem 5.15
*
* Proof*
We prove this theorem for the case of admissible semantics. The proof for preferred (stable) semantics is analogous. Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ , and $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ (with root $\phi$ ) be subtrees constructed from $\mathcal{T}(\delta)$ . By Lemma A.5, we know all subtrees in $\mathcal{T}(\delta)$ are dialogue trees drawn from focused sub-dialogues $\delta_{i}$ , ( $i=1,\ldots,m$ ) of $\delta$ and each tree is focused. Assume that $\mathcal{T}(\delta)$ is ideal. Since $\mathcal{T}(\delta)$ is ideal, $\mathcal{T}(\delta_{i})$ is ideal. By Definition 5.15, $\mathcal{T}(\delta_{i})$ is defensive. By the correspondence principle, there is an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{DE}(\mathcal{T}(\delta_{ i}))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{CU}(\mathcal{T}(\delta_{ i}))$ . For such abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ , we need to show that:
1. $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible, and
1. for no opponent node O in it there exists an admissible dialogue tree for the opponent argument. Similar to the proof of Theorem 5.13, (1) holds. Since $\mathcal{T}(\delta)$ is ideal, by Definition 5.15, there is a dialogue tree $\mathcal{T}(\delta_{i})$ such that none of the opponent arguments drawn from $\mathcal{T}(\delta_{i})$ belongs to an admissible set of arguments in $\mathcal{AF}_{\delta}$ drawn from $\delta$ . Then, (2) holds. We have shown that $\mathcal{T}_{\texttt{{G}}}^{i}$ is defensive and none of the opponent arguments belongs to an admissible set of arguments in $\mathcal{AF}_{\delta}$ drawn from $\delta$ . By Definition A.10 (analogous to Definition 9 in [52]), $\delta$ is sceptical-successful. By Corollary A.11 (analogous to Corollary 1 in [52]), $\phi$ is sceptically accepted in $\mathcal{AF}_{\delta}$ . â
## Appendix C Proofs for Section 5.3
To prove the completeness results, we
1. partition a dialogue $\delta$ for $\phi$ into its focused sub-dialogues of $\delta$ (by Definition 4.3),
1. apply Corollary C.1 and Definition A.10 (analogous to Definition 9 in [52]) to obtain the existence of an abstract dialogue tree drawn from each focused sub-dialogue of $\delta$ wrt argumentation semantics,
1. use the correspondence principle to transfer from each abstract dialogue tree for $\phi$ into a dialogue tree for $\phi$ (by Theorem A.7), thereby proving the completeness results.
### C.1. Preliminaries
Corollary A.11 is used for the proof of the soundness results. To prove the completeness result, we need to extend Corollary A.11 as follows:
**Corollary C.1**
*Let $\mathcal{K}$ be a KB, $\phi\in\mathcal{L}$ a formula and $\mathcal{AF}_{\mathcal{K}}$ be the corresponding P-SAF of $\mathcal{K}$ . We say that if $\phi$ is - credulously accepted in some admissible/preferred extension of $\mathcal{AF}_{\mathcal{K}}$ , then there is a focused sub-dialogue $\delta_{i}$ , with $i=1,\ldots,m$ , of a dialogue for $\phi$ such that $\delta_{i}$ is admissible/preferred-successful;
- groundedly accepted in a grounded extension of $\mathcal{AF}_{\mathcal{K}}$ , then there is a focused sub-dialogue $\delta_{i}$ of a dialogue for $\phi$ such that $\delta_{i}$ is grounded-successful;
- sceptically accepted in all preferred extensions of $\mathcal{AF}_{\mathcal{K}}$ , then there is a focused sub-dialogue $\delta_{i}$ of a dialogue for $\phi$ such that $\delta_{i}$ is sceptical-successful.*
* Proof*
Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ and $\mathcal{T}(\delta_{1}),\ldots,\mathcal{T}(\delta_{m})$ (with root $\phi$ ) be subtrees of $\mathcal{T}(\delta)$ . By Lemma A.5, all sub-trees of $\mathcal{T}(\delta)$ are the dialogue trees drawn from focused sub-dialogues $\delta_{i}$ , with $i=1,\ldots,m$ , of $\delta$ and each such subtree is focused. By the correspondence principle, there is an abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for an argument $A$ with conclusion $\phi$ , or simply, an abstract dialogue $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ , which corresponds to the dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ . It is clear that there is a focused sub-dialogue $\delta_{i}$ such that it is admissible-successful if $\phi$ is credulously accepted in some admissible/preferred extension of $\mathcal{AF}_{\mathcal{K}}$ . The argument given in Definition 2 and Lemma 1 of [49] for binary attacks generalizes to collective attacks, implying that $A$ is accepted in some admissible extension iff $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible which in turn holds iff P wins and no argument labels both a proponent and an opponent node. By Definition A.10, $\delta_{i}$ is admissible-successful iff $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible. Thus, the statement is proved. $\delta_{i}$ is preferred-successful if $\delta_{i}$ is admissible-successful. This result directly follows from the results of [6] that states that an extension is preferred if it is admissible. Thus, if $\phi$ is credulously accepted in some preferred extension, then $\delta_{i}$ is preferred-successful. The other statement follows in a similar way as a straightforward generalization of Theorem 1 of [49] for the âgrounded-successfulâ semantic; Definition 3.3 and Theorem 3.4 of [13] for the âsceptical-successfulâ semantic. â
### C.2. Proof of Theorem 8
*
* Proof*
Given $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ , we assume that $\phi$ is credulously accepted under adm in $\mathcal{AF}_{\delta}$ drawn from $\delta$ and $\delta$ is admissible-successful. We prove that there exists a dialogue tree drawn from the sub-dialogue of $\delta$ such that the dialogue tree is defensive and non-redundant. Let $\delta_{1},\ldots,\delta_{m}$ , where $i=1,\ldots,m$ , be sub-dialogues of $\delta$ and each sub-dialogue is focused. Since $\phi$ is credulously accepted under adm in $\mathcal{AF}_{\delta}$ drawn from the dialogue $\delta$ , by Corollary C.1, the focused sub-dialogue $\delta_{i}$ is admissible-successful. By Definition A.10 (analogous to Definition 9 in [52]), there is an admissible abstract dialogue tree $\mathcal{T}^{i}_{\texttt{{G}}}$ for $\phi$ drawn from the admissible-successful dialogue $\delta_{i}$ . By the correspondence principle, there exists a dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ that corresponds to the abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{DE}(\mathcal{T}(\delta_{ i}))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^{i})=\mathcal{CU}(\mathcal{T}(\delta_{ i}))$ . Since $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible, $\mathcal{T}(\delta_{i})$ is defensive and non-redundant. Thus, the statement is proved. â
### C.3. Proof of Theorem 8
*
* Proof*
Given $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ , we assume that $\phi$ is groundedly accepted under grd in $\mathcal{AF}_{\delta}$ drawn from $\delta$ and $\delta$ is groundedly-successful. We prove that there exists a dialogue tree drawn from the sub-dialogue of $\delta$ such that the dialogue tree is defensive and finite. Let $\delta_{1},\ldots,\delta_{m}$ , where $i=1,\ldots,m$ , be sub-dialogues of $\delta$ and each sub-dialogue is focused. Since $\phi$ is groundedly accepted under grd in $\mathcal{AF}_{\delta}$ drawn from the dialogue $\delta$ , by Corollary C.1, the focused sub-dialogue $\delta_{i}$ is grounded-successful. By Definition A.10 (analogous to Definition 9 in [52]), there is an admissible and finite abstract dialogue tree $\mathcal{T}^{i}_{\texttt{{G}}}$ for $\phi$ drawn from the grounded-successful dialogue $\delta_{i}$ . By the correspondence principle, there is a dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ that corresponds to the abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}(\delta_{i}))=\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^ {i})$ and $\mathcal{CU}(\mathcal{T}(\delta_{i}))=\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^ {i})$ . Since $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible, $\mathcal{T}(\delta_{i})$ is defensive. Since $\mathcal{T}_{\texttt{{G}}}^{i}$ is finite, $\mathcal{T}(\delta_{i})$ is finite. Thus, the statement is proved. â
### C.4. Proof of Theorem 8
*
* Proof*
We prove this theorem for the case of admissible semantics. The proof for preferred (stable) semantics is analogous. Given $\delta$ be a dialogue for a formula $\phi\in\mathcal{L}$ , we assume that $\phi$ is credulously accepted under adm in $\mathcal{AF}_{\delta}$ drawn from $\delta$ and $\delta$ is admissible-successful. We prove that there is an ideal dialogue tree $\mathcal{T}(\delta)$ for $\phi$ drawn from the dialogue $\delta$ . Let $\delta_{1},\ldots,\delta_{m}$ , where $i=1,\ldots,m$ , be focused sub-dialogues of $\delta$ . Since $\phi$ is sceptically accepted under adm in $\mathcal{AF}_{\delta}$ drawn from the dialogue $\delta$ , by Corollary C.1, the focused sub-dialogue $\delta_{i}$ is sceptical-successful. By Definition A.10 (analogous to Definition 9 in [52]), there is an abstract dialogue tree $\mathcal{T}^{i}_{\texttt{{G}}}$ for $\phi$ drawn from the sceptical-successful dialogue $\delta_{i}$ such that $\mathcal{T}^{i}_{\texttt{{G}}}$ is admissible and for no opponent node in it there exists an admissible abstract dialogue tree for the argument labelling an opponent node. Since $\mathcal{T}^{i}_{\texttt{{G}}}$ is admissible, by the correspondence principle, there is a dialogue tree $\mathcal{T}(\delta_{i})$ for $\phi$ that corresponds to the abstract dialogue tree $\mathcal{T}_{\texttt{{G}}}^{i}$ for $\phi$ such that $\mathcal{DE}(\mathcal{T}(\delta_{i}))=\mathcal{DE}(\mathcal{T}_{\texttt{{G}}}^ {i})$ and $\mathcal{CU}(\mathcal{T}(\delta_{i}))=\mathcal{CU}(\mathcal{T}_{\texttt{{G}}}^ {i})$ . For such the dialogue tree $\mathcal{T}(\delta_{i})$ , we need to show that:
1. $\mathcal{T}(\delta_{i})$ is defensive and non-redundant,
1. none of the opponent arguments obtained from $\mathcal{T}(\delta_{i})$ belongs to an admissible set of potential arguments in $\mathcal{AF}_{\delta_{i}}$ drawn from $\mathcal{T}(\delta_{i})$ . Since the abstract dialogue $\mathcal{T}_{\texttt{{G}}}^{i}$ is admissible, (1) holds. We have that, for no opponent node in $\mathcal{T}_{\texttt{{G}}}^{i}$ , there exists an admissible abstract dialogue tree for the argument labelling by O. From this, we obtain that (2) holds. By Definition 5.15, $\mathcal{T}(\delta_{i})$ is ideal. Thus, $\mathcal{T}(\delta)$ is ideal. Thus, the statement is proved. â
## References
- [1] Cali, A., Gottlob, G., Lukasiewicz, T. & Pieris, A. Datalog+-: A Family of Languages for Ontology Querying. Workshop, Datalog. (2011)
- [2] Baget, J., LeclĂšre, M., Mugnier, M. & Salvat, E. On rules with existential variables: Walking the decidability line. Artificial Intelligence. (2011)
- [3] Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P. & Kovtunova, A. Finding Small Proofs for Description Logic Entailments: Theory and Practice. (2020)
- [4] Thang, P., Dung, P. & Pooksook, J. Infinite arguments and semantics of dialectical proof procedures. Argument Comput.. 13, 121-157 (2022)
- [5] Marnette, B. Generalized Schema-Mappings: From Termination to Tractability. ACM Symposium On Principles Of Database Systems. (2009)
- [6] Dung, P. On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Person Games. Artif. Intell.. 77, 321-358 (1995)
- [7] Ho, L., Arch-int, S., Acar, E., Schlobach, S. & Arch-int, N. An argumentative approach for handling inconsistency in prioritized Datalog $\pm$ ontologies. AI Commun.. 35, 243-267 (2022)
- [8] Yun, B., Croitoru, M., Vesic, S. & Bisquert, P. Graph Theoretical Properties of Logic Based Argumentation Frameworks: Proofs and General Results. Proceeding Of GKR. (2017)
- [9] Yun, B., Vesic, S. & Croitoru, M. Toward a More Efficient Generation of Structured Argumentation Graphs. COMMA. (2018)
- [10] Amgoud, L. Postulates for logic-based argumentation systems. IJAR. (2014)
- [11] Borg, A. & Bex, F. A Basic Framework for Explanations in Argumentation. IEEE Intelligent Systems. (2021)
- [12] Vreeswijk, G. & Prakken, H. Credulous and Sceptical Argument Games for Preferred Semantics. JELIA. 1919 pp. 239-253 (2000)
- [13] Dung, P., Mancarella, P. & Toni, F. Computing ideal sceptical argumentation. Artificial Intelligence. 171, 642-674 (2007)
- [14] Zhang, X. & Lin, Z. An argumentation framework for description logic ontology reasoning and management. J. Intell. Inf. Syst.. 40, 375-403 (2013)
- [15] Lacave, C. & Diez, F. A review of explanation methods for heuristic expert systems. The Knowledge Engineering Review. (2024)
- [16] Lukasiewicz, T., Malizia, E., Martinez, M., Molinaro, C., Pieris, A. & Simari, G. Inconsistency-tolerant query answering for existential rules. Artificial Intelligence. (2022)
- [17] Lukasiewicz, T., Malizia, E. & Molinaro, C. Explanations for Negative Query Answers under Inconsistency-Tolerant Semantics. Proceedings Of IJCAI. (2022)
- [18] Lukasiewicz, T., Malizia, E. & Molinaro, C. Explanations for Inconsistency-Tolerant Query Answering under Existential Rules. The Thirty-Fourth AAAI Conference On Artificial Intelligence. pp. 2909-2916 (2020)
- [19] Arioua, A., Croitoru, M. & Vesic, S. Logic-based argumentation with existential rules. Int. J. Approx. Reason.. 90 pp. 76-106 (2017)
- [20] Arioua, A. & Croitoru, M. Dialectical Characterization of Consistent Query Explanation with Existential Rules. Proceedings Of The Twenty-Ninth International Florida Artificial Intelligence Research Society Conference, FLAIRS. (2016)
- [21] Arioua, A., Tamani, N. & Croitoru, M. Query Answering Explanation in Inconsistent Datalog $\pm$ Knowledge Bases. In DEXA. 9261 pp. 203-219 (2015)
- [22] Bienvenu, M., Bourgaux, C. & Goasdoué, F. Computing and Explaining Query Answers over Inconsistent DL-Lite Knowledge Bases. J. Artif. Intell. Res.. 64 pp. 563-644 (2019)
- [23] Prakken, H. Formal systems for persuasion dialogue. Knowl. Eng. Rev.. 21, 163-188 (2006)
- [24] Alrabbaa, C., Borgwardt, S., Koopmann, P. & Kovtunova, A. Explaining Ontology-Mediated Query Answers Using Proofs over Universal Models. RuleML+RR. 13752 pp. 167-182 (2022)
- [25] Nielsen, S. & Parsons, S. A Generalization of Dungâs Abstract Framework for Argumentation: Arguing with Sets of Attacking Arguments. Argumentation In Multi-Agent Systems. pp. 54-73 (2007)
- [26] CalĂŹ, A., Gottlob, G. & Lukasiewicz, T. A general Datalog-based framework for tractable query answering over ontologies. Jour. Of Web Semantics. 14 pp. 57-83 (2012)
- [27] Halpern, J. Defining Relative Likelihood in Partially-Ordered Preferential Structures. Procceeding Of UAI. (1996)
- [28] Cayrol, C., Dubois, D. & Touazi, F. On the Semantics of Partially Ordered Bases.
- [29] Modgil, S. & Caminada, M. Proof Theories and Algorithms for Abstract Argumentation Frameworks. (2009)
- [30] Deagustini, C., Martinez, M., Falappa, M. & Simari, G. On the Influence of Incoherence in Inconsistency-tolerant Semantics for Datalog $\pm$ . IJCAI. (2015)
- [31] Amgoud, L. & Vesic, S. Rich preference-based argumentation frameworks. International Journal Of Approximate Reasoning. 55, 585-606 (2014)
- [32] Kaci, S., Der Torre, L., Vesic, S. & Villata, S. Preference in Abstract Argumentation. Handbook Of Formal Argumentation, Volume 2. (2021)
- [33] Arioua, A., Buche, P. & Croitoru, M. Explanatory dialogues with argumentative faculties over inconsistent knowledge bases. Expert Systems With Applications. 80 pp. 244-262 (2017)
- [34] Arioua, A., Tamani, N., Croitoru, M. & Buche, P. Query Failure Explanation in Inconsistent Knowledge Bases Using Argumentation. Comma. (2014)
- [35] Yun, B., Vesic, S. & Croitoru, M. Sets of Attacking Arguments for Inconsistent Datalog Knowledge Bases. Comma. (2020)
- [36] Dunne, P. & Bench-Capon, T. Two party immediate response disputes: Properties and efficiency. Artificial Intelligence. 149, 221-250 (2003)
- [37] Cayrol, C., Doutre, S. & Mengin, J. Dialectical Proof Theories for the Credulous Preferred Semantics of Argumentation Frameworks. ECSQARU, Proceedings. pp. 668-679 (2001)
- [38] Arieli, O. & StraĂer, C. Sequent-based logical argumentation. Argument Comput.. 6, 73-99 (2015)
- [39] DâAgostino, M. & Modgil, S. Classical logic, argument and dialectic. Artif. Intell.. 262 pp. 15-51 (2018)
- [40] Amgoud, L. & Besnard, P. Logical limits of abstract argumentation frameworks. J. Appl. Non Class. Logics. 23, 229-267 (2013)
- [41] Schulz, C. & Toni, F. Justifying answer sets using argumentation. Theory And Practice Of Logic Programming. 16, 59-110 (2016)
- [42] Prakken, H. Coherence and Flexibility in Dialogue Games for Argumentation. J. Log. Comput.. 15, 1009-1040 (2005)
- [43] Dung, P., Kowalski, R. & Toni, F. Dialectic proof procedures for assumption-based, admissible argumentation. Artif. Intell.. 170, 114-159 (2006)
- [44] Dung, P., Kowalski, R. & Toni, F. Assumption-Based Argumentation. Argumentation In Artificial Intelligence. pp. 199-218 (2009)
- [45] Garcia, A. & Simari, G. Defeasible logic programming: DeLP-servers, contextual queries, and explanations for answers. Argument Comput.. 5, 63-88 (2014)
- [46] Prakken, H. & Vreeswijk, G. Logics for Defeasible Argumentation. Handbook Of Philosophical Logic. (2002)
- [47] Fan, X. & Toni, F. A general framework for sound assumption-based argumentation dialogues. Artif. Intell.. 216 pp. 20-54 (2014)
- [48] Thang, P., Dung, P. & Hung, N. Towards Argument-based Foundation for Sceptical and Credulous Dialogue Games. Proceedings Of COMMA. 245 pp. 398-409 (2012)
- [49] Thang, P., Dung, P. & Hung, N. Towards a Common Framework for Dialectical Proof Procedures in Abstract Argumentation. J. Log. Comput.. 19 (2009)
- [50] Castagna, F. A Dialectical Characterisation of Argument Game Proof Theories for Classical Logic Argumentation. Proceedings Of AIxIA. 3086 (2021)
- [51] DâAgostino, M. & Modgil, S. Classical logic, argument and dialectic. Artif. Intell.. 262 pp. 15-51 (2018)
- [52] Ho, L. & Schlobach, S. A General Dialogue Framework for Logic-based Argumentation. Proceedings Of The 2nd International Workshop On Argumentation For EXplainable AI. 3768 pp. 41-55 (2024)
- [53] Dimopoulos, Y., Dvoråk, W., König, M., Rapberger, A., Ulbricht, M. & Woltran, S. Redefining ABA+ Semantics via Abstract Set-to-Set Attacks. AAAI. pp. 10493-10500 (2024)
- [54] Bienvenu, M. & Bourgaux, C. Querying and Repairing Inconsistent Prioritized Knowledge Bases: Complexity Analysis and Links with Abstract Argumentation. Proceedings Of KR. pp. 141-151 (2020)
- [55] Borg, A., Arieli, O. & StraĂer, C. Hypersequent-Based Argumentation: An Instantiation in the Relevance Logic RM. Proceeding Of TAFA. (2017)
- [56] Hunter, A. Base Logics in Argumentation. Proceedings Of COMMA. 216 pp. 275-286 (2010)
- [57] Priest, G. Reasoning About Truth. Artif. Intell.. 39, 231-244 (1989)
- [58] Belnap, N. A Useful Four-Valued Logic. Modern Uses Of Multiple-Valued Logic. pp. 5-37 (1977)
- [59] Besnard, P. & Hunter, A. A logic-based theory of deductive arguments. Artif. Intell.. 128, 203-235 (2001)
- [60] Heyninck, J. & Arieli, O. Simple contrapositive assumption-based argumentation frameworks. Int. J. Approx. Reason.. 121 pp. 103-124 (2020)
- [61] Amgoud, L. Five Weaknesses of ASPIC +. IPMU 2012 Proceedings. 299 pp. 122-131 (2012)
- [62] Modgil, S. & Prakken, H. The ASPIC+ framework for structured argumentation: a tutorial. Argument Comput.. 5, 31-62 (2014)
- [63] Arieli, O. & Heyninck, J. Collective Attacks in Assumption-Based Argumentation. Proceedings Of The 39th ACM/SIGAPP Symposium On Applied Computing,SAC. pp. 746-753 (2024)
- [64] Caminada, M. & Amgoud, L. On the evaluation of argumentation formalisms. Artif. Intell.. 171, 286-310 (2007)
- [65] Jesse Heyninck, O. Simple contrapositive assumption-based argumentation frameworks. International Journal Of Approximate Reasoning. 121 pp. 103-124 (2020)
- [66] Krötzsch, M., Rudolph, S. & Schmitt, P. A closer look at the semantic relationship between Datalog and description logics. Semantic Web. 6, 63-79 (2015)
- [67] Rapberger, A., Ulbricht, M. & Toni, F. On the Correspondence of Non-flat Assumption-based Argumentation and Logic Programming with Negation as Failure in the Head. CoRR. abs/2405.09415 (2024)
- [68] Lehtonen, T., Rapberger, A., Toni, F., Ulbricht, M. & Wallner, J. Instantiations and Computational Aspects of Non-Flat Assumption-based Argumentation. CoRR. abs/2404.11431 (2024)
- [69] Arieli, O. & StraĂer, C. Logical argumentation by dynamic proof systems. Theor. Comput. Sci.. 781 pp. 63-91 (2019)
- [70] Alsinet, T., BĂ©jar, R. & Godo, L. A characterization of collective conflict for defeasible argumentation. Computational Models Of Argument: Proceedings Of COMMA 2010. 216 pp. 27-38 (2010)
- [71] Amgoud, L. & Besnard, P. Bridging the Gap between Abstract Argumentation Systems and Logic. Scalable Uncertainty Management. pp. 12-27 (2009)
- [72] Bloom, S. Some Theorems on Structural Consequence Operations. Studia Logica: An International Journal For Symbolic Logic. 34, 1-9 (1975)
- [73] Hecham, A., Bisquert, P. & Croitoru, M. On the Chase for All Provenance Paths with Existential Rules. Rules And Reasoning - International Joint Conference, RuleML+RR. 10364 pp. 135-150 (2017)