Dealing with Generic Contrariness in Structured Argumentation

1 Introduction

Research on structured argumentation has witnessed an increasing interest in formalisms lying at an intermediate level of abstraction between specific argumentation systems and Dung's argumentation frameworks (AFs) [Dung, 1995]. Among these formalisms, a preminent role is played by ASPIC+, presented in [Prakken, 2010] "as a general abstract model of argumentation with structured arguments" and developed in [Modgil and Prakken, 2013]. ASPIC+ is an extension of ASPIC [Amgoud et al., 2006], able to satisfy the same rationality postulates [Caminada and Amgoud, 2007] while offering a more general account of structured argumentation. Indeed, in [Modgil and Prakken, 2013] ASPIC+ is shown to capture a variety of existing argumentation systems. A key aspect in this respect is the adoption of a generic, possibly asymmetric, relation of contrariness between formulas while ASPIC assumes standard negation, i.e. a binary and symmetric contrariness relation. While in [Prakken, 2010; Modgil and Prakken, 2013] it is mainly emphasized that generic contrariness is useful to encompass a larger variety of more specific literature proposals, it can be observed that this notion also opens the way to novel investigation directions, like the use of multivalued logics in the construction of Zhejiang University - Univ. of Luxembourg Hangzhou, China - Luxembourg baiseliao@zju.edu.cn arguments (see [Baroni et al., 2015] for an initial analysis on this issue). Consider for instance a logic encompassing three truth values, namely T, F, U, standing for true, false, and unknown (or, better, unknowable like in [Baroni et al., 2015]). In this context, an argument concluding that the truth value of a proposition P is F is not just in conflict with any argument concluding that the truth value of P is T, but also with any argument concluding that the truth value of P is U and so on.

As to the evaluation of argument acceptance, both ASPIC and ASPIC+ rely on AFs. The rationality postulates prescribe that the outcomes of this evaluation respect some closure and consistency properties when mapped back at the instantiated level. Both in ASPIC and in ASPIC+ postulate satisfaction is ensured on the basis of some well-formedness assumptions, including some closure properties of the set of strict rules. However, we show that the combination of a generic contrariness relation and rule closure may give rise to counterintuitive results. To solve this problem while preserving the generality of ASPIC+, we propose a modified version of the formalism based on two main standpoints:

• a notion of closure of the contrariness relation, involving sets of formulas rather than individual ones;
• an abstract representation for the evaluation of argument acceptance using sets of arguments and their conflicts.

On the technical side, the proposed formalism is shown to satisfy the rationality postulates of [Caminada and Amgoud, 2007], as a first and essential soundness requirement. On the conceptual side, being based on a non-binary notion of argument conflict and being oriented to making the actual roots of conflicts explicit, the formalism turns out to provide an alternative approach to the representation and management of articulated conflicts (like the tandem example in [Baroni et al., 2011]) also with standard negation. Further, since it shares several intuitions with the formalism of Abstract Argumentation Systems (AASs) [Vreeswijk, 1997], our proposal provides original formal tools enabling novel investigations about the relationships between AASs, AFs, and ASPIC+.

The paper is organized as follows. Section 2 provides the necessary background and Section 3 points out a problematic aspect of ASPIC+. Section 4 introduces the proposed modifications to the formalism and Section 5 deals with the satisfaction of the rationality postulates. Section 6 provides an example and, finally, Section 7 concludes the paper.

2 Background

The following definition gives the minimal elements of Dung's theory of AFs used in this paper. The reader is referred to [Dung, 1995; Baroni et al., 2011] for more details. We recall the definition of complete extension only since many literature semantics (grounded, stable, preferred, semistable, ideal) are complete-based (their extensions are a subset of the complete extensions) and the results proved in this paper directly carry over to any complete-based semantics.

Definition 1 An AF is a pair F = 〈A,→〉 where A is a set of arguments and→⊆ A×A describes their attack relation, so that (α, β) ∈→ (denoted α → β) indicates that α attacks β. For a set S ⊆ A, the attackers of S are defined as S- = {α ∈ A | ∃β ∈ S : α → β} and the attackees of S are defined as S+ = {α ∈ A | ∃β ∈ S : β → α}. A set S ⊆ A is conflict-free iff S ∩ S+ = ∅. S defends an argument α iff {α}- ⊆ S+. The set of arguments defended by S in F is denoted as DF(S). A set S is a complete extension of F, denoted S ∈ ECO(F), iff S is conflict-free and S = DF(S).

We recall in the sequel the essentials of the definition of the ASPIC+ argumentation system, omitting some details not required by the present paper.

Definition 2 An argumentation system is a tuple AS = (L,¯, R, n) where:

