# Dialogue-based Explanations for Logical Reasoning using Structured Argumentation
**Authors**: Loan Ho, Stefan Schlobach
> loanthuyho.cs@gmail.com
> k.s.schlobach@vu.nlVrije 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}^{±}$ [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}^{±}$ , 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}^{±}$ , 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}^{±}$ , 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}^{±}$ [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}}→ 2^{\mathcal{L}}$ such that $\overline{\texttt{{CN}}}(X)=\bigcup_{n≥ 0}\texttt{{CN}}^{n}(X)$ satisfies the axioms:
- ( $A_{1}$ ) Expansion $X⊂eq\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}}→ 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)⊂eq\bigcup\{\overline{\texttt{{CN}}}(Y)\mid Y%
⊂_{f}X\}$ where the notation $Y⊂_{f}X$ means that $Y$ is a finite proper subset of $X$ .
- ( $A_{4}$ ) Coherence $\overline{\texttt{{CN}}}(\emptyset)≠\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},...,p_{n}}{c}$ where its conclusion is $c$ and the premises are $p_{1},...,p_{n}$ . $c$ is called a direct consequence of $p_{1},...,p_{n}$ by virtue of $r$ . If we define $\texttt{{CN}}(X)$ as the set of direct consequences of $X⊂eq\mathcal{L}$ , then $\overline{\texttt{{CN}}}$ coincides with $\overline{\texttt{{CN}}}(X)=\{\alpha∈\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⊂eq\mathcal{L}$ . We say that:
- $X$ is consistent wrt $(\mathcal{L},\texttt{{CN}})$ iff $\overline{\texttt{{CN}}}(X)≠\mathcal{L}$ . It is inconsistent otherwise;
- $X$ is a minimal conflict of $\mathcal{K}$ if $X^{\prime}⊂neq 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}⊂eq\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⊂eq\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⊂ 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∈\mathcal{L}$ is entailed in
- some maximal consistent subset iff for some $\Delta∈\texttt{{MCS}}(\mathcal{K})$ , $\phi∈\overline{\texttt{{CN}}}(\Delta)$ ;
- the intersection of all maximal consistent subsets iff for $\Psi=\bigcap\{\Delta\mid\Delta∈\texttt{{MCS}}(\mathcal{K})\}$ , $\phi∈\overline{\texttt{{CN}}}(\Psi)$ ;
- all maximal consistent subsets iff for all $\Delta∈\texttt{{MCS}}(\mathcal{K})$ , $\phi∈\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}^{±}$ . Table 1 summarizes properties holding for consequence operators of the instantiations.
| $A_{1}$ $A_{2}$ $A_{3}$ | $×$ $×$ $×$ | $×$ $×$ $×$ | $×$ $×$ $×$ | $×$ $×$ $×$ | $×$ $×$ |
| --- | --- | --- | --- | --- | --- |
| $A_{4}$ | $×$ | $×$ | | | |
| $A_{5}$ | $×$ | $×$ | | | |
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}}→ 2^{\mathcal{L}_{c}}$ as follows: For $X⊂eq\mathcal{L}_{c}$ , a formula $x∈\mathcal{L}_{c}$ satisfies $x∈\texttt{{CN}}_{c}(X)$ iff the inference rule $\frac{y}{x}$ is applied to $X$ such that $y∈ X$ . Define $\overline{\texttt{{CN}}}_{c}(X)=\bigcup_{n≥ 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∈ 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 $⊃$ , $\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}}→ 2^{\mathcal{L}_{p}}$ be defined as follows: for $X⊂eq\mathcal{L}_{p}$ , an element $x∈\mathcal{L}_{p}$ satisfies $x∈\texttt{{CN}}_{p}(X)$ iff there are $y_{1},...,y_{j}∈ X$ such that $x$ can be obtained from $y_{1},...,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⊃\neg y\}⊂eq\mathcal{L}_{p}$ . Consider a set $\{x,x⊃\neg y\}⊂eq\mathcal{K}_{1}$ . If the inference rule (modus ponens) $\frac{A,A⊃ B}{B}$ is applied to this set, then $\texttt{{CN}}_{p}(\{x,x⊃\neg y\})=\{x,x⊃\neg y,\neg y\}$ .*
Consider $\overline{\texttt{{CN}}}_{p}(X)=\bigcup_{n≥ 0}\texttt{{CN}}_{p}^{n}(X)$ . For instance, $\overline{\texttt{{CN}}}_{p}(\mathcal{K}_{1})=\{x,y,x⊃\neg y,\neg y,x%
\wedge y,...\}$ . Since propositional logic is coherent and complete, then $x∈\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⊃\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},... x_{i}→_{s}x_{i+1}$ ( $x_{1},... x_{i}→_{d}x_{i+1}$ ) where $x_{1},... x_{i},x_{i+1}$ are literals and $→_{s}$ (denote strict rules) and $→_{d}$ (denotes defeasible rules) are implication symbols.
**Definition 2.8**
*Define $\texttt{{CN}}_{d}:2^{\mathcal{L}_{d}}→ 2^{\mathcal{L}_{d}}$ as follows: for $X⊂eq\mathcal{L}_{d}$ , a formula $x∈\mathcal{L}_{d}$ satisfies $x∈\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},...,y_{j})→_{s}x∈ X$ , or $(y_{1},...,y_{j})→_{d}x∈ X$ st. $\{y_{1},...,y_{j}\}⊂eq X$ .
Define $\overline{\texttt{{CN}}}_{d}(X)=\bigcup_{n≥ 0}\texttt{{CN}}_{d}^{n}(X)$ .*
**Remark 2.9**
*One can describe $\overline{\texttt{{CN}}}_{d}$ explicitly. We have $x∈\overline{\texttt{{CN}}}_{d}(X)$ iff there exists a finite sequence of literals $x_{1},...,x_{n}$ such that
1. $x$ is $x_{n}$ , and
1. for each $x_{i}∈\{x_{1},...,x_{n}\}$ ,
- there is $y_{1},...,y_{j}→_{s}x_{i}∈ X$ , or $y_{1},...,y_{j}→_{d}x_{i}∈ X$ , such that $\{y_{1},...,y_{j}\}⊂eq\{x_{1},...,x_{i-1}\}$ ,
- or $x_{i}$ is a literal in $X$ . Note that if $x∈\texttt{{CN}}_{d}^{n}(X)$ , the above sequence $x_{1},...,x_{n}$ might have length $m≠ 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→_{s}y,t→_{d}z\}⊂eq\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→_{s}y,t→_{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⊂eq\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},...,\phi_{n}→_{s}\alpha∈\mathcal{R}_{s}$ iff $s=\phi_{1},...,\phi_{i-1},\neg\alpha,\phi_{i+1},...,\phi_{n}→_%
{s}\neg\phi_{i}$ for $1≤ i≤ n$ .
**Definition 2.14**
*Define $\texttt{{CN}}_{co}:2^{\mathcal{L}_{co}}→ 2^{\mathcal{L}_{co}}$ as follows: for a set of literals $X⊂eq\mathcal{L}_{co}$ , a formula $x∈\mathcal{L}_{co}$ satisfies $x∈\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},...,y_{j})→_{s}x∈\mathcal{R}_{s}\cup\texttt{ {%
Contrapositives}}(\mathcal{R}_{s})$ , or $(y_{1},...,y_{j})→_{d}x∈\mathcal{R}_{d}\cup\texttt{{%
Contrapositives}}(\mathcal{R}_{d})$ such that $\{y_{1},...,y_{j}\}⊂eq X$ .
Define $\overline{\texttt{{CN}}}_{co}(X)=\bigcup_{n≥ 0}\texttt{{CN}}_{co}^{n}(X)$ .*
**Remark 2.15**
*Similarly, one can represent $\overline{\texttt{{CN}}}_{co}$ as follows: $x∈\overline{\texttt{{CN}}}_{co}(X)$ iff there exists a sequence of literals $x_{1},...,x_{n}$ such that
1. $x$ is $x_{n}$ , and
1. for each $x_{i}∈\{x_{1},...,x_{n}\}$ ,
- there is $y_{1},...,y_{j}→_{s}x_{i}∈\mathcal{R}_{s}\cup\texttt{{%
Contrapositives}}(\mathcal{R}_{s})$ , or $y_{1},...,y_{j}→_{d}x_{i}∈\mathcal{R}_{d}\cup\texttt{{%
Contrapositives}}(\mathcal{R}_{d})$ , such that $\{y_{1},...,y_{j}\}⊂eq\{x_{1},...,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→_{d}r,\neg p→_{s}u\}$ , $\texttt{{Contrapositives}}(\mathcal{K}_{3})=\{\neg r\wedge q→_{d}%
\neg p,\neg r\wedge p→_{d}\neg q,\neg u→_{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→_{s}u\}$ and $\{q,p\wedge q→_{d}r,\neg p→_{s}u\}$ .*
2.3. $\text{Datalog}^{±}$
We consider $\text{Datalog}^{±}$ [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 $∀\vec{x}∀\vec{y}\phi(\vec{x},\vec{y})→∃\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 $∀\vec{x}$ $\phi(\vec{x})→\bot$ where $\phi(\vec{x})$ is a conjunction of atoms. We may leave out the universal restriction. A language for $\text{Datalog}^{±}$ $\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}}→ 2^{\mathcal{L}_{da}}$ as follows: Let $X$ be a set of facts of $\mathcal{L}_{da}$ , an element $x∈\mathcal{L}_{da}$ satisfies $x∈\texttt{{CN}}_{da}(X)$ iff there are $y_{1},...,y_{j}∈ X$ s.t. $x$ can be obtained from $y_{1},...,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≥ 0}\texttt{{CN}}_{da}^{n}(X)$ . Similar to proposition logic, $x∈\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}^{±}$ , such as guarded, weakly guarded $\text{Datalog}^{±}$ .
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}^{±}$ ):
| | $\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∈\mathcal{L}$ is tree-derivable from a set of fact-premises $H⊂eq\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},...,\beta_{n}$ such that $\beta_{0}∈\texttt{{CN}}(\{\beta_{1},...,\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∈\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}}∈\texttt{{CN}}^{i_{1}}(H)$ , …, $\beta_{a_{k}}∈\texttt{{CN}}^{i_{k}}(H)$ , then $\beta∈\texttt{{CN}}^{i+1}(X)$ where $i=\max\{i_{1},...,i_{k}\}$ because by the extension property $\texttt{{CN}}^{i_{1}}(H),...,\texttt{{CN}}^{i_{k}}(H)⊂eq\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∈\texttt{{CN}}^{i}(H)$ , then also $\beta∈\texttt{{CN}}^{i+1}(H)$ , $\beta∈\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⊂eq\mathcal{L}_{c}$ and $\phi∈\mathcal{L}_{c}$ iff $\phi∈\overline{\texttt{{CN}}}_{c}(H)$ , $H$ is minimal (i.e., there is no $H^{\prime}⊂ H$ such that $\phi∈\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⊃\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∈\overline{\texttt{{CN}}}_{d}(H)$ and there is no $H^{\prime}⊂ H$ such that $\phi∈\overline{\texttt{{CN}}}_{d}(H^{\prime})$ and it is not the case that there is $\alpha$ such that $\alpha∈\overline{\texttt{{CN}}}_{d}(H)$ and $\neg\alpha∈\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∈\overline{\texttt{{CN}}}_{d}(H)$ where $H⊂eq\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→_{s}\neg c,\ \neg b\wedge\neg c%
→_{d}s,\ s→_{s}t,\ a\wedge t→_{d}u\}$ , the following is an argument in defeasible logic programming $B:\{a,\neg b,a→_{s}\neg c,\neg b\wedge\neg c→_{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→\neg r,\neg q\wedge\neg r\wedge s%
→ t,t\wedge p→ u,v\}$ , the following is an argument in ABA $C:\{p,\neg q,s,p→\neg r,\neg q\wedge\neg r\wedge s→ 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},...,A_{n}→_{s}/→_{d}\phi$ in these systems as follows:
1. Rules of the form $→_{s}/→_{d}\alpha$ , are arguments with conclusion $\alpha$ .
1. Let $r$ be a strict/defeasible rule of the form $\beta_{1},...,\beta_{n}→_{s}/→_{d}\phi$ , $n≥ 0$ . Further suppose that $A_{1},...,A_{n}$ , $n≥ 0$ , are arguments with conclusions $\beta_{1},...,\beta_{n}$ respectively. Then $A_{1},...,A_{n}→_{s}/→_{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},...,A_{n}→_{s}/→_{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 $→_{s}/→_{d}\alpha_{i}$ such that $\alpha_{i}∈\texttt{{CN}}^{0}_{d}(H)$ . In this view, the root of the tree is labelled by $\phi$ such $\phi∈\texttt{{CN}}^{n}_{d}(H)$ ; the children $\beta_{i}$ , $i=1,...,n$ , of the root are the roots of subtrees $A_{1},...,A_{n}$ ; if $\phi∈\texttt{{CN}}^{n}_{d}(H)$ , then $\beta_{i}∈\texttt{{CN}}^{n-1}_{d}(H)$ . Since $\overline{\texttt{{CN}}}_{d}(H)=\bigcup_{n}\texttt{{CN}}^{n}_{d}(H)$ , it follows that $\phi∈\overline{\texttt{{CN}}}_{d}(H)$ . Note that if $n=0$ , the tree consists of just the root that is the rule of the form $→_{s}/→_{d}\phi$ .
- In argumentation framework for $\text{Datalog}^{±}$ [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⊂eq\mathcal{F}$ and $\phi∈\mathcal{L}_{da}$ , $H\Rightarrow\phi$ is an argument in the sense of Definition 3.1 iff $\phi∈\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}^{±}$ $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
## Diagram: Logical Inference Tree
### Overview
The image depicts a logical inference tree, showing the derivation of a statement involving negation and set membership. The tree structure illustrates how a conclusion is reached from two premises.
### Components/Axes
* **Nodes:** The tree consists of three nodes, each representing a statement.
* **Root Node (Top):** ¬y ∈ CN¹(H)
* **Leaf Nodes (Bottom):**
* x ∈ CN⁰(H)
* x ⊃ ¬y ∈ CN⁰(H)
* **Branches:** Two branches connect the leaf nodes to the root node, indicating the inference steps.
### Detailed Analysis
* **Root Node:** The statement at the root node is "¬y ∈ CN¹(H)". This indicates that the negation of 'y' (¬y) is an element of the set CN¹(H).
* **Leaf Nodes:**
* The left leaf node states "x ∈ CN⁰(H)", meaning 'x' is an element of the set CN⁰(H).
* The right leaf node states "x ⊃ ¬y ∈ CN⁰(H)", meaning 'x' implies the negation of 'y' (x ⊃ ¬y) is an element of the set CN⁰(H).
* **Inference:** The tree structure implies that if 'x' is in CN⁰(H) and 'x' implies '¬y' is in CN⁰(H), then '¬y' is in CN¹(H).
### Key Observations
* The diagram represents a logical deduction.
* The sets CN⁰(H) and CN¹(H) are involved.
* The implication operator (⊃) and negation operator (¬) are used.
### Interpretation
The diagram illustrates a basic inference rule within a formal system. It shows how membership in CN¹(H) can be derived from membership in CN⁰(H) and an implication involving negation. The specific meaning of CN⁰(H) and CN¹(H) would depend on the context of the larger document or theory this diagram is part of. The diagram suggests a hierarchical relationship between these sets, where CN¹(H) might represent a higher-level or derived set based on elements and relationships within CN⁰(H).
</details>
<details>
<summary>x2.png Details</summary>
### Visual Description
## Diagram: Logic Tree
### Overview
The image presents a tree diagram representing a logical structure. The tree originates from a root node labeled "s" and branches out to represent logical relationships and propositions.
### Components/Axes
* **Root Node:** "s" (positioned at the top-center)
* **Branches:** Lines connecting nodes, indicating relationships.
* **Nodes:** Represent logical propositions or variables.
* "¬c" (top-left branch)
* "¬b" (top-center branch)
* "¬b ∧ ¬c → d s" (top-right branch)
* "a" (bottom-left branch)
* "a →s ¬c" (bottom-right branch)
### Detailed Analysis
The tree structure can be broken down as follows:
1. **Root:** The tree starts with the proposition "s".
2. **First Level:** "s" branches into three paths:
* Path 1: "¬c" (negation of c)
* Path 2: "¬b" (negation of b)
* Path 3: "¬b ∧ ¬c → d s" (negation of b AND negation of c implies d, and s)
3. **Second Level:** The "¬c" node branches further:
* Path 1: "a"
* Path 2: "a →s ¬c" (a implies s, and negation of c)
### Key Observations
* The diagram uses logical negation (¬), conjunction (∧), and implication (→).
* The tree structure visually represents the dependencies and relationships between the logical propositions.
* The "s" subscript in "a →s ¬c" suggests a specific type of implication or a contextual relationship.
### Interpretation
The diagram likely represents a logical argument or a set of rules. The root node "s" could be a goal or a conclusion, and the branches represent the conditions or premises that lead to it. The presence of negations and implications suggests a complex logical structure where the truth of certain propositions depends on the truth or falsity of others. The subscript 's' in the implication "a →s ¬c" could indicate a specific type of implication, possibly related to the initial proposition 's', or a contextual dependency.
</details>
<details>
<summary>x3.png Details</summary>
### Visual Description
## Diagram: Proof Tree
### Overview
The image depicts a proof tree, a diagrammatic representation of a logical deduction. It starts with an initial statement at the top and branches down to simpler statements, eventually reaching axioms or previously proven statements at the bottom.
### Components/Axes
* **Nodes:** Each node in the tree represents a logical statement or formula.
* **Edges:** The lines connecting the nodes represent the application of inference rules.
* **Labels:** Labels are present at each node, indicating the logical statement, and on the edges, indicating the inference rule applied.
### Detailed Analysis
The proof tree can be broken down as follows:
1. **Top Node:** The root of the tree contains the statement: "p, p ⊃ q ⇝ q". This reads as "p, p implies q yields q".
2. **First Branching:** The root node branches into two child nodes. The edge on the right branch is labeled "[⊃⇝]". This indicates the application of an inference rule related to implication.
* **Left Child Node:** The left child node contains the statement: "p ⇝ p, q". This reads as "p yields p, q".
* **Right Child Node:** The right child node contains the statement: "p, q ⇝ q". This reads as "p, q yields q".
3. **Second Branching:**
* **Left Child Node Branch:** The left child node "p ⇝ p, q" has a single child node. The edge connecting them is labeled "[Mon]".
* **Left Grandchild Node:** The left grandchild node contains the statement: "p ⇝ p". This reads as "p yields p".
* **Right Child Node Branch:** The right child node "p, q ⇝ q" has a single child node. The edge connecting them is labeled "[Mon]".
* **Right Grandchild Node:** The right grandchild node contains the statement: "q ⇝ q". This reads as "q yields q".
### Key Observations
* The tree demonstrates a logical deduction, starting from a complex statement and breaking it down into simpler, self-evident statements.
* The "[Mon]" rule is applied to both "p ⇝ p, q" and "p, q ⇝ q" to derive "p ⇝ p" and "q ⇝ q" respectively.
* The "[⊃⇝]" rule is applied to "p, p ⊃ q ⇝ q" to derive "p ⇝ p, q" and "p, q ⇝ q".
### Interpretation
The proof tree visually represents a logical argument. The initial statement "p, p ⊃ q ⇝ q" is proven by breaking it down into simpler statements using inference rules. The "[⊃⇝]" rule likely represents the elimination of the implication operator. The "[Mon]" rule likely represents monotonicity, where adding a premise does not invalidate the conclusion. The tree demonstrates that if 'p' is true and 'p implies q' is true, then 'q' must be true. The tree shows how this conclusion can be reached through a series of logical steps. The final statements "p ⇝ p" and "q ⇝ q" are axioms, representing self-evident truths.
</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}⊂eq\texttt{{Arg}}_{\mathcal{K}}$ be a set of arguments such that $\bigcup_{X∈\mathcal{X}}\texttt{{Sup}}(X)$ is consistent. We say that
- $\mathcal{X}$ undercut-attacks $A$ iff there is $\Gamma^{\prime}⊂eq\Gamma$ s.t $\bigcup_{X∈\mathcal{X}}\{\texttt{{Con}}(X)\}\cup\Gamma^{\prime}$ is inconsistent.
- $\mathcal{X}$ rebuttal-attacks $A$ iff $\bigcup_{X∈\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}}⊂eq 2^{\texttt{{Arg}}_{\mathcal{K}}}×%
\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}^{±}$ , 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}^{±}$ [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 $⊃$ 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∈\mathcal{L}_{s}$ the axiom $p\leadsto p$ are a s-formula in $\mathcal{L}_{s}$ . In general, for any set of formulas $\Psi⊂eq\mathcal{L}_{s}$ and $\phi∈\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⊂eq\mathcal{L}_{s}$ , a formula $\phi∈\mathcal{L}_{s}$ satisfies $\phi∈\texttt{{CN}}_{s}(X)$ iff an inference rule $\frac{\Psi_{1}\leadsto\phi_{1}...\Psi_{n}\leadsto\phi_{n}}{\Psi\leadsto\phi}$ , where the sequents $\Psi\leadsto\phi$ and $\Psi_{i}\leadsto\phi_{i}$ ( $i=1,...,n$ ) are s-formulas of $\mathcal{L}_{s}$ , is applied to $X$ such that $\Psi_{1},...,\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≥ 0}\texttt{{CN}}_{s}^{n}(X)$ .
Let us define arguments in the sense of Definition 3.1: For a set of formulas $H⊂eq\mathcal{L}_{s}$ , $H\Rightarrow\phi$ is an argument iff $\phi∈\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},...,\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,...,n$ ), can be viewed as arguments $A_{i}:\Psi_{i}\Rightarrow\phi_{i}$ in the sense of Definition 3.1 where $\phi_{i}∈\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⊃ y,\neg y\}⊂eq\mathcal{L}_{s}$ . The following is an argument in propositional logic $A:\{x,x⊃ y\}\Rightarrow y$ , $B:\{\neg y\}\Rightarrow\neg y$ . $A$ attacks $B$ since $\{x,x⊃ y,\neg y\}$ is inconsistent, i.e., $\overline{\texttt{{CN}}}_{s}(\{x,x⊃ y,\neg y\})=\mathcal{L}_{s}$ . Tree-representations of the arguments are shown in Figure 1 (Right), in which $[Mon]$ and $[⊃,\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 $⊃$ is deductive (i.e., it is a $\vdash$ -implication in contrapositive ABAs) and converting such implications $⊃$ (i.e., $\phi_{1}\wedge·s\wedge\phi_{n}⊃\psi$ ) to rules of the form $\phi_{1},...,\phi_{n}→\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},...,\phi_{n}→\psi∈\mathcal{L}_{co}\mid\phi_{1},%
...,\phi_{n}\vdash\psi\}$ ; their contrapositions treated as $\vdash$ - contrapositive, i.e., $\{\phi_{1},...,\phi_{i-1},\neg\psi,\phi_{i+1},...\phi_{n}→\neg%
\phi_{i}\mid\phi_{1},...,\phi_{i-1},\neg\psi,\phi_{i+1},...\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⊂eq\mathcal{L}_{co}$ be a set of assumptions and $\phi∈\mathcal{L}_{co}$ , $H\Rightarrow\phi$ is an argument iff $\phi∈\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}⊂eq\texttt{{Arg}}_{\mathcal{K}}$ . $\mathcal{S}$ attacks $\mathcal{X}$ iff $∃ A∈\mathcal{X}$ s.t. $\mathcal{S}$ attacks $A$ . $\mathcal{S}$ defends $A$ if for each $\mathcal{X}⊂eq\texttt{{Arg}}_{\mathcal{K}}$ s.t. $\mathcal{X}$ attacks $A$ , some $\mathcal{S}^{\prime}⊂eq\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}}∈\{\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}}∈\{\texttt{{adm}},\texttt{{stb}},\texttt{{prf}}\}$ . A formula $\phi∈\mathcal{L}$ is
- credulously accepted under sem iff for some $\mathcal{E}∈\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi∈\texttt{{Cons}}(\mathcal{E})$ .
- groundedly accepted under grd iff for some $\mathcal{E}∈\texttt{{Exts}}_{\texttt{{grd}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi∈\texttt{{Cons}}(\mathcal{E})$ .
- sceptically accepted under sem iff for all $\mathcal{E}∈\texttt{{Exts}}_{\texttt{{sem}}}(\mathcal{AF}_{\mathcal{K}})$ , $\phi∈\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∈\mathcal{L}$ a formula and $\texttt{{sem}}∈\{\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}}∈\{\texttt{{adm}},\texttt{{stb}},\texttt{{prf}},\texttt{{grd}}\}$ , $\mathcal{AF}_{\mathcal{K}}$ is
1. closed under $\overline{\texttt{{CN}}}$ iff for all $\mathcal{E}∈\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}∈\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},...,\mathcal{E}_{6}\}$ , where $\mathcal{E}_{1}=\texttt{{Args}}(\{\texttt{{taOf}}(\texttt{{v}},\texttt{{KD}}),%
\texttt{{UC}}(\texttt{{KD}})\})$ Fix $\mathcal{F}^{\prime}⊂eq\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},...,\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∈\{1,2\}$ has the form $u=(a_{i},\texttt{{TG}},\texttt{{C}},\texttt{{ID}})$ , where:
- $\texttt{{ID}}∈\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}}∈\mathcal{L}_{c}$ (the content) is one of the following forms: Fix $\phi∈\mathcal{L}$ and $\Delta⊂eq\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∈\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}∈\mathcal{U}$ , $u_{i}≠ 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},...,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},...,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},...,\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}}}∈\{\texttt{{P}},\texttt{{O}}\},%
\texttt{{L}}≠\texttt{{L}}_{\texttt{{ta}}})$ :
1. If $\texttt{{C}}=\texttt{{offer}}(\Delta,\ \alpha)$ with $\Delta=\{\beta_{1},...,\beta_{m}\}$ and $\alpha∈\texttt{{CN}}(\Delta)$ , then $\mathcal{T}^{i+1}$ is obtained:
- For all $\beta_{j}∈\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}∈\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},...,\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}∈\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}}}∈\{\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},...,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∈\delta^{\prime}$ , $u∈\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
## Diagram: Agent Interactions
### Overview
The image presents a table describing interactions between two agents, labeled a1 and a2. Each row represents a specific interaction or action (u1 to u8), detailing the agent involved, a numerical value, the type of action (claim, offer, contrary, concede), and associated parameters.
### Components/Axes
* **Columns:** Two columns labeled "a1" and "a2", representing the two agents.
* **Rows:** Each row represents a specific interaction or action, labeled u1 through u8.
* **Interaction Format:** Each interaction is represented in the format: `u[number] = (a[agent number], [numerical value], [action type]([parameters]), [interaction number])`
### Detailed Analysis or Content Details
**Agent a1:**
* **u1 = (a1, 0, claim(Re(v)), 1)**: Agent a1 makes a claim related to Re(v).
* **u2 = (a1, 1, offer(FP(v), Re(v)), 2)**: Agent a1 makes an offer involving FP(v) and Re(v).
* **u3 = (a1, 2, offer({te(v, KR), GC(KR)}, FP(v)), 3)**: Agent a1 makes an offer involving te(v, KR), GC(KR), and FP(v).
* **u6 = (a1, 4, contrary(Le(v), TA(v)), 6)**: Agent a1 expresses a contrary view regarding Le(v) and TA(v).
* **u7 = (a1, 6, offer(te(v, KD), Le(v)), 7)**: Agent a1 makes an offer involving te(v, KD) and Le(v).
**Agent a2:**
* **u4 = (a2, 2, contrary(TA(v), Re(v)), 4)**: Agent a2 expresses a contrary view regarding TA(v) and Re(v).
* **u5 = (a2, 4, offer({ta0f(v, KD), UC(KD)}, TA(v)), 5)**: Agent a2 makes an offer involving ta0f(v, KD), UC(KD), and TA(v).
* **u8 = (a2, 0, concede(Re(v)), 8)**: Agent a2 concedes regarding Re(v).
### Key Observations
* Both agents perform actions such as "claim", "offer", "contrary", and "concede".
* The actions involve different parameters, including Re(v), FP(v), te(v, KR), GC(KR), Le(v), TA(v), ta0f(v, KD), and UC(KD).
* The numerical values within the interactions seem to represent some form of state or progression.
* The interaction numbers (1 through 8) indicate a sequence of events.
### Interpretation
The diagram represents a simplified model of interactions between two agents in a negotiation or argumentation process. The agents exchange claims, offers, and counter-arguments, eventually leading to a concession by agent a2. The parameters within the actions likely represent different aspects or variables being negotiated. The numerical values could represent the agents' internal states or the progress of the negotiation. The diagram provides a high-level overview of the interaction flow and the types of actions performed by each agent.
</details>
Figure 2. Given $\mathcal{L}_{t}$ is $\mathcal{K}_{1}$ , a dialogue $D(\texttt{{Re}}(\texttt{{v}}))$ $=u_{1},...,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
## Diagram: Tree Structures with Labeled Nodes and Arrows
### Overview
The image presents seven tree-like diagrams, labeled T1(δ) through T7(δ). Each diagram consists of nodes containing tuples of symbols and values, connected by arrows labeled with 'r' followed by a number or 'c' followed by a number. The nodes represent states or entities, and the arrows represent transitions or relationships between them.
### Components/Axes
* **Nodes:** Each node contains a tuple of the form (Symbol(v), [Attribute, Value1, Value2]).
* Symbols include: Re, FP, te, GC, TA, taOf, UC, Le.
* Attributes include: um, nf, fa.
* Values are represented by P, 0, and numerical constants (1, 2, 3, 4, 5, 6, 7).
* **Arrows:** Arrows connect the nodes, indicating relationships or transitions.
* Arrows are labeled with r1, r3, r4, r5, r6, c1, and c2.
* **Diagram Titles:** Each diagram is labeled T1(δ) through T7(δ).
### Detailed Analysis
**T1(δ):**
* Top node: (Re(v), [um, P, 1])
**T2(δ):**
* Top node: (Re(v), [nf, P, 1])
* Bottom node: (FP(v), [nf, P, 2])
* Connection: Dotted line between the nodes.
**T3(δ):**
* Top node: (Re(v), [nf, P, 1])
* Intermediate node: (FP(v), [nf, P, 2])
* Bottom left node: (te(v, KR), [fa, P, 3])
* Bottom right node: (GC(KR), [fa, P, 4])
* Connections: Dotted lines from the intermediate node to the bottom nodes, labeled r6. An "and" symbol (∧) and "r3" connect the top and intermediate nodes.
**T4(δ):**
* Top node: (Re(v), [nf, P, 1])
* Intermediate node: (FP(v), [nf, P, 2])
* Bottom left node: (te(v, KR), [fa, P, 3])
* Bottom right node: (GC(KR), [fa, P, 3])
* Lowest node: (TA(v), [nf, 0, 4])
* Connections: Dotted lines from the intermediate node to the bottom left and right nodes, labeled r6. An arrow labeled c1 points from the right of the intermediate node to the right of the diagram. Dotted lines from the bottom left and right nodes to the lowest node, labeled r4. An "and" symbol (∧) and "r3" connect the top and intermediate nodes.
**T5(δ):**
* Top node: (Re(v), [nf, P, 1])
* Intermediate node: (FP(v), [nf, P, 2])
* Bottom left node: (te(v, KR), [fa, P, 3])
* Bottom right node: (GC(KR), [fa, P, 3])
* Second lowest node: (TA(v), [nf, 0, 4])
* Lowest left node: (taOf(v, KD), [fa, 0, 5])
* Lowest right node: (UC(KD), [fa, 0, 5])
* Connections: Dotted lines from the intermediate node to the bottom left and right nodes, labeled r6. An arrow labeled c1 points from the right of the intermediate node to the right of the diagram. Dotted lines from the bottom left and right nodes to the second lowest node, labeled r4. Dotted lines from the second lowest node to the lowest left and right nodes. An "and" symbol (∧) and "r3" connect the top and intermediate nodes.
**T6(δ):**
* Top node: (Re(v), [nf, P, 1])
* Intermediate node: (FP(v), [nf, P, 2])
* Bottom left node: (te(v, KR), [fa, P, 3])
* Bottom right node: (GC(KR), [fa, P, 3])
* Second lowest node: (TA(v), [nf, 0, 4])
* Third lowest left node: (taOf(v, KD), [fa, 0, 5])
* Third lowest right node: (UC(KD), [fa, 0, 5])
* Lowest node: (Le(v), [nf, P, 6])
* Connections: Dotted lines from the intermediate node to the bottom left and right nodes, labeled r6. An arrow labeled c1 points from the right of the intermediate node to the right of the diagram. An arrow labeled c2 points from the left of the intermediate node to the left of the diagram. Dotted lines from the bottom left and right nodes to the second lowest node, labeled r4. Dotted lines from the second lowest node to the third lowest left and right nodes. Dotted line from the third lowest left node to the lowest node. An "and" symbol (∧) and "r3" connect the top and intermediate nodes.
**T7(δ):**
* Top node: (Re(v), [nf, P, 1])
* Intermediate node: (FP(v), [nf, P, 2])
* Bottom left node: (te(v, KR), [fa, P, 3])
* Bottom right node: (GC(KR), [fa, P, 3])
* Second lowest node: (TA(v), [nf, 0, 4])
* Third lowest left node: (taOf(v, KD), [fa, 0, 5])
* Third lowest right node: (UC(KD), [fa, 0, 5])
* Fourth lowest node: (Le(v), [nf, P, 6])
* Lowest node: (te(v, KD), [fa, P, 7])
* Connections: Dotted lines from the intermediate node to the bottom left and right nodes, labeled r6. An arrow labeled c1 points from the right of the intermediate node to the right of the diagram. An arrow labeled c2 points from the left of the intermediate node to the left of the diagram. Dotted lines from the bottom left and right nodes to the second lowest node, labeled r4. Dotted lines from the second lowest node to the third lowest left and right nodes. Dotted line from the third lowest left node to the fourth lowest node, labeled r5. Dotted line from the fourth lowest node to the lowest node. An "and" symbol (∧) and "r3" connect the top and intermediate nodes.
### Key Observations
* The diagrams represent a progression or evolution, with increasing complexity from T1(δ) to T7(δ).
* The nodes represent states or entities, and the arrows represent transitions or relationships between them.
* The labels on the arrows (r1, r3, r4, r5, r6, c1, c2) likely denote different types of transitions or relationships.
* The values within the nodes change as the diagrams progress, suggesting a change in state or properties.
### Interpretation
The diagrams likely represent a formal system or process, possibly related to knowledge representation or automated reasoning. The nodes represent states or concepts, and the arrows represent rules or inferences. The progression from T1(δ) to T7(δ) could represent the application of these rules to derive new knowledge or reach a conclusion. The symbols and attributes within the nodes likely have specific meanings within the context of this system. The 'c' arrows likely represent some kind of control flow or communication between different parts of the system. The 'r' arrows likely represent rules or transformations.
</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
## Diagram: State Transition Diagram
### Overview
The image is a state transition diagram representing a process or system. It shows various states, labeled with expressions involving 'v', 'P', 'O', 'KR', and 'KD', and transitions between these states, labeled with 'c1' and 'c2'. The diagram also includes labels 'r3', 'r4', 'r5', and 'r6' associated with some transitions or states. The diagram is titled "T(δ)".
### Components/Axes
* **Nodes (States):**
* (Re(v), P): Located at the top-center of the diagram.
* (FP(v), P): Located below (Re(v), P).
* (te(v, KR), P): Located to the left and below (FP(v), P).
* (GC(KR), P): Located to the right and below (FP(v), P).
* (TA(v), O): Located to the right of (GC(KR), P) and (te(v, KR), P).
* (Le(v), P): Located below (te(v, KR), P) and to the left of (TA(v), O).
* (te(v, KD), P): Located below and to the left of (Le(v), P).
* (taOf(v, KD), O): Located below and to the left of (TA(v), O).
* (UC(KD), O): Located below and to the right of (TA(v), O).
* **Edges (Transitions):**
* c1: A directed edge from (TA(v), O) to (FP(v), P).
* c2: A directed edge from (GC(KR), P) to (Le(v), P).
* **Labels:**
* T(δ): Title of the diagram, located at the top.
* r3: Located above the dotted line connecting (Re(v), P) and (FP(v), P).
* r6: Located below the dotted line connecting (FP(v), P) to (te(v, KR), P) and (GC(KR), P).
* r4: Located above the dotted line connecting (TA(v), O) to (taOf(v, KD), O) and (UC(KD), O).
* r5: Located above the dotted line connecting (Le(v), P) to (te(v, KD), P).
### Detailed Analysis or ### Content Details
* **State Descriptions:**
* (Re(v), P): Represents a state with 'Re(v)' and 'P'.
* (FP(v), P): Represents a state with 'FP(v)' and 'P'.
* (te(v, KR), P): Represents a state with 'te(v, KR)' and 'P'.
* (GC(KR), P): Represents a state with 'GC(KR)' and 'P'.
* (TA(v), O): Represents a state with 'TA(v)' and 'O'.
* (Le(v), P): Represents a state with 'Le(v)' and 'P'.
* (te(v, KD), P): Represents a state with 'te(v, KD)' and 'P'.
* (taOf(v, KD), O): Represents a state with 'taOf(v, KD)' and 'O'.
* (UC(KD), O): Represents a state with 'UC(KD)' and 'O'.
* **Transition Descriptions:**
* c1: Transition from (TA(v), O) to (FP(v), P).
* c2: Transition from (GC(KR), P) to (Le(v), P).
* **Connectivity:**
* (Re(v), P) is connected to (FP(v), P) via a dotted line, labeled 'r3'.
* (FP(v), P) is connected to (te(v, KR), P) and (GC(KR), P) via dotted lines, labeled 'r6'.
* (TA(v), O) is connected to (taOf(v, KD), O) and (UC(KD), O) via dotted lines, labeled 'r4'.
* (Le(v), P) is connected to (te(v, KD), P) via a dotted line, labeled 'r5'.
### Key Observations
* The diagram shows a flow of states and transitions.
* 'P' and 'O' appear to be parameters or properties associated with the states.
* 'KR' and 'KD' appear to be identifiers or categories.
* The dotted lines with labels 'r3', 'r4', 'r5', and 'r6' might represent relationships or dependencies between states.
### Interpretation
The diagram likely represents a state machine or a process flow in a system. The states represent different stages or conditions, and the transitions represent the movement between these states based on certain events or conditions. The labels 'P', 'O', 'KR', and 'KD' likely represent parameters or properties that define the state. The transitions 'c1' and 'c2' represent specific actions or events that trigger the change from one state to another. The dotted lines and 'r' labels may represent relationships or dependencies between states that are not direct transitions. The diagram provides a visual representation of the system's behavior and can be used to analyze and understand its dynamics.
</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},...,\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)→ A(x),\ r_{2}:D(x)→ 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
## Tree Diagram: Hierarchical Structure
### Overview
The image presents a tree diagram illustrating a hierarchical structure. The diagram consists of nodes labeled with expressions like "A(a), [um, P, 1]" and directed edges (arrows) indicating relationships between the nodes. The structure appears to represent some form of dependency or derivation.
### Components/Axes
* **Nodes:** Each node is labeled with an expression in the format "(X(a), [Y, Z, N])", where X is a letter (A, B, C, D, or E), Y is a string ("um", "fa", or "0"), Z is "P", and N is a number.
* **Edges:** Directed edges (arrows) connect the nodes, indicating the hierarchical relationships. Dashed lines are used for some connections.
* **Root Node:** The root node is located at the top of the diagram.
* **Leaf Nodes:** The leaf nodes are located at the bottom of the diagram.
### Detailed Analysis or ### Content Details
Here's a breakdown of the nodes and their connections:
* **Level 1 (Root):**
* Node: (A(a), [um, P, 1])
* **Level 2:**
* Node: (B(a), [fa, P, 2]) - Connected to the root node (A(a), [um, P, 1]) with a dashed line.
* Node: (C(a), [fa, P, 2]) - Connected to the root node (A(a), [um, P, 1]) with a dashed line.
* Node: (C(a), [fa, P, 9]) - Connected to the root node (A(a), [um, P, 1]) with a dashed line.
* **Level 3:**
* Node: (D(a), [fa, 0, 3]) - Connected to (C(a), [fa, P, 2]) with a solid line.
* Node: (C(a), [fa, 0, 4]) - Connected to (C(a), [fa, P, 2]) with a solid line.
* Node: (D(a), [fa, 0, 10]) - Connected to (C(a), [fa, P, 9]) with a solid line.
* **Level 4:**
* Node: (E(a), [fa, P, 5]) - Connected to (D(a), [fa, 0, 3]) with a solid line.
* Node: (C(a), [fa, P, 6]) - Connected to (D(a), [fa, 0, 3]) with a solid line.
* Node: (D(a), [fa, P, 7]) - Connected to (C(a), [fa, 0, 4]) with a solid line.
* Node: (E(a), [fa, P, 11]) - Connected to (D(a), [fa, 0, 10]) with a solid line.
* Node: (C(a), [fa, P, 12]) - Connected to (D(a), [fa, 0, 10]) with a solid line.
### Key Observations
* The root node is (A(a), [um, P, 1]).
* The connections between the root node and the second-level nodes are dashed lines, while all other connections are solid lines.
* The letter 'a' appears consistently within the first part of each node label.
* The second element in the square brackets varies between "um", "fa", and "0".
* The third element in the square brackets is always "P".
* The fourth element in the square brackets is a number that appears to increase as you move down the tree.
### Interpretation
The diagram likely represents a hierarchical structure, possibly a derivation tree or a dependency graph. The labels within the nodes could represent attributes or properties associated with each node. The dashed lines might indicate a different type of relationship than the solid lines. The increasing numbers in the node labels could represent an order or level within the hierarchy. Without further context, it's difficult to determine the exact meaning of the diagram, but the structure suggests a systematic relationship between the elements.
</details>
<details>
<summary>x8.png Details</summary>
### Visual Description
## Diagram: Hierarchical Structure with Annotations
### Overview
The image depicts a hierarchical diagram consisting of nodes labeled with expressions and connected by arrows. The arrows indicate a directional relationship between the nodes. The diagram appears to represent a flow or dependency between the nodes, with annotations providing additional information about each node.
### Components/Axes
* **Nodes:** Each node is represented by an expression in the form `(X(a), [Y, Z, N])`, where:
* `X` is a capital letter (A, C, D, E).
* `a` is a variable.
* `Y` is a two-letter code (um, fa).
* `Z` is either 'P' or '0'.
* `N` is a numerical value.
* **Arrows:** Solid arrows indicate a direct relationship, while a dashed arrow indicates a different type of relationship. The arrows point upwards, indicating the direction of the relationship.
### Detailed Analysis
The diagram consists of four nodes arranged vertically, connected by arrows.
1. **Top Node:** `(A(a), [um, P, 1])`
* Located at the top of the diagram.
* Connected to the node below it by a dashed arrow pointing upwards.
2. **Second Node:** `(C(a), [fa, P, 9])`
* Located below the top node.
* Connected to the node below it by a solid arrow pointing upwards.
3. **Third Node:** `(D(a), [fa, 0, 10])`
* Located below the second node.
* Connected to the bottom node by a solid arrow pointing upwards.
4. **Bottom Node:** `(E(a), [fa, P, 11])`
* Located at the bottom of the diagram.
The arrows indicate a flow from the bottom node `(E(a), [fa, P, 11])` to the top node `(A(a), [um, P, 1])`.
### Key Observations
* The two-letter code `Y` alternates between "um" and "fa".
* The value of `Z` is either "P" or "0".
* The numerical value `N` increases from bottom to top, with values 11, 10, 9, and 1.
* The arrow between the top two nodes is dashed, while the other arrows are solid.
### Interpretation
The diagram represents a hierarchical structure or a process flow. The nodes represent states or entities, and the arrows represent transitions or relationships between them. The annotations within each node provide additional information about the state or entity. The dashed arrow between the top two nodes may indicate a different type of relationship or a less direct dependency compared to the solid arrows. The increasing numerical values from bottom to top could represent a progression or a level in the hierarchy. The diagram could be used to model a system, a process, or a classification scheme.
</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}∈\Delta$ , then all the nodes $(\beta_{1},[\_,\texttt{{L}},\texttt{{id}}]),...,(\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}}∈\{\texttt{{P}},\texttt{{O}}\}$ and $\texttt{{T}}∈\{\texttt{{fa}},\texttt{{nf}}\}$ , such that $N$ has children $M_{1},...,M_{k}$ labelled by $\texttt{{L}}^{\prime}∈\{\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≤ j≤ 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
## Diagram: State Transition Diagram
### Overview
The image is a state transition diagram, visually representing a sequence of states and transitions between them. Each state is labeled with a tuple, and transitions are marked with arrows and labels.
### Components/Axes
* **States:** Represented by text in the format `(Label, [Attribute1, Attribute2, Attribute3, Number])`.
* **Transitions:** Represented by arrows labeled with `c1`, `c2`, `r3`, `r4`, `r5`, and `r6`.
* **Root Node:** `T(δ)` at the top of the diagram.
### Detailed Analysis
* **Top Node:** `T(δ)`
* **Level 1:**
* `(Re(v), [nf, P, 1])` is directly below `T(δ)`.
* Transition `r3` points upwards to this node.
* **Level 2:**
* `(FP(v), [nf, P, 2])` is below `(Re(v), [nf, P, 1])`.
* Transition `r6` points upwards to this node.
* **Level 3:**
* `(te(v, KR), [fa, P, 3])` and `(GC(KR), [fa, P, 3])` are below `(FP(v), [nf, P, 2])`.
* Transition `c1` goes from `(te(v, KR), [fa, P, 3])` to `(FP(v), [nf, P, 2])`.
* **Level 4:**
* `(TA(v), [nf, 0, 4])` is to the right of `(te(v, KR), [fa, P, 3])` and `(GC(KR), [fa, P, 3])`.
* Transition `c2` goes from `(TA(v), [nf, 0, 4])` downwards.
* Transition `r4` points upwards to this node.
* **Level 5:**
* `(ta0f(v, KD), [fa, 0, 5])` and `(UC(KD), [fa, 0, 5])` are below `(TA(v), [nf, 0, 4])`.
* **Level 6:**
* `(Le(v), [nf, P, 6])` is below and to the left of `(ta0f(v, KD), [fa, 0, 5])`.
* Transition `r5` points upwards to this node.
* **Level 7:**
* `(te(v, KD), [fa, P, 7])` is below `(Le(v), [nf, P, 6])`.
### Key Observations
* The diagram represents a hierarchical structure with transitions between different states.
* The states are labeled with tuples containing a label and a list of attributes.
* Transitions are labeled with `c1`, `c2`, `r3`, `r4`, `r5`, and `r6`, possibly indicating different types of transitions.
### Interpretation
The diagram likely represents a state machine or a decision tree used in a formal system or algorithm. The labels within the states and the transition labels probably denote specific conditions or actions that trigger the transitions between the states. The diagram's structure suggests a flow of control or data through a series of processing steps, where each state represents a particular stage in the process. The attributes within the states could represent flags, counters, or other relevant data associated with that state. The diagram provides a visual representation of the system's logic and can be used to understand and analyze its behavior.
</details>
<details>
<summary>x10.png Details</summary>
### Visual Description
## Diagram: Tree Structure of Logical Derivation
### Overview
The image depicts a tree diagram representing a logical derivation. It shows the steps and components involved in deriving a conclusion from initial premises. The diagram uses labels and annotations to indicate the logical operations and the flow of reasoning.
### Components/Axes
* **Nodes:** The nodes in the tree represent logical statements or expressions. Each node is labeled with a term and a list of attributes.
* **Edges:** The edges, represented by dotted lines, indicate the derivation steps. Each edge is labeled with a rule number.
* **Labels:**
* `(Re(v), [nf, P, 1])`: Represents a real-valued variable 'v' with attributes 'nf', 'P', and '1'. Located at the top of the diagram.
* `(FP(v), [nf, P, 2])`: Represents a floating-point variable 'v' with attributes 'nf', 'P', and '2'. Located in the middle of the diagram.
* `(te(v, KR), [fa, P, 3])`: Represents a term 'te' involving 'v' and 'KR' with attributes 'fa', 'P', and '3'. Located at the bottom-left of the diagram.
* `(GC(KR), [fa, P, 3])`: Represents a term 'GC' involving 'KR' with attributes 'fa', 'P', and '3'. Located at the bottom-right of the diagram.
* **Rules:**
* `r3`: The rule applied to derive `(FP(v), [nf, P, 2])` from `(Re(v), [nf, P, 1])`.
* `r6`: The rule applied to derive `(te(v, KR), [fa, P, 3])` and `(GC(KR), [fa, P, 3])` from `(FP(v), [nf, P, 2])`.
### Detailed Analysis
The diagram shows a derivation process that starts with a real-valued variable `Re(v)` and proceeds through a floating-point representation `FP(v)` to two terms `te(v, KR)` and `GC(KR)`. The rules `r3` and `r6` represent the logical steps in this derivation.
### Key Observations
* The derivation starts with a real-valued variable and ends with two terms.
* The attributes associated with each node change as the derivation progresses.
* The rules `r3` and `r6` are crucial for understanding the logical steps involved.
### Interpretation
The diagram illustrates a logical derivation process, possibly within a formal system or programming language. It shows how a real-valued variable can be transformed into other terms through specific rules. The attributes associated with each node likely represent properties or constraints relevant to the derivation. The diagram provides a visual representation of the logical flow and the transformations applied at each step.
</details>
<details>
<summary>x11.png Details</summary>
### Visual Description
## Diagram: Tree Structure with Labels
### Overview
The image depicts a tree-like diagram with nodes and connecting dotted lines. Each node contains a label consisting of a function and a list of parameters. The diagram illustrates a hierarchical relationship between the nodes.
### Components/Axes
* **Nodes:** Three nodes are present, one at the top and two at the bottom.
* **Edges:** Dotted lines connect the top node to the two bottom nodes.
* **Labels:** Each node has a label in the format "(Function(arguments), [parameters])".
* **Arrow:** An upward-pointing arrow is located between the top node and the intersection of the dotted lines.
* **Rule Label:** The label "r4" is positioned near the arrow.
### Detailed Analysis
* **Top Node:** The top node is labeled "(TA(v), [nf, 0, 4])".
* **Bottom Left Node:** The bottom left node is labeled "(ta0f(v, KD), [fa, 0, 5])".
* **Bottom Right Node:** The bottom right node is labeled "(UC(KD), [fa, 0, 5])".
* **Connecting Lines:** Dotted lines connect the top node to each of the bottom nodes. The lines converge at a point below the top node.
* **Arrow and Rule:** An upward-pointing arrow is positioned between the top node and the convergence point of the dotted lines. The label "r4" is located to the left of the arrow.
### Key Observations
* The diagram represents a hierarchical structure, with the top node acting as a parent node and the bottom nodes as child nodes.
* The labels within the nodes provide information about the functions and parameters associated with each node.
* The dotted lines indicate a relationship or flow between the nodes.
* The arrow and rule label "r4" suggest a transformation or derivation process.
### Interpretation
The diagram likely represents a step in a formal system, such as a proof or a derivation in logic or computer science. The top node "(TA(v), [nf, 0, 4])" is transformed into the two bottom nodes "(ta0f(v, KD), [fa, 0, 5])" and "(UC(KD), [fa, 0, 5])" according to rule "r4". The functions TA, ta0f, and UC, along with their arguments and parameters, likely have specific meanings within the context of the system being represented. The diagram illustrates how a term or expression is decomposed or rewritten into other terms or expressions.
</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}}∈\{\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
## Diagram: State Transition Diagram
### Overview
The image presents a state transition diagram with three states, labeled A, B, and C. Each state is associated with a tuple containing information about the state and its properties. Transitions between states are represented by arrows.
### Components/Axes
* **States:** A, B, C
* **State Properties:** Each state is associated with a tuple of the form (State(a), [Property1, Property2, Value]).
* A(a) has properties [um, P, 1] and [fa, P, 3]
* B(a) has property [fa, 0, 2]
* C(a) has properties [fa, 0, 2] and [fa, P, 3]
* **Transitions:** Arrows indicate transitions between states.
### Detailed Analysis
* **Top:** State A(a) with properties [um, P, 1]. An arrow points upwards from a central point.
* **Left-Center:** State B(a) with properties [fa, 0, 2]. An arrow points upwards from a central point.
* **Right-Center:** State C(a) with properties [fa, 0, 2].
* **Bottom-Left:** State A(a) with properties [fa, P, 3].
* **Bottom-Right:** State C(a) with properties [fa, P, 3].
* Arrows connect the bottom states to the center states, and the top state.
### Key Observations
* States A and C at the bottom share the same properties: [fa, P, 3].
* States B and C in the center share the same properties: [fa, 0, 2].
* State A at the top has unique properties: [um, P, 1].
* The arrows indicate transitions from the bottom states (A and C) to the center states (B and C) and the top state (A).
### Interpretation
The diagram represents a state machine or a system with different states and transitions. The properties associated with each state likely define the characteristics or conditions of that state. The arrows indicate how the system can move from one state to another. The diagram suggests a flow from the bottom states (A and C with properties [fa, P, 3]) to the center states (B and C with properties [fa, 0, 2]) and finally to the top state (A with properties [um, P, 1]). The properties "um", "fa", "P", and "0" likely represent different attributes or flags associated with each state. The numerical values (1, 2, 3) might represent quantities or levels associated with these attributes.
</details>
<details>
<summary>x13.png Details</summary>
### Visual Description
## Diagram: State Transition Diagram
### Overview
The image depicts a state transition diagram showing transitions between states labeled with expressions involving A(a) and B(a), along with associated parameters. The transitions are represented by upward-pointing arrows, indicating a progression or sequence of states. The diagram appears to be truncated at the bottom, indicated by ellipsis.
### Components/Axes
* **States:** Each state is represented by an expression of the form (X(a), [p1, p2, p3, n]), where X is either A or B, 'a' is a variable, p1, p2, and p3 are parameters (um, fa, P, 0), and n is an integer.
* **Transitions:** Upward-pointing arrows indicate transitions between states.
* **Ellipsis:** "..." at the bottom indicates that the diagram continues.
### Detailed Analysis
The diagram consists of the following states and transitions:
1. **(B(a), [fa, 0, 4])**
2. Transition (upward arrow)
3. **(A(a), [fa, P, 3])**
4. Transition (upward arrow)
5. **(B(a), [fa, 0, 2])**
6. Transition (upward arrow)
7. **(A(a), [um, P, 1])**
8. Transition (upward arrow)
9. "..."
The states alternate between A(a) and B(a). The integer parameter increases by 1 with each transition. The first parameter alternates between "fa" and "um". The second parameter alternates between "0" and "P".
### Key Observations
* The diagram shows a sequence of states alternating between A(a) and B(a).
* The integer parameter in each state's label increments by 1 with each transition.
* The diagram is truncated, suggesting it is part of a larger sequence.
### Interpretation
The diagram represents a state machine or a process that alternates between two types of states, A(a) and B(a). The parameters associated with each state likely represent different properties or conditions of the state. The increasing integer parameter could represent a counter or a step number in the process. The ellipsis indicates that the process continues beyond what is shown in the diagram. The diagram could be used to model a variety of systems, such as a control system, a communication protocol, or a computational algorithm.
</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}}∈\{\texttt{{P}},\texttt{{O}}\}$ and $N_{1}≠ 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}≠\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.
{restatable}
theorem thmcredulous Let $\delta$ be a dialogue for a formula $\phi∈\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.
{restatable}
theorem thmpreferred Let $\delta$ be a dialogue for a formula $\phi∈\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. {restatable} theorem thmground Let $\delta$ be a dialogue for a formula $\phi∈\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.
{restatable}
theoremthmsceptical Let $\delta$ be a dialogue for a formula $\phi∈\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}}∈\{\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}^{±}$ .
**Example 5.16**
*Consider a query $q_{6}=P(a)$ to a $\text{Datalog}^{±}$ KB $\mathcal{K}_{6}=(\mathcal{R}_{6},\mathcal{C}_{6},\mathcal{F}_{6})$ where
| | $\displaystyle\mathcal{R}_{6}=$ | $\displaystyle\{r_{1}:P(x)→ Q(x),r_{2}:Q(x)→ 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
## Diagram: State Transition Diagram Illustrating Infinite Loops
### Overview
The image presents a state transition diagram with two branches, labeled B1 and B2. Branch B1 demonstrates a sequence of states and transitions that lead to an infinite loop. Branch B2 shows a single state.
### Components/Axes
* **Branch Labels:** B1 (top-left), B2 (top-right)
* **States:** P(a), Q(a), R(a)
* **Transitions:** r1, r2
* **Loop Indicator:** "infinite loops" with a bracket encompassing the repeating section of the B1 branch.
### Detailed Analysis
**Branch B1:**
* Starts with state P(a).
* Transitions to the next state via r2.
* Moves to state Q(a).
* Transitions to the next state via r1.
* Returns to state P(a), creating a loop.
* The sequence P(a) -> r2 -> Q(a) -> r1 repeats, indicated by the "infinite loops" label and a bracket.
* The diagram ends with "....." indicating the loop continues indefinitely.
**Branch B2:**
* Consists of a single state R(a).
* No transitions are shown.
### Key Observations
* Branch B1 demonstrates a cyclical process, while Branch B2 represents a static state.
* The "infinite loops" annotation highlights the repeating nature of the transitions in Branch B1.
### Interpretation
The diagram illustrates a scenario where a system can enter an infinite loop due to a specific sequence of states and transitions (Branch B1). This contrasts with a stable state (Branch B2) where no transitions occur. The diagram is likely used to explain or demonstrate a potential problem in a system's design or behavior, where a cyclical process prevents the system from reaching a desired outcome or termination point.
</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}^{±}$ 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.
{restatable}
theoremcompadm Let $\delta$ be a dialogue for a formula $\phi∈\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. {restatable} theoremcomppreferred Let $\delta$ be a dialogue for a formula $\phi∈\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. {restatable} theoremcompground Let $\delta$ be a dialogue for a formula $\phi∈\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.
{restatable}
theoremcompsceptical Let $\delta$ be a dialogue for a formula $\phi∈\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}}∈\{\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}^{±}$ 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},...,\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}⊂eq\mathcal{K}$ be a set of facts and $\mathcal{S}⊂eq\texttt{{Arg}}_{\mathcal{K}}$ be a set of arguments induced from $\mathcal{K}$ . Then,
- $\texttt{{Args}}(\mathcal{X})=\{A∈\texttt{{Arg}}_{\mathcal{K}}\mid\texttt{{%
Sup}}(A)⊂eq\mathcal{X}\}$ are the set of arguments generated by $\mathcal{X}$ ,
- $\texttt{{Base}}(\mathcal{S})=\underset{A∈\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)⊂eq\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}}},...,%
\mathcal{T}^{h}_{\texttt{{G}}}\}$ , such that: For each abstract dialogue tree $\mathcal{T}^{j}_{\texttt{{G}}}$ ( $j=1,...,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}}},...,%
\mathcal{T}^{h}_{\texttt{{G}}}\}$ . For such abstract dialogue tree $\mathcal{T}^{j}_{\texttt{{G}}}$ ( $i=1,...,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∀ A∈\mathcal{%
B}_{1},\alpha∈\texttt{{Sup}}(A)\}⊂eq\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∀ B∈\mathcal{B%
}_{2},\beta∈\texttt{{Sup}}(B)\}⊂eq\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}),...,\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}),...,\mathcal{T}(\delta_{m})$ constructed from $\mathcal{T}(\delta)$ , the focused sub-dialogue $\delta_{i}$ ( $1≤ i≤ 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∈\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}}})⊂eq\mathcal{DE}(\mathcal{T}(%
\delta))$ and $\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})⊂eq\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))⊂eq\mathcal{DE}(\mathcal{T}_{\texttt{{G%
}}})$ and $\mathcal{CU}(\mathcal{T}(\delta))⊂eq\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},...,\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},...,\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≤ k≤ 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}}∈\{\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,...,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,...,m$ , such that $\sigma∈\texttt{{CN}}(\{\omega_{l}\})$ ,
- or (2) $N$ has children that are opponent nodes labelling $\beta_{k}$ , $k=1,...,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,...,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,...,m$ , such that $\sigma∈\texttt{{CN}}(\{\omega_{l}\})$ ,
- or (2) $N$ has children that are proponent nodes labelling $\beta_{k}$ , with $k=1,...,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∈\mathcal{CU}(\mathcal{T}_{\texttt{{G}}})$ , let $arg(\beta_{k})$ , with $k=1,...,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∈\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}),...,\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∈\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∈\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∈\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
\thmcredulous
*
* Proof*
Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ . Let $\mathcal{T}(\delta_{1}),...,\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,...,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})≠\mathcal{DE}(\mathcal{T}_{%
\texttt{{G}}}^{l})$ , with $1≤ i,\ l≤ m,\ i≠ 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·s$ . 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∈\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)≤ 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. ∎
\thmground
*
* Proof*
Let $\mathcal{T}(\delta)$ be a dialogue tree drawn from a dialogue $\delta$ for $\phi$ and $\mathcal{T}(\delta_{1}),...,\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,...,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},...,\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})≠\mathcal{DE}(\mathcal{T}_{%
\texttt{{G}}}^{l})$ , with $1≤ i,\ l,≤ m,\ i≠ 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
\thmsceptical
*
* 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}),...,\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,...,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∈\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,...,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}),...,\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,...,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
\compadm
*
* Proof*
Given $\delta$ be a dialogue for a formula $\phi∈\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},...,\delta_{m}$ , where $i=1,...,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
\compground
*
* Proof*
Given $\delta$ be a dialogue for a formula $\phi∈\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},...,\delta_{m}$ , where $i=1,...,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
\compsceptical
*
* 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∈\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},...,\delta_{m}$ , where $i=1,...,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 $±$ 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 $±$ 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 $±$ . 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)