A formal characterization of the outcomes of rule-based argumentation systems

Abstract

Rule-based argumentation systems are developed for reasoning about defeasible information. As a major feature, their logical language distinguishes between strict rules (encoding strict information) and defeasible rules (describing general behavior with exceptional cases). They build arguments by chaining such rules, define attacks between them, use a semantics for evaluating the arguments and finally identify the plausible conclusions that follow from the rules. Focusing on the family of inconsistency-based attack relations, this paper presents the first study of the outcomes of such systems under various acceptability semantics, namely naive, stable, semi-stable, preferred, grounded and ideal. It starts by extending the existing list of rationality postulates that any rule-based system should satisfy. Then, it defines the key notion of option of a theory (a theory being a set of facts, a set of strict rules and a set of defeasible rules). For each of the cited semantics, it characterizes the extensions of a rule-based system that satisfies all the postulates in terms of options of the theory under which the system is built. It also fully characterizes the set of plausible conclusions of the system. The results show that designing a rule-based argumentation system requires great care.

1 Introduction

Argumentation is a promising approach for reasoning about inconsistent information. It consists of generating arguments that support claims, defining attacks between them, evaluating the arguments using a given semantics and finally identifying the plausible claims on the basis of the strength of their arguments.

Dung proposed in [1] various semantics at an abstract level, i.e., without taking into account the structure of arguments or the nature of attacks. His abstract framework was instantiated by several scholars. The idea is as follows: Start with a knowledge base whose elements are encoded in a logical language, generate arguments using the consequence operator attached to the language, identify the attacks and apply Dung’s semantics for the evaluation task. There were two major categories of instantiations for this abstract framework. The first category uses deductive logics (such as propositional logic [2, 3] or any Tarskian logic [4]), whereas the second category uses rule-based languages. These languages distinguish between:

• facts which are information about particular instances like “My laptop is heavy.”

• strict rules which encode general laws about classes of instances like “First generation laptops are heavy.” Such rules do not have exceptions.

• defeasible rules which describe general behavior with exceptional cases. Defeasible rules correspond thus to what is called defaults in [5] or conditional assertions in [6, 7].

Examples of rule-based argumentation systems are: aspic [8], its extended version aspic+ [9], DeLP [10] and the systems developed in [11,12,13,14,15]. Despite the popularity of these systems, the results they return have not been characterized yet, except the system discussed in [11]. The following questions are thus still open:

• what are the underpinnings of the extensions under various semantics?

• do the semantics return different results as at the abstract level?

• what is the number of extensions a system may have?

• what are the plausible conclusions with such systems?

In this paper, we answer all the four questions in three steps: We start by defining a rule-based argumentation system over a knowledge base called theory (a set of facts, a set of strict rules and a set of defeasible rules). The system uses a notion of derivation schema for generating arguments from the theory. For the sake of generality, the attack relation is left unspecified. However, it has the property of being conflict-dependent, that is, it captures the inconsistency that may be present in the theory. It is worth mentioning that all existing attack relations (like rebuttal and assumption attack) are conflict-dependent. A notable exception is undercutting which aims at blocking the application of defeasible rules [16].

In a second step, we extend the list of postulates (consistency, closure under strict rules) proposed in [17]. The aim of those postulates is to mathematically capture what humans perceive as rationale behavior from the semantics of defeasible theories. They are thus desirable properties that a system should satisfy. We introduce three new postulates. The first one, strict precedence, ensures that any claim that follows from the strict part of a theory is a plausible conclusion of the argumentation system. The second postulate, exhaustiveness, ensures a form of completeness of the extensions of an argumentation system. The third postulate, closure under sub-arguments, states that an argument cannot be accepted if one of its sub-parts is questionable.

Finally, we investigate the outputs of rule-based argumentation systems that satisfy all the postulates. We show that naive extensions return options of the theory (an option being a sub-theory that gathers a maximal-up to consistency-set of the facts, strict rules, and defeasible rules). Furthermore, the set of plausible conclusions under the naive semantics contains all the conclusions that are drawn from all the options. Stable extensions return preferred options but not necessarily all of them; it depends on the attack relation at work. Unlike options, preferred options are options that contain the strict part. Should not all preferred options be picked as stable extensions, defining an attack relation that discards exactly the spurious ones thus turns out to be tricky. The same results hold under preferred semantics. We also characterize both ideal and grounded extensions. We show that the ideal extension of an argumentation system is the set of arguments built from the free part of a theory (i.e., the sub-theory that contains the strict part as well as all defeasible rules that are not involved in any minimal conflict). The grounded extension is a subset of the ideal extension. This means that under grounded semantics, an argumentation system may miss intuitive conclusions.

The paper is structured as follows: Section 2 recalls Dung’s semantics. Section 3 introduces the logical language that will be used in the paper. Section 4 defines rule-based argumentation systems. Section 5 introduces a list of postulates that such systems should satisfy. Section 6 studies the outcomes of rule-based systems under naive, stable, semi-stable, preferred, grounded and ideal semantics. Section 7 discusses how our results may apply to existing systems, and the last section concludes.

2 Abstract argumentation framework

An argumentation framework consists of a set of arguments and a binary relation expressing attacks among the arguments. Throughout this section, the structure and the origin of arguments are left unspecified.

Definition 1

(Argumentation framework) An argumentation framework is a pair ${\mathcal {H}}= ({\mathcal {A}}, {\mathcal {R}})$ where ${\mathcal {A}}$ is a non-empty (possibly infinite) set of arguments and ${\mathcal {R}}\subseteq {\mathcal {A}}\times {\mathcal {A}}$ is an attack relation. A pair $(a,b) \in {\mathcal {R}}$ means that a attacks b. A set ${\mathcal {E}}\subseteq {\mathcal {A}}$ attacks an argument b iff $\exists a \in {\mathcal {E}}$ such that $(a,b) \in {\mathcal {R}}$.

Notation :

We sometimes use the infix notation $a {\mathcal {R}}b$ to denote $(a, b) \in {\mathcal {R}}$.

An argumentation framework $({\mathcal {A}}, {\mathcal {R}})$ is represented as a graph, argumentation graph, whose nodes are the arguments of ${\mathcal {A}}$ and its edges are the attacks in ${\mathcal {R}}$. Arguments are evaluated using a semantics, i.e., a set of criteria that should be satisfied by an argument in order to be acceptable. Throughout this paper, we focus on extension-based semantics initially introduced by Dung [1]. Such semantics look for acceptable sets of arguments, called extensions. Each extension represents a coherent point of view and satisfies two basic properties: conflict-freeness and defense.

Definition 2

(Conflict-freeness, defense, admissibility) Let ${\mathcal {H}}= ({\mathcal {A}}, {\mathcal {R}})$ be an argumentation framework and ${\mathcal {E}}\subseteq {\mathcal {A}}$.

• ${\mathcal {E}}$ is conflict-free iff $\not \exists a, b \in {\mathcal {E}}$ such that $(a, b) \in {\mathcal {R}}$.

• ${\mathcal {E}}$defends an argument a iff $\forall b \in {\mathcal {A}}$, if $(b, a) \in {\mathcal {R}}$, then ${\mathcal {E}}$ attacks b.

• ${\mathcal {E}}$ is an admissible set iff ${\mathcal {E}}$ is conflict-free and defends all its elements.

The following definition recalls the main semantics that were proposed in [1, 18, 19]. It is worth noticing that all those semantics are based on the notion of admissibility.

Definition 3

(Semantics) Let ${\mathcal {H}}= ({\mathcal {A}}, {\mathcal {R}})$ be an argumentation framework, and ${\mathcal {E}}\subseteq {\mathcal {A}}$ be a conflict-free set.

• ${\mathcal {E}}$ is a naive extension iff it is a maximal (w.r.t. $\subseteq$) conflict-free set.

• ${\mathcal {E}}$ is a complete extension iff ${\mathcal {E}}$ is an admissible set that contains any argument it defends.

• ${\mathcal {E}}$ is a preferred extension iff ${\mathcal {E}}$ is a maximal (w.r.t. $\subseteq$) complete extension.

• ${\mathcal {E}}$ is a stable extension iff ${\mathcal {E}}$ attacks any argument in ${\mathcal {A}}{\setminus } {\mathcal {E}}$.

• ${\mathcal {E}}$ is a semi-stable extension iff ${\mathcal {E}}$ is a complete extension and the union of the set ${\mathcal {E}}$ and the set of all arguments attacked by ${\mathcal {E}}$ is maximal (w.r.t. $\subseteq$).

• ${\mathcal {E}}$ is a grounded extension iff ${\mathcal {E}}$ is a minimal (w.r.t. $\subseteq$) complete extension.

• ${\mathcal {E}}$ is an ideal extension iff ${\mathcal {E}}$ is a maximal (w.r.t. $\subseteq$) admissible set contained in every preferred extension.

An argumentation framework has a single grounded (respectively ideal) extension. However, it may have several naive, admissible, complete, preferred, stable and semi-stable extensions. It may also have zero stable extensions.

Notations :

Let ${\mathcal {H}}= ({\mathcal {A}}, {\mathcal {R}})$ be an argumentation framework. We denote by $\mathtt {Ext}_x({\mathcal {H}})$ the set of all extensions of ${\mathcal {H}}$ under semantics $x \in \{n, p, s, ss\}$, where n (respectively p, s, ss) stands for naive (respectively preferred, stable and semi-stable). We denote by $\mathtt {GE}({\mathcal {H}})$ (respectively $\mathtt {IE}({\mathcal {H}})$) the single grounded (respectively ideal) extension of ${\mathcal {H}}$. When we do not need to refer to a particular semantics, we write $\mathtt {Ext}({\mathcal {H}})$ for short.

The following result recalls some key properties of these semantics.

Property 1

[1, 18, 19] Let ${\mathcal {H}}= ({\mathcal {A}}, {\mathcal {R}})$ be an argumentation framework.

• $\mathtt {Ext}_s({\mathcal {H}})\subseteq \mathtt {Ext}_n({\mathcal {H}})$

• $\mathtt {Ext}_s({\mathcal {H}})\subseteq \mathtt {Ext}_p({\mathcal {H}})$

• If $|\mathtt {Ext}_s({\mathcal {H}})| > 0$, then $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})$

• ${\mathcal {H}}$ has one grounded (respectively ideal) extension

• $\mathtt {GE}({\mathcal {H}})\subseteq \mathtt {IE}({\mathcal {H}})$

When $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_p({\mathcal {H}})$, the framework ${\mathcal {H}}$ is said to be coherent. It is also worth recalling that an argumentation framework that has an infinite set of arguments may have an infinite number of extensions (under multiple-extensions semantics).

Let us now illustrate the different semantics on the argumentation framework ${\mathcal {H}}_1$ depicted below.

This framework has eight naive extensions:

• ${\mathcal {E}}_1 = \{a, c, g\}$,

• ${\mathcal {E}}_2 = \{d, e, f\}$,

• ${\mathcal {E}}_3 = \{b, d, f\}$,

• ${\mathcal {E}}_4 = \{a, e, g\}$,

• ${\mathcal {E}}_5 = \{a, b, g\}$,

• ${\mathcal {E}}_6 = \{b, e, g\}$,

• ${\mathcal {E}}_7 = \{b, d, g\}$, and

• ${\mathcal {E}}_8 = \{c, f\}$.

${\mathcal {H}}_1$ has one stable/semi-stable extension ${\mathcal {E}}_3$ and two preferred extensions: ${\mathcal {E}}_3$ and ${\mathcal {E}}_6 = \{a, g\}$. Its grounded and ideal extensions are empty ($\mathtt {GE}({\mathcal {H}}_1) = \mathtt {IE}({\mathcal {H}}_1) = \emptyset$).

Consider now the following argumentation framework ${\mathcal {H}}_2$ borrowed from [19]. It lays bare some differences between ideal and grounded semantics.

It can be checked that:

• $\mathtt {GE}({\mathcal {H}}_2) = \emptyset$,

• $\mathtt {Ext_p}({\mathcal {H}}_2) = \{\{b,c\}, \{b,d\}\}$, and

• $\mathtt {IE}({\mathcal {H}}_2) = \{b\}$.

Throughout the paper, we will refer to the seven semantics of Definition 3 by the reviewed semantics, and by extension-based semantics to any semantics, which partitions the power set of the set of arguments into two parts: extensions and non-extensions. Note that there are other semantics in the literature like recursive [20] and stage [21] that follow this line of research. This distinction is important since some of the results in the next sections hold for any extension-based semantics, while others hold under the reviewed ones.

3 Rule-based logical language

In what follows, ${\mathcal {L}}$ is a set of literals, i.e., atoms or negation of atoms. The negation of an atom x from ${\mathcal {L}}$ is denoted $\lnot x$. We consider two additional constants $\top$ and $\sigma$ such that $\top \notin {\mathcal {L}}$ and $\sigma \notin {\mathcal {L}}$. Three kinds of information are distinguished:

• Facts, which are elements of ${\mathcal {L}}\cup \{\top \}$

• Strict rules, which are of the form $x_1, \ldots , x_n \rightarrow x$ ($x, x_1,\ldots , x_n$ denoting literals in ${\mathcal {L}}$)

• Defeasible rules, which are of the form $x_1, \ldots , x_n \Rightarrow x$ or of the form $\top \Rightarrow x$ ($x, x_1,\ldots , x_n$ denoting literals in ${\mathcal {L}}$)

Facts are information about particular instances. A strict rule expresses general information that has no exception. It is read as follows: If $x_1, \ldots , x_n$ hold, then x always holds. A defeasible rule of the form $x_1, \ldots , x_n \Rightarrow x$ expresses general information that may have exceptions and is read as follows: If $x_1, \ldots , x_n$ hold, then generally x holds as well. A defeasible rule of the form $\top \Rightarrow x$ expresses that x is a defeasible fact and is read as follows: generally x holds. Unlike existing systems like ASPIC [8] where a strict rule with an empty body represents a fact, in our formalism we keep general information and factual information separate.

Let ${\mathcal {L}}'$ be a set of atoms used for naming rules with the constraints ${\mathcal {L}}\cap {\mathcal {L}}' = \emptyset$, $\top \notin {\mathcal {L}}'$ and $\sigma \notin {\mathcal {L}}'$. Every rule has a unique name and two rules cannot have the same name. Throughout the paper, rules are named $r, r_1, r_2, \ldots$

Definition 4

(Theory) A theory is a triple ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ where ${\mathcal {F}}= \{\top \} \cup X$, with $X \subseteq {\mathcal {L}}$, is a set of facts, and ${\mathcal {S}}\subseteq {\mathcal {L}}'$ (respectively ${\mathcal {D}}\subseteq {\mathcal {L}}'$) is a set of strict (respectively defeasible) rules’ names. ${\mathcal {T}}$ is finite iff all three sets ${\mathcal {F}}$, ${\mathcal {S}}$ and ${\mathcal {D}}$ are finite.

Note that $\top$ is a fact in any theory. Note also that the two sets ${\mathcal {S}}$ and ${\mathcal {D}}$ contain names of rules and not the corresponding rules themselves. Throughout the paper, $({\mathcal {F}}, {\mathcal {S}}, \emptyset )$ is referred to as the strict part of a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$.

Notations :

Let $r \in {\mathcal {L}}'$, the function $\mathtt {Rule}(r)$ returns the (strict or defeasible) rule whose name is r. For each rule $x_1, \ldots , x_n \rightarrow x$ (respectively $x_1, \ldots , x_n \Rightarrow x$ or $\top \Rightarrow x$) whose name is r, the head of the rule is $\mathtt {Head}(r) = x$ and the body of the rule is $\mathtt {Body}(r) = \{x_1, \ldots , x_n\}$ or $\mathtt {Body}(r) = \{\top \}$. Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ and ${\mathcal {T}}' = ({\mathcal {F}}', {\mathcal {S}}', {\mathcal {D}}')$ be two theories. We say that ${\mathcal {T}}$ is a sub-theory of ${\mathcal {T}}'$, written ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$, iff ${\mathcal {F}}\subseteq {\mathcal {F}}'$ and ${\mathcal {S}}\subseteq {\mathcal {S}}'$ and ${\mathcal {D}}\subseteq {\mathcal {D}}'$. The relation $\sqsubset$ is the strict version of $\sqsubseteq$ (i.e., it is the case that at least one of the three inclusions is strict).

The notion of consistency is defined as follows:

Definition 5

(Consistency) A set $X \subseteq {\mathcal {L}}$ is consistent iff $\not \exists x, y \in X$ such that $x = \lnot y$. It is inconsistent otherwise.

This simple definition of consistency is sufficient since the language ${\mathcal {L}}$ contains only literals. However, it is not suitable in case of richer languages. Assume that ${\mathcal {L}}$ is a propositional language. Thus, the set $\{x, y, \lnot x \vee \lnot y\}$ is consistent with respect to the above definition while it is clearly not the case. Thus, richer languages require a stronger definition of consistency like the one proposed in [22].

Without loss of generality, throughout the paper we make the three following assumptions about rules.

Assumptions :

The body of every (strict/defeasible) rule is finite and not empty. Moreover, for each rule r, $\mathtt {Body}(r) \cup \{\mathtt {Head}(r)\}$ is consistent. We say that r is consistent.

Note that the fact that rules are consistent does not ensure the consistency of a set of rules. [23] discussed different forms of rule consistency. One of them is illustrated by the example $\{x \Rightarrow y, y \Rightarrow \lnot x\}$ where both defeasible rules are consistent whereas together lead to an inconsistent rule $x \Rightarrow \lnot x$.

Let us now show how new information (i.e., literal) is produced from a given theory. This is generally the case when (strict and/or defeasible) rules are fired in a derivation schema. Below we provide a definition which generalizes derivations as defined by [10, 24] and others.

Definition 6

(Derivation schema) Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory, $x \in {\mathcal {L}}$. A derivation schema for x from ${\mathcal {T}}$ is a finite sequence $d = \langle (x_1, r_1),\ldots ,(x_n, r_n)\rangle$ such that:

• $x_n = x$

• for $i \in \{1, \ldots , n\}$,

  • $x_i \in {\mathcal {F}}$ and $r_i = \sigma$, or

  • $x_i = \mathtt {Head}(r_i)$, with $r_i \in {\mathcal {S}} \cup {\mathcal {D}}$ and $\mathtt {Body}(r_i) \subseteq \{x_1,..,x_{i-1}\}$

• $\mathtt {Seq}(d)$ = $\{x_1, \ldots , x_n\}$.

• $\mathtt {Facts}(d)$ = $\{x_i \mid i \in \{1,\ldots ,n\}, r_i = \sigma \}$.

• $\mathtt {Strict}(d)$ = $\{r_i \mid i \in \{1,\ldots ,n\}, r_i \in {\mathcal {S}} \}$.

• $\mathtt {Def}(d)$ = $\{r_i \mid i \in \{1,\ldots ,n\}, r_i \in {\mathcal {D}} \}$.

In order to improve readability, we somehow abuse the notation: we use the rules themselves instead of their names.

Example 1

Consider the theory ${\mathcal {T}}_1$ such that ${\mathcal {F}}_1$, ${\mathcal {S}}_1$, ${\mathcal {D}}_1$ are as follows.

$$\begin{aligned} {\mathcal {F}}_1 \left\{ \begin{array}{@{}l} p \\ q \end{array}\right. \qquad \qquad {\mathcal {S}}_1 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l} p &{} \rightarrow &{} s &{} (r_1) \\ q &{} \rightarrow &{} \lnot s &{} (r_2) \\ p,s &{} \rightarrow &{} u &{} (r_3) \end{array}\right. \qquad \qquad {\mathcal {D}}_1 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} \lnot s &{} \Rightarrow &{} t &{} (r_4) \\ t,u &{} \Rightarrow &{} v &{} (r_5) \\ p &{} \Rightarrow &{} q &{} (r_6) \end{array}\right. \end{aligned}$$

Each of (1)–(7) below is a derivation schema from theory ${\mathcal {T}}_1$

$$\begin{aligned} \langle (p,\sigma )\rangle \end{aligned}$$

(1)

$$\begin{aligned} \langle (q,\sigma ),(\lnot s,r_2)\rangle \end{aligned}$$

(2)

$$\begin{aligned} \langle (p,\sigma ),(s,r_1),(u,r_3)\rangle \end{aligned}$$

(3)

$$\begin{aligned} \langle (p,\sigma ),(s,r_1),(p,\sigma ),(u,r_3)\rangle \end{aligned}$$

(4)

$$\begin{aligned} \langle (p,\sigma ),(q,\sigma ),(s,r_1),(u,r_3)\rangle \end{aligned}$$

(5)

$$\begin{aligned} \langle (p,\sigma ),(q,r_6),(\lnot s,r_2)\rangle \end{aligned}$$

(6)

$$\begin{aligned} \langle (p,\sigma ),(q,\sigma ),(\lnot s,r_2),(s,r_1),(u,r_3),(t,r_4), (v,r_5)\rangle \end{aligned}$$

(7)

A derivation schema is not necessarily consistent (such as (7) above), as it may contain opposite literals in the form $x_i = \lnot x_j$ for some i and j. (A derivation d is consistent iff $\mathtt {Seq}(d)$ is consistent.) Moreover, a derivation schema is not necessarily minimal (for set inclusion) as shown in Example 1: compare (3) with (4). The former is a proper sub-sequence of the latter.

Definition 7

(Minimal derivation schema) Let ${\mathcal {T}}$ be a theory and $x \in {\mathcal {L}}$. A derivation schema for x from ${\mathcal {T}}$ is minimal iff none of its proper subsequences is a derivation schema for x from ${\mathcal {T}}$.

Interestingly enough, there are two ways for a derivation schema not to be minimal for set inclusion: (i) involving superfluous literals, i.e., literals that do not serve toward inferring the conclusion as is illustrated by (5) in Example 1 (q is of no use there), (ii) involving redundancy (hence, repeated literals) as illustrated by (4) in Example 1 (p is repeated twice).