1. ¯ is a contrariness function from L to 2L such that: (i) ϕ is a contrary of ψ if ϕ ∈ ψ, ψ /∈ ϕ; (ii) ϕ is a contradictory of ψ (denoted by ϕ = -ψ) if ϕ ∈ ψ, ψ ∈ ϕ; (iii) each ϕ ∈ L has at least one contradictory
2. L is a logical language
3. R = RS ∪ RD is a set of strict (RS) and defeasible (RD) inference rules of the form ϕ1, . . . , ϕn → ϕ and ϕ1, . . . , ϕn ⇒ ϕ respectively (where ϕi, ϕ are metavariables ranging over wff in L), and RS ∩ RD = ∅

A knowledge base is a subset of L including certain (called axioms) and defeasible (called ordinary) premises. It gives rise to the notion of argumentation theory.

1. n : RD → L is a naming convention for RD.

Definition 3 A knowledge base in an argumentation system AS = (L,¯,R, n) is a set K ⊆ L consisting of two disjoint subsets Kn (the axioms) and Kp (the ordinary premises). The tuple AT = (AS, K) is called an argumentation theory.

Two notions of consistency are considered in ASPIC+.

Definition 4 For any S ⊆ L, let the closure of S under strict rules, denoted ClRS (S), be the smallest set containing S and the consequent of any strict rule in RS, whose antecedents are in ClRS (S). Then a set S ⊆ L is: (i) directly consistent iff ∄ϕ, ψ ∈ S such that ϕ ∈ ψ; (ii) indirectly consistent iff ClRS (S) is directly consistent.

Arguments are built from a knowledge base using rules.

Definition 5 An argument a on the basis of a knowledge base K in an argumentation system (L,¯, R, n) is:

1. ϕ if ϕ ∈ K with: Prem(a) = {ϕ}; Conc(a) = ϕ; Sub(a) = {ϕ}; Rules(a) = ∅; T op(a) = undefined.
2. a1, . . . an → (⇒) ψ if a1, . . . an are arguments such that there exists a strict (defeasible) rule Conc(a1), . . .Conc(an) → (⇒) ψ in RS (RD) with: Prem(a) = Prem(a1) ∪ . . . ∪ Prem(an); Conc(a) = ψ; Sub(a) = Sub(a1) ∪ . . . ∪ Sub(an) ∪ {a}; Rules(a) = Rules(a1) ∪ . . . ∪ Rules(an) ∪ {Conc(a1), . . . ,Conc(an) → (⇒) ψ}; Top(a) = Conc(a1), . . . , Conc(an) → (⇒) ψ; DefRules(a) = {r | r ∈ Rules(a) ∩ RD}; StRules(a) = {r | r ∈ Rules(a) ∩ RS}.

For any argument a, Premn(a) = Prem(a) ∩ Kn; Premp(a) = Prem(a) ∩Kp. a is: strict if DefRules(a) = ∅, defeasible if DefRules(a) ̸= ∅; firm if Prem(a) ⊆ Kn; plausible if Prem(a) ⊈ Kn; fallible if a is plausible or defeasible; finite if Rules(a) is finite.

We assume, as in [Modgil and Prakken, 2013], that the set Prem(a) of premises of an argument a is always finite. An argument may include both fallible (ordinary premises and defeasible rules) and infallible (axioms and strict rules) elements. The following definition is based on this distinction.

Definition 6 For any set of arguments {a1, . . . , an} the argument a is a strict continuation of {a1, . . . , an} iff Premp(a) = ⋃ni=1 Premp(ai); DefRules(a) = ⋃ni=1 DefRules(ai); StRules(a) ⊇ ⋃ni=1 StRules(ai); P remn(a) ⊇ ⋃ni=1 P remn(ai).

Some further notations are worth introducing.

• Notation 1 1. Given S ⊆ L, S ⊢ ϕ denotes that there exists a strict argument a such that Conc(a) = ϕ, with P rem(a) ⊆ S.
• S ⊢min ϕ denotes that S ⊢ ϕ and ∄T ⊊ S : T ⊢ ϕ.
• Given a set of arguments Σ, Prem(Σ) ≜ ⋃a∈Σ Prem(a), and similarly for Conc(Σ), Sub(Σ), Rules(Σ), Top(Σ), DefRules(Σ), StRules(Σ).

The notion of c-consistency is based on contradiction.

Definition 7 A set S ⊆ L is c-consistent if for no ϕ it holds that S ⊢ ϕ,-ϕ. Otherwise S is c-inconsistent. S is minimally c-inconsistent iff S is c-inconsistent and ∀S′ ⊊ S, S′ is c-consistent. An argument a on the basis of a knowledge-base K in an argumentation system (L,¯,R, n) is c-consistent iff Prem(a) is c-consistent.

Accordingly, several properties for an argumentation theory can be formulated.

Definition 8 Let AT = (AS,K) be an argumentation theory, where AS = (L,¯, R, n). AT is:

1. closed under contraposition iff for all S ⊆ L, ψ ∈ S, ϕ ∈ L, if S ⊢ ϕ then S \ {ψ} ∪ {-ϕ} ⊢ -ψ;
2. closed under transposition iff if ϕ1, . . . , ϕn → ψ ∈ RS then, for i = 1 . . . n, ϕ1, . . . , ϕi-1, -ψ, ϕi+1, . . . , ϕn → -ϕi ∈ RS;
3. axiom consistent iff ClRS (Kn) is directly consistent;
4. c-classical iff for any minimal c-inconsistent S ⊆ L and for any ϕ ∈ S, it holds that S \ {ϕ} ⊢ -ϕ;

1. well formed if whenever ϕ is a contrary of ψ then ψ /∈ Kn and ψ is not the consequent of a strict rule.

Three kinds of attack among arguments are considered.

Definition 9 An argument a attacks an argument b iff a undercuts, rebuts, or undermines b where:

• a undercuts b (on b′ ) iff Conc(a) ∈ n(r) for some b′ ∈ Sub(b) such that r = Top(b′ ) is defeasible.
• a rebuts b (on b′ ) iff Conc(a) ∈ ϕ for some b′ ∈ Sub(b) of the form b′′ 1 , . . . , b′′n ⇒ ϕ. In such a case a contraryrebuts b iff Conc(a) is a contrary of ϕ.
• a undermines b (on b′ ) iff Conc(a) ∈ ϕ for some b′ = ϕ, ϕ ∈ Premp(b). In such a case a contrary-undermines b iff Conc(a) is a contrary of ϕ.

Attack effectiveness, in some cases, depends on an ordering ⪯ among arguments, where a ⪯ b means that argument b is at least as preferred as a and, following [Prakken, 2010], we assume that ⪯ is a preorder. As usual a ≺ b iff a ⪯ b and b ⪯̸ a; a ≈ b iff a ⪯ b and b ⪯ a.

Definition 10 An argument ordering ⪯ is reasonable iff:

1. ∀a, b if a is strict and firm and b is plausible or defeasible, then b ≺ a;
2. ∀a, b if a is strict and firm then a ⊀ b;
3. ∀a, a′ , b with a′ a strict continuation of {a}, if a ⊀ b then a′ ⊀ b and if b ⊀ a then b ⊀ a′
4. let Θ = {a1, . . . , an} be a finite set of arguments and for i = 1 . . . n let a+\i be some strict continuation of Θ \ {ai}. Then, it is not the case that ∀i a+\i ≺ ai.

Effective attacks give rise to defeat.

Definition 11 Let a attack b on b′ . If a undercuts, contraryrebuts, or contrary-undermines b on b′ , then a preferenceindependent attacks b on b′ , otherwise a preferencedependent attacks b on b′ . Then, a defeats b iff for some b′ either a preference-independent attacks b on b′ or a preferencedependent attacks b on b′ and a ⊀ b′ . a strictly defeats b iff a defeats b and b does not defeat a.

Two kinds of structured argumentation frameworks are defined from an argumentation theory, using the attack relation.

Definition 12 Let AT = (AS,K) be an argumentation theory. A (c-)structured argumentation framework ((c)-SAF) defined by AT is a triple (Σ, C,⪯) where Σ is the set of all (c-consistent) finite arguments constructed from K in AS (henceforth called the set of arguments on the basis of AT), ⪯ is an ordering on Σ and (a, b) ∈ C iff a attacks b.

Well-definedness of (c-)structured argumentation frameworks depends on the properties of the underlying theory.

Definition 13 A SAF defined by an AT is well-defined iff AT is c-classical, axiom consistent, well formed and closed under contraposition or closed under transposition; A c-SAF defined by an AT is well-defined iff AT is axiom consistent, well formed and closed under contraposition or closed under transposition.

A traditional Dung's framework is derived from a (c)-SAF using the defeat relation.

Definition 14 Let ∆ = (Σ, C, ⪯) be a (c)-SAF , and D ⊆ Σ×Σ be the defeat relation according to Def. 11. The AF corresponding to ∆ is defined as F∆ = (Σ, D).

Compliance with rationality postulates is then proved in [Modgil and Prakken, 2013] under the assumptions above.

Theorem 1 Let ∆ = (Σ, C, ⪯) be a well-defined (c)-SAF with reasonable ⪯ and E a complete extension of F∆. Then

• {Conc(a) | a ∈ E} = ClRS ({Conc(a) | a ∈ E});
• ∀a ∈ E if a′ ∈ Sub(a) then a′ ∈ E;
• {Conc(a) | a ∈ E} is consistent;
• ClRS ({Conc(a) | a ∈ E}) is consistent.

3 A problem in ASPIC+ without negation

Def. 2 is liberal about the notion of contrariness and contradiction. In particular, it requires every ϕ ∈ L to have a contradictory (to ensure that the items of Def. 8 using - are well-founded) but leaves open the possibility of having more than one contradictory. However this may give rise to difficulties with the closure properties stated in Def. 8. To see this, consider a simple language L6 = {B, M, D, T, A, O} meant to intuitively correspond to the properties of being Bachelor, Married, Divorced, Teen-ager, Adult, and Old respectively, where the former three properties are mutually exclusive and so are the three latter ones, hence B = {M, D}, M = {B, D}, D = {B, M}, and T = {A, O}, A = {T, O}, O = {T, A}. Assume then that as a strict rule (e.g. imposed by law) a teenager is a bachelor, i.e. T→B ∈ RS.