Definition 8

(Focused derivation schema) Let ${\mathcal {T}} = ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory and $x \in {\mathcal {L}}$. A derivation schema $d = \langle (x_1,r_1),\ldots ,(x_n,r_n)\rangle$ for x from ${\mathcal {T}}$ is focused iff it can be reduced to a minimal one by just deleting repeated pairs $(x_i,r_i)$.

Property 2

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory and $x \in {\mathcal {L}}$. A derivation schema $d = \langle (x_1,r_1), \ldots , (x_n,r_n)\rangle$ for x from ${\mathcal {T}}$ is minimal iff d is focused and the literals $x_1, \ldots , x_n$ are pairwise distinct.

Notations :

For a theory ${\mathcal {T}}$, $\mathtt {CN}({\mathcal {T}})$ denotes the set of all literals that have a derivation schema from ${\mathcal {T}}$. We call $\mathtt {CN}({\mathcal {T}})$ the potential consequences drawn from ${\mathcal {T}}$ (for short, consequences) but they need not be definitive as they may happen to be dismissed by opposite conclusions.

The following property applies to the consequences drawn from a given theory.

Property 3

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

• $\mathtt {CN}({\mathcal {T}}) \subseteq {\mathcal {F}}\cup \{\mathtt {Head}(r) \mid r \in {\mathcal {S}}\cup {\mathcal {D}}\} \subseteq {\mathcal {L}}$

• If ${\mathcal {T}}$ is finite, then $\mathtt {CN}({\mathcal {T}})$ is finite

• ${\mathcal {F}}\subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq \mathtt {CN}({\mathcal {T}})$

• $\top \in \mathtt {CN}({\mathcal {T}})$

• $\mathtt {CN}({\mathcal {T}}) = \{\top \}$ iff ${\mathcal {F}}= \{\top \}$ and $\not \exists r \in {\mathcal {D}}$ such that $\mathtt {Body}(r) = \{\top \}$.

• If d is a derivation schema from ${\mathcal {T}}$, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {T}})$

Some rules may not be activated (i.e., the literals in their body have no derivation schema). Let us consider the following example.

Example 2

Let ${\mathcal {T}}_2 = ({\mathcal {F}}_2, {\mathcal {S}}_2, {\mathcal {D}}_2)$ be a theory such that

$$\begin{aligned} {\mathcal {F}}_2 \left\{ \begin{array}{@{}l} p \\ q \end{array}\right. \qquad \qquad {\mathcal {S}}_2 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l} p &{} \rightarrow &{} t &{} (r_1) \\ s &{} \rightarrow &{} u &{} (r_2) \end{array}\right. \qquad \qquad {\mathcal {D}}_2 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} p &{} \Rightarrow &{} q &{} (r_3) \\ u &{} \Rightarrow &{} v &{} (r_4) \end{array}\right. \end{aligned}$$

There are rules here whose head is not a consequence of ${\mathcal {T}}_2$. In symbols, $\mathtt {CN}({\mathcal {T}}_2) = \{p, q, t\} \subset \{p, q, t, u, v\} = {\mathcal {F}}_2 \cup \{\mathtt {Head}(r) \ | \ r \in {\mathcal {S}}_2 \cup {\mathcal {D}}_2\}$. Namely, the two rules $r_2$ and $r_4$ are not activated.

It is also easy to show that $\mathtt {CN}$ is monotonic. Note that a similar result was shown in [25] for the logic underlying the ASPIC system [8].

Property 4

Let ${\mathcal {T}}$ and ${\mathcal {T}}'$ be two theories. If ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$ then $\mathtt {CN}({\mathcal {T}}) \subseteq \mathtt {CN}({\mathcal {T}}')$.

Let us now introduce the key notion of option which is useful for characterizing the extensions of argumentation systems under various semantics. An option is a maximal (for set inclusion) consistent sub-theory of a given theory.

Definition 9

(Option) Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory. An option of ${\mathcal {T}}$ is a sub-theory ${\mathcal {T}}' = ({\mathcal {F}}', {\mathcal {S}}', {\mathcal {D}}')$ of ${\mathcal {T}}$ such that:

• ${\mathcal {F}}' \subseteq {\mathcal {F}}$, ${\mathcal {S}}' \subseteq {\mathcal {S}}$ and ${\mathcal {D}}' \subseteq {\mathcal {D}}$

• $\mathtt {CN}({\mathcal {T}}')$ is consistent

• $\not \exists {\mathcal {T}}'' \sqsubseteq {\mathcal {T}}$ such that ${\mathcal {T}}' \sqsubset {\mathcal {T}}''$ and $\mathtt {CN}({\mathcal {T}}'')$ is consistent.

$\mathtt {Opt}({\mathcal {T}})$ denotes the set of all options of ${\mathcal {T}}$.

Let us illustrate this new notion by the following example.

Example 3

Consider ${\mathcal {T}}_3$ such that ${\mathcal {F}}_3$, ${\mathcal {S}}_3$, ${\mathcal {D}}_3$ are as follows.

$$\begin{aligned} {\mathcal {F}}_3 \left\{ \begin{array}{l} p \\ q \\ \lnot s \end{array}\right. \qquad \qquad {\mathcal {S}}_3 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l} t, v\rightarrow & {} s&(r_1) \end{array}\right. \qquad \qquad {\mathcal {D}}_3 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} p &{} \Rightarrow &{} t &{} (r_2) \\ q &{} \Rightarrow &{} u &{} (r_3) \\ u &{} \Rightarrow &{} v &{} (r_4) \end{array}\right. \qquad \qquad \end{aligned}$$

The theory ${\mathcal {T}}_3$ has seven options:

• ${\mathcal {O}}_1 = ({\mathcal {F}}_3, {\mathcal {S}}_3, \{r_2, r_3\})$

• ${\mathcal {O}}_2 = ({\mathcal {F}}_3, {\mathcal {S}}_3, \{r_2, r_4\})$

• ${\mathcal {O}}_3 = ({\mathcal {F}}_3, {\mathcal {S}}_3, \{r_3, r_4\})$

• ${\mathcal {O}}_4 = ({\mathcal {F}}_3, \emptyset , {\mathcal {D}}_3)$

• ${\mathcal {O}}_5 = (\{p, q\}, {\mathcal {S}}_3, {\mathcal {D}}_3)$

• ${\mathcal {O}}_6 = (\{p, \lnot s\}, {\mathcal {S}}_3, {\mathcal {D}}_3)$

• ${\mathcal {O}}_7 = (\{q, \lnot s\}, {\mathcal {S}}_3, {\mathcal {D}}_3)$

A theory has at least one option which is the theory itself in case it is consistent. This is the case in Example 2: $\mathtt {Opt}({\mathcal {T}}_2) = \{{\mathcal {T}}_2\}$.

Property 5

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

• $\mathtt {Opt}({\mathcal {T}}) \ne \emptyset$.

• $\mathtt {Opt}({\mathcal {T}}) = \{{\mathcal {T}}\}$ iff $\mathtt {CN}({\mathcal {T}})$ is consistent.

We show next that options are all pairwise distinct.

Proposition 1

For all ${\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Opt}({\mathcal {T}})$, if $\mathtt {CN}({\mathcal {O}}) = \mathtt {CN}({\mathcal {O}}')$, then ${\mathcal {O}}= {\mathcal {O}}'$.

The definition of option does not make any difference between the strict part of a theory (i.e., its facts and strict rules) and its defeasible part. In rule systems [24], the former takes precedence over the latter since it represents the “certain” information of a theory. For instance, in default logic the certain part belongs to every extension of a theory [5]. This precedence is captured by the following notion of preferred option.

Definition 10

(Preferred option) Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory. A preferred option of ${\mathcal {T}}$ is a sub-theory ${\mathcal {T}}' = ({\mathcal {F}}', {\mathcal {S}}', {\mathcal {D}}')$ of ${\mathcal {T}}$ such that:

• ${\mathcal {F}}' = {\mathcal {F}}$ and ${\mathcal {S}}' = {\mathcal {S}}$, ${\mathcal {D}}' \subseteq {\mathcal {D}}$,

• $\mathtt {CN}({\mathcal {T}}')$ is consistent,

• $\forall r \in {\mathcal {D}}{\setminus } {\mathcal {D}}'$, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}' \cup \{r\}))$ is inconsistent.

$\mathtt {POpt}({\mathcal {T}})$ denotes the set of all preferred options of ${\mathcal {T}}$.

Let us illustrate this notion by an example.

Example 3 (Cont)

The theory ${\mathcal {T}}_3$ has three preferred options: ${\mathcal {O}}_1$, ${\mathcal {O}}_2$ and ${\mathcal {O}}_3$. $\square$

Unlike options, the defeasible rules of a theory do not necessarily belong to at least one preferred option of the theory as shown by the following example.

Example 4

The theory ${\mathcal {T}}_4$ such that

$$\begin{aligned} {\mathcal {F}}_4 \left\{ \begin{array}{l} p \\ q \end{array}\right. \qquad \qquad {\mathcal {S}}_4 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l} p\rightarrow & {} s&(r_1) \end{array}\right. \qquad \qquad {\mathcal {D}}_4 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} p\Rightarrow & {} \lnot s&(r_2) \end{array}\right. \end{aligned}$$

has a single preferred option ${\mathcal {O}}= ({\mathcal {F}}_4, {\mathcal {S}}_4, \emptyset )$ which does not contain the unique defeasible rule $r_2$.

Every preferred option is an option. The converse holds only when the theory is consistent in which case the latter is the only (preferred) option (cf. Property 5).

Property 6

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

• $\mathtt {POpt}({\mathcal {T}})\subseteq \mathtt {Opt}({\mathcal {T}})$.

• $\mathtt {Opt}({\mathcal {T}}) \subseteq \mathtt {POpt}({\mathcal {T}})$ iff $\mathtt {CN}({\mathcal {T}})$ is consistent.

A theory may not have preferred options. This is in particular the case when the strict part (the set of facts and strict rules) is inconsistent.

Property 7

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

• $\mathtt {POpt}({\mathcal {T}})= \emptyset$ iff $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ is inconsistent.

• For all $r \in {\mathcal {D}}$, if $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \{r\}))$ is consistent, then there exists a preferred option ${\mathcal {O}}$ such that $({\mathcal {F}}, {\mathcal {S}}, \{r\}) \sqsubseteq {\mathcal {O}}$.

Notice that the set of consequences of an (preferred) option is not necessarily maximal for set inclusion as shown by Example 3.

Example 3 (Cont)

We have $\mathtt {CN}({\mathcal {O}}_1) = \{p, q, \lnot s, t, u\}$ and $\mathtt {CN}({\mathcal {O}}_2) = \{p, q, \lnot s, t\}$. Thus, $\mathtt {CN}({\mathcal {O}}_2) \subseteq \mathtt {CN}({\mathcal {O}}_1)$. $\square$

Notations :

For a set ${\mathcal {B}}$ of theories, we denote the set of its maximal elements as $\mathtt {Max}({\mathcal {B}}) = \{{\mathcal {T}}\in {\mathcal {B}}\mid \not \exists {\mathcal {T}}' \in {\mathcal {B}} \text{ such } \text{ that } \mathtt {CN}({\mathcal {T}}) \varsubsetneq \mathtt {CN}({\mathcal {T}}')\}$.

Note that in general, maximal preferred options may be different from maximal options. Consider, for instance, the theory in Example 3. Its maximal options are ${\mathcal {O}}_4$ and ${\mathcal {O}}_5$, while its maximal preferred options are ${\mathcal {O}}_1$ and ${\mathcal {O}}_3$.

Let us now introduce the concept of free part of a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. It is the sub-theory that is made of the set of facts, the set of strict rules and the defeasible rules which are involved in every preferred option of ${\mathcal {T}}$.

Definition 11

(Free sub-theory) The free sub-theory of a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ is $\mathtt {Free}({\mathcal {T}})= ({\mathcal {F}}, {\mathcal {S}}, \bigcap \limits _{({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}_i) \in \mathtt {POpt}({\mathcal {T}})} {\mathcal {D}}_i).$

The following result summarizes some basic properties of this sub-theory.

Property 8

Let ${\mathcal {T}}$ be a theory.

• For any ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$, $\mathtt {Free}({\mathcal {T}})\sqsubseteq {\mathcal {O}}$

• $\mathtt {CN}(\mathtt {Free}({\mathcal {T}}))$ is consistent

4 Rule-based argumentation systems

In this section, we propose an instantiation of Dung’s framework that allows reasoning about defeasible information, i.e., drawing conclusions from a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. The instantiation is referred to as argumentation system keeping thus the term framework for the abstract formalism of Dung. The backbone of an argumentation system is naturally the notion of argument. Intuitively, an argument is a justification of a claim, i.e., it provides evidence that the claim is true. Thus, it should satisfy at least the three following basic properties: (i) internal coherence, (ii) relevance to the claim it justifies and (iii) truth preserving (i.e., it guarantees the truth of the claim). It is true that humans’ arguments may be inconsistent, but they are seen as fallacious by reasonable people. Furthermore, the topic of the paper is not reasoning about humans’ arguments. It is rather reasoning about inconsistent theories by using arguments as a building block of the proposed logic.

Definition 12

(Argument) Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory. An argument defined from ${\mathcal {T}}$ is a pair (d, x) such that:

• $x \in {\mathcal {L}}$

• d is a derivation schema for x from ${\mathcal {T}}$     (Truth preserving)

• $\mathtt {Seq}(d)$ is consistent     (Internal coherence)

• $\not \exists {\mathcal {T}}' \sqsubset (\mathtt {Facts}(d), \mathtt {Strict}(d), \mathtt {Def}(d))$ such that $x \in \mathtt {CN}({\mathcal {T}}')$     (Relevance)

An argument (d, x) is strict iff $\mathtt {Def}(d) = \emptyset$.

Example 1 (Cont)

Below are the nine arguments that are built from the theory ${\mathcal {T}}_1$.

• $(\langle (p,\sigma )\rangle , p)$

• $(\langle (q,\sigma )\rangle , q)$

• $(\langle (p,\sigma ), (q, r_6)\rangle , q)$

• $(\langle (p,\sigma ), (s, r_1)\rangle , s)$

• $(\langle (q,\sigma ), (\lnot s, r_2)\rangle , \lnot s)$

• $(\langle (p,\sigma ), (q, r_6), (\lnot s, r_2)\rangle , \lnot s)$

• $(\langle (p,\sigma ), (s, r_1), (u, r_3)\rangle , u)$

• $(\langle (q,\sigma ), (\lnot s, r_2), (t, r_4)\rangle , t)$

• $(\langle (p,\sigma ), (q, r_6), (\lnot s, r_2), (u, r_3)\rangle , t)$

Note that there is no argument in favor of v since all derivation schemas for v are inconsistent. Derivations (4) and (5) do not give birth to arguments since they are not minimal. $\square$

Notations :

Let ${\mathcal {T}}$ be a theory, ${\mathtt {Arg}}({\mathcal {T}})$ denotes the set of all arguments built from ${\mathcal {T}}$ in the sense of Definition 12. If $a = (d, x)$ is an argument, then $\mathtt {Conc}(a) = x$. For a set ${\mathcal {E}}$ of arguments, $\mathtt {Concs}({\mathcal {E}}) = \{x \mid (d,x) \in {\mathcal {E}}\}$ and $\mathtt {Th}({\mathcal {E}})$ is a theory such that

$$\begin{aligned} \mathtt {Th}({\mathcal {E}}) = \left( \bigcup _{(d,x) \in {\mathcal {E}}} \mathtt {Facts}(d), \bigcup _{(d,x) \in {\mathcal {E}}} \mathtt {Strict}(d), \bigcup _{(d,x) \in {\mathcal {E}}} \mathtt {Def}(d)\right) . \end{aligned}$$

The following result shows that an argument provides a minimal derivation schema for a conclusion.

Theorem 1

Let ${\mathcal {T}}$ be a theory. For any consistent sequence $d = \langle (x_1,r_1), \ldots , (x_n,r_n)\rangle$ from ${\mathcal {T}}$, the following two statements are equivalent:

• (d, x) is an argument (from ${\mathcal {T}}$)

• d is a focused derivation schema from ${\mathcal {T}}$ such that $x = x_n$

An argument may have several sub-parts, each of which may give birth to an argument, called sub-argument of the original argument.

Definition 13

(Sub-argument) An argument (d, x) is a sub-argument of $(d',x')$ iff $(\mathtt {Facts}(d)$, $\mathtt {Strict}(d)$, $\mathtt {Def}(d))$$\sqsubseteq$$(\mathtt {Facts}(d')$, $\mathtt {Strict}(d')$, $\mathtt {Def}(d'))$.

Notations :

The function $\mathtt {Sub}(.)$ returns the set of all sub-arguments of a given argument.

Example 1 (Cont)

The argument $(\langle (q,\sigma ), (\lnot s,r_2)\rangle , \lnot s)$ has two sub-arguments: $(\langle (q,\sigma )\rangle , q)$ and itself. By contrast, $(\langle (q,\sigma )\rangle , q)$ is not a sub-argument of $(\langle (p,\sigma )$, $(q,r_6)\rangle$, q). $\square$

Property 9

If (d, x) is a sub-argument of $(d',x')$, then $\mathtt {Seq}(d) \subseteq \mathtt {Seq}(d')$.

The converse is not true as shown next.

Example 5

Consider the two arguments a and b:

• $a = (\langle (p,\sigma ),(t, p \rightarrow t)\rangle , t)$

• $b = (\langle (p,\sigma ),(q, p \rightarrow q),(t, q \Rightarrow t)\rangle , t)$

Note that $\mathtt {Seq}(a) = \{p,t\} \subseteq \{p,q,t\} = \mathtt {Seq}(b)$ but a is not a sub-argument of b since the theory $(\{p\}, \{p \rightarrow t\}, \sigma )$ is not a sub-theory of $(\{p\}, \{p \rightarrow q\}, \{q \Rightarrow t\})$.

Argumentation systems that use a Tarskian logic such as propositional logic may have infinite sets of arguments even when the theories (called knowledge bases) over which they are built are themselves finite (cf. [26]). We show that this is not the case for rule-based argumentation systems. Indeed, the sets of arguments are finite as soon as the theories are finite.

Proposition 2

If a theory ${\mathcal {T}}$ is finite, then ${\mathtt {Arg}}({\mathcal {T}})$ is finite.

The set of arguments built from a given theory cannot be empty since the set of facts of a theory contains at least $\top$.

Property 10

For a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$, ${\mathtt {Arg}}({\mathcal {T}}) \ne \emptyset$.

The construction of arguments in all existing structured argumentation systems is a monotonic process. By structured systems, we mean argumentation systems that build their arguments from knowledge bases encoded in particular logics. These include ASPIC [8], ASPIC+ [9], DeLP [10], ABA [27] and those discussed in [4]. Thus, unlike Dung’s framework where arguments are abstract entities, in structured systems arguments have a clear origin and a precise structure. Hunter studied in [25] the properties of the logics underlying existing structured systems. The results show that the set of arguments built from a knowledge base cannot be shrunk when the base is extended by new information. The following result shows that this property holds also for the kind of logic discussed in this paper.

Proposition 3

Let ${\mathcal {T}}$ and ${\mathcal {T}}'$ be two theories. If ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$, then ${\mathtt {Arg}}({\mathcal {T}}) \subseteq {\mathtt {Arg}}({\mathcal {T}}')$.

A rule-based instantiation of Dung’s abstract framework is defined as follows:

Definition 14

(Argumentation system) An argumentation system defined over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ is a pair ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ where ${\mathtt {Arg}}({\mathcal {T}})$ is the set of arguments built from ${\mathcal {T}}$ in the sense of Definition 12 and ${\mathcal {R}}\subseteq {\mathtt {Arg}}({\mathcal {T}}) \times {\mathtt {Arg}}({\mathcal {T}})$ is an attack relation.

For the sake of generality, the attack relation of an argumentation system is left unspecified in the sequel. Thus, it may be instantiated in different ways. In existing rule-based argumentation systems like the ASPIC system as defined in [8, 17] and its extended version ASPIC+ [9], three kinds of attack relations are used: (i) rebut, initially proposed in [28], which requires that two arguments have opposite conclusions, (ii) assumption attack, proposed also in [28], according to which an argument undermines a premise of another argument, and (iii) undercut, proposed in [16], which allows an argument to prevent the application of a defeasible rule in another argument. The two first relations are conflict-dependent, i.e., they capture the inconsistency of the theory over which an argumentation system is built. Such relations should show no attack from argument a to b unless their derivation schemas contain opposite literals.

Definition 15

(Conflict-dependency) Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system. The attack relation ${\mathcal {R}}$ is conflict-dependent iff for all $(d,x), (d',x') \in {\mathtt {Arg}}({\mathcal {T}})$, if $(d,x) \ {\mathcal {R}}\ (d',x')$ then $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent.

An important feature of conflict-dependent attack relations is that they do not admit self-attacking arguments, mainly since arguments are consistent.

Proposition 4

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system. If ${\mathcal {R}}$ is conflict-dependent, then for all $a \in {\mathtt {Arg}}({\mathcal {T}})$$(a,a) \notin {\mathcal {R}}$.

Conflict-dependency is somehow related to the notion of conflict-freeness of sets of arguments. Indeed, when the attack relation is conflict-dependent, the set of arguments built from any consistent theory is conflict-free with respect to this relation.

Proposition 5

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. For every ${\mathcal {T}}' \sqsubseteq {\mathcal {T}}$, if $\mathtt {CN}({\mathcal {T}}')$ is consistent and ${\mathcal {R}}$ is conflict-dependent, then ${\mathtt {Arg}}({\mathcal {T}}')$ is conflict-free.

Another feature of all the attack relations in existing rule-based argumentation systems is the fact that they privilege strict arguments.

Definition 16

(Strict argument precedence) Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. An attack relation ${\mathcal {R}}$privileges strict arguments iff for all $a = (d,x), b = (d',x') \in {\mathtt {Arg}}({\mathcal {T}})$, if a is strict and $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent, then $a {\mathcal {R}}b$.

A consequence of this property is that the set ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is admissible (i.e., it is conflict-free and defends all its elements). We will show in a subsequent section that this result is crucial for characterizing ideal extension.

Theorem 2

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ is consistent. If ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments, then ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is an admissible set of ${\mathcal {H}}$.

Unless stated otherwise, in what follows we do not make any assumption about the attack relation of a rule-based argumentation system. However, the arguments of the latter are evaluated using any of the semantics recalled in Definition 3. The extensions of a system are used for defining the plausible conclusions to be drawn from the theory over which the system is built. A literal is a plausible conclusion of a system iff it is a common conclusion to all the extensions.

Definition 17

(Plausible conclusions) Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. The set of plausible conclusions of ${\mathcal {H}}$ under semantics x is

$\begin{array}{ll} \mathtt {Output}({\mathcal {H}}) = &{} \left\{ \begin{array}{ll} \{z \in {\mathcal {L}}\ | \ \forall {\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}}), \ \exists a \in {\mathcal {E}} \text{ s.t. } \mathtt {Conc}(a) = z\} &{} \text{ if } \mathtt {Ext}_x({\mathcal {H}})\ne \emptyset \\ \emptyset &{} \text{ else } \end{array}\right. \end{array}$

The set of plausible conclusions coincides with the set of common conclusions of the extensions, of course when extensions exist.

Property 11

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that $\mathtt {Ext}_x({\mathcal {H}})\ne \emptyset$ where x is any of the reviewed semantics. The equality $\mathtt {Output}({\mathcal {H}}) = \bigcap \nolimits _{{\mathcal {E}}_i \in \mathtt {Ext}_x({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i)$ holds.

Finally, it is obvious that the plausible conclusions of an argumentation system are consequences of the theory over which it is built.

Property 12

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. The inclusion $\mathtt {Output}({\mathcal {H}}) \subseteq \mathtt {CN}({\mathcal {T}})$ holds under any extension-based semantics.

It is worth noticing that under admissible semantics, the set of plausible conclusions of any argumentation system is empty. This is mainly due to the fact that the empty set is always an admissible extension. This makes this semantics unsuitable for defeasible reasoning. Complete semantics suffers from the same problem. Indeed, since under this semantics extensions are not maximal for set inclusion, the empty set may be an extension leading thus to an empty set of plausible conclusions. Stable semantics may also be unsuitable for argumentation systems that do not have extensions. However, we show in a subsequent section that rule-based systems that satisfy some desirable properties do have stable extensions, in particular when the attack relation is conflict-dependent.

5 Postulates for rule-based argumentation systems

Like any reasoning model, argumentation systems should enjoy some desirable properties or rationality postulates that ensure their soundness. The first work on postulates in argumentation was done by [17] in the context of rule-based systems. Starting from the observation that some existing systems like those proposed in [12, 29] suffer from two main problems: (i) returning inconsistent sets of plausible conclusions and (ii) forgetting intuitive conclusions, the authors proposed three postulates which prevent the encountered problems. In what follows, we recall the three postulates and propose three new ones. The first postulate proposed in [17] concerns the consistency of the set of conclusions supported by every extension.

Postulate 1

(Consistency) An argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ satisfies consistency under semantics x iff for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, $\mathtt {Concs}({\mathcal {E}})$ is consistent.

A rule-based system which satisfies this postulate has necessarily a consistent set of plausible conclusions.

Property 13

[17] If an argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ satisfies consistency under semantics x (x being any extension-based semantics), then $\mathtt {Output}({\mathcal {H}})$ is consistent.

The second postulate ensures a form of “completeness” of the outputs of an argumentation system. It says that if there is an argument with conclusion x in an extension of the system, and there exists a strict rule $x \rightarrow y$ in the theory over which the system is built, then y should also be supported by an argument in the same extension. Recall that a strict rule has no exception. Thus, as soon as x is true, y holds for sure.

Postulate 2

(Closure under strict rules) An argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ is closed under strict rules under semantics x iff for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}((\mathtt {Concs}({\mathcal {E}}), {\mathcal {S}}, \emptyset ))$.

If an argumentation system is closed under strict rules, then its set of plausible conclusions is also closed under strict rules.

Property 14

[17] Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. If ${\mathcal {H}}$ is closed under strict rules under semantics x (x being any extension-based semantics), then $\mathtt {Output}({\mathcal {H}})= \mathtt {CN}((\mathtt {Output}({\mathcal {H}}), {\mathcal {S}}, \emptyset ))$.

A third postulate, called indirect consistency, was proposed in [17]. It ensures that every closed (under strict rules) extension should satisfy consistency. It was shown that a system that satisfies consistency and closure under strict rules satisfies this form of indirect consistency.

Property 15

[17] Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}$, ${\mathcal {S}}$, ${\mathcal {D}})$. If ${\mathcal {H}}$ satisfies consistency and is closed under strict rules under semantics x (x being any extension-based semantics), then for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, $\mathtt {CN}((\mathtt {Concs}({\mathcal {E}}), {\mathcal {S}}, \emptyset ))$ is consistent.