A well-defined c-SAF does not require a c-classical AT , but arguments must be c-consistent, which, in this case, implies in particular that neither M nor D can be a premise. To put it in other words, the fact that a teen-ager must be bachelor prevents you to have as a premise that a person is married or divorced. Note that these observations do not affect the correctness of the results in [Modgil and Prakken, 2013], rather they show that multiple contradictories may give rise to a collapse of the expressiveness of the system: consistency is preserved at the price of very counterintuitive limitations.

Suppose now that closure under transposition is applied to this rule. We get -B → -T, however both -B and -T admit two replacements, namely M or D and A or O respectively. Hence a plain application of closure under transposition generates four strict rules: M → A, M → O, D → A, D → O. It follows that both {M} and {D} are c-inconsistent. Then a c-classical AT (required for a well-defined SAF) would impose ∅ ⊢ -M and ∅ ⊢ -D, leading to ∅ ⊢ B, D, M, i.e. contradictory conclusions should be strictly derived from the empty set. Given that AT must be axiom consistent, it follows that L6 with T → B ∈ RS is forbidden in a well-defined SAF .

One could fix this problem by requiring in Def. 8 every element of the language to have exactly one contradictory. Indeed the main example presented in [Modgil and Prakken, 2013] is coherent with this restriction. It may be noted however that this amounts to actually reintroduce negation within the language, though in disguise. While using negation (and possibly also disjunction) would be appropriate to this toy example, proposing it as the general solution to these difficulties would compromise the aim of ASPIC+ of being as language-independent as possible. Quoting [Prakken, 2010], "formulas like bachelor and married can, if desired, be declared contradictory without having to reason with an axiom ¬(bachelor ∧married)". For similar reasons, we do not consider other possible very specific technical fixes, like for instance forbidding that two contraries of a formula are in turn contrary each other. Thus, the goal of this paper is to devise an alternative solution to achieve the same desirable results obtained in [Modgil and Prakken, 2013] while keeping the underlying language as generic as possible, namely equipped only with a basic contrariness function.

4 Revising ASPIC+

We assume the same basic elements of ASPIC+ just removing any further specification and constraint on the contrariness function. Thus, in Def. 2 items 1, 3, and 4, are unmodified while in item 2 we drop (iii). Defs. 3, 4, 5, 6, as well as Notation 1 are also left unmodified.

We then leave apart c-consistency (Def. 7) and consider the properties of Def. 8, used to introduce well-definedness. To start, we keep only the properties of axiom consistency and well-formedness and focus on the closure requirements. Closure under transposition imposes a sort of explicit completeness of the set of strict rules, based on the - relation, while closure under contraposition imposes this completeness implicitly through the notion of strict derivation ⊢.

The use of - being problematic, (explicit or implicit) closure of strict rules cannot be defined. One can, however, pursue the complementary idea of establishing a closure of the contrariness relation on the basis of the strict rules, according to the fact that the contrariness relation captures some form of (directional) incompatibility. The relevant intuition is as follows. Let ϕ ∈ ψ and χ → ϕ ∈ RS. Since ϕ is incompatible with ψ and ϕ strictly follows from χ, one may require that χ too is regarded as (directionally) incompatible with ψ. Further, let ω → ψ ∈ RS. Since ϕ is incompatible with ψ and when ω holds also ψ necessarily holds, one may require ϕ to be incompatible with ω too. This needs two complements.

First, a strict rule may have multiple premises, e.g. in RS we may have η, θ → ϕ. Then, it is the set {η, θ} to be incompatible with ψ. Similarly, if κ, λ → ψ we get that ϕ is incompatible with {κ, λ}. These examples show that an extended contrariness relation involving sets of formulas is needed. Intuitively, this can be justified by the fact that negation is a collective notion (it includes whatever is incompatible with the negated entity): if it is removed, the underlying collections of elements have to be dealt with explicitly.

Second, strict derivation may involve several rules. Hence the previous considerations need to be generalized to the cases where we have ⊢ instead of → in the formulas above. More precisely, in order to ensure minimality in the identification of incompatibilities, ⊢min should be considered.

Accordingly, we introduce an extended contrariness relation between subsets of L obtained as a "completion" of the basic contrariness relation¯. A preliminary precisation is required. Taking into account Def. 5 and Notation 1, in an argumentation theory strict derivation must start from the knowledge base, i.e. S ⊢min ϕ implies S ⊆ K. However, we aim at defining a notion of closure that does not depend on the set of premises but only on the contrariness relation and the set of strict rules. To this purpose we need to define a notion of strict derivability, rather than of strict derivation, namely the possibility to derive a conclusion from some elements of the language using strict rules only, independently of the presence of these elements in the knowledge base.