It is worth mentioning that the three previous results hold for any attack relation and under any extension-based acceptability semantics, thus under any of the semantics recalled in Definition 3 and others like recursive semantics [20].

In any axiomatic approach, the axioms (or postulates) should ideally all be independent from each other, i.e., none is deduced from the others. Thus, in the sequel indirect consistency is abandoned since it follows from Postulates 1 and 2. We propose next three new postulates which were already defined in [30] for argumentation systems that use a logic in the sense of [22]. The first one says that if an argument belongs to an extension, then all its sub-arguments should be in the extension. Thus, an argument cannot be accepted if one of its sub-parts is questionable. This is a natural requirement since plausible conclusions inferred from a theory rely on their supporting arguments which should be unassailable.

Postulate 3

(Closure under sub-arguments) An argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ is closed under sub-arguments under semantics x iff for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, if $a \in {\mathcal {E}}$ then $\mathtt {Sub}(a) \subseteq {\mathcal {E}}$.

Argumentation systems that satisfy both consistency and closure under sub-arguments enjoy a strong version of consistency. Indeed, the set of consequences that follow from the theory of an extension is consistent.

Proposition 6

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {Ext}_x({\mathcal {H}})$$\ne$$\emptyset$ (x being any extension-based semantics). If ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments, then for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ is consistent.

Let us illustrate this result with an example.

Example 6

Let ${\mathcal {T}}_5 = ({\mathcal {F}}_5, {\mathcal {S}}_5, {\mathcal {D}}_5)$ be a theory such that ${\mathcal {S}}_5 = \emptyset$ and

$$\begin{aligned} {\mathcal {F}}_5 \left\{ \begin{array}{@{}l} x \\ \lnot x \end{array}\right. \qquad \qquad {\mathcal {D}}_5 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} x &{} \Rightarrow &{} y &{} (r_1) \\ \lnot x &{} \Rightarrow &{} z &{} (r_2) \end{array}\right. \end{aligned}$$

Consider the two arguments $(d_1,y), (d_2,z)$ with $d_1 = \langle (x,\sigma ), (y,r_1)\rangle$ and $d_2 = \langle (\lnot x,\sigma ), (z,r_2)\rangle$. Assume that the set ${\mathcal {E}}= \{(d_1,y), (d_2,z)\}$ is an extension of $({\mathtt {Arg}}({\mathcal {T}}_5), {\mathcal {R}})$ under a given semantics. Clearly, $\mathtt {CN}((\mathtt {Concs}({\mathcal {E}}), {\mathcal {S}}, \emptyset )) = \{y, z\}$ is consistent. However, $\mathtt {Th}{({\mathcal {E}})} = {\mathcal {T}}$ and $\mathtt {CN}({\mathcal {T}}) = \{x, \lnot x, y, z\}$ is inconsistent. Proposition 6 ensures that the argumentation system $({\mathtt {Arg}}({\mathcal {T}}_5), {\mathcal {R}})$ violates at least one of the consistency or closure under sub-arguments postulates.

Since facts and strict rules are the certain part in a theory (facts being observable and strict rules having no exceptions), they should be plausible conclusions of any argumentation system. It is worth mentioning that this principle is applied, for instance, in default logic where the non-defeasible information of a default theory is part of all extensions [5]. Of course this makes sense when the non-defeasible information is consistent.

Postulate 4

(Strict precedence) An argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ satisfies strict precedence under semantics x iff $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq \mathtt {Output}({\mathcal {H}})$.

Notice that argumentation systems that have no extensions violate this postulate. Similarly, systems that evaluate their arguments using a semantics which considers the empty set as an extension (like admissible semantics) violate strict precedence. Such systems are thus not suitable for defeasible reasoning since they may miss intuitive conclusions.

Proposition 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\emptyset \in \mathtt {Ext}_x({\mathcal {H}})$. ${\mathcal {H}}$ violates strict precedence under semantics x.

We show next that if an argumentation system satisfies consistency and strict precedence, then the strict part of the theory over which it is built is consistent.

Proposition 8

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {Ext}_x({\mathcal {H}})\ne \emptyset$. If ${\mathcal {H}}$ satisfies consistency and strict precedence under semantics x, then $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ is consistent.

The last postulate ensures a form of completeness of the extensions of an argumentation system under any semantics. It says that if the sequence of an argument is part of the conclusions of a given extension, then the argument should belong to the extension. Informally: If each step in the argument is good enough to be in the extension, then so is the argument itself. It is worth pointing out that this postulates holds for both strict and defeasible rules.

Postulate 5

(Exhaustiveness) An argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ satisfies exhaustiveness under semantics x iff for any ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, for any $(d,x) \in {\mathtt {Arg}}({\mathcal {T}})$, if $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$, then $(d,x) \in {\mathcal {E}}$.

Argumentation systems that satisfy exhaustiveness and closure under sub-arguments have complete extensions, i.e., they are closed in terms of arguments.

Proposition 9

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system such that $\mathtt {Ext}_x({\mathcal {H}})\ne \emptyset$ (x being any extension-based semantics). If ${\mathcal {H}}$ is closed under sub-arguments and satisfies exhaustiveness under semantics x, then for all ${\mathcal {E}}\in \mathtt {Ext}_x({\mathcal {H}})$, ${\mathcal {E}}= {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$.

When an argumentation system satisfies strict precedence and exhaustiveness, then its strict arguments are part of any extension. This holds under any extension-based semantics.

Proposition 10

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ (under an extension-based semantics). If ${\mathcal {H}}$ satisfies exhaustiveness and strict precedence, then for any ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$, ${\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq {\mathcal {E}}$.

An axiomatic approach should obey an important feature: The postulates should be compatible, i.e., they can be satisfied all together by an argumentation system under a given semantics. Fortunately, this is the case of the five postulates discussed in this section.

Proposition 11

The five postulates are compatible.

The four postulates (consistency, closure under sub-arguments, closure under strict rules, strict precedence) are independent. None of them follows from a subset of the three others. However, as will be shown in the next section, exhaustiveness follows from consistency and closure under sub-arguments when an argumentation system uses a conflict-dependent attack relation and naive or stable semantics for evaluating arguments.

6 Outcomes of rule-based argumentation systems

This section analyzes the outputs of rule-based argumentation systems under the reviewed semantics, i.e., those recalled in Definition 3, that are suitable for defeasible reasoning. Recall that complete semantics is not a good candidate for such reasoning since its extensions are not maximal (for set inclusion) and may thus lead to an empty set of plausible conclusions, and missing intuitive conclusions. We analyze the extensions under each semantics. Indeed, we characterize the set $\mathtt {Concs}(.)$ of conclusions and the theory $\mathtt {Th}(.)$ of each extension. We also characterize the set $\mathtt {Output}(.)$ of plausible conclusions that are drawn by a rule-based argumentation system from a theory.

Note that the argumentation system described in Sect. 4 is not fully specified since its attack relation is left undefined and may thus be instantiated in different ways. For the purpose of our study, we do not need to consider a particular attack relation. Since any reasonable argumentation system should satisfy the discussed postulates, throughout this section we only focus on systems that satisfy the postulates. Such systems exist and ASPIC, defined in [17], is one of them. Indeed, it was shown in [17] that ASPIC, which uses restricted rebut as attack relation, satisfies consistency and closure under both sub-arguments and strict rules under all Dung’s semantics. Furthermore, the attack relation in ASPIC privileges strict arguments (by definition) and the strict part of a theory is assumed to be consistent. Thus, the system satisfies strict precedence under the same semantics. Finally, from our Proposition 15 (respectively Proposition 13), it follows that it also satisfies exhaustiveness under stable (respectively naive) semantics. The results we provide next hold for any instantiation of the attack relation ${\mathcal {R}}$. This means that whatever the attack relation that is considered, the outcome will be the same. This shows also that all the reasonable rule-based argumentation systems that can be built over the same theory are equivalent [31, 32], in the sense they provide the same extensions and the set of plausible conclusions under a given semantics.

Before presenting the formal results concerning the reviewed semantics, below are some results that hold under any extension-based semantics, thus under all the reviewed semantics but also under several other semantics (e.g., recursive semantics [20], the one used in DeLP system [10], stage semantics [21], ...). The first result characterizes the set of conclusions of each extension of an argumentation system which is closed under sub-arguments.

Proposition 12

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system such that $\mathtt {Ext}({\mathcal {H}})$$\ne$$\emptyset$ (under an extension-based semantics). If ${\mathcal {H}}$ is closed under sub-arguments, then for any ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$,

• $\mathtt {Concs}({\mathcal {E}}) = X \cup \{\mathtt {Head}(r) \mid r \in Y \cup Z\}$ where $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$

• $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$

• $\forall (d,x) \in {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$, $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$

The next result shows that if an argumentation system over a theory satisfies strict precedence, closure under both sub-arguments and strict rules, then the set of literals deduced from $\mathtt {Th}({\mathcal {E}})$, the theory of an extension ${\mathcal {E}}$, is exactly the same set that is obtained from $\mathtt {Th}({\mathcal {E}})$ extended by all facts and strict rules which are not in $\mathtt {Th}({\mathcal {E}})$.

Theorem 3

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ (under an extension-based semantics). If ${\mathcal {H}}$ satisfies strict precedence and closure under both strict rules and sub-arguments, then for any ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$,

$$\begin{aligned} \mathtt {CN}\left( \mathtt {Th}({\mathcal {E}})\right) = \mathtt {CN}\left( \left( {\mathcal {F}}, {\mathcal {S}}, \bigcup _{(d,x) \in {\mathcal {E}}}\mathtt {Def}(d)\right) \right) . \end{aligned}$$

We also show that the theory of an extension can be extended into a sub-theory (of the argumentation system) which infers, using the notion of derivation, all the conclusions that are supported by arguments of the extension. This (i.e., Theorem 4) will be useful in proving various results in the next sections.

Theorem 4

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ (under an extension-based semantics). If ${\mathcal {H}}$ satisfies strict precedence, and closure under both strict rules and sub-arguments, then for any ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$,

$\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$ for ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, \zeta )$ such that

$$\begin{aligned} \zeta = \left( \bigcup _{(d,x) \in {\mathcal {E}}} \mathtt {Def}(d)\right) \cup \left\{ r \mid r \in {\mathcal {D}} \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))\right\} . \end{aligned}$$

6.1 Naive semantics

Before characterizing the extensions as well as the plausible conclusions of a rule-based argumentation system, let us first show some additional links between the postulates in the particular case of naive semantics. The first result shows that exhaustiveness follows from consistency and closure under sub-arguments. This is the case when the attack relation is conflict-dependent.

Proposition 13

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent. If ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics, ${\mathcal {H}}$ satisfies exhaustiveness under naive semantics.

The second result shows that when an argumentation system is closed under sub-arguments and satisfies the consistency postulate under naive semantics, then every naive extension of the system is closed in terms of arguments.

Proposition 14

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. For any ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, ${\mathcal {E}}= {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$.

Strict precedence is problematic in case of naive semantics since it may be violated by a rule-based argumentation system. This is mainly due to the fact that the orientation of attacks is not taken into account when computing naive extensions; thus, there is no way to enforce the postulate. We show next that strict arguments are part of any naive extension only when they neither are attacked nor attack any argument.

Theorem 5

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent. For any ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, ${\mathtt {Arg}}(({\mathcal {F}}, S, \emptyset ))$$\subseteq$${\mathcal {E}}$ iff for any $a \in {\mathtt {Arg}}(({\mathcal {F}}, S, \emptyset ))$, $\not \exists b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$.

We have previously shown that the five postulates are compatible in the general case. Indeed, under stable and preferred semantics, it was shown that the ASPIC system satisfies all the postulates. In case of naive semantics, this is not always true. Strict precedence is not compatible with consistency when the strict part is inconsistent, or it is consistent but in conflict with the defeasible part. For instance, any argumentation system built over the theory of Example 3 will violate at least one of the two postulates under naive semantics.

Theorem 6

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent. If $\exists a, b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $a \in {\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ and $\mathtt {Conc}(a) = \lnot \mathtt {Conc}(b)$, then ${\mathcal {H}}$ cannot satisfy both strict precedence and consistency under naive semantics.

In case of the ASPIC system, the argument b cannot be strict since the strict part (i.e., $\mathtt {CN}({\mathcal {F}}, {\mathcal {S}}, \emptyset )$) is assumed to be consistent. Moreover, there is only one conflict between a and b and which emanates from a since strict arguments cannot be attacked by defeasible ones. Thus, strict precedence is violated.

We show next that, assuming consistency and closure under sub-arguments, naive extensions are maximal.

Theorem 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. For all ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_n({\mathcal {H}})$, if $\mathtt {Concs}({\mathcal {E}}') \subseteq \mathtt {Concs}({\mathcal {E}})$ then ${\mathcal {E}}= {\mathcal {E}}'$.

The following theorem characterizes naive extensions. It says that every naive extension of an argumentation system which satisfies consistency and closure under sub-arguments has a unique corresponding maximal option in the theory at hand.

Theorem 8

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. For any ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, there exists a unique option ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$.

Note that the inclusion $\mathtt {Th}({\mathcal {E}}) \subseteq {\mathcal {O}}$ is due to the fact that a theory $\mathtt {Th}({\mathcal {E}})$ of an extension ${\mathcal {E}}$ contains only activated (strict and defeasible) rules, while maximal options may contain non-activated ones. Thus, the elements which in ${\mathcal {O}}$ but not in $\mathtt {Th}({\mathcal {E}})$ are non-activated rules.

Notations :

For ${\mathcal {E}}$ any extension of ${\mathcal {H}}$ such that ${\mathcal {O}}$ in $\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ satisfies $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$, let

$$\begin{aligned} \mathtt {Option}({\mathcal {E}}) {\mathop {=}\limits ^\mathrm{def}} {\mathcal {O}}. \end{aligned}$$

We prove that no two naive extensions return the same option. Moreover, every extension is exactly the set of all arguments that can be built from its corresponding option.

Theorem 9

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics.

• For all ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_n({\mathcal {H}})$, if $\mathtt {Option}({\mathcal {E}}) = \mathtt {Option}({\mathcal {E}}')$, then ${\mathcal {E}}= {\mathcal {E}}'$

• For any ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, ${\mathcal {E}}= \mathtt {Arg}(\mathtt {Option}({\mathcal {E}}))$

We have shown that each naive extension captures exactly one maximal option and it supports all, and only, the consequences of that option. Theorem 10 states that every maximal option has a corresponding naive extension. So, there is a bijection from the set of naive extensions to the set of maximal options.

Theorem 10

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics.

• For any ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$, $\mathtt {Arg}({\mathcal {O}}) \in \mathtt {Ext}_n({\mathcal {H}})$

• For any ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$, ${\mathcal {O}}= \mathtt {Option}(\mathtt {Arg}({\mathcal {O}}))$

• For all ${\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$, if $\mathtt {Arg}({\mathcal {O}}) = \mathtt {Arg}({\mathcal {O}}')$ then ${\mathcal {O}}= {\mathcal {O}}'$

Example 3 (Cont)

The theory ${\mathcal {T}}_3$ has seven options, of which only two are maximal: $\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}_3)) = \{{\mathcal {O}}_4, {\mathcal {O}}_5\}$. For all argumentation system ${\mathcal {H}}$ built over ${\mathcal {T}}_3$, if the attack relation of ${\mathcal {H}}$ is to be conflict-dependent and consistency and closure under sub-arguments satisfied, then $\mathtt {Ext}_n({\mathcal {H}})= \{{\mathtt {Arg}}({\mathcal {O}}_4), {\mathtt {Arg}}({\mathcal {O}}_5)\}$.

From the previous results, it follows that there is a bijection between the set of naive extensions of an argumentation system and the maximal options of the theory over which the system is built.

Corollary 1

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. There is a bijection between $\mathtt {Ext}_n({\mathcal {H}})$ and $\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$.

The previous results require only the satisfaction of two postulates: consistency and closure under sub-arguments. We show next that when a rule-based argumentation system satisfies all the five postulates, there is a bijection between the set of naive extensions of the system and the maximal preferred options of the theory over which it is built. The reason is that in such a case, the maximal options of the theory coincide with the maximal preferred ones. Recall that in general, maximal preferred options may be different from maximal options.

Theorem 11

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both strict rules and sub-arguments under naive semantics. The equality $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}})) = \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ holds.

Corollary 2

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both strict rules and sub-arguments under naive semantics. There is a bijection between $\mathtt {Ext}_n({\mathcal {H}})$ and $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$.

It is possible to delimit the number of naive extensions of any argumentation system that satisfies consistency and closure under sub-arguments. It is exactly the number of maximal options of the theory at hand.

Corollary 3

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. The equality $|\mathtt {Ext}_n({\mathcal {H}})| = |\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))|$ holds.

It follows also that when a theory is finite, then any system built over it has a finite number of naive extensions.

Corollary 4

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics. If ${\mathcal {T}}$ is finite, then ${\mathcal {H}}$ has a finite number of naive extensions.

What about the plausible conclusions that are drawn from a theory using an argumentation system that satisfies the postulates? From the previous results, it is easy to show that they are the literals that follow from all the maximal options.

Theorem 12

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under naive semantics.

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))} \mathtt {CN}({\mathcal {O}}_i) \end{aligned}$$

Example 3 (Cont)

Any argumentation system ${\mathcal {H}}$ that can be built over the theory ${\mathcal {T}}_3$ and has a conflict-dependent attack relation and satisfies consistency and closure under sub-arguments will have as output the set $\mathtt {Output}({\mathcal {H}})= \mathtt {CN}({\mathcal {O}}_4) \cap \mathtt {CN}({\mathcal {O}}_5) = \{p, q, t, u, v\}$.

Let us summarize the main results: under naive semantics, any rule-based argumentation system may violate strict precedence. However, the other postulates can be satisfied. In such a case , if the attack relation is conflict-dependent, then any argumentation system will infer exactly the literals that follow from all the maximal options of the theory over which the system is built. This is due to the bijection that holds between the set of naive extensions and the set of maximal options. In case the system satisfies also strict precedence and closure under strict rules, then the maximal options of the theory coincide with the maximal preferred options.

6.2 Stable semantics

As for naive semantics, exhaustiveness follows from consistency and closure under sub-arguments in case of stable semantics.

Proposition 15

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent. If ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments under stable semantics, then the following two properties hold:

• ${\mathcal {H}}$ satisfies exhaustiveness under stable semantics.

• For any ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$, ${\mathcal {E}}= {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$.

Stable extensions of rule-based argumentation systems satisfying the five postulates return maximal preferred options. This means that if one instantiates Dung’s framework and does not get maximal preferred options with stable extensions, then the instantiation certainly violates at least one of the postulates. Note that strict precedence may be satisfied by an argumentation system under stable semantics while it is violated by the same system under naive semantics. This is due to the fact that the orientation of attacks plays an important role in stable semantics, then strict precedence can be enforced by choosing an appropriate orientation.

Theorem 13

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system defined over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent. If ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both sub-arguments and strict rules under stable semantics, and $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$, then for any ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$, there exists a unique option ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that:

• $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$

• $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$

• ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}})$

Two stable extensions cannot capture the same maximal preferred option.

Theorem 14

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system defined over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent. If ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both sub-arguments and strict rules under stable semantics and $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$, then for all ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_s({\mathcal {H}})$, if $\mathtt {Option}({\mathcal {E}}) = \mathtt {Option}({\mathcal {E}}')$ then ${\mathcal {E}}= {\mathcal {E}}'$.

The previous results characterize the stable extensions of rule-based argumentation systems that satisfy the postulates. However, they do not guarantee that each maximal preferred option of a theory has a corresponding stable extension. To put it differently, it does not guarantee a bijection between the sets $\mathtt {Ext}_s({\mathcal {H}})$ and $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ and thus does not ensure the equality $|\mathtt {Ext}_s({\mathcal {H}})| = |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$. In case of argumentation systems that use a Tarskian logic for representing information and for computing arguments, it was shown in [4] that this equality depends on the attack relation that is chosen. We show next that this is also the case for rule-based systems.

Given ${\mathcal {T}}$, let $\mathfrak {R}_s$ be the set of all attack relations that are conflict-dependent and that ensure the five postulates under stable semantics:

$\mathfrak {R}_s = \{{\mathcal {R}}\subseteq {\mathtt {Arg}}({\mathcal {T}}) \times {\mathtt {Arg}}({\mathcal {T}})$ | ${\mathcal {R}}$ is conflict-dependent and $({\mathtt {Arg}}({\mathcal {T}}),{\mathcal {R}})$ satisfies the five postulates under stable semantics for any theory ${\mathcal {T}}\}$.

This set contains three disjoints subsets of attack relations, i.e., $\mathfrak {R}_s = \mathfrak {R}_{s_1} \cup \mathfrak {R}_{s_2} \cup \mathfrak {R}_{s_3}$:

• $\mathfrak {R}_{s_1}$: the set of relations such that $|\mathtt {Ext}_s({\mathcal {H}})| = 0$

• $\mathfrak {R}_{s_2}$: the set of relations such that $|\mathtt {Ext}_s({\mathcal {H}})| = |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$

• $\mathfrak {R}_{s_3}$: the set of relations such that $|\mathtt {Ext}_s({\mathcal {H}})| < |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$

Let us analyze separately each category of attack relations. The following result shows that the set $\mathfrak {R}_{s_1}$ is empty, meaning that there is no attack relation which prevents the existence of stable extensions. To say it differently, any argumentation system which satisfies the postulates has at least one stable extension.

Theorem 15

$\mathfrak {R}_{s_1} = \emptyset$.

A consequence of this postulate is that stable extensions coincide with semi-stable ones. Indeed, it was shown in [18] that when stable extensions exist, they coincide with semi-stable extensions.

Corollary 5

For all argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$, if ${\mathcal {R}}\in \mathfrak {R}_{s_2} \cup \mathfrak {R}_{s_3}$, then $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})$.

From the previous results, it is possible to delimit the number of stable extensions of rule-based argumentation systems that satisfy the five postulates.

Corollary 6

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system defined over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent. If ${\mathcal {H}}$ satisfies the five postulates, then

$$\begin{aligned} 1 \le |\mathtt {Ext}_s({\mathcal {H}})| \le |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|. \end{aligned}$$

It follows that when a theory is finite, any argumentation system built over it has a finite number of stable extensions.

Corollary 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. If ${\mathcal {T}}$ is finite, then ${\mathcal {H}}$ has a finite number of stable extensions.

Attack relations of category $\mathfrak {R}_{s_2}$ induce a bijection between the set of stable extensions of an argumentation system and the set of maximal preferred options of the theory over which the system is built. Indeed, every preferred option gives a stable extension.

Theorem 16

Let ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$. For any ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$, ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_s({\mathcal {H}})$.

Example 3 (Cont)

The theory ${\mathcal {T}}_3$ has seven options, of which only two are preferred maximal: $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}_3)) = \{{\mathcal {O}}_1, {\mathcal {O}}_3\}$. Thus, for all argumentation system ${\mathcal {H}}$ built over ${\mathcal {T}}_3$, if the attack relation of ${\mathcal {H}}$ is of category $\mathfrak {R}_{s_2}$, then $\mathtt {Ext}_s({\mathcal {H}})= \{{\mathtt {Arg}}({\mathcal {O}}_1), {\mathtt {Arg}}({\mathcal {O}}_3)\}$. Recall that under naive semantics, there is no argumentation system over ${\mathcal {T}}_3$ that can satisfy strict precedence. The ones that guarantee consistency and closure under sub-arguments will all have the following naive extensions: $\mathtt {Ext}_n({\mathcal {H}})= \{{\mathtt {Arg}}({\mathcal {O}}_4), {\mathtt {Arg}}({\mathcal {O}}_5)\}$.

Argumentation systems with an attack relation from $\mathfrak {R}_{s_2}$ are coherent, meaning that the preferred extensions exhaust all the stable ones. It follows thus that the three semantics (semi-stable, stable, preferred) coincide. This means that semi-stable and preferred semantics have no added value with respect to stable semantics since they guarantee the same results.

Theorem 17

For any argumentation system ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}})$, ${\mathcal {R}})$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$, it holds $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})= \mathtt {Ext}_p({\mathcal {H}})$.

In case an argumentation system satisfies strict precedence under naive semantics (see Theorem 5), then its extensions coincide with the stable ones. To put differently, in case naive semantics can guarantee strict precedence, stable semantics becomes useless since it provides no added value with respect to naive semantics.

Theorem 18

For all argumentation system ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}})$, ${\mathcal {R}})$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$, if ${\mathcal {H}}$ satisfies the postulates under naive semantics, then

$$\begin{aligned} \mathtt {Ext}_n({\mathcal {H}})= \mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})= \mathtt {Ext}_p({\mathcal {H}}). \end{aligned}$$

Plausible conclusions of rule-based argumentation systems that use attack relations in category $\mathfrak {R}_{s2}$ are exactly the literals that follow from all the maximal preferred options of the theory at hand.

Theorem 19

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$.

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {O}}_i \in \ \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))} \mathtt {CN}({\mathcal {O}}_i). \end{aligned}$$

Systems that use relations in $\mathfrak {R}_{s_3}$ choose a proper subset of the maximal preferred options of ${\mathcal {T}}$ and make inferences from them. Their output sets are as follows:

Theorem 20

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_3}$.

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {O}}_i \in {\mathcal {X}}} \mathtt {CN}({\mathcal {O}}_i) \end{aligned}$$

with ${\mathcal {X}}= \{{\mathcal {O}}_i \in \ \mathtt {Max}(\mathtt {POpt}({\mathcal {T}})) \mid {\mathcal {E}}_i = {\mathtt {Arg}}({\mathcal {O}}_i) \in \mathtt {Ext}_s({\mathcal {H}})\}$.

These attack relations introduce a critical discrimination between the maximal preferred options of a theory. Hence, great care must be exercised when designing rule-based argumentation systems based on stable semantics: The principles governing the interaction between $\Rightarrow$ and ${\mathcal {R}}$ must be both rigorously and meticulously specified so as to avoid trouble of which the following example is an easy case.

Example 7

Consider ${\mathcal {T}}_6$ such that ${\mathcal {F}}_6$, ${\mathcal {S}}_6$, ${\mathcal {D}}_6$ are as follows:

$$\begin{aligned} {\mathcal {F}}_6 \left\{ \begin{array}{l} p \\ q \\ \end{array}\right. \quad \quad {\mathcal {S}}_6 = \emptyset \quad \quad {\mathcal {D}}_6 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} p &{} \Rightarrow &{} s &{} (r_1) \\ q &{} \Rightarrow &{} \lnot s &{} (r_2) \end{array}\right. \end{aligned}$$

The theory ${\mathcal {T}}_6$ has two maximal preferred options:

• ${\mathcal {O}}_1 = ({\mathcal {F}}_6, {\mathcal {S}}_6, \{r_1\})$

• ${\mathcal {O}}_2 = ({\mathcal {F}}_6, {\mathcal {S}}_6, \{r_2\})$

For a system ${\mathcal {H}}$ whose attack relation is in $\mathfrak {R}_{s_3}$ either (i) ${\mathtt {Arg}}({\mathcal {O}}_1)$ or (ii) ${\mathtt {Arg}}({\mathcal {O}}_2)$ is its unique stable extension. In case (i), $s \in \mathtt {Output}({\mathcal {H}})$ and $\lnot s \notin \mathtt {Output}({\mathcal {H}})$.

In case (ii), $\lnot s$ is the plausible conclusion. By the obvious symmetry (don’t be misled by negation!¹), either choice would be arbitrary, and this is an instance where an attack relation from $\mathfrak {R}_{s_2}$ is alright.

To sum up, attack relations satisfying the postulates can be split into two categories: $\mathfrak {R}_{s_2}$ and $\mathfrak {R}_{s_3}$. Relations from $\mathfrak {R}_{s_2}$ make semi-stable semantics and preferred semantics to collapse into stable semantics. They offer no added value with respect to the latter. Stable semantics may, however, be more valuable than naive semantics. Indeed, the theories for which strict precedence cannot be satisfied under naive semantics are handled correctly under stable semantics. This latter can enforce the satisfaction of strict precedence if the attack relation is defined in an appropriate way. For those theories where the postulate is satisfied, stable semantics collapses into naive semantics. With attack relations from category $\mathfrak {R}_{s_3}$, pitfalls threaten as preferred options are discarded, and a lot of care must be exercised when designing such an argumentation system.

6.3 Preferred semantics

Preferred semantics was originally proposed in order to overcome the limitation of stable semantics which does not guarantee the existence of extensions. Indeed, any argumentation system has at least one preferred extension which may be empty. We show that in case of rule-based systems the empty set cannot be an extension.

Theorem 21

Let ${\mathcal {H}}$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {H}}$ satisfies the strict precedence postulate under preferred semantics. $\mathtt {Ext}_p({\mathcal {H}})\ne \{\emptyset \}$.

Unlike the cases of naive and stable extensions, a preferred extension may capture a proper sub-part of a maximal preferred option. For instance, it is not impossible that a preferred extension captures only the strict part of theory ${\mathcal {T}}_6$ in Example 7.

Theorem 22

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates under preferred semantics. For any ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$, $\exists {\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}})$.

Each preferred extension corresponds to exactly one maximal preferred option. It either returns all the consequences of that option, or chooses a subset. The latter contains all the conclusions that follow from the strict part and some conclusions that follow using defeasible rules. We show next that there is at least one maximal preferred option which is captured by a preferred extension. This is mainly due to the fact that stable extensions exist.

Theorem 23

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates under preferred semantics. There exists ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_p({\mathcal {H}})$.

Example 7 (Cont)

At least one of ${\mathtt {Arg}}({\mathcal {O}}_1)$ and ${\mathtt {Arg}}({\mathcal {O}}_2)$ is a preferred extension of an argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}_6), {\mathcal {R}})$ which satisfies the five postulates.

Two preferred extensions refer to different preferred options.

Theorem 24

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies exhaustiveness and closure under sub-arguments under preferred semantics. Let ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_p({\mathcal {H}})$ and ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. If $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Th}({\mathcal {E}}') \sqsubseteq {\mathcal {O}}$, then ${\mathcal {E}}= {\mathcal {E}}'$.

We show next that the free part of a theory, i.e., the sub-theory, which consists of the set of facts, the set of strict rules and the defeasible rules which are involved in every preferred option, is part of any preferred extension of argumentation systems that satisfy the postulates. Indeed, the set ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is part of every preferred extension of any argumentation system which satisfies consistency, exhaustiveness, strict precedence and closure under sub-arguments.

Theorem 25

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments (recall Definition 16), and ${\mathcal {H}}$ satisfies consistency, exhaustiveness, strict precedence and closure under sub-arguments under preferred semantics.

$$\begin{aligned} {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})) \subseteq \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_p({\mathcal {H}})} {\mathcal {E}}_i. \end{aligned}$$

From the previous results, it follows that the number of preferred extensions does not exceed the number of maximal preferred options of the theory over which the system is built.

Theorem 26

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates under preferred semantics.

$$\begin{aligned} 1 \le |\mathtt {Ext}_p({\mathcal {H}})| \le |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))| \end{aligned}$$

When a theory is finite, any argumentation system built over it has a finite number of preferred extensions.

Corollary 8

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates under preferred semantics. If ${\mathcal {T}}$ is finite, then ${\mathcal {H}}$ has a finite number of preferred extensions.

Let us now characterize the plausible conclusions that are drawn from a theory ${\mathcal {T}}$ by an argumentation system ${\mathcal {H}}$ satisfying the rationality postulates under preferred semantics. Let $\mathfrak {R}_p$ be the set of all attack relations that ensure the postulates under preferred semantics:

$\mathfrak {R}_p = \{{\mathcal {R}}\subseteq \mathtt {Arg}({\mathcal {T}}) \times \mathtt {Arg}({\mathcal {T}}) \ | \ {\mathcal {R}} \text{ is } \text{ conflict-dependent } \text{ and } (\mathtt {Arg}({\mathcal {T}}), {\mathcal {R}})$ $\mathrm{satisfies~the~five~postulates~under~preferred~semantics}\}.$

In his seminal paper [1], Dung has shown that the stable extensions of an argumentation system are also preferred extensions of the system. Consequently, the set $\mathfrak {R}_p$ is a subset of $\mathfrak {R}_s$.

Property 16

$\mathfrak {R}_p \subseteq \mathfrak {R}_s$.

Then, $\mathfrak {R}_p$ contains three disjoint subsets of attack relations: $\mathfrak {R}_p = \mathfrak {R}_{p_1} \cup \mathfrak {R}_{p_2} \cup \mathfrak {R}_{p_3}$:

• $\mathfrak {R}_{p_1}$: the relations which are in $\mathfrak {R}_p \cap \mathfrak {R}_{s_1}$.

• $\mathfrak {R}_{p_2}$: the relations which are in $\mathfrak {R}_p \cap \mathfrak {R}_{s_2}$.

• $\mathfrak {R}_{p_3}$: the relations which are in $\mathfrak {R}_p \cap \mathfrak {R}_{s_3}$.

Let us analyze each category of attack relations separately. The first set is empty (i.e., $\mathfrak {R}_{p_1} = \emptyset$) since we have shown previously that there is no attack relation which prevents an argumentation system from having stable extensions ($\mathfrak {R}_{s_1} = \emptyset$).

Attack relations of category $\mathfrak {R}_{p_2}$ lead to coherent argumentation systems (i.e., $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_p({\mathcal {H}})$) as shown in Theorem 17. Thus, preferred semantics does not provide an added value with respect to stable semantics. Moreover, there is a bijection between the two sets: $\mathtt {Ext}_p({\mathcal {H}})$ and $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$.

Corollary 9

Let ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}}),{\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{p_2}$.

• For any ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$, $\exists {\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$ and $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$.

• For any ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$, $\mathtt {Arg}({\mathcal {O}}) \in \mathtt {Ext}_p({\mathcal {H}})$.

• For any ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$, ${\mathcal {O}}= \mathtt {Option}({\mathtt {Arg}}({\mathcal {O}}))$.

In the case of attack relations of category $\mathfrak {R}_{p_2}$, ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is equal to the intersection of all preferred extensions.

Theorem 27

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$. If ${\mathcal {R}}\in \mathfrak {R}_{p_2}$, then

$$\begin{aligned} {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})) = \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_x({\mathcal {H}})} {\mathcal {E}}_i \end{aligned}$$

where $x \in \{p, s, ss\}$.

The output of an argumentation system is in this case the same as under stable semantics, i.e., the plausible conclusions given in Theorem 19.

Let us now analyze attack relations of category $\mathfrak {R}_{p_3}$. Remember that in this case stable semantics chooses only some maximal preferred options of the theory at hand. Four situations may be encountered:

• 1. The stable extensions and the preferred extensions of an argumentation system coincide. Thus, preferred semantics has no added value with respect to stable semantics. Moreover, it may lead to arbitrary results as discussed in the previous subsection when ${\mathcal {R}}\in \mathfrak {R}_{s_3}$ (see Example 7 where one of the defeasible rules is chosen in an arbitrary way).

• 2. The preferred extensions consider additional but not all maximal preferred options (other than the ones chosen by stable semantics). This case is similar to the previous one, and the argumentation system may return arbitrary results. Note that Example 7 is not sufficient to show this case since stable semantics will return one of ${\mathcal {O}}_1$ and ${\mathcal {O}}_2$ while preferred semantics will return the second one, which corresponds more to the case above. In order to exemplify this case, consider the following theory ${\mathcal {T}}_7$.

Example 8

Consider ${\mathcal {T}}_7$ such that ${\mathcal {F}}_7$, ${\mathcal {S}}_7$, ${\mathcal {D}}_7$ are as follows:

$$\begin{aligned} {\mathcal {F}}_7 \left\{ \begin{array}{l} p \\ t \\ \end{array}\right. \qquad \qquad {\mathcal {S}}_7 = \emptyset \qquad \qquad {\mathcal {D}}_7 \left\{ \begin{array}{l@{\;}c@{\;}l@{\quad }l@{}} p &{} \Rightarrow &{} q &{} (r_1) \\ q &{} \Rightarrow &{} s &{} (r_2) \\ t &{} \Rightarrow &{} \lnot s &{} (r_3) \\ t &{} \Rightarrow &{} \lnot q &{} (r_4) \end{array}\right. \end{aligned}$$

The theory ${\mathcal {T}}_7$ has three maximal preferred options:

• ${\mathcal {O}}_1 = ({\mathcal {F}}_7, {\mathcal {S}}_7, \{r_1, r_2\})$

• ${\mathcal {O}}_2 = ({\mathcal {F}}_7, {\mathcal {S}}_7, \{r_1, r_3\})$

• ${\mathcal {O}}_3 = ({\mathcal {F}}_7, {\mathcal {S}}_7, \{r_3, r_4\})$

Assume that ${\mathtt {Arg}}({\mathcal {O}}_1)$ is the single stable extension of an argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}_7), {\mathcal {R}})$ which satisfies the five postulates. Thus, ${\mathtt {Arg}}({\mathcal {O}}_1)$ is also a preferred extension of ${\mathcal {H}}$. Case 2 suggests either ${\mathtt {Arg}}({\mathcal {O}}_2)$ or ${\mathtt {Arg}}({\mathcal {O}}_3)$ (not both) is another preferred extension. Thus, as in Example 7, some rules are discarded in an arbitrary way.

• 3. The preferred extensions return all the maximal preferred options of the theory. This means that stable semantics chooses some maximal preferred options and preferred semantics considers the remaining ones. This case coincides exactly with the case of attack relations of category $\mathfrak {R}_{p_2}$ (see Theorem 19). Indeed, the argumentation system returns all the conclusions that follow from all maximal preferred options of the theory. Note that this output is also ensured by stable semantics when ${\mathcal {R}}\in \mathfrak {R}_{s2}$.

• 4. Some of the preferred extensions provide proper sub-parts of maximal preferred options. In this case, the result of the argumentation system may be arbitrary as can be seen on the following example.

Example 8 (Cont)