Definition 15 Given an argumentation system AS = (L,¯, R, n) the strict knowledge base K∗AS for AS is given by Kn = L, Kp = ∅ and the corresponding argumentation theory is defined as AT ∗AS = (AS, K∗AS ). S ⊢∗ ϕ and S ⊢∗min ϕ denote respectively that S ⊢ ϕ and S ⊢min ϕ in AT ∗AS .

Note that from the finiteness of the set of premises of any argument, it follows that whenever S ⊢∗min ϕ, S is finite.

Definition 16 Given an argumentation system AS = (L,¯,R, n), let EC 1 (AS), EC 2 (AS),EC 3 (AS) be the following subsets of 2L × 2L

• EC 2 (AS) = {(S, {ψ}) | S ⊢∗min ϕ and ϕ ∈ ψ};
• EC 1 (AS) = {({ϕ}, {ψ}) | ϕ ∈ ψ};
• EC 3 (AS) = {(S, T) | T ⊢∗min ψ and (S, {ψ}) ∈ EC 1 (AS) ∪ EC 2 (AS)}.

The extended contrariness relation is defined as EC(AS) = EC 1 (AS) ∪ EC 2 (AS) ∪ EC 3 (AS) ⊆ 2L × 2L.

A set is EC-incompatible if it corresponds to the union of two contrary subsets according to EC(AS).

Definition 17 Given an AS = (L,¯,R, n), a set S ⊆ L is EC-incompatible, denoted as S ∈ ECI(AS), if there is some T, U such that S = T ∪ U and (T, U) ∈ EC(AS).

We can now revise accordingly the various forms of attack.

Definition 18 Given an argumentation theory AT = (AS,K), a set of arguments Σ attacks an argument b iff Σ undercuts, rebuts, or undermines b where:

• Σ undercuts b (on b′ ) iff Conc(Σ)∪{n(r)} ∈ ECI(AS) for some b′ ∈ Sub(b) such that r = Top(b′ ) ∈ RD.
• Σ undermines b (on b′ ) iff for some b′ = ϕ, ϕ ∈ Premp(b) the following condition holds: ∃T,U such that T ∪ U = Conc(Σ) ∪ {ϕ}, (T,U) ∈ EC(AS) and ϕ ∈ U. In this case Σ contrary undermines b if there is no V,W such that V ∪W = Conc(Σ) ∪ {ϕ}, (V,W) ∈ EC(AS) and ϕ ∈ V .
• Σ rebuts b (on b′ ) iff for some b′ ∈ Sub(b) of the form b′′ 1 , . . . , b′′n ⇒ ϕ the following condition holds: ∃T,U such that T ∪ U = Conc(Σ) ∪ {ϕ}, (T, U) ∈ EC(AS) and ϕ ∈ U. In this case Σ contrary rebuts b if there is no V,W such that V ∪W = Conc(Σ)∪{ϕ}, (V,W) ∈ EC(AS) and ϕ ∈ V .

As the effectiveness of some attacks depends on the preference relation, we need to generalize the notion of preference ordering to our extended context.

Definition 19 Given an argument ordering ⪯ on a set of arguments Σ, we extend ⪯ to 2Σ × Σ as follows. An argument a is at least as preferred as a set of arguments Θ, denoted as Θ ⪯ a iff ∃b ∈ Θ such that b ⪯ a. a is strictly preferred to Θ, denoted Θ ≺ a iff ∃b ∈ Θ such that b ≺ a, not strictly preferred to Θ, denoted Θ ⊀ a iff ∄b ∈ Θ such that b ≺ a.

Accordingly, we can define an extended notion of defeat.

Definition 20 Let the set of arguments Θ attack an argument b on b′ according to Def. 18. If Θ undercuts, contrary-rebuts, or contrary-undermines b on b′ , then Θ preference-independent attacks b on b′ , otherwise Θ preference-dependent attacks b on b′ . Then, Θ defeats b, denoted as Θ ⇝ b, iff either Θ preference-independent attacks b on b′ or Θ preference-dependent attacks b on b′ and Θ ⊀ b′ .

Lemmata 1 and 2 are used later (the proofs are omitted).

Lemma 1 If Θ is finite then ∃a ∈ Θ : (Θ \ {a}) ⊀ a.

Lemma 2 Given an argumentation theory AT = (AS, K), if Θ ⇝ a then Θ ⇝ b for every b such that a ∈ Sub(b).

We can now define an AF based on the above relation of defeat in order to evaluate the justification status of arguments. The idea is that the nodes of the framework represent relevant sets of arguments. In particular we need a node for each singleton corresponding to a produced argument, and a node for each set that defeats some produced argument.

Definition 21 Given an argumentation theory AT = (AS,K) with ordering ⪯, let ARGS(AT) be the set of the arguments produced in AS on the basis of K. The set of relevant sets of arguments of AT, denoted as RS(AT), is defined as RS(AT) = {{a} | a ∈ ARGS(AT)} ∪ {Θ | Θ ⊆ ARGS(AT ) and ∃b ∈ ARGS(AT ) : Θ ⇝ b}.