Consider an argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}_7),{\mathcal {R}})$ such that ${\mathcal {R}}\in \mathfrak {R}_{p_3}$. Assume that ${\mathcal {H}}$ has two preferred extensions: ${\mathcal {E}}_1$ and ${\mathcal {E}}_2$. From Theorem 23, one of them captures necessarily a maximal preferred option. Let ${\mathcal {E}}_1$ be such extension, and let $\mathtt {Option}({\mathcal {E}}_1) = {\mathcal {O}}_1$. Case 4 suggests that there is at least another preferred extension, say ${\mathcal {E}}_2$ such that $\mathtt {Option}({\mathcal {E}}_2) \sqsubset {\mathcal {O}}_i$ ($i = 2, 3$). Assume that $i = 2$ and $\mathtt {Th}({\mathcal {E}}_2) = ({\mathcal {F}}_7, {\mathcal {S}}_7, \{r_3\})$. Note that since preferred extensions are maximal for set inclusion, it cannot be the case that $\mathtt {Th}({\mathcal {E}}_2) = ({\mathcal {F}}_7, {\mathcal {S}}_7, \{r_1\})$ (since ${\mathcal {E}}_2$ would be a subset of ${\mathcal {E}}_1$). One can notice that among the four rules, $r_4$ is not used, which is unjustified.

To sum up, attack relations of category $\mathfrak {R}_{p_3}$ may lead either to arbitrary results or to results which can be provided by stable semantics.

6.4 Grounded: ideal semantics

This section analyzes the outcomes of rule-based systems under grounded and ideal semantics. Recall that both semantics ensure only one extension, which may be empty, for an argumentation system. Moreover, the grounded extension $\mathtt {GE}({\mathcal {H}})$ of an argumentation system ${\mathcal {H}}$ is a sub-part of the ideal extension $\mathtt {IE}({\mathcal {H}})$ of the same system. Consequently, the conclusions supported by the former are also supported by the latter, i.e., $\mathtt {Concs}(\mathtt {GE}({\mathcal {H}})) \subseteq \mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$. Note also that the output set of an argumentation system is exactly $\mathtt {Concs}(\mathtt {GE}({\mathcal {H}}))$ (respectively $\mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$) in case of grounded (respectively ideal) semantics. Before presenting the formal results, it is worth mentioning that an argumentation system that satisfies the postulates under preferred semantics does not necessarily satisfy the postulates under grounded/ideal semantics. Similarly, a system that satisfies the postulates under ideal semantics may violate some of the postulates under grounded semantics. That is why in the following we study each semantics separately.

The ideal extension, introduced in [19], is a maximal (for set inclusion) admissible set that is a subset of each preferred extension. In case of a rule-based argumentation system which satisfies the postulates, it returns a sub-part of one of the preferred options of the theory over which the system is built. Formally:

Theorem 28

If an argumentation system ${\mathcal {H}}$ satisfies the five postulates under ideal semantics, then there exists a preferred option ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$ such that $\mathtt {Th}(\mathtt {IE}({\mathcal {H}})) \sqsubseteq {\mathcal {O}}$ and $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset )) \subseteq \mathtt {Concs}(\mathtt {IE}({\mathcal {H}})) \subseteq \mathtt {CN}({\mathcal {O}})$.

Note that the outcome under ideal semantics may be arbitrary. This is in particular the case when the semantics selects one preferred option and draws all the conclusions that follow from this option. However, when the attack relation is of category $\mathfrak {R}_{p_2}$ and privileges strict arguments (recall Definition 16), then the ideal extension is exactly the set ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$.

Theorem 29

If an argumentation system ${\mathcal {H}}$ satisfies the five postulates under ideal semantics and ${\mathcal {R}}\in \mathfrak {R}_{p_2}$ and privileges strict arguments, then $\mathtt {IE}({\mathcal {H}})= {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$.

The above result shows that ideal semantics allows the inference of literals only from the free part of a theory.

Corollary 10

If an argumentation system ${\mathcal {H}}$ satisfies the five postulates under ideal semantics and ${\mathcal {R}}\in \mathfrak {R}_{p_2}$ and privileges strict arguments, then $\mathtt {Output}({\mathcal {H}})= \mathtt {CN}(\mathtt {Free}({\mathcal {T}}))$.

Note that in this case grounded extension may be more cautious than ideal one and may miss intuitive (free) conclusions since $\mathtt {GE}({\mathcal {H}})\subseteq {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$.

The grounded extension of any argumentation system which satisfies the postulates under grounded semantics captures a sub-part of a preferred option, i.e., it behaves exactly like ideal extension.

Theorem 30

If an argumentation system ${\mathcal {H}}$ satisfies the five postulates under grounded semantics, then there exists a preferred option ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$ such that $\mathtt {Th}(\mathtt {GE}({\mathcal {H}})) \sqsubseteq {\mathcal {O}}$ and $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset )) \subseteq \mathtt {Concs}(\mathtt {GE}({\mathcal {H}})) \subseteq \mathtt {CN}({\mathcal {O}})$.

7 Related work

The abstract argumentation framework proposed by Dung [1] was used for reasoning about defeasible information, and more generally for handling inconsistency. It was thus instantiated in different ways, considering different logical languages for representing information. Examples of such languages are propositional language (e.g.,[2, 3]) and rule-based ones (e.g., [8, 9, 11, 27, 29, 33]).

All the instantiations are defined in a similar way: define arguments and attacks, then apply Dung’s semantics on the defined graph, and infer the formulas that follow from all extensions. Some of these works are incomplete since there is one important step which is missing: characterizing the set of inferences that are drawn from a theory/knowledge base, i.e., describing formally how the output relates to the theory.

For filling this gap, in [4], we considered argumentation systems that use Tarskian logics, covering thus the systems studied in [2, 3]. In [11, 33], we focused on rule-based logics. Here we faced two issues: First, the logical languages that are considered in the literature are different. In ASPIC [8], defeasible rules express defaults and any uncertain information. In ABA [27], uncertain information is encoded by assumptions. In ASPIC+ [9], several types of information are considered (axioms, ordinary premises, issues, assumptions, strict rules and defeasible rules). The differences between all these types are unclear, especially between strict rules and axioms (both represent certain and non-defeasible information), and between ordinary premises, assumptions and defeasible rules (which all represent uncertain and defeasible information). Consequently, we have chosen the logical language used in the ASPIC system [8, 17]. It considers facts and strict rules (for encoding strict information) and defeasible rules (for encoding assumptions, defeasible rules, ordinary premises). Another issue with rule-based argumentation systems is that there are two types of attack relations: inconsistency-based ones and undercut which amounts to blocking the application of defeasible rules. For a better understanding of each type of attack relation, we studied in [11] argumentation systems that use undercut as their sole attack relation, and in this paper we studied the impact of inconsistency-based ones.

Our formalism uses the same logical language as ASPIC and a more general inconsistency-based attack relation. Our results apply thus to ASPIC when its undercut relation is empty. Note that our results and those from [11] should be combined for characterizing the outcomes of the ASPIC system when it uses the two kinds of relations. This is left for future work.

ASPIC+ uses a “richer” logical language since its aim was to unify all existing argumentation systems. It can thus be seen a union of several elementary systems: ABA for dealing with assumptions, ASPIC for dealing with strict/defeasible information, and the systems defined in [4] for dealing with Tarskian logics. In [4], we have characterized this sub-class of ASPIC+. In this paper, we characterized the sub-class capturing ASPIC.

The last well-known argumentation system, called ABA, cannot be compared to our formalism since the two systems use different logical languages. While ABA uses assumptions for capturing the defeasible information in a theory, our formalism uses defeasible rules.

8 Conclusion

The paper provides the first investigation on the outputs of rule-based argumentation systems that use inconsistency-based attack relations. The study is general in the sense that it keeps the attack relation unspecified. Thus, the system can be instantiated with any of the attack relations that are used in existing systems. The results show that under naive semantics, the systems return the literals that follow from all the options of the theory at hand. Stable and preferred semantics either do not provide an added value with respect to naive semantics or the attack relation of a system should be formalized in a very rigorous way in order to avoid arbitrary results. Ideal semantics returns the free part of a theory, whereas the grounded semantics returns a sub-part of the free part meaning that it may miss interesting conclusions.

Appendix: Proofs

Proof of Property 2

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory and $x \in {\mathcal {L}}$. Let $d = \langle (x_1,r_1), \ldots , (x_n,r_n)\rangle$ be a derivation schema for x from ${\mathcal {T}}$.

$(\longrightarrow )$ Let us assume that there exist $x_i$ and $x_j$ such that $x_i = x_j$ but $i \ne j$. Clearly, we can further assume $i < j$ without loss of generality. For each $(x_k,r_k)$ in d where $k > j$, $x_j \in \mathtt {Body}(r_k)$ is trivially equivalent to $x_i \in \mathtt {Body}(r_k)$ hence $\mathtt {Body}(r_k) \subseteq \{x_1,\ldots ,x_{j-1},x_{j+1},\ldots ,x_{k-1}\}$. Therefore, $\langle (x_1,r_1), \ldots , (x_{j-1},r_{j-1})$, $(x_{j+1},r_{j+1}), \ldots , (x_n,r_n)\rangle$ is also a derivation schema, but it is a proper subsequence of d, a contradiction arises. Now, let us assume that d fails to be focused. There exists $i \in \{1,\ldots ,n-1\}$ such that $x_i \not \in \mathtt {Body}(r_j)$ for every $j > i$. Consequently, $\langle (x_1,r_1),\ldots ,(x_{i-1},r_{i-1}),(x_{i+1},r_{i+1}),\ldots ,(x_n,r_n)\rangle$ is also a derivation schema for x in ${\mathcal {T}}$, contradicting the minimality of d.

$(\longleftarrow )$ Let us assume that d fails to be minimal although d is focussed and the literals $x_1,\ldots ,x_n$ are pairwise distinct. As d is not minimal, there exists a proper subsequence $d'$ of d which is a derivation schema for x in ${\mathcal {T}}$. Let us write $\langle (x_{k+1},r_{k+1}), \ldots , (x_n,r_n)\rangle$ for the largest common final subsequence of d and $d'$. Now, k exists (and $k > 0$) because $d'$ is a proper subsequence of d. As $d'$ is a derivation schema for $x_n$ and $d'$ is a subsequence of d and $x_1,\ldots ,x_n$ are pairwise distinct, $k < n$ ensues. Since d is focussed, $x_k \in \mathtt {Body}(r_j)$ for some $j > k$. So, $(x_j,r_j)$ is in $\langle (x_{k+1},r_{k+1}),\ldots ,(x_n,r_n)\rangle$. As $d'$ is a derivation schema, $\mathtt {Body}(r_j) \subseteq \{x_1,\ldots ,x_{k-1}\}$ (remember, $d'$ is a subsequence of $\langle (x_1,r_1), \ldots , (x_{k-1}$, $r_{k-1})$, $(x_{k+1}$, $r_{k+1}), \ldots , (x_n,r_n)\rangle$). Hence, $x_k \in \{x_1,\ldots ,x_{k-1}\}$. That is, $x_1,\ldots ,x_n$ are not pairwise distinct. $\square$

Proof of Property 3

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

• The inclusions $\mathtt {CN}({\mathcal {T}}) \subseteq {\mathcal {F}}\cup \{\mathtt {Head}(r) \mid r \in {\mathcal {S}}\cup {\mathcal {D}}\} \subseteq {\mathcal {L}}$ follow trivially from Definition 6.

• If ${\mathcal {T}}$ is finite, then ${\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}$ are finite. Thus, the set ${\mathcal {F}}\cup \{\mathtt {Head}(r) \mid r \in {\mathcal {S}}\cup {\mathcal {D}}\}$ is finite. From the first item, $\mathtt {CN}({\mathcal {T}})$ is finite.

• For any $x \in {\mathcal {F}}$, the sequence $\langle (x,\sigma )\rangle$ is a derivation schema for x from ${\mathcal {T}}$. Thus, $x \in \mathtt {CN}({\mathcal {T}})$ and this proves the inclusion ${\mathcal {F}}\subseteq \mathtt {CN}({\mathcal {T}})$.

• $\top \in \mathtt {CN}({\mathcal {T}})$ since $\top \in {\mathcal {F}}$ and ${\mathcal {F}}\subseteq \mathtt {CN}({\mathcal {T}})$.

• Assume that ${\mathcal {F}}= \{\top \}$ and $\not \exists r \in {\mathcal {D}}$ such that $\mathtt {Body}(r) = \{\top \}$. Thus, since the body of any other rule in ${\mathcal {T}}$ is assumed to be non-empty, no rule in ${\mathcal {S}}\cup {\mathcal {D}}$ can be applied, hence $\mathtt {CN}({\mathcal {T}}) = \{\top \}$. Conversely, if $\mathtt {CN}({\mathcal {T}}) = \{\top \}$, then ${\mathcal {F}}= \{\top \}$ (since ${\mathcal {F}}\subseteq \mathtt {CN}({\mathcal {T}})$) and $\not \exists r \in {\mathcal {D}}$ such that $\mathtt {Body}(r) = \{\top \}$ (since each such rule is applicable when it exists).

• Let $d = \langle (x_1,r_1),\ldots ,(x_n,r_n)\rangle$ be a derivation schema for $x \in {\mathcal {L}}$ from ${\mathcal {T}}$. From Definition 6, for each $x_i$ ($i = 1, \ldots , n$), there exists a derivation schema from ${\mathcal {T}}$ for $x_i$. Thus, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {T}})$. $\square$

Proof of Property 4

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ and ${\mathcal {T}}' = ({\mathcal {F}}', {\mathcal {S}}', {\mathcal {D}}')$ be two theories such that ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$. Let $x \in \mathtt {CN}({\mathcal {T}})$. So, there exists a derivation schema $d = \langle (x_1,r_1), \ldots , (x_n,r_n)\rangle$ for x from ${\mathcal {T}}$. Since ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$, $\mathtt {Facts}(d) \subseteq {\mathcal {F}}'$ and $\mathtt {Strict}(d) \subseteq {\mathcal {S}}'$ and $\mathtt {Def}(d) \subseteq {\mathcal {D}}'$. Therefore, d is also a derivation schema for x from ${\mathcal {T}}'$. $\square$

Proof of Property 5

The two properties follow trivially from the definition of option. $\square$

Proof of Property 6

The inclusion $\mathtt {POpt}({\mathcal {T}})\subseteq \mathtt {Opt}({\mathcal {T}})$ follows trivially from Definitions 9 and 10.

Assume that $\mathtt {CN}({\mathcal {T}})$ is consistent. From Property 5, $\mathtt {Opt}({\mathcal {T}}) = \{{\mathcal {T}}\}$. Since $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubseteq {\mathcal {T}}$, $\mathtt {POpt}({\mathcal {T}})= \{{\mathcal {T}}\}$. Assume now that $\mathtt {Opt}({\mathcal {T}}) \subseteq \mathtt {POpt}({\mathcal {T}})$. Since $\mathtt {Opt}({\mathcal {T}}) \ne \emptyset$, for all ${\mathcal {O}}\in \mathtt {Opt}({\mathcal {T}})$ it holds that ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$. Thus, for all ${\mathcal {O}}\in \mathtt {Opt}({\mathcal {T}})$, $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubseteq {\mathcal {O}}$. It follows that $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubseteq \mathtt {Free}({\mathcal {T}})$.² Assume that $\mathtt {CN}({\mathcal {T}})$ is inconsistent. Then, there exists a minimal conflict$^2$$C = (X, Y, Z) \sqsubseteq {\mathcal {T}}$. Since $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubseteq \mathtt {Free}({\mathcal {T}})$, $X = Y = \emptyset$. But, by assumption, the body of every defeasible rule is not empty. Thus, $\mathtt {CN}(C) = \emptyset$. This contradicts the fact that $\mathtt {CN}(C)$ is inconsistent. $\square$

Proof of Property 7

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory.

Assume that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ is consistent. Thus, there exists a preferred option ${\mathcal {O}}$ such that either (i) for all $r \in {\mathcal {D}}$, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \{r\}))$ is inconsistent meaning that ${\mathcal {O}}= \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ or (ii) there exists $r \in {\mathcal {D}}$ such that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \{r\}))$ is consistent thus $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubset {\mathcal {O}}$. In both cases, $\mathtt {POpt}({\mathcal {T}})\ne \emptyset$. Assume now that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ is inconsistent. Since ${\mathcal {F}}$ and ${\mathcal {S}}$ should be part of any preferred option and the set of consequences of a preferred option should be consistent, then $\mathtt {POpt}({\mathcal {T}})= \emptyset$.

Let $r \in {\mathcal {D}}$ and assume that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \{r\}))$ is consistent. From Definition 10, $({\mathcal {F}}, {\mathcal {S}}, \{r\})$ is either a preferred option (iff for all $r' \in {\mathcal {D}}$ such that $r \ne r'$, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \{r, r'\}))$ is inconsistent). Or, there exists a preferred option ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, \{r\} \cup {\mathcal {D}}')$ where ${\mathcal {D}}' \subseteq {\mathcal {D}}{\setminus } \{r\}$. $\square$

Proof of Property 8

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory and $\mathtt {Free}({\mathcal {T}})= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}')$. From the definition of $\mathtt {Free}({\mathcal {T}})$, $\mathtt {Free}({\mathcal {T}})\sqsubseteq {\mathcal {O}}$ for all ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$. From Property 4, $\mathtt {CN}(\mathtt {Free}({\mathcal {T}})) \subseteq \mathtt {CN}({\mathcal {O}})$. Since $\mathtt {CN}({\mathcal {O}})$ is consistent, then so is for $\mathtt {CN}(\mathtt {Free}({\mathcal {T}}))$. $\square$

Proof of Property 9

Let (d, x) be a sub-argument of $(d',x')$. Let $x_i \in \mathtt {Seq}(d)$. There are two possibilities:

• $x_i \in \mathtt {Facts}(d)$, thus $x_i \in \mathtt {Facts}(d')$ since $\mathtt {Facts}(d) \subseteq \mathtt {Facts}(d')$. So, $x_i \in \mathtt {Seq}(d')$.

• $x_i = \mathtt {Head}(r)$ with $r \in \mathtt {Strict}(d) \cup \mathtt {Def}(d)$; thus, $r \in \mathtt {Strict}(d') \cup \mathtt {Def}(d')$ since $\mathtt {Strict}(d) \subseteq \mathtt {Strict}(d')$ and $\mathtt {Def}(d) \subseteq \mathtt {Def}(d')$. So, $x_i \in \mathtt {Seq}(d')$.

$\square$

Proof of Property 10

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ be a theory. Since $\top \in {\mathcal {F}}$ by Definition 4, $(\langle \top , \sigma \rangle , \top ) \in {\mathtt {Arg}}({\mathcal {T}})$ and thus ${\mathtt {Arg}}({\mathcal {T}}) \ne \emptyset$. $\square$

Proof of Property 11

Let ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$ and $\mathtt {Ext}({\mathcal {H}})$ its set of extensions under any extension-based semantics. Assume that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$.

Let $x \in \mathtt {Output}({\mathcal {H}})$. Thus, for all ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$, $\exists a \in {\mathcal {E}}$ such that $\mathtt {Conc}(a) = x$. It follows that $x \in \mathtt {Concs}({\mathcal {E}}_i)$, $\forall {\mathcal {E}}_i \in \mathtt {Ext}({\mathcal {H}})$ and hence $x \in \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i)$.

Assume now that $x \in \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i)$. Thus, $\forall {\mathcal {E}}_i$, $\exists a_i \in {\mathcal {E}}_i$ such that $\mathtt {Conc}(a_i) = x$. Consequently, $x \in \mathtt {Output}({\mathcal {H}})$. $\square$

Proof of Property 12

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. Let $x \in \mathtt {Output}({\mathcal {H}})$. From Definition 17, $\exists (d,x) \in {\mathtt {Arg}}({\mathcal {T}})$. From Definition 12, d is a derivation for x from ${\mathcal {T}}$. Thus, $x \in \mathtt {CN}({\mathcal {T}})$. $\square$

Proof of Property 16

Let ${\mathcal {R}}\in \mathfrak {R}_p$ and let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be a rule-based argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. Since ${\mathcal {H}}$ satisfies the five postulates, thus for all ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$,

• $\mathtt {Concs}({\mathcal {E}})$ is consistent

• $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Concs}({\mathcal {E}}), {\mathcal {S}}, \emptyset )$

• For all $a \in {\mathcal {E}}$, $\mathtt {Sub}(a) \subseteq {\mathcal {E}}$

• for all $(d,x) \in {\mathtt {Arg}}({\mathcal {T}})$, if $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$, then $(d,x) \in {\mathcal {E}}$.