In the AF a relevant set of arguments attacks another one (denoted as D-attacks) simply if it defeats one of its members.

Definition 22 Let Σ,Θ ∈ RS(AT) for an argumentation theory AT. Σ D-attacks Θ, denoted as Σ ↠ Θ, iff ∃a ∈ Θ : Σ ⇝ a.

The relevant-set-based AF is defined accordingly.

Definition 23 Given an argumentation theory AT = (AS,K), the RS-based argumentation framework induced by AT is defined as RS-AF(AT) = (RS(AT),↠).

Notation 2 Each node of the induced RS-based argumentation framework RS-AF(AT) corresponds to a set Σ of arguments of AT. To make this more explicit, we write ‖Σ‖ to denote the node of RS-AF (AT ) corresponding to Σ. The set of (instantiated) arguments supported by an extension E of RS-AF (AT ) is defined as SA(E) = ⋃‖Σ‖∈E Σ.

5 Rationality properties

In this section we show that the revised version of ASPIC+ is well-behaved and satisfies the rationality postulates (some proofs are omitted due to space limitations). The following lemmata show that the acceptance of sets of arguments and of singletons in RS-AF(AT) are in accordance.

Lemma 3 Given an argumentation theory AT = (AS,K), let C ∈ ECO(RS-AF(AT)). If ‖Σ‖ ∈ C then ∀a ∈ Σ ‖{a}‖ ∈ C. If a ∈ SA(C) then ‖{a}‖ ∈ C.

Proof: Note that the second statement is a direct consequence of the first one, proved below. From Def. 21, if Σ ∈ RS(AT) then ∀a ∈ Σ, {a} ∈ RS(AT). Let ‖Σ‖ ∈ C and a ∈ Σ. C ∪ {‖{a}‖} is conflict-free. In fact, from Def. 22, for any Θ ∈ RS(AT), if Θ ↠ {a}, then Θ ↠ Σ, and ‖Θ‖ ∈ C would contradict the conflict-freeness of C. The case {a} ↠ Θ leads to Θ ↠ {a} since C defends itself and hence to the same contradiction. Analogously, we get ‖{a}‖- ⊆ ‖Σ‖- and since ‖Σ‖- ⊆ C+, also ‖{a}‖- ⊆ C+. Hence C defends ‖{a}‖ and, from the properties of complete extensions, it must be the case that ‖{a}‖ ∈ C. ✷

Lemma 4 Let AT = (AS,K), C ∈ ECO(RS-AF(AT)) and Σ ∈ RS(AT ). If ∀a ∈ Σ ‖{a}‖ ∈ C then ‖Σ‖ ∈ C.

The next lemma follows directly from the previous ones.

Lemma 5 Let AT = (AS,K), C ∈ ECO(RS-AF(AT)) and Σ,Θ, (Σ ∪ Θ) ∈ RS(AT). If ‖{Σ}‖, ‖{Θ}‖ ∈ C then ‖Σ ∪ Θ‖ ∈ C.

We now prove the properties established in Theorems 1215 of [Modgil and Prakken, 2013] and corresponding to the rationality postulates of [Caminada and Amgoud, 2007].

Theorem 2 Let AT = (AS,K), C ∈ ECO(RS-AF(AT)). If a ∈ SA(C) then ∀b ∈ Sub(a) b ∈ SA(C).

Proof: From Lemma 3 ‖{a}‖ ∈ C. We show that ∀b ∈ Sub(a) ‖{b}‖ ∈ C, implying b ∈ SA(C). From Lemma 2 and Defs. 21-22, if Θ ↠ {b} then Θ ↠ {a}. It follows that ‖{b}‖- ⊆ ‖{a}‖-. Since ‖{a}‖ ∈ C we get ‖{b}‖- ⊆ C+ and ‖{b}‖-∩C = ∅. Further, it cannot be that ‖{b}‖+∩C ̸= ∅ since, by the properties of complete extensions, this would contradict ‖{b}‖- ∩ C = ∅. Using again the properties of complete extensions we get ‖{b}‖ ∈ C. ✷

Theorem 3 Let AT = (AS,K), C ∈ ECO(RS-AF(AT)). Then {Conc(a) | a ∈ SA(C)} = ClRS ({Conc(a) | a ∈ SA(C)}).

Proof: Suppose by contradiction that ∃ϕ such that ϕ ∈ ClRS ({Conc(a) | a ∈ SA(C)}) and ϕ /∈ {Conc(a) | a ∈ SA(C)}. Since ϕ ∈ ClRS ({Conc(a) | a ∈ SA(C)}) there is an argument b with Conc(b) = ϕ such that b is a strict continuation of a set of arguments Σ ⊆ SA(C). Moreover from ϕ /∈ {Conc(a) | a ∈ SA(C)} we get b /∈ SA(C) and ‖{b}‖ /∈ C. From the properties of complete extensions, it follows ‖{b}‖- ̸= ∅. Given that b is a strict continuation of a set of arguments Σ, by Def. 18 it can only receive attacks through some of its subarguments belonging to Sub(Σ). Hence ‖{b}‖- = ⋃c∈Sub(Σ) ‖{c}‖-. From Σ ⊆ SA(C) and Theorem 2 we get Sub(Σ) ⊆ SA(C) and from Lemma 3 we get ∀c ∈ Sub(Σ) ‖{c}‖ ∈ C. From the properties of complete extensions and the equality ‖{b}‖- = ⋃c∈Sub(Σ) ‖{c}‖- it follows ‖{b}‖- ⊆ C+ and ‖{b}‖- ∩ C = ∅. Further, it cannot be that ‖{b}‖+ ∩ C ̸= ∅ since, by the properties of complete extensions, this would contradict ‖{b}‖- ∩C = ∅. It follows that it must be the case that ‖{b}‖ ∈ C. Contradiction. ✷

Theorem 4 Given AT = (AS,K) with argument ordering ⪯ satisfying item 1 of Def. 10, let C ∈ ECO(RS-AF(AT)). If AT is axiom consistent and well-formed then {Conc(a) | a ∈ SA(C)} is directly consistent.

Theorem 5 Given AT = (AS,K) with argument ordering ⪯ satisfying item 1 of Def. 10, let C ∈ ECO(RS-AF(AT)). If AT is axiom consistent and wellformed then ClRS ({Conc(a) | a ∈ SA(C)}) is directly consistent.

6 An example

Consider language L10 = L6 ∪ {HC, GC, FC, WR}, where intuitively HC means that the person we are talking about has a birth certificate dated 16 years ago, GC represents the default assumption that the certificate is genuine, FC means that the certificate is fake, and WR means that the person wears a wedding ring. The contrariness relation is as in Sect. 3 with the only addition of GC = {FC}, i.e. FC is a contrary of GC. Let RS = {T → B; HC, GC → T} and RD = {WR ⇒ M}. From RS we obtain {T} ⊢∗min B, {HC, GC} ⊢∗min T, {HC, GC} ⊢∗min B. Applying Def. 16 and omitting EC 1 (AS), we get EC 2 (AS) = {({T}, {M}), ({T}, {D}), ({HC, GC}, {A}), ({HC, GC}, {O}), ({HC, GC}, {M}), ({HC, GC}, {D})} and then EC 3 (AS) = {({M}, {T}), ({D}, {T}), ({A}, {HC, GC}), ({O}, {HC, GC}), ({M}, {HC, GC}), ({D}, {HC, GC})}.

From Def. 18 we have that both {a4} and {a5} rebut a6, {a1, a2} rebuts a6, and {a1, a6} undermines (and also rebuts) a2 and its superarguments a4 and a5. All these attacks are preference dependent. To keep the presentation simple we assume that all fallible arguments (i.e. a2, a4, a5, a6) are equally preferred and are less preferred than the firm arguments a1 and a3. Under this assumption, all the above attacks are successful and give rise to a defeat according to Def. 20, i.e., summing up, {a4} ⇝ a6, {a5} ⇝ a6, {a1, a2} ⇝ a6, {a1, a6} ⇝ a2, {a1, a6} ⇝ a4, {a1, a6} ⇝ a5. Then, by Def. 21, RS(AT) = {{a1}, {a2}, {a3}, {a4}, {a5}, {a6}, {a1, a2}, {a1, a6}} and the D-attack relation ↠ consists of the replication of the defeat relation described above (with the attacked arguments replaced by the corresponding singletons) with the addition of a mutual D-attack between {a1, a2} and {a1, a6} and of attacks from {a4} and {a5} to {a1, a6}.

Suppose now Kn = {HC, WR} (it is certain that the person has a birth certificate and wears a wedding ring) and Kp = {GC} (it is defeasibly assumed that the certificate is genuine). We get the following arguments: a1 = HC, a2 = GC, a3 = WR, a4 = [a1, a2 → T], a5 = [a4 → B], a6 = [a3 ⇒ M].

Figure 1 shows the resulting AF. Its complete extensions are C1 = {‖{a1}‖, ‖{a3}‖}, C2 = {‖{a1}‖, ‖{a3}‖, ‖{a6}‖, ‖{a1, a6}‖}, C3 = {‖{a1}‖, ‖{a2}‖, ‖{a3}‖, ‖{a4}‖, ‖{a5}‖, ‖{a1, a2}‖}. C1 is the grounded extension [Dung, 1995] supporting only the conclusions HC and WR. C2 and C3 correspond to the two alternative choices arising from the incompatibility between the fallible arguments a2 (the certificate is genuine) and a6 (the person is married) given that it is certain that s/he has a certicate asserting that s/he is a teenager and that there is no preference between the alternatives. Note that the structure of the AF evidences this mutual attack as the root of all the inconsistencies. In fact, the acceptance of all other arguments (apart the unattacked ones) basically depends on the choice between ‖{a1, a2}‖ and ‖{a1, a6}‖. It may also be noted that the attacks from ‖{a4}‖ and ‖{a5}‖ against ‖{a6}‖ and ‖{a1, a6}‖ could be suppressed without affecting the final outcome. This suggests that, at least in some cases, the same results can be achieved with a more compact representation. This issue is an important direction of future work.