From Property 1, $\mathtt {Ext}_s({\mathcal {H}})\subseteq \mathtt {Ext}_p({\mathcal {H}})$, then for all ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$, ${\mathcal {E}}$ satisfies the above four properties. Thus, ${\mathcal {H}}$ satisfies consistency, exhaustiveness and closure under both sub-arguments and strict rules. Let us now show that it also satisfies strict precedence under stable semantics. From Property 11, $\mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_p({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i)$. Thus, for all ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$, $\mathtt {Output}({\mathcal {H}})\subseteq \mathtt {Concs}({\mathcal {E}})$. Since ${\mathcal {H}}$ satisfies strict precedence under preferred semantics, $\mathtt {CN}({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \subseteq \mathtt {Concs}({\mathcal {E}})$. Thus, the property is satisfied by every stable extension. $\square$

Proof of Proposition 1

Let ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. Let ${\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Opt}({\mathcal {T}})$ be such that $\mathtt {CN}({\mathcal {O}}) = \mathtt {CN}({\mathcal {O}}')$. Let ${\mathcal {O}}= (X, Y, Z)$ and ${\mathcal {O}}' = (X', Y', Z')$. For all $x \in X$, $x \in \mathtt {CN}({\mathcal {O}})$ and thus $x \in X'$. The same holds for all $x' \in X'$. Thus, $X = X'$.

Let $r \in Y \cup Z$. There are two cases: (i) $\mathtt {Body}(r) \not \subseteq \mathtt {CN}({\mathcal {O}})$. Consequently, $\mathtt {Body}(r) \not \subseteq \mathtt {CN}({\mathcal {O}}')$. Thus, $\mathtt {CN}({\mathcal {O}}' \oplus r)$ is consistent. So, $r \in Y' \cup Z'$ (by definition of an option).

(ii) $\mathtt {Body}(r) \subseteq \mathtt {CN}({\mathcal {O}})$. Consequently, $\mathtt {Body}(r) \subseteq \mathtt {CN}({\mathcal {O}}')$. Thus, $\mathtt {CN}({\mathcal {O}}' \oplus r)$ is consistent. So, $r \in Y' \cup Z'$ (by definition of an option). $\square$

Proof of Proposition 2

If ${\mathcal {T}}$ is finite, then $\mathtt {CN}({\mathcal {T}})$ is finite (apply Property 3). Consequently, ${\mathtt {Arg}}({\mathcal {T}})$ is finite. $\square$

Proof of Proposition 3

Let ${\mathcal {T}}$ and ${\mathcal {T}}'$ be two theories such that ${\mathcal {T}}\sqsubseteq {\mathcal {T}}'$. Let (d, x) be an argument defined from ${\mathcal {T}}$. All items in Definition 12 are independent from ${\mathcal {T}}$ except for d being a derivation schema for x from ${\mathcal {T}}$. Hence, for (d, x) to be an argument defined from ${\mathcal {T}}'$, it is enough that d be a derivation schema for x from ${\mathcal {T}}'$. Now, this is equivalent to $x \in \mathtt {CN}({\mathcal {T}}')$. By Property 4, the latter follows from $x \in \mathtt {CN}({\mathcal {T}})$ (which is itself proved from the fact that d is a derivation schema for x from ${\mathcal {T}}$). Thus, (d, x) is an argument defined from ${\mathcal {T}}'$. $\square$

Proof of Proposition 4

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system such that ${\mathcal {R}}$ is conflict-dependent. Let $a = (d,x) \in {\mathtt {Arg}}({\mathcal {T}})$ be such that $(a,a) \in {\mathcal {R}}$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d)$ is inconsistent. This is impossible since a is an argument (thus $\mathtt {Seq}(d)$ should be consistent). $\square$

Proof of Proposition 5

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that $\mathtt {CN}({\mathcal {T}})$ is consistent and ${\mathcal {R}}$ is conflict-dependent. Assume that ${\mathtt {Arg}}({\mathcal {T}})$ is not conflict-free. Thus, there exist $(d,x), (d',x') \in {\mathtt {Arg}}({\mathcal {T}})$ such that $(d,x) {\mathcal {R}}(d',x')$. Consequently, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. Besides, from Property 3, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {T}})$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {T}})$. Thus, $\mathtt {CN}({\mathcal {T}})$ is inconsistent. Contradiction. $\square$

Proof of Proposition 6

Let ${\mathcal {H}}$ be an argumentation system which satisfies consistency and closure under sub-arguments. From Proposition 12, $\forall {\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$$\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Since ${\mathcal {H}}$ satisfies consistency, $\forall {\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$$\mathtt {Concs}({\mathcal {E}})$ is consistent. Thus, so is for $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. $\square$

Proof of Proposition 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\emptyset \in \mathtt {Ext}({\mathcal {H}})$. Thus, $\mathtt {Output}({\mathcal {H}})= \emptyset$. Assume that ${\mathcal {H}}$ satisfies strict precedence, then $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$$\subseteq$$\mathtt {Output}({\mathcal {H}})$. Since $\top \in {\mathcal {F}}$ and from Property 3, it holds that ${\mathcal {F}}\subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$, then $\top \in \mathtt {Output}({\mathcal {H}})$. $\square$

Proof of Proposition 8

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. Assume that ${\mathcal {H}}$ satisfies consistency and strict precedence. From Property 13, it holds that $\mathtt {Output}({\mathcal {H}})$ is consistent. From strict precedence, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$$\subseteq$$\mathtt {Output}({\mathcal {H}})$. Thus, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ is consistent. $\square$

Proof of Proposition 9

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ (under an extension-based semantics). Assume that ${\mathcal {H}}$ is closed under sub-arguments and satisfies exhaustiveness. Let ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$. From the monotonicity of ${\mathtt {Arg}}$, it holds that ${\mathcal {E}}\subseteq {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$. Let $(d,x) \in {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$. From Proposition 12, $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$. From the exhaustiveness postulate, $(d,x) \in {\mathcal {E}}$. $\square$

Proof of Proposition 10

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ (under an extension-based semantics). Assume that ${\mathcal {H}}$ satisfies exhaustiveness and strict precedence. Since ${\mathcal {H}}$ satisfies strict precedence, $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset )) \subseteq \mathtt {Output}({\mathcal {H}})$. From Property 11, for all ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$, $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset )) \subseteq \mathtt {Concs}({\mathcal {E}})$. Let $(d,x) \in {\mathtt {Arg}}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$. Thus, $\mathtt {Seq}(d) \subseteq \mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$. From exhaustiveness, $(d,x) \in {\mathcal {E}}$. $\square$

Proof of Proposition 11

In order to prove the compatibility of the postulates, it is sufficient to give an example of a system which satisfies all the five postulates. This system is ASPIC as defined in [17]. Proposition 1 in [17] shows that the system is closed under sub-arguments under any Dung’s semantics. Proposition 8 in [17] shows that the system is closed under strict rules under complete semantics, thus under stable semantics. Property 2 in [17] shows that the system satisfies consistency under any Dung’s semantics. From Proposition 13, the system satisfies exhaustiveness. Let us now show that the system satisfies strict precedence. This follows from the definition of attack relation (Definition 16 in [17]) according to which a strict argument cannot be attacked. Thus, it belongs to any stable extension. $\square$

Proof of Proposition 12

Let ${\mathcal {H}}$ be an argumentation system such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$ where $\mathtt {Ext}({\mathcal {H}})$ is its set of extensions under an extension-based semantics. Assume that ${\mathcal {H}}$ is closed under sub-arguments and let ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$.

• Let $x \in \mathtt {Concs}({\mathcal {E}})$. Thus, $\exists (d, x) \in {\mathcal {E}}$ where d is a derivation for x from $(\mathtt {Facts}(d)$, $\mathtt {Strict}(d)$, $\mathtt {Def}(d))$. From Property 3, $x \in \mathtt {Facts}(d)$ (thus $x \in X$), or $x = \mathtt {Head}(r)$ where $r \in \mathtt {Strict}(d)$ (thus $r \in Y$) or $x \in \mathtt {Def}(d)$ (thus $x \in Z$).

  Assume now that $x \in X$. Thus, $\exists (d,y) \in {\mathcal {E}}$ such that $x \in \mathtt {Facts}(d)$. Besides, $(\langle (x,\sigma )\rangle , x)$ is a sub-argument of (d, y). Since ${\mathcal {H}}$ is closed under sub-arguments, $(\langle (x,\sigma )\rangle , x) \in {\mathcal {E}}$, and thus, $x \in \mathtt {Concs}({\mathcal {E}})$.

  Let $r \in Y \cup Z$. Thus, $\exists (d,x) \in {\mathcal {E}}$ such that $r \in \mathtt {Strict}(d) \cup \mathtt {Def}(d)$. Let $d = \langle (x_1,r_1), \ldots , (x_i,r), (x_{i+1},r_{i+1}) \ldots , (x_n = x,r_n)\rangle$ with $x_i = \mathtt {Head}(r)$. Thus, there exists a sub-sequence $d'$ of d which is a derivation for $x_i$. This derivation is minimal (for set inclusion since (d, x) is an argument). Thus, $(d', x_i)$ is an argument. Moreover, it is a sub-argument of (d, x). Since ${\mathcal {H}}$ is closed under sub-arguments, $(d',x_i) \in {\mathcal {E}}$. Consequently, $x_i \in \mathtt {Concs}({\mathcal {E}})$. Thus, $\mathtt {Concs}({\mathcal {E}}) = X \cup \{\mathtt {Head}(r) \mid r \in Y \cup Z\}$.

• From the definitions of the two functions $\mathtt {Concs}$ and $\mathtt {Th}$, it follows that $\mathtt {Concs}({\mathcal {E}})$$\subseteq$$\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. From Property 3, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) \subseteq X \cup \{\mathtt {Head}(r) \mid r \in Y \cup Z\}$. From above, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) \subseteq \mathtt {Concs}({\mathcal {E}})$.

• Assume now that $a = (d, x) \in {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$. For all $x_i \in \mathtt {Seq}(d)$, $x_i \in \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {Concs}({\mathcal {E}})$. Then, $x_i \in \mathtt {Concs}({\mathcal {E}})$. Thus, $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$.

$\square$

Proof of Proposition 13

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments. Assume that ${\mathcal {H}}$ violates exhaustiveness. Thus, there exists ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ and there exists $a = (d,x) \in {\mathtt {Arg}}({\mathcal {T}})$ such that $\mathtt {Seq}(d) \subseteq \mathtt {Concs}({\mathcal {E}})$ but $(d,x) \notin {\mathcal {E}}$. So, $\exists b = (d',x') \in {\mathcal {E}}$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. Thus, $\exists y \in \mathtt {Seq}(d)$ such that $\lnot y \in d'$. But, $y, \lnot y \in \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {Concs}({\mathcal {E}})$. Thus, $y, \lnot y \in \mathtt {Concs}({\mathcal {E}})$. This contradicts the fact that ${\mathcal {H}}$ satisfies consistency. $\square$

Proof of Proposition 14

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments. From Proposition 13, ${\mathcal {H}}$ satisfies exhaustiveness. From Proposition 9, it follows that for all ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, ${\mathcal {E}}= {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$. $\square$

Proof of Proposition 15

The proof is similar to that of Propositions 13 and 14. $\square$

Proof of Theorem 1

Let ${\mathcal {T}}$ be a theory and $d = \langle (x_1,r_1),\ldots ,(x_n,r_n)\rangle$ a consistent sequence from ${\mathcal {T}}$.

$(\longrightarrow )$ Assume that (d, x) is an argument from ${\mathcal {T}}$. $d = \langle (x_1,r_1),\ldots ,(x_n,r_n)\rangle$ yields $x = x_n$ (Definition 12). Assume that d is not focused. Let $d^*$ be obtained from d by deleting all repeated pairs. Since d is not focused, $d^*$ is not minimal. Therefore, there exists $(x_k,r_k)$ in $d^*$ (hence in d) such that depriving $d^*$ from $(x_k,r_k)$ still gives a derivation of x from ${\mathcal {T}}$. Since $d^*$ contains no repeated pair, for every $(x_i,r_i)$ in $d^*$, if $i \ne k$ then either $x_i \ne x_k$ or $r_i \ne r_k$. For $r_k \ne \sigma$, the former implies the latter hence $r_i \ne r_k$ whenever $i \ne k$. Thus, depriving $d^*$ from $(x_k,r_k)$ gives a derivation $d'$ of x from ${\mathcal {T}}$ such that $\mathtt {Facts}(d') \subseteq \mathtt {Facts}(d)$ and $\mathtt {Strict}(d') \subseteq \mathtt {Strict}(d)$ and $\mathtt {Def}(d') \subseteq \mathtt {Def}(d)$, with one of the latter two inclusions being strict. That is, there exists ${\mathcal {T}}' \sqsubset (\mathtt {Facts}(d), \mathtt {Strict}(d), \mathtt {Def}(d))$ such that $x \in \mathtt {CN}({\mathcal {T}}')$, thereby contradicting Definition 12. The remaining case is $r_k = \sigma$. Since $d^*$ contains no repeated pair, no $(x_i,r_i)$ in $d^*$ is $(x_k,\sigma )$ except for $i = k$ and it follows that $d^*$ deprived from $(x_k,r_k)$ gives a derivation $d'$ of x from ${\mathcal {T}}$ such that $\mathtt {Facts}(d') \subset \mathtt {Facts}(d)$ while $\mathtt {Strict}(d') \subseteq \mathtt {Strict}(d)$ and $\mathtt {Def}(d') \subseteq \mathtt {Def}(d)$. As above, a contradiction arises.

$(\longleftarrow )$ Assume that d is a focused derivation schema from ${\mathcal {T}}$ such that $x_n = x$. By the definitions, $x \in {\mathcal {L}}$ and d is a derivation schema for x from ${\mathcal {T}}$. Due to the hypothesis in the statement of the theorem, $\mathtt {Seq}(d)$ is consistent. Assume that there exists ${\mathcal {T}}' = ({\mathcal {F}}', {\mathcal {S}}', {\mathcal {D}}') \sqsubset (\mathtt {Facts}(d),\mathtt {Strict}(d),\mathtt {Def}(d))$ such that $x \in \mathtt {CN}({\mathcal {T}}')$. That is, there exists a derivation $d' = \langle (x'_1,r'_1),\ldots ,(x'_m,r'_m)\rangle$ for some $m < n$ such that $\mathtt {Facts}(d') = {\mathcal {F}}'$ and $\mathtt {Strict}(d') = {\mathcal {S}}'$ and $\mathtt {Def}(d') = {\mathcal {D}}'$. Let $d^*$ be a minimal derivation schema for x from ${\mathcal {T}}$ obtained from d by deleting all repeated pairs. Accordingly, $\mathtt {Facts}(d^*) = \mathtt {Facts}(d)$ and $\mathtt {Strict}(d^*) = \mathtt {Strict}(d)$ and $\mathtt {Def}(d^*) = \mathtt {Def}(d)$. Since $\mathtt {Strict}(d') \subseteq \mathtt {Strict}(d)$ and $\mathtt {Def}(d') \subseteq \mathtt {Def}(d)$, if $(x'_i,r'_i)$ is in $d'$ with $r'_i \ne \sigma$ then there exists k such that $(x_k,r_k)$ is in $d^*$ where $r_k = r'_i$ (also, $x_k = x'_i$ because $x'_i = \mathtt {Head}(r'_i) = \mathtt {Head}(r_k) = x_k$). Similarly, since $\mathtt {Facts}(d') \subseteq \mathtt {Facts}(d)$, if $(x'_i,r'_i)$ is in $d'$ with $r'_i = \sigma$ then there exists k such that $(x_k,r_k)$ is in $d^*$ where $x'_i = x_k$ and $r_k = r'_i = \sigma$. That is, $d'$ is a proper subsequence of a reordering of $d^*$, thereby contradicting the minimality of $d^*$.

Indeed, let us show that no initial proper fragment of a reordering $d^{*}_\iota$ of $d^*$ is a minimal derivation of x. Assume a reordering $d^{*}_\iota = \langle (x^*_{\iota 1},r^*_{\iota 1}),\ldots ,(x^*_{\iota p},r^*_{\iota p})\rangle$ of $d^* = \langle (x^*_1,r^*_1),\ldots ,(x^*_p,r^*_p)\rangle$ such that $d_{\iota } = \langle (x^*_{\iota 1},r^*_{\iota 1}),\ldots ,(x^*_{\iota q},r^*_{\iota q})\rangle$ is a minimal derivation of x from ${\mathcal {T}}$ for some $q < p$. Let j be the greatest index from $1 \ldots p$ such that $x^*_j$ is in $\mathtt {Seq}(d^*)$ but not in $\mathtt {Seq}(d_{\iota })$ (clearly, $j < p$). Since $d^*$ is minimal, there must exist $h > j$ such that $x^*_j \in \mathtt {Body}(r^*_h)$ (otherwise $d^*$ deprived of $(x^*_j,r^*_j)$ would give a proper subsequence also being a derivation of x). By Property 2, $x^*_h \ne x^*_i$ for $i \ne h$. Hence, $\mathtt {Head}(r^*_i) \ne x^*_h$ for $i \ne h$. Together with $x^*_j \not \in \mathtt {Seq}(d_{\iota })$ and $x^*_j \in \mathtt {Body}(r^*_h)$, this entails $x^*_h \not \in \mathtt {Seq}(d_{\iota })$. Therefore, j is not the greatest index such that $x^*_j$ is in $\mathtt {Seq}(d^*)$ but not in $\mathtt {Seq}(d_{\iota })$. $\square$

Lemma 1

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ is consistent and ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments. For all $a \in {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$, $b \in {\mathtt {Arg}}({\mathcal {T}})$, if $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$, then $\exists a' \in \mathtt {Sub}(a)$ such that $a'$ is strict and $a' {\mathcal {R}}b$.

Proof

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ is consistent. Assume that ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments.

Assume that $\exists a = (d,x) \in {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ and $\exists b = (d',x') \in {\mathtt {Arg}}({\mathcal {T}})$ such that $b {\mathcal {R}}a$ or $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent and thus $\mathtt {CN}(\mathtt {Th}(\{a\})) \cup \mathtt {CN}(\mathtt {Th}(\{b\}))$ is inconsistent (since from Property 3, $\mathtt {Seq}(d) \subseteq \mathtt {CN}(\mathtt {Th}(\{a\}))$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}(\{b\}))$).

Let $\mathtt {Th}(\{a\}) = (X,Y,Z)$ and $\mathtt {Th}(\{b\}) = (X',Y',Z')$. Let us show that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z'))$ is inconsistent. Assume that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z'))$ is consistent. Thus, there exists a preferred option ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$ such that $({\mathcal {F}}, {\mathcal {S}}, Z') \sqsubseteq {\mathcal {O}}$. Since $(X,Y,Z) \sqsubseteq \mathtt {Free}({\mathcal {T}})$ and $\mathtt {Free}({\mathcal {T}})\sqsubseteq {\mathcal {O}}$, $({\mathcal {F}}, {\mathcal {S}}, Z\cup Z') \sqsubseteq {\mathcal {O}}$. From Property 4, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z\cup Z')) \subseteq \mathtt {CN}({\mathcal {O}})$. Thus, $\mathtt {CN}({\mathcal {O}})$ is inconsistent. This contradicts the fact that ${\mathcal {O}}$ is an option.

Let $Z^*$ be the smallest (for set inclusion) subset of $Z'$ such that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z^*))$ is inconsistent. Thus, for all $r \in Z^*$, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z^*{\setminus }\{r\}))$ is consistent. It follows that for all $r \in Z^*$, there exists a preferred option ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$ such that $({\mathcal {F}}, {\mathcal {S}}, Z \cup Z^*{\setminus }\{r\}) \sqsubseteq {\mathcal {O}}$ by Property 8.

Assume that for every strict $a'' \in \mathtt {Sub}(a)$, $\mathtt {Seq}(d'') \cup \mathtt {Seq}(d')$ is consistent. However, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent (since $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$ while ${\mathcal {R}}$ is conflict-dependent). Hence, $\mathtt {Head}(\mathtt {Def}(d)) \cup \mathtt {Head}(\mathtt {Def}(d'))$ is inconsistent, say $y \in \mathtt {Head}(\mathtt {Def}(d))$ and $\lnot y \in \mathtt {Head}(\mathtt {Def}(d'))$. Should no such y be in ${\mathcal {F}}\cup \mathtt {Head}(S)$, then there would be a preferred option $O=(F,S,D_O)$ with $\lnot y \in \mathtt {Head}(D_O)$. A contradiction arises, because $a=(d,x)$ being in ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ means that $\mathtt {Def}(d)$ is a subset of $D_O$ for every preferred option $O=(F,S,D_O)$.

That is, there exists $a'' = (d'',x'') \in \mathtt {Sub}(a)$ such that $a''$ is strict and $\mathtt {Seq}(d'') \cup \mathtt {Seq}(d')$ is inconsistent. Since ${\mathcal {R}}$ privileges strict arguments, $a'' {\mathcal {R}}b$. $\square$

Proof of Theorem 2

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ is consistent. Assume that ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments.

We show first that ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is conflict-free. From Property 8, $\mathtt {CN}(\mathtt {Free}({\mathcal {T}}))$ is consistent. Since ${\mathcal {R}}$ is conflict-dependent, from Proposition 5, ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is conflict-free.

Let us now show that ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ defends its elements. Assume that $\exists a = (d,x) \in {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ and $\exists b = (d',x') \in {\mathtt {Arg}}({\mathcal {T}})$ such that $b {\mathcal {R}}a$. From Lemma 1, there exists $a' = (d'',x'') \in \mathtt {Sub}(a)$ such that $a'$ is strict, hence $a \in {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$, and $a' {\mathcal {R}}b$. $\square$

Proof of Theorem 3

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that $\mathtt {Ext}({\mathcal {H}})\ne \emptyset$. Assume that ${\mathcal {H}}$ satisfies strict precedence and closure under both strict rules and sub-arguments. Let ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$. Since $X \subseteq {\mathcal {F}}$ and $Y \subseteq {\mathcal {S}}$, $(X, Y, Z) \sqsubseteq ({\mathcal {F}}, {\mathcal {S}}, Z)$. From Property 4, $\mathtt {CN}((X, Y, Z)) \subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z))$.

Let us now show that $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z)) \subseteq \mathtt {CN}((X, Y, Z))$. Since ${\mathcal {H}}$ satisfies strict precedence, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq \mathtt {Output}({\mathcal {H}})$. From Property 11, $\mathtt {Output}({\mathcal {H}})\subseteq \mathtt {Concs}({\mathcal {E}})$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ by Proposition 12. Hence, $\mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq \mathtt {CN}((X, Y, Z))$. Furthermore, from Property 3, ${\mathcal {F}}\subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$. Thus, $X = {\mathcal {F}}$, i.e., $\mathtt {Th}({\mathcal {E}}) = ({\mathcal {F}}, Y, Z)$. Let $x \in \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z))$. Then, there exists a derivation schema

$$\begin{aligned} d = \langle (x_1,r_1), \ldots , (x_n, r_n)\rangle \end{aligned}$$

for x from $({\mathcal {F}}, {\mathcal {S}}, Z)$. There are two cases:

• For any $i = 1, \ldots , n$, $r_i \in \{\sigma \} \cup Y \cup Z$. Hence, d is also a derivation schema for x from $({\mathcal {F}}, Y, Z)$. Thus, $x \in \mathtt {CN}(({\mathcal {F}}, Y, Z))$.

• There exists $1 < i \le n$ such that $r_i \in {\mathcal {S}}{\setminus } Y$ (note that the two theories $({\mathcal {F}}, Y, Z)$ and $({\mathcal {F}}, {\mathcal {S}}, Z)$ differ only on ${\mathcal {S}}{\setminus } Y$). Let i be the first step where an element of ${\mathcal {S}}{\setminus } Y$ is used in the derivation d. Note also that $i > 1$ since strict rules have non-empty bodies. Thus, for any $j < i$, $r_j \in \{\sigma \} \cup Y \cup Z$ and $\langle (x_1,r_1), \ldots , (x_j, r_j)\rangle$ is a derivation schema of $x_j$ from $({\mathcal {F}}, Y, Z)$. Thus, $x_j \in \mathtt {CN}(({\mathcal {F}}, Y, Z))$. Furthermore, $\mathtt {Body}(r_i) \subseteq \{x_1, \ldots , x_{i-1}\}$, so $\mathtt {Body}(r_i) \subseteq \mathtt {CN}(({\mathcal {F}}, Y, Z))$. Since $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$, $\mathtt {Body}(r_i) \subseteq \mathtt {Concs}({\mathcal {E}})$. Since ${\mathcal {H}}$ is closed under strict rules, $\mathtt {Head}(r_i) \in \mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(({\mathcal {F}}, Y, Z))$, i.e., $x_i \in \mathtt {CN}(({\mathcal {F}}, Y, Z))$. We repeat the same reasoning for showing that each $x_i \in \mathtt {CN}(({\mathcal {F}}, Y, Z))$ and conclude that $x \in \mathtt {CN}(({\mathcal {F}}, Y, Z))$.

$\square$

Proof of Theorem 4

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {H}}$ satisfies strict precedence, and closure under both strict rules and sub-arguments.

Let ${\mathcal {E}}\in \mathtt {Ext}({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$. From Theorem 3 and Proposition 12, it holds that

$$\begin{aligned} \mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z)) = \mathtt {Concs}({\mathcal {E}}). \end{aligned}$$

(*)

Let ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, Z \cup Z')$ where $Z' = \{r \ | \ r \in {\mathcal {D}}{\setminus } Z \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))\}$. Since $({\mathcal {F}}, {\mathcal {S}}, Z) \sqsubseteq {\mathcal {O}}$, then from Property 4 and (*), $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}})$. Let us now show that $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {Concs}({\mathcal {E}})$. Let $x \in \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z \cup Z'))$. Then, there exists a derivation schema

$$\begin{aligned} d = \langle (x_1,r_1), \ldots , (x_n, r_n)\rangle \end{aligned}$$

for x from $({\mathcal {F}}, {\mathcal {S}}, Z \cup Z')$. There are two cases:

• For any $i = 1, \ldots , n$, $r_i \in \{\sigma \} \cup {\mathcal {S}}\cup Z$. Hence, d is also a derivation schema for x from $({\mathcal {F}}, {\mathcal {S}}, Z)$. Thus, $x \in \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z))$, and from (1), $x \in \mathtt {Concs}({\mathcal {E}})$.

• Assume that there exists $1 < i \le n$ such that $r_i \in Z'$ (note that the two theories $({\mathcal {F}}, {\mathcal {S}}, Z)$ and $({\mathcal {F}}, {\mathcal {S}}, Z \cup Z')$ differ only on $Z'$). Let i be the first step where an element of $Z'$ is used in the derivation d. Since the bodies of defeasible rules are not empty, $i > 1$. It follows that for any $j < i$, $r_i \in \{\sigma \} \cup {\mathcal {S}}\cup Z$, thus $\langle (x_1,r_1), \ldots , (x_j, r_j)\rangle$ is a derivation schema of $x_j$ from $({\mathcal {F}}, {\mathcal {S}}, Z)$. Thus, $x_j \in \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z))$. Furthermore, by Definition 6, $\mathtt {Body}(r_i) \subseteq \{x_1, \ldots , x_{i-1}\}$. Then, $\mathtt {Body}(r_i) \subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, Z))$. This contradicts the fact that $r_i \in Z'$ and thus such $r_i$ does not exist.

$\square$

Proof of Theorem 5

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent. Assume that for all ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$, ${\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq {\mathcal {E}}$. Assume now that $\exists a \in {\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ and $\exists b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $(b,b) \notin {\mathcal {R}}$ (cf. Proposition 4). Thus, $\exists {\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ such that $b \in {\mathcal {E}}$. Consequently, $a, b \in {\mathcal {E}}$, this contradicts the fact that ${\mathcal {E}}$ is conflict-free (since it is a naive extension).

Assume now that for all $a \in {\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$, $\not \exists b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. This means that arguments of ${\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ are not attacked. Thus, they belong to every naive extension. $\square$

Proof of Theorem 6

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent. Assume that $\exists a, b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $a \in {\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ and $\mathtt {Conc}(a) = \lnot \mathtt {Conc}(b)$. Thus, $(b,b) \notin {\mathcal {R}}$ and $\exists {\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ such that $b \in {\mathcal {E}}$. If ${\mathcal {H}}$ satisfies strict precedence, then $\mathtt {Conc}(a) \in \mathtt {Concs}({\mathcal {E}})$ meaning that $\mathtt {Concs}({\mathcal {E}})$ is inconsistent. Thus, ${\mathcal {H}}$ violates consistency. If ${\mathcal {H}}$ satisfies consistency, then $\mathtt {Conc}(a) \notin \mathtt {Concs}({\mathcal {E}})$ meaning that ${\mathcal {H}}$ violates strict precedence. $\square$

Proof of Theorem 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments. Let ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_n({\mathcal {H}})$ such that $\mathtt {Concs}({\mathcal {E}}') \subseteq \mathtt {Concs}({\mathcal {E}})$.

Assume that $\exists a = (d,x) \in {\mathcal {E}}{\setminus }{\mathcal {E}}'$. Thus, $\exists b = (d',x') \in {\mathcal {E}}'$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. But ${\mathcal {H}}$ is closed under sub-arguments. Thus, Proposition 12 gives $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ and $\mathtt {Concs}({\mathcal {E}}') = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}'))$. Besides, $\mathtt {Seq}(d) \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}'))$ using Propositions 12 and 14. Since $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}')) \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Thus, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ is inconsistent. This contradicts the fact that ${\mathcal {H}}$ satisfies consistency.

The same reasoning holds for $a = (d',x') \in {\mathcal {E}}'{\setminus }{\mathcal {E}}$. $\square$

Proof of Theorem 8

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments. Let ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$.

From Proposition 6, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ is consistent. Thus, $\exists {\mathcal {O}}\in \mathtt {Opt}({\mathcal {T}})$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$. From Property 4, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) \subseteq \mathtt {CN}({\mathcal {O}})$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {Concs}({\mathcal {E}})$ by Proposition 12. Thus, $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}})$. Assume now that $\exists x \in \mathtt {CN}({\mathcal {O}}){\setminus }\mathtt {Concs}({\mathcal {E}})$. Then, there exists a minimal derivation d for x from ${\mathcal {O}}$. From Property 3, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {O}})$. Since $\mathtt {CN}({\mathcal {O}})$ is consistent, (d, x) is an argument. In addition $(d,x) \notin {\mathcal {E}}$. Then, $\exists (d',x') \in {\mathcal {E}}$ such that $(d,x) {\mathcal {R}}(d',x')$ or $(d',x') {\mathcal {R}}(d,x)$. Since ${\mathcal {R}}$ is conflict-dependent, then $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. But, $\mathtt {Seq}(d') \subseteq \mathtt {Concs}({\mathcal {E}})$. So, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {O}})$. This contradicts the fact that ${\mathcal {O}}$ is an option. So, $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {Concs}({\mathcal {E}})$.

Since both $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}})$ and $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {Concs}({\mathcal {E}})$ have now been proved, the required $\mathtt {CN}({\mathcal {O}}) = \mathtt {Concs}({\mathcal {E}})$ follows.

Let us now show that ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. Assume that $\exists {\mathcal {O}}' \in \mathtt {Opt}({\mathcal {T}})$ such that $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. Thus, $\exists x \in \mathtt {CN}({\mathcal {O}}')$ and $x \notin \mathtt {CN}({\mathcal {O}})$. Thus, there exists a minimal derivation d for x from ${\mathcal {O}}'$. Since $\mathtt {CN}({\mathcal {O}}')$ is consistent and $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {O}}')$ (from Property 3), (d, x) is an argument. In addition $(d,x) \notin {\mathcal {E}}$ (since $x \notin \mathtt {CN}({\mathcal {O}})$). Then, $\exists (d',x') \in {\mathcal {E}}$ such that $(d,x) {\mathcal {R}}(d',x')$ or $(d',x') {\mathcal {R}}(d,x)$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. But, $\mathtt {Seq}(d') \subseteq \mathtt {Concs}({\mathcal {E}})$. So, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {O}}')$. This contradicts the fact that ${\mathcal {O}}'$ is an option.

From Proposition 1, it follows that for all ${\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$, if $\mathtt {CN}({\mathcal {O}}) = \mathtt {CN}({\mathcal {O}}') = \mathtt {Concs}({\mathcal {E}})$, then ${\mathcal {O}}= {\mathcal {O}}'$. $\square$

Proof of Theorem 9

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments.

• Let ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_n({\mathcal {H}})$. From Theorem 8, $\exists {\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$ and $\mathtt {Concs}({\mathcal {E}}') = \mathtt {CN}({\mathcal {O}}')$. If ${\mathcal {O}}= {\mathcal {O}}'$, then $\mathtt {Concs}({\mathcal {E}}) = \mathtt {Concs}({\mathcal {E}}')$. From Theorem 7, ${\mathcal {E}}= {\mathcal {E}}'$.

• Let ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ and ${\mathcal {O}}= \mathtt {Option}({\mathcal {E}})$. Thus, $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$. From Proposition 3, $\mathtt {Arg}(\mathtt {Th}({\mathcal {E}})) \subseteq \mathtt {Arg}({\mathcal {O}})$. From Proposition 14, $\mathtt {Arg}(\mathtt {Th}({\mathcal {E}})) = {\mathcal {E}}$. Thus, ${\mathcal {E}}\subseteq \mathtt {Arg}({\mathcal {O}})$. Assume now that $\exists a = (d,x) \in \mathtt {Arg}({\mathcal {O}})$ and $a \notin {\mathcal {E}}$. Thus, $\exists b = (d',x') \in {\mathcal {E}}$ and $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. Besides, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {O}})$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {CN}({\mathcal {O}})$. Thus, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {O}})$. This contradicts the fact that ${\mathcal {O}}$ is an option.

$\square$

Proof of Theorem 10

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments.

• Let ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. Thus, $\mathtt {CN}({\mathcal {O}})$ is consistent. From Proposition 5, since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Arg}({\mathcal {O}})$ is conflict-free. Assume now that $\mathtt {Arg}({\mathcal {O}}) \notin \mathtt {Ext}_n({\mathcal {H}})$. Thus, $\exists a = (d,x) \in \mathtt {Arg}({\mathcal {T}})$ such that $a \notin \mathtt {Arg}({\mathcal {O}})$ and $\mathtt {Arg}({\mathcal {O}}) \cup \{a\}$ is conflict-free. Consequently, $\exists {\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ such that $\mathtt {Arg}({\mathcal {O}}) \cup \{a\} \subseteq {\mathcal {E}}$. It follows that $\mathtt {Concs}(\mathtt {Arg}({\mathcal {O}}) \cup \{a\}) \subseteq \mathtt {Concs}({\mathcal {E}})$. Since $\mathtt {CN}({\mathcal {O}})$ is consistent, $\mathtt {Concs}(\mathtt {Arg}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}})$. Thus, $\mathtt {CN}({\mathcal {O}}) \cup \{x\} \subseteq \mathtt {Concs}({\mathcal {E}})$. From Theorem 8, $\exists {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}}')$. Then, $\mathtt {CN}({\mathcal {O}}) \cup \{x\} \subseteq \mathtt {CN}({\mathcal {O}}')$. This contradicts the fact that ${\mathcal {O}}$ is a maximal option.

• Let ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. By definition of $\mathtt {Th}$, $\mathtt {Th}(\mathtt {Arg}({\mathcal {O}})) \sqsubseteq {\mathcal {O}}$. From Property 4, $\mathtt {CN}(\mathtt {Th}(\mathtt {Arg}({\mathcal {O}}))) \subseteq \mathtt {CN}({\mathcal {O}})$. Besides, from first item, $\mathtt {Arg}({\mathcal {O}}) \in \mathtt {Ext}_n({\mathcal {H}})$. From Theorem 8, $\exists {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Th}(\mathtt {Arg}({\mathcal {O}})) \sqsubseteq {\mathcal {O}}'$ and $\mathtt {Concs}(\mathtt {Arg}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}}')$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}(\mathtt {Arg}({\mathcal {O}}))) = \mathtt {Concs}(\mathtt {Arg}({\mathcal {O}}))$. Consequently, $\mathtt {CN}({\mathcal {O}}') \subseteq \mathtt {CN}({\mathcal {O}})$. From Proposition 1, ${\mathcal {O}}= {\mathcal {O}}'$.

• Let ${\mathcal {O}}, {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. Assume that $\mathtt {Arg}({\mathcal {O}}) = \mathtt {Arg}({\mathcal {O}}')$.

  It follows that $\mathtt {Option}(\mathtt {Arg}({\mathcal {O}})) = \mathtt {Option}(\mathtt {Arg}({\mathcal {O}}'))$. From item 2, it follows that ${\mathcal {O}}= {\mathcal {O}}'$.

$\square$

Proof of Theorem 11

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both strict rules and sub-arguments.

Let us show that $\mathtt {Max}(\mathtt {Opt}({\mathcal {T}})) \subseteq \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. Let ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. From (item 1) of Theorem 10, ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_n({\mathcal {H}})$. From Theorem 8, $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}(\mathtt {Option}({\mathtt {Arg}}({\mathcal {O}})))$. From Corollary 1, $\mathtt {Option}({\mathtt {Arg}}({\mathcal {O}})) = {\mathcal {O}}$. Hence, $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}})$. From Theorem 4, there exists ${\mathcal {O}}' = ({\mathcal {F}}, {\mathcal {S}}, Z)$ such that

$$\begin{aligned} Z = \left( \bigcup _{(d,x) \in {\mathtt {Arg}}({\mathcal {O}})} \mathtt {Def}(d) \right) \cup \left\{ r \ | \ r \in {\mathcal {D}} \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}\left( \mathtt {Th}\left( {\mathtt {Arg}}({\mathcal {O}})\right) \right) \right\} \end{aligned}$$

and $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}}')$. Since $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}})$ and using Proposition 12, $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}(\mathtt {Th}({\mathtt {Arg}}({\mathcal {O}})))$, then $\mathtt {CN}(\mathtt {Th}({\mathtt {Arg}}({\mathcal {O}}))) = \mathtt {CN}({\mathcal {O}})$ and we get

$$\begin{aligned} Z = \left( \bigcup _{(d,x) \in {\mathtt {Arg}}({\mathcal {O}})} \mathtt {Def}(d) \right) \cup \left\{ r \ | \ r \in {\mathcal {D}} \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}({\mathcal {O}})\right\} \end{aligned}$$

and $\mathtt {CN}({\mathcal {O}}) = \mathtt {CN}({\mathcal {O}}')$. From Proposition 1, it follows that ${\mathcal {O}}= {\mathcal {O}}'$. Furthermore, ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ and is maximal (for set inclusion) up to consistency and contains the strict part of ${\mathcal {T}}$, then ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$.

Let us now show that $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}})) \subseteq \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. Let ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. By definition of preferred option, $\mathtt {CN}({\mathcal {O}})$ is consistent. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Arg}({\mathcal {O}})$ is conflict-free by Proposition 5. Assume now that $\mathtt {Arg}({\mathcal {O}}) \notin \mathtt {Ext}_n({\mathcal {H}})$. Thus, $\exists a \in \mathtt {Arg}({\mathcal {T}}){\setminus }\mathtt {Arg}({\mathcal {O}})$ such that ${\mathtt {Arg}}({\mathcal {O}}) \cup \{a\}$ is conflict-free. Consequently, $\exists {\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$ such that ${\mathtt {Arg}}({\mathcal {O}}) \cup \{a\} \subseteq {\mathcal {E}}$. Thus, $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}}) \cup \{a\}) \subseteq \mathtt {Concs}({\mathcal {E}})$. Since $\mathtt {CN}({\mathcal {O}})$ is consistent, $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}})$. Thus, $\mathtt {CN}({\mathcal {O}}) \cup \{\mathtt {Conc}(a)\} \subseteq \mathtt {Concs}({\mathcal {E}})$. From Theorem 8, $\exists {\mathcal {O}}' \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}}')$. Then, $\mathtt {CN}({\mathcal {O}}) \cup \{\mathtt {Conc}(a)\} \subseteq \mathtt {CN}({\mathcal {O}}')$. This means that ${\mathcal {O}}' \in \mathtt {POpt}({\mathcal {T}})$ (since it contains all consequences of the strict part of ${\mathcal {T}}$). This contradicts the fact that ${\mathcal {O}}$ is a maximal preferred option. Consequently, ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_n({\mathcal {H}})$. From Theorem 8, ${\mathcal {O}}\in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$. $\square$

Proof of Theorem 12

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments. From Property 11, $\mathtt {Output}({\mathcal {H}}) = \bigcap \limits _{{\mathcal {E}}_i \in \mathtt {Ext}_n({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i)$. From Theorem 8, for all ${\mathcal {E}}_i \in \mathtt {Ext}_n({\mathcal {H}})$, there exists a unique ${\mathcal {O}}_i \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}_i) = \mathtt {CN}({\mathcal {O}}_i)$. Also, Corollary 1 guarantees that $\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))$ does not have any additional elements that do not have a mapping in $\mathtt {Ext}_n({\mathcal {H}})$. Thus,

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap \limits _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))} \mathtt {CN}({\mathcal {O}}_i). \end{aligned}$$

$\square$

Lemma 2

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. For any ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$, it holds that $({\mathcal {F}}, {\mathcal {S}}, Z) \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ whenever

$$\begin{aligned} Z = \left( \bigcup _{(d,x) \in {\mathcal {E}}} \mathtt {Def}(d)\right) \cup \left\{ r \mid r \in {\mathcal {D}} \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))\right\} . \end{aligned}$$

Proof

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. Let ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$. Let ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, Z \cup Z')$ where $Z' = \{r \ | \ r \in {\mathcal {D}}{\setminus } Z \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))\}$. Clearly, $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$. From Theorem 4, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$. Since ${\mathcal {H}}$ satisfies consistency, then $\mathtt {Concs}({\mathcal {E}})$ is consistent, and thus, $\mathtt {CN}({\mathcal {O}})$ is consistent as well. Since $({\mathcal {F}}, {\mathcal {S}}, \emptyset ) \sqsubseteq {\mathcal {O}}$ and $\mathtt {CN}({\mathcal {O}})$ is consistent, from Property 7, $\exists {\mathcal {O}}' \in \mathtt {POpt}({\mathcal {T}})$ such that ${\mathcal {O}}\sqsubseteq {\mathcal {O}}'$. From Proposition 3, ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}})) \subseteq {\mathtt {Arg}}({\mathcal {O}}) \subseteq {\mathtt {Arg}}({\mathcal {O}}')$. From Proposition 9, ${\mathcal {E}}= {\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}))$. Hence, ${\mathcal {E}}\subseteq {\mathtt {Arg}}({\mathcal {O}}) \subseteq {\mathtt {Arg}}({\mathcal {O}}')$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {CN}({\mathcal {O}})$ and $\mathtt {CN}({\mathcal {O}}')$ are consistent, then from Proposition 5${\mathtt {Arg}}({\mathcal {O}})$ and ${\mathtt {Arg}}({\mathcal {O}}')$ are both conflict-free. From Property 1, ${\mathcal {E}}\in \mathtt {Ext}_n({\mathcal {H}})$. Then, ${\mathcal {E}}$ is maximal (for set inclusion) among conflict-free sets. Thus, ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}}) = {\mathtt {Arg}}({\mathcal {O}}')$. From consistency of $\mathtt {CN}({\mathcal {O}})$ and $\mathtt {CN}({\mathcal {O}}')$, it follows that $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}})) = \mathtt {CN}({\mathcal {O}})$ and $\mathtt {Concs}({\mathtt {Arg}}({\mathcal {O}}')) = \mathtt {CN}({\mathcal {O}}')$. Then, $\mathtt {CN}({\mathcal {O}}) = \mathtt {CN}({\mathcal {O}}')$ and ${\mathcal {O}}\in \mathtt {POpt}({\mathcal {T}})$.

Let us now show that ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. Assume that $\exists {\mathcal {O}}' \in \mathtt {POpt}({\mathcal {T}})$ such that $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. Since $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$, $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. Let $x \in \mathtt {CN}({\mathcal {O}}')$ and $x \notin \mathtt {Concs}({\mathcal {E}})$. Since $\mathtt {CN}({\mathcal {O}}')$ is consistent, there exists an argument $(d,x) \in {\mathtt {Arg}}({\mathcal {O}}')$, i.e., d is a derivation of x from ${\mathcal {O}}'$. Clearly, $(d,x) \notin {\mathcal {E}}$. Thus, $\exists (d',x') \in {\mathcal {E}}$ such that $(d', x') {\mathcal {R}}(d, x)$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. But, $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ and $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {O}}')$. Proposition 13 gives $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {Concs}({\mathcal {E}})$. Then, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) \subseteq \mathtt {CN}({\mathcal {O}}')$. Finally, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {O}}')$. This contradicts the fact that $\mathtt {CN}({\mathcal {O}}')$ is consistent. $\square$

Proof of Theorem 13

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency, exhaustiveness, strict precedence and closure under both strict rules and sub-arguments. Assume that $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$. Let ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$. From Lemma 2, the option ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, Z') \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ with $Z' = Z \cup \{r \mid r \in {\mathcal {D}}{\setminus } Z \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))\}$. Since $X \subseteq {\mathcal {F}}$, $Y \subseteq {\mathcal {S}}$ and $Z \subseteq Z'$, $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$. From Theorem 4, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$.

Let us show that ${\mathcal {E}}$ has a unique corresponding preferred maximal option. Assume that $\exists {\mathcal {O}}_1, {\mathcal {O}}_2 \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}_1$, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}}_1)$, $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}_2$ and $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}}_2)$. Obviously, $\mathtt {CN}({\mathcal {O}}_1) = \mathtt {CN}({\mathcal {O}}_2)$. However, ${\mathcal {O}}_1, {\mathcal {O}}_2 \in \mathtt {POpt}({\mathcal {T}})$ according to Property 6 hence Proposition 1 gives ${\mathcal {O}}_1 = {\mathcal {O}}_2$.

Let us now show that ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}})$. Since $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$, from Proposition 3, ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}})) \subseteq {\mathtt {Arg}}({\mathcal {O}})$. From Proposition 15, ${\mathcal {E}}\subseteq {\mathtt {Arg}}({\mathcal {O}})$. Assume now that $\exists a = (d,x) \in \mathtt {Arg}({\mathcal {O}})$ such that $a \notin {\mathcal {E}}$. Thus, $\exists b = (d',x') \in {\mathcal {E}}$ and $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. Besides, $\mathtt {Seq}(d) \subseteq \mathtt {CN}({\mathcal {O}})$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Since ${\mathcal {H}}$ is closed under sub-arguments, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}})) = \mathtt {CN}({\mathcal {O}})$ by Proposition 12. Thus, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}({\mathcal {O}})$. This contradicts the fact that ${\mathcal {O}}$ is an option. $\square$

Proof of Theorem 14

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies consistency, strict precedence and closure under both strict rules and sub-arguments. Assume that $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$. Let ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_s({\mathcal {H}})$. From Theorem 13, $\exists {\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$ and $\exists {\mathcal {O}}' \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}') = \mathtt {CN}({\mathcal {O}}')$. If ${\mathcal {O}}= {\mathcal {O}}'$, then $\mathtt {Concs}({\mathcal {E}}) = \mathtt {Concs}({\mathcal {E}}')$. Assume that $\exists a = (d,x) \in {\mathcal {E}}{\setminus }{\mathcal {E}}'$. Thus, $\exists b = (d',x') \in {\mathcal {E}}'$ such that $b {\mathcal {R}}a$. Since ${\mathcal {R}}$ is conflict-dependent, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d')$ is inconsistent. But ${\mathcal {H}}$ is closed under sub-arguments. Thus, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ and $\mathtt {Concs}({\mathcal {E}}') = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}'))$. Besides, $\mathtt {Seq}(d) \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ and $\mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}'))$. Since $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}')) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$, $\mathtt {Seq}(d) \cup \mathtt {Seq}(d') \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$. Thus, $\mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ is inconsistent. This contradicts the fact that ${\mathcal {H}}$ satisfies consistency. The same reasoning holds for $a = (d',x') \in {\mathcal {E}}'{\setminus }{\mathcal {E}}$. $\square$

Proof of Theorem 15

Any argumentation system ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ that satisfies strict precedence should have ${\mathcal {F}}$ as plausible conclusions, i.e., ${\mathcal {F}}\subseteq \mathtt {CN}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq \mathtt {Output}({\mathcal {H}})$. Since $\top \in {\mathcal {F}}$, then $\mathtt {Output}({\mathcal {H}})\ne \emptyset$. However, since ${\mathcal {R}}\in \mathfrak {R}_{s_1}$, $\mathtt {Ext}_s({\mathcal {H}})= \emptyset$. Thus, $\mathtt {Output}({\mathcal {H}})= \emptyset$. $\square$

Proof of Theorem 16

Let ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$. Let ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. Since $|\mathtt {Ext}_s({\mathcal {H}})| = |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$, from Theorems 13 and 14, $\exists {\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$ such that ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}})$, hence ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_s({\mathcal {H}})$. $\square$

Proof of Theorem 17

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s2}$. From Corollary 5, $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})$. Assume that $\exists {\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}}){\setminus }\mathtt {Ext}_s({\mathcal {H}})$. From Theorem 22, there exists ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$. Since $|\mathtt {Ext}_s({\mathcal {H}})| = |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$, from Theorem 16, ${\mathtt {Arg}}({\mathcal {O}}) \in \mathtt {Ext}_s({\mathcal {H}})$. From Theorems 13 and 14, ${\mathcal {O}}= \mathtt {Option}({\mathtt {Arg}}({\mathcal {O}}))$. From Theorem 24, ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}})$. $\square$

Proof of Theorem 18

Let ${\mathcal {H}}= (\mathtt {Arg}({\mathcal {T}})$, ${\mathcal {R}})$ be an argumentation system such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$. If ${\mathcal {H}}$ satisfies all the postulates under naive semantics, then from Corollary 1 and Theorem 11, there is a bijection between $\mathtt {Ext}_n({\mathcal {H}})$ and $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. From Theorems 13 and 16, $|\mathtt {Ext}_s({\mathcal {H}})| = |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$. Since every stable extension is a naive one, $\mathtt {Ext}_n({\mathcal {H}})= \mathtt {Ext}_s({\mathcal {H}})$. $\square$

Proof of Theorem 19

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_2}$. From Property 11,

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_s({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i). \end{aligned}$$

From Theorems 13 and 14, for all ${\mathcal {E}}_i \in \mathtt {Ext}_s({\mathcal {H}})$, there exists a unique ${\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}_i) = \mathtt {CN}({\mathcal {O}}_i)$. Thus,

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))} \mathtt {CN}({\mathcal {O}}_i). \end{aligned}$$

$\square$

Proof of Theorem 20

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{s_3}$. From Property 11,

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_s({\mathcal {H}})} \mathtt {Concs}({\mathcal {E}}_i). \end{aligned}$$

From Theorem 13, for all ${\mathcal {E}}_i \in \mathtt {Ext}_s({\mathcal {H}})$, there exists a unique ${\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Concs}({\mathcal {E}}_i) = \mathtt {CN}({\mathcal {O}}_i)$. Since ${\mathcal {R}}\in \mathfrak {R}_{s_3}$, $|\mathtt {Ext}_s({\mathcal {H}})| < |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$. Thus,

$$\begin{aligned} \mathtt {Output}({\mathcal {H}})= \bigcap _{{\mathcal {O}}_i \in {\mathcal {X}}} \mathtt {CN}({\mathcal {O}}_i) \end{aligned}$$

with ${\mathcal {X}}= \{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}})) \mid {\mathcal {E}}_i = {\mathtt {Arg}}({\mathcal {O}}_i) \in \mathtt {Ext}_s({\mathcal {H}})\}$. $\square$

Proof of Theorem 21

Let ${\mathcal {H}}$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {H}}$ satisfies the strict precedence postulate, i.e., ${\mathcal {F}}\subseteq \mathtt {Output}({\mathcal {H}})$. Since $\top \in {\mathcal {F}}$, $\mathtt {Output}({\mathcal {H}})\ne \emptyset$. Hence, $\mathtt {Ext}_p({\mathcal {H}})\ne \{\emptyset \}$. $\square$

Proof of Theorem 22

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}),{\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. Let ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$ and $\mathtt {Th}({\mathcal {E}}) = (X, Y, Z)$. From Theorem 4, $\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}({\mathcal {O}})$ where ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, Z \cup Z')$ and $Z' \subseteq {\mathcal {D}}{\setminus } Z$. Clearly $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$. From consistency, $\mathtt {Concs}({\mathcal {E}})$ is consistent. Then, $\mathtt {CN}({\mathcal {O}})$ is consistent as well. Then, there exists ${\mathcal {O}}' \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that ${\mathcal {O}}\sqsubseteq {\mathcal {O}}'$. Therefore, $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. Thus, $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. $\square$

Proof of Theorem 23

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates under preferred semantics. Since $\mathtt {Ext}_s({\mathcal {H}})\subseteq \mathtt {Ext}_p({\mathcal {H}})$, ${\mathcal {H}}$ satisfies the postulates under stable semantics. Consequently, from Theorem 15, $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$. Let ${\mathcal {E}}\in \mathtt {Ext}_s({\mathcal {H}})$. From Theorem 13, $\exists {\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that ${\mathcal {E}}= {\mathtt {Arg}}({\mathcal {O}})$. $\square$

Proof of Theorem 24

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies exhaustiveness and closure under sub-arguments. Let ${\mathcal {E}}, {\mathcal {E}}' \in \mathtt {Ext}_p({\mathcal {H}})$ and ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Th}({\mathcal {E}}') \sqsubseteq {\mathcal {O}}$. We show that ${\mathcal {E}}\cup {\mathcal {E}}'$ is a preferred extension (which contradicts the fact that ${\mathcal {E}}$ and ${\mathcal {E}}'$ are preferred extensions).

From Proposition 3, ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}})) \subseteq {\mathtt {Arg}}({\mathcal {O}})$ and ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}')) \subseteq {\mathtt {Arg}}({\mathcal {O}})$. Since ${\mathcal {H}}$ satisfies exhaustiveness and closure under sub-arguments, from Proposition 9, ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}})) = {\mathcal {E}}$ and ${\mathtt {Arg}}(\mathtt {Th}({\mathcal {E}}')) = {\mathcal {E}}'$. Thus, ${\mathcal {E}}\cup {\mathcal {E}}' \subseteq {\mathtt {Arg}}({\mathcal {O}})$. Since $\mathtt {CN}({\mathcal {O}})$ is consistent and ${\mathcal {R}}$ is conflict-dependent, from Proposition 5${\mathtt {Arg}}({\mathcal {O}})$ is conflict-free. Consequently, ${\mathcal {E}}\cup {\mathcal {E}}'$ is also conflict-free. Moreover, ${\mathcal {E}}\cup {\mathcal {E}}'$ defends its elements since ${\mathcal {E}}$ and ${\mathcal {E}}'$ are preferred extensions. Thus, ${\mathcal {E}}\cup {\mathcal {E}}'$ is an admissible set. Due to ${\mathcal {E}}$ and ${\mathcal {E}}'$ being preferred extensions, it follows that ${\mathcal {E}}\cup {\mathcal {E}}' = {\mathcal {E}}= {\mathcal {E}}'$. $\square$

Proof of Theorem 25

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$ such that ${\mathcal {R}}$ is conflict-dependent and privileges strict arguments, and ${\mathcal {H}}$ satisfies consistency, exhaustiveness, strict precedence and closure under sub-arguments. From consistency and strict precedence, it follows by Proposition 8 that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ is consistent.

The conclusion of the theorem, i.e., ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})) \subseteq \bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_p({\mathcal {H}})} {\mathcal {E}}_i$, is trivial in the case that ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is empty. Consider $a \in {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$. Let ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$.

Let us show that ${\mathcal {E}}\cup \{a\}$ is conflict-free. Assume that $\exists b = (d_2,x_2) \in {\mathcal {E}}$ such that $a {\mathcal {R}}b$ or $b {\mathcal {R}}a$. From Lemma 1, there exists $a' \in \mathtt {Sub}(a)$ such that $a' = (d'_1,x'_1) \in {\mathtt {Arg}}(({\mathcal {F}},{\mathcal {S}},\emptyset ))$ and $a' {\mathcal {R}}b$. Then, $\mathtt {Seq}(d'_1) \cup \mathtt {Seq}(d_2)$ is inconsistent. Since ${\mathcal {H}}$ satisfies strict precedence and exhaustiveness, ${\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq {\mathcal {E}}$ by Proposition 10, so $a' \in {\mathcal {E}}$. Consequently, $\mathtt {Seq}(d'_1) \cup \mathtt {Seq}(d_2) \subseteq \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ by Proposition 12. Since ${\mathcal {H}}$ satisfies consistency and closure under sub-arguments, by Proposition 6$\mathtt {Concs}({\mathcal {E}}) = \mathtt {CN}(\mathtt {Th}({\mathcal {E}}))$ is consistent. Contradiction.

Let us show that ${\mathcal {E}}$ defends a. Consider $b \in {\mathtt {Arg}}({\mathcal {T}})$ such that $b {\mathcal {R}}a$. From Lemma 1, there exists $a' \in \mathtt {Sub}(a)$ such that $a' \in {\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset ))$ and $a' {\mathcal {R}}b$. Since ${\mathcal {H}}$ satisfies strict precedence and exhaustiveness, ${\mathtt {Arg}}(({\mathcal {F}}, {\mathcal {S}}, \emptyset )) \subseteq {\mathcal {E}}$, thus $a' \in {\mathcal {E}}$.

Summing up, ${\mathcal {E}}\cup \{a\}$ is an admissible set. However, ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$ means that ${\mathcal {E}}$ is a maximal admissible set; hence, ${\mathcal {E}}\cup \{a\} \subseteq {\mathcal {E}}$. Therefore, $a \in {\mathcal {E}}$. $\square$

Proof of Theorem 26

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be a system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. From Theorem 22, for all ${\mathcal {E}}\in \mathtt {Ext}_p({\mathcal {H}})$, $\exists {\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Concs}({\mathcal {E}}) \subseteq \mathtt {CN}({\mathcal {O}})$. From Theorem 24, there cannot exist two maximal preferred extensions ${\mathcal {E}}$ and ${\mathcal {E}}'$ such that $\mathtt {Th}({\mathcal {E}}) \sqsubseteq {\mathcal {O}}$ and $\mathtt {Th}({\mathcal {E}}') \sqsubseteq {\mathcal {O}}$ for some ${\mathcal {O}}\in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))$. Thus, every maximal preferred option is captured by at most one preferred extension. Then, $|\mathtt {Ext}_p({\mathcal {H}})| \le |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$. $\square$

Proof of Theorem 27

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}= ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}})$. Assume that ${\mathcal {R}}\in \mathfrak {R}_{p_2}$. The following equalities hold by Theorems 16 and 17: $\mathtt {Ext}_p({\mathcal {H}})= \mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})= \{{\mathtt {Arg}}({\mathcal {O}}_i) \ | \ {\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))\}.$ Let us now show the equality

$$\begin{aligned} \bigcap \limits _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))} {\mathtt {Arg}}({\mathcal {O}}_i) = {\mathtt {Arg}}(\bigcap \limits _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))} {\mathcal {O}}_i). \end{aligned}$$

Let $\mathtt {Max}(\mathtt {POpt}({\mathcal {T}})) = \{{\mathcal {O}}_1 = ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}_1), \ldots , {\mathcal {O}}_n = ({\mathcal {F}}, {\mathcal {S}}, {\mathcal {D}}_n)\}$. Assume that $(d,x) \in \bigcap \limits _{i = 1}^{n} {\mathtt {Arg}}({\mathcal {O}}_i)$. For any $i = 1, \ldots , n$, $(d,x) \in {\mathtt {Arg}}({\mathcal {O}}_i)$ and thus

$$\begin{aligned} (\mathtt {Facts}(d), \mathtt {Strict}(d), \mathtt {Def}(d)) \sqsubseteq {\mathcal {O}}_i. \end{aligned}$$

This means that $\mathtt {Def}(d) \subseteq \bigcap \nolimits _{i = 1}^{n} {\mathcal {D}}_i$. Consequently, d is also a derivation schema from $({\mathcal {F}}, {\mathcal {S}}, \bigcap \nolimits _{i = 1}^{n} {\mathcal {D}}_i) = \bigcap \nolimits _{i = 1}^{n} {\mathcal {O}}_i$. Finally, $(d,x) \in {\mathtt {Arg}}(\bigcap \nolimits _{i = 1}^{n} {\mathcal {O}}_i)$.

Assume now that $(d,x) \in {\mathtt {Arg}}(\bigcap \nolimits _{i = 1}^{n} {\mathcal {O}}_i)$. Then, d is a derivation schema from $({\mathcal {F}}, {\mathcal {S}}, \bigcap \nolimits _{i = 1}^{n} {\mathcal {D}}_i)$. Hence, $\mathtt {Def}(d) \subseteq \bigcap \nolimits _{i = 1}^{n} {\mathcal {D}}_i$. Hence, for any $i = 1, \ldots , n$, $\mathtt {Def}(d) \subseteq {\mathcal {D}}_i$. Thus, d is a derivation schema from each theory ${\mathcal {O}}_i$ and (d, x) is an argument in each ${\mathtt {Arg}}({\mathcal {O}}_i)$.

From above, it follows that

$$\begin{aligned} \bigcap _{{\mathcal {O}}_i \in \mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))} {\mathtt {Arg}}({\mathcal {O}}_i) = {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})). \end{aligned}$$

$\square$

Proof of Theorem 28

Let ${\mathcal {H}}$ be an argumentation system which satisfies the five postulates. From strict precedence and the fact that $\mathtt {Output}({\mathcal {H}})= \mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$, it holds that $\mathtt {CN}(({\mathcal {F}},{\mathcal {S}},\emptyset )) \subseteq \mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$. From Theorem 4, $\mathtt {Concs}(\mathtt {IE}({\mathcal {H}})) = \mathtt {CN}({\mathcal {O}})$ such that ${\mathcal {O}}= ({\mathcal {F}}, {\mathcal {S}}, Z)$ where

$$\begin{aligned} Z = \left( \bigcup _{(d,x) \in \mathtt {IE}({\mathcal {H}})} \mathtt {Def}(d)\right) \cup \left\{ r \mid r \in {\mathcal {D}} \text{ and } \mathtt {Body}(r) \not \subseteq \mathtt {CN}(\mathtt {Th}(\mathtt {IE}({\mathcal {H}})))\right\} . \end{aligned}$$

It holds that $\mathtt {Th}(\mathtt {IE}({\mathcal {H}})) \sqsubseteq {\mathcal {O}}$. From consistency postulate, it follows that $\mathtt {CN}({\mathcal {O}})$ is consistent (since $\mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$ is consistent). Thus, there exists ${\mathcal {O}}' \in \mathtt {POpt}({\mathcal {T}})$ such that ${\mathcal {O}}\sqsubseteq {\mathcal {O}}'$. From Property 4, $\mathtt {CN}({\mathcal {O}}) \subseteq \mathtt {CN}({\mathcal {O}}')$. Consequently, $\mathtt {Concs}(\mathtt {IE}({\mathcal {H}}))$$\subseteq$$\mathtt {CN}({\mathcal {O}}')$. $\square$

Proof of Theorem 29

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$. Assume that ${\mathcal {R}}\in \mathfrak {R}_{p_2}$ and privileges strict arguments. From Theorem 27, $\bigcap _{{\mathcal {E}}_i \in \mathtt {Ext}_p({\mathcal {H}})} {\mathcal {E}}_i = {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$. From Theorem 2, ${\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$ is an admissible extension of ${\mathcal {H}}$. Thus, $\mathtt {IE}({\mathcal {H}})= {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$. $\square$

Proof of Theorem 30

The proof is similar to that of Theorem 28. $\square$

Proof of Corollary 1

It follows directly from Theorems 8 and 10. $\square$

Proof of Corollary 2

It follows directly from Theorem 11 and Corollary 1. $\square$

Proof of Corollary 3

It follows from Corollary 1. $\square$

Proof of Corollary 4

It follows from Corollary 3, i.e., the equality $|\mathtt {Ext}_n({\mathcal {H}})| = |\mathtt {Max}(\mathtt {Opt}({\mathcal {T}}))|$ and the fact that if a theory ${\mathcal {T}}$ is finite, then it has a finite number of options, thus of maximal options. $\square$

Proof of Corollary 5

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be such that ${\mathcal {R}}\in \mathfrak {R}_{s_2} \cup \mathfrak {R}_{s_3}$. From Theorem 15, $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$. From Property 1, $\mathtt {Ext}_s({\mathcal {H}})= \mathtt {Ext}_{ss}({\mathcal {H}})$. $\square$

Proof of Corollary 6

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. From Theorem 15, $\mathtt {Ext}_s({\mathcal {H}})\ne \emptyset$. From Theorem 13, $|\mathtt {Ext}_s({\mathcal {H}})| \le |\mathtt {Max}(\mathtt {POpt}({\mathcal {T}}))|$. $\square$

Proof of Corollary 7

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system built over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}$ is conflict-dependent and ${\mathcal {H}}$ satisfies the five postulates. If ${\mathcal {T}}$ is finite, then ${\mathcal {T}}$ has a finite number of maximal preferred options. From Corollary 6, ${\mathcal {H}}$ has a finite number of stable extensions. $\square$

Proof of Corollary 8

It follows immediately from Theorem 26. $\square$

Proof of Corollary 9

It follows immediately from Theorems 17, 13 and 16. $\square$

Proof of Corollary 10

Let ${\mathcal {H}}= ({\mathtt {Arg}}({\mathcal {T}}), {\mathcal {R}})$ be an argumentation system over a theory ${\mathcal {T}}$ such that ${\mathcal {R}}\in \mathfrak {R}_{p_2}$ and privileges strict arguments. From Theorem 29, $\mathtt {IE}({\mathcal {H}})= {\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}}))$. Then, $\mathtt {Output}({\mathcal {H}})= \mathtt {Concs}(\mathtt {IE}({\mathcal {H}})) = \mathtt {Concs}({\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})))$. Since $\mathtt {CN}(\mathtt {Free}({\mathcal {T}}))$ is consistent, $\mathtt {CN}(\mathtt {Free}({\mathcal {T}})) = \mathtt {Concs}({\mathtt {Arg}}(\mathtt {Free}({\mathcal {T}})))$. $\square$