As a variation of the example, assume that we add an ordinary premise FC since there is some evidence suggesting the falsity of the certificate. Then we get an additional argument a7 = FC which preference-independent attacks a2 and its superarguments a4 and a5. Skipping some obvious steps we obtain a modified framework where, in particular, ‖{a7}‖ ↠ ‖{a1, a2}‖ and, as expected, there is exactly one complete extension C ′1 = {‖{a1}‖, ‖{a3}‖, ‖{a6}‖, ‖{a7}‖, ‖{a1, a6}‖} corresponding to the unique surviving (but still defeasible) alternative.

Due to space limitations, other application examples can not be presented in detail. We remark however that the proposed formalism provides a natural treatment of cases where conflicts between arguments arise from ternary (or, generally, more than binary) incompabilities. These cases have attracted attention in the literature since they are somehow challenging for modelling approaches (like AF s) based on binary incompatibility/attack relations. For instance the tandem example [Baroni et al., 2011] concerns three persons (John, Mary, and Suzy) who all want to go cycling on a tandem (represented by three axioms jw, mw, sw) and one assumes defeasibly that if one wants to go then s/he will go (represented by three rules jw ⇒ jt, mw ⇒ mt, sw ⇒ st). Clearly only two of them (no matter who) can actually go. Using ASPIC this is modeled with a constraint ¬(jt ∧mt ∧ st). Altogether this representation gives rise in ASPIC to the construction of ten arguments, three of which, concluding respectively ¬jt, ¬mt, and ¬st, are in mutual conflict each other. In the RS-AF(AT) representation the mutual conflict involves three nodes corresponding to three couples of arguments with conclusions {jt,mt}, {jt, st}, {mt, st} respectively, thus making more explicit that the root of the conflicts is the incompatibility among the three possible pairs of tandem riders.

7 Conclusions

The ability to properly deal with generic contrariness is an important feature for structured argumentation, as it ensures a very high expressiveness and appears to enable novel developments like the use of multivalued logics for argument construction. In this paper we have focused on generic contrariness in ASPIC+, an expressively rich and technically complex formalism whose properties are an important and evolving investigation topic, currently witnessing a great deal of interest. As an example, recently Dung [Dung, 2014] has proposed a new definition of attack relation 1 in ASPIC+ in order to ensure the satisfaction of some axioms not respected by the attack relations considered in [Modgil and Prakken, 2013].

This paper contributes to the advancement of ASPIC+ on a different side, by pointing out that the use of a generic contrariness relation without explicit negation can become problematic in some cases and by providing a solution based on two main pillars: a notion of closure of the contrariness relation at a set level and, accordingly, a notion of conflict and an AF representation involving sets of arguments. The revised version of ASPIC+ satisfies the same rationality postulates, while posing fewer requirements on the properties of argument ordering than in [Modgil and Prakken, 2013].

Starting from the results provided in this paper, many further technical developments can be envisaged, including, for instance, the characterization of the cases where our proposal and the one in [Modgil and Prakken, 2013] are equivalent, the identification of necessary/sufficient conditions for the problems pointed out in Sect. 3 to occur, and the study of the complexity properties of computing the closure of the contrariness relation and the induced AF in specific instances of the ASPIC+ framework. Further, it will be interesting to explore the relationships and, possibly, the intertranslatability between the abstract representation based on Dung's AF s in Def. 23 and alternative representations based on frameworks where attacks originating from sets of arguments are encompassed [Bochman, 2003; Nielsen and Parsons, 2006; Oren and Norman, 2008; Gabbay, 2009].

We remark however that the contribution of this paper goes beyond the technical advancement of ASPIC+. Indeed, we believe that the notions proposed in this paper are useful as general conceptual tools in the study of rule-based structured argumentation and can enable fruitful theoretical developments, independently of the specific framework adopted. To exemplify, we plan to investigate the relationship between argumentation and the four-valued Belnap-Dunn logic [Belnap, 1977] and to exploit the set-based abstract representation to provide a unifying view of different rule-based argumentation systems available in the literature, including in particular the one proposed in [Vreeswijk, 1997] where a collective notion of conflict is encompassed.

Acknowledgments

This paper was partially supported by the National Natural Science Foundation of China (No.61175058) and Zhejiang Provincial Natural Science Foundation of China (No. LY14F030014).

1 While we used the original definition of ASPIC+, our considerations and results also apply to the version of [Dung, 2014].