Annotated Sequent Calculi for Paraconsistent Reasoning and Their Relations to Logical Argumentation

1 Introduction

In this paper we introduce a proof-theoretic approach for nonmonotonic reasoning with conflicting information. It consists of analytic sequent calculi [Gentzen, 1934] together with rules for modeling conflicts between sequents, which are similar to attack relations in argumentation theory [Dung, 1995].

The basic idea behind these calculi is to add annotations to sequents, 1 intuitively representing their statuses in a derivation. An annotated sequent is thus an expression of the form Γ⇒[a] ∆, where Γ⇒∆ is an ordinary sequent and the superscript [a] is the annotation of the sequent. Informally, the annotation [i] means that the sequent is introduced (conditionally accepted), but is not yet inferred (finally accepted), because it may be attacked by a counter-sequent. The annotation [e] means that the sequent is eliminated, since it is attacked by an accepted sequent, and the annotation [!] is attached to finally accepted sequents, whose attackers are counter-attacked altogether.

A distinctive property of annotated sequent calculi is their modularity, namely: they can be based on any (propositional) logic with a sound and complete calculus, and any set of attack rules. In this paper, we demonstrate this novel approach by focusing on defeat attacks (and the corresponding reactivation and final acceptance rules described in what follows), mainly due to its commonness and simplicity. We show that the resulting proof systems are paraconsistent (in the sense that a contradictory set of premises does not have an explosive set of finally accepted conclusions), and faithfully represent the semantics of logical argumentation frameworks. The nature of derivations of annotated sequent calculi, and in particular the annotation revision process that proceeds the derivation steps (and that is expressed in the object level of the derivation) indicate that, despite of the relative simplicity of the calculi, they are particularly appropriate for modeling and describing inference processes involving revision of beliefs and defeasible reasoning.

1 Note that unlike annotated logics [Abe et al., 2019], we attach annotations to sequents instead of formulas in the language.

2 Annotated Sequent Calculi

In the sequel, we denote by L an arbitrary propositional language. Sets of formulas are denoted by S, T , finite sets of formulas are denoted by Γ, ∆, formulas are denoted by φ, ψ, and atomic formulas are denoted by p, q, r (all possibly indexed). The set of (well-formed) formulas of L is denoted by WFF(L), and the power set of WFF(L) by ℘(WFF(L)).

A propositional logic is a pair L = 〈L, ⊢〉, where L is a propositional language and ⊢ is a consequence relation on ℘(WFF(L))×WFF(L), satisfying reflexivity (if φ ∈ S, then S ⊢ φ), monotonicity (if S ′ ⊢ φ and S ′ ⊆ S, then S ⊢ φ), and transitivity (if S ⊢ φ and S ′ , φ ⊢ ψ then S, S ′ ⊢ ψ). A logic L is assumed to be non-trivial (S ⊬ φ for some S ̸= ∅ and φ), structural (if S ⊢ φ, then {θ(ψ) | ψ ∈ S} ⊢ θ(φ) for every substitution θ), and compact (if S ⊢ φ then Γ ⊢ φ for some finite Γ ⊆ S).

In what follows, we assume that L contains at least a ⊢- negation operator ¬, satisfying p ̸⊢ ¬p and ¬p ̸⊢ p (for atomic p), and a ⊢-conjunction operator ∧, for which S ⊢ ψ ∧ φ iff S ⊢ ψ and S ⊢ φ. 2 Also, we denote by ∧Γ the conjunction of all the formulas in Γ.

Given a logic L and a set S of L-formulas, an L-sequent based on S [Gentzen, 1934] is a structure of the form Γ ⇒ ∆, where ⇒ is a symbol not in L, and Γ ⊢ ∧∆ for some Γ ⊆ S. Definition 1. An annotated L-sequent (annotated sequent,

for short) is a structure of the form Γ ⇒[a] ∆, where Γ ⇒ ∆

2 By the definition of ∧, we have that φ∧ψ ⊢ φ; φ∧ψ ⊢ ψ, and φ, ψ ⊢ φ ∧ ψ, thus S, φ, ψ ⊢ σ iff S, φ ∧ ψ ⊢ σ.

is an L-sequent and a ∈ {i, e, !}. We denote by s[a] the sequent s whose annotation is [a] and use [∗] when the annotation of the sequent may be arbitrary.

Next, we define an annotated sequent calculus C, extending a sequent calculus C. We suppose that C is sound and complete (adequate) for L (so Γ ⇒ ∆ is C-provable iff Γ ⊢ ∧∆).

Definition 2. An annotated sequent calculus C consists of the following components:

1. The axioms and inference rules of C, where the sequents in the rules' conditions are annotated by [∗] and the sequent in the conclusion is annotated by [i].
2. Attack rules. These are inference rules for changing the annotations of an attacked sequent from [i] to [e]. To avoid arbitrary attacks, these rules are restricted to a set S of premises, thus the attacking and the attacked sequents must be S-based. For instance, given such an S, the rule Defeat looks as follows: for Γ1, Γ′1 , Γ2 ⊆ S,

Here, the introduced sequent Γ2 ⇒ ψ2 attacks Γ1, Γ′1 ⇒ ψ1, and so changes the latter's status from 'introduced' to 'eliminated'. The status of the attack condition (rightmost) does not matter, as long as it is logically valid. 3

This attack rule is accompanied by a variation, in which Γ2 ⇒[i] ψ2 is replaced by Γ2 ⇒[!] ψ2, i.e., attacking sequents are either accepted or finally accepted (as defined in Item 5).

1. Reactivation rules. These are inference rules for changing the annotations of a sequent that is to be reactivated from [e] to [i]. Each attack rule has a corresponding reactivation rule. For instance, if Defeat is an attack rule, the following corresponding reactivation rule may be added to the calculus:

This rule indicates that if the sequent in the first condition was attacked (due to the third condition, whose current status does not matter as as long as it is logically valid), but the attacker (the second sequent in the rule's condition) is later counter-attacked, then the originally attacked sequent changes its status from 'eliminated' back to 'introduced' (i.e., conditionally accepted).

1. Retrospective attack rules. Unlike attack rules, that allow only introduced attackers, retrospective attack rules allow also eliminated attackers, provided that the attackers can be reactivated. 4 These rules may thus be viewed

3 Undercut is a similar rule, where Γ1 ⇒[∗] ¬ψ2 is added to the conditions of Defeat. In Undercut, the conclusion of the attacker is equivalent to the negation of some premises of the attacked sequent. Further sequent-based attack rules can be imported from, e.g., [Arieli and Straßer, 2019], using annotations similar to Defeat.

4 Intuitively, retrospective attacks will deal with attack cycles.

as pairs of attack and reactivation rules. For instance, for Γ1, Γ′1 , Γ2, Γ′2 , Γ3 ⊆ S, one may define:

(attack rule with eliminated attacker)

(the eliminated attacker is reactivated)

Note that the rules above need not be consecutive in the derivation, but the reactivation of the attacker need to be part of the revision process following the attack rule (see Definition 3 below). A retrospective attack rule is only applicable in case that the revision process leads to a reactivation (see also the examples in Section 3).

1. Final acceptability rules. These are rules for assuring inferences of sequents. These rules depend on the attack rules and the sequent whose final acceptability is verified. The rules are relative to a finite set S of premises. For instance, let Att(Γ) = {∆ ⊆ S | ∆ ⊢ ¬∧Γ} and suppose that Defeat is the attack rule, then:

This final acceptability rule means that Γ ⇒ ψ is finally accepted if it is conditionally accepted (the first condition of the rule), all of its attackers are produced in the derivation (this is the second condition of the rule), 5 and each such attacker is counter-attacked by a finally accepted sequent (the last condition of the rule). 6

Sequents that cannot be Defeat-attacked by any S-based sequent, either since their left-hand side is empty these are tautological sequents), or because S ̸∈ Att(Γ), are accepted. Thus, when Defeat is the attack rule (or any other premise-attack rule), we also have:

Further (admissible) final derivability rules may be expressed. For instance, for premise-attack rules (e.g., Defeat), we may have rules expressing that if a sequent is finally derived, so is any sequent with a weaker support:

5 Alternatively, that all attackers are produced in a derivation, may be verified by a refutation calculus R (where Γ ̸⇒ ψ is Rprovable iff Γ ̸⊢ ψ), like those in [Bonatti and Olivetti, 2002] (for classical logic) and [Pkhakadze and Tompits, 2020] (for L3).

6 By monotonicity, instead of Att(Γ), it suffices to refer in the rule to MinAtt(Γ) = {∆ ∈ Att(Γ) | (∀∆′ ⊊ ∆) ∆′ ̸∈ Att(Γ)}.

Definition 3. An S-based derivation D of an annotated calculus is a sequence of tuples. Each tuple T contains an index (the tuple's order in the derivation), the derived annotated sequent (the tuple's sequent), the derivation rule that is applied (the tuple's rule), and the indexes of the tuples whose sequents serve as the conditions of the tuple's rule. The tuples' rules are those described in Definition 2, and some of them (like the attack rules) are S-dependent. After each extension of the derivation with a tuple with an attack or a retrospective attack rule, an annotation revision process is initiated, and the derivation is extended with new attack or reactivation rules for updating the sequent annotations when necessary.

The annotation revision process. Let p(s) be the plain sequent (without annotation) of the annotated sequent s. Also, if s[a1] is derived and at no later point s[a2] is derived, we say that the most updated status of s is [a1]. Now, when a tuple T with a [retrospective] attack on s is introduced in the derivation, we let RevSeq = {p(s)}7 and the derivation sequence is traversed backwards, starting from the tuple before T .

• Suppose that during the traversal a tuple T of a [retrospective] attack is encountered, with attacker s1 and attacked s2, such that p(s1) ∈ RevSeq while p(s2) ̸∈ RevSeq. 8 Then:
• If the most updated status of s1 is [e] (i.e., p(s1) was (counter-)attacked during the revision), T should be "rolled-back" by means of a reactivation rule for p(s2). 9 As a consequence, the most updated status of p(s2) in the derivation becomes [i].
• If the most updated status of s1 is [i] (i.e,. p(s1) was reactivated during the revision), but still the most updated status of the attacked sequent p(s2) is also [i], T should be "reinstated" by means of an attack in which p(s1) re-attacks p(s2). As a consequence, the most updated status of p(s2) in the derivation becomes [e].

In both cases, p(s2) is added to RevSeq.

• Suppose that during the traversal a reactivating tuple T is encountered, where the condition of the reactivation is s1 and the reactivated sequent is s2, such that p(s1) ∈ RevSeq and p(s2) ̸∈ RevSeq. If the most updated status of s1 is [i] (i.e, p(s1) has been reactivated during the traversal), T should be "rolled-back" and the original attack is reinstated in the derivation by re-applying the original attack rule on p(s2), using a new tuple T ′ . As a consequence, the most updated status of p(s2) becomes [e] and p(s2) is added to RevSeq.

Definition 4. Let s[i] be an attacking sequent of a derivation tuple T. Then T is coherent, if at the end of the revision process following the introduction of T , the most updated status of s is still [i].

A derivation is coherent if all its tuples are coherent, and there is no tuple such that the most updated statuses of both its attacking and attacked sequents are in {[!], [i]}.

7 The set RevSeq consists of the sequents whose annotation are revised during the traversal.

8 That is, the status of the attacker has been modified, but the status of the attacked sequent has not been modified yet.

9 Reactivation rules are applied only during a revision process.

Definition 5. For an annotated calculus C, we write S |∼C ψ (henceforth, C is omitted) if there is an S-based C-derivation D and a subset Γ ⊆ S, such that Γ ⇒[!] ψ is derived in D (i.e., the sequent Γ ⇒ ψ is finally accepted in D).

3 Some Examples and Properties

Below are some illustrations of derivations by annotated sequent calculi and some basic properties of the induced entailment relation, |∼. In all of the examples we use the proof system in Definition 2 with Defeat as the sole attack rule (and the corresponding reactivation and final acceptance rules). 10

Example 1. Consider the set of assumptions S = {p, ¬p, q} and let L be classical logic. To see that q ⇒ q is finally accepted from S (i.e., there is a derivation of q ⇒[!] q), note that q ⇒[i] q and ⇒[i] p ∨ ¬p are derivable (e.g., by using Gentzen's LK). Moreover, by one of the final acceptability rules, ⇒ p ∨ ¬p is finally accepted (since its left-hand side is empty). Now, the S-based attackers of q ⇒ q are p, ¬p ⇒ ¬q and p, ¬p, q ⇒ ¬q (thus Att(q) = {{p, ¬p}, {p, ¬p, q}}). These attackers are also derivable, but ⇒[!] p ∨ ¬p attacks both of them. For instance, we have

By the final acceptability rule q ⇒[!] q is derived, thus S |∼ q. The situation regarding the other formulas in S is different, and we have that S ̸|∼ p and S ̸|∼ ¬p. Indeed, while both p ⇒[i] p and ¬p ⇒[i] ¬p are derivable, none of them is finally accepted. This may be explained by the fact that each one of them attacks the other, causing a revision of their statuses, and so there are no finally accepted sequents that can eliminate at once all of the attackers. Indeed, after

p ⇒ p is accepted and ¬p ⇒ ¬p is eliminated. By extending the derivation with the retrospective attack

the situation is reversed, and now ¬p ⇒ ¬p is accepted while p ⇒ p is eliminated. Another application of the retrospective attack rule, this time when p ⇒[e] p retrospectively attacks ¬p ⇒[i] ¬p, reverses their statuses again, and so forth.

Example 2. The previous example demonstrates, e.g., a cyclic attack of size two (p ⇒ p and ¬p ⇒ ¬p attack each other). Figure 1 shows a cycle of size four. The left-hand side of the figure, Stage I, represents a 3-chain of attacks. In the middle of the figure (Stage II), the chain turns into a 4-cycle.

10 To preserve readability of the examples, in what follows we only consider the sequents of tuples occurring in a derivation (complete tuples may be easily reconstructed).

Note that in order to close the cycle, a retrospective attack is needed. After the revision process (denoted by the dashed arrows) s2 and s4 are accepted, while s1 and s3 are eliminated. These statuses may be reversed by an application of another retrospective attack, as shown in Stage III of the figure. As a result, s1 and s3 are accepted while s2 and s4 are eliminated. The last two steps may be repeated interchangeably, revising each time the statuses of the sequents involved in the cycle of attacks. It follows that each of the four sequents is exposed to repeated attacks, and so none of them is finally accepted.

A similar analysis holds for any even-length cycle of attacks, thus derivation tuples in even-length cycles are coherent (Definition 4). In contrast, derivations with an odd-length cyclic attack must be incoherent. See, e.g., derivation step 3 in Figure 2 Stage II, for a 3-cycle. Indeed, for 'closing' such a cycle with an attack rule the attacker must be eliminated at the end of the revision process (this may be verified by induction on the length of the cycle). Moreover, if a retrospective attack is initiated in such cases, the attacker cannot be reactivated.

Example 3. Consider a logic whose negation ¬ does not respect double-negation introduction (i.e., p ̸⊢ ¬¬p), and suppose again that Defeat is the only attack rule. Let S = {p, ¬p, ¬¬p, ¬¬¬p}. We denote by ¬ip the formula in which p is preceded by i negations (in particular, ¬0 p is p) and by si[a] the annotated sequent ¬ip ⇒[a] ¬ip for a ∈ {i, e, !}. By reflexivity, si[i] is derivable for every 0 ≤ i ≤ 3. Now, consider the following derivation (D and R denote Defeat and Reactivation, respectively).

At this point, the derived sequents and their most updated statuses are s0[e], s1[i], s2[e] and s3[i]. Moreover, this is a kind of a 'steady state', in which all the sequents that are conditionally accepted (and only them) can in fact be finally accepted (note that all their S-based attackers are derived). Indeed, since S ̸∈ Att(¬3p), we have that Att(¬3p) = ∅ (i.e., s3 cannot be attacked by any S-based sequent), and so by the final acceptability rule we can derive s3[!]. In turn, s3[!] attacks s2 , the single attacker of s1, thus s1[!] is derived. Finally, s1[!] attacks s0 , and so the latter cannot be finally accepted. It follows, then, that S |∼ ¬p and S |∼ ¬¬¬p. Now, suppose that ¬4p is added to the set of assertions: i.e., S ′ = {p, ¬p, ¬¬p, ¬¬¬p, ¬¬¬¬p}. Then s4[i] is derived, and so the previous derivation may be extended as follows:

The derived sequents and their most updated statuses are now: s0[i], s1[e], s2[i], s3[e] and s4[i]. Again, for similar reasons as before, all the sequents that are conditionally accepted (and only them) are also finally accepted, so this time we conclude that S ′ |∼ p and S ′ |∼ ¬¬p and S ′ |∼ ¬¬¬¬p.

An alternative representation of the derivation in this example is presented in Figure 3.

Next, we consider some basic properties of the entailment relation |∼ that is induced by annotated calculi. We start with two observations about derivations in annotated calculi.

Proposition 1. Let D be a derivation (Definition 3).

1. For a fixed set of assumptions, a finally accepted sequent cannot be eliminated. 11
2. Suppose that D is coherent. Then at the end of a revision process (following a derivation step) no sequent attacks another sequent and is eliminated at the same time.

Proof. Item (a) holds simply because a finally accepted sequent cannot be attacked. For item (b) suppose that s1 attacks s2. This may happen in one of the following two cases:

1. The attack is part of a derivation step. If this step is an application of an attack rule, then the status of s1 is [i] (or [!]), and thus by coherence (or by the first item, in case that s1 is finally derived), s1 cannot be eliminated. The other possibility is that a retrospective attack rule is applied, in which case s1 must be reactivated, turning its status back to [i] (and it cannot be modified again in the revision process, since s1 is in RevSeq).
2. The attack is reinstated as part of the annotation revision process. This may happen only if s1 was reactivated earlier in the revision process, so its status was changed to [i] (and cannot be changed again during the revision).

In both cases s1 is not eliminated.

Proof. If S is ⊢-consistent, no attack rule is applied, thus no sequent is eliminated (and so no reactivation or retrospective attack is applied either). It follows that in this case a derivation consists only of rules of C and the final acceptability rules. Moreover, for every Γ ⊆ S it holds that Att(Γ) = ∅, thus any derived sequent is also finally accepted (and, ofcourse, any finally accepted sequent must be derived). It follows that S ⊢ ψ iff S ⇒[i] ψ is derived, iff S ⇒ ψ is finally accepted in that derivation, iff S |∼ ψ.

Proposition 3. If ⊢ is paraconsistent (i.e., p, ¬p ̸⊢ q) or contrapositive (i.e., if Γ ⊢ ψ then Γ, ¬ψ ⊢ ¬γ for every γ ∈ Γ), then |∼ is paraconsistent .

Proof. If ⊢ is paraconsistent, then p, ¬p ⇒ q is not derivable. Since neither p ⇒ q nor ¬p ⇒ q is derivable (the logic is not trivial), there is no derivable {p, ¬p}-based argument whose conclusion is q. Thus, no such sequent is finally derived, and so p, ¬p ̸|∼ q. Suppose then that ⊢ is not paraconsistent. Then p, ¬p ⇒ is derivable, and so by contraposition ⇒¬(p ∧ ¬p) is also derivable. The latter is finally accepted (by the final acceptability rule), and moreover {p, ¬p} ∈ Att(q). Thus, even if p, ¬p ⇒ q is derived, the last condition in the final acceptability rule is not met. So, Γ ⇒ q is not finally derived for Γ ⊆ {p, ¬p}, thus p, ¬p ̸|∼ q in this case as well.

11 In other words, there is no extension of D (by further derivation steps and revisions), based on the same set of assumptions, in which the annotation of a sequent changes from [!] to [e]. This resembles the notion of final derivability in adaptive logics [Batens, 2007; Straßer, 2014] and in [Arieli and Straßer, 2019].

12 Recall, ⊢ is the consequence relation of the base logic verifying sequents, and |∼ is the entailment relation given by final acceptance.

4 Relations to Logical Argumentation

Annotated calculi, and in particular the attack rules, are inspired by similar concepts in formal argumentation [Dung, 1995; Baroni et al., 2018; Gabbay et al., 2021]. In this section, we show some relations between the two formalisms.

Definition 6. Let C be an annotated sequent calculus and let D be an S-based C-derivation. Then:

• Derived(D) is the set of S-based sequents s s.t. s[i] ∈ D;
• Accept(D) is the set of sequents s in Derived(D) such that their most updated status is [i] or [!];
• Final(D) is the set of sequents s in Derived(D) such that s[!] ∈ D;
• Attack(D) is the set of pairs (s1, s2) such that s1 attacks or retrospectively attacks s2 in D (s1, s2 ∈ Derived(D)).

AF(D) = 〈Derived(D), Attack(D)〉 is called the (sequentbased) argumentation framework that is induced by D.

Example 4. The possible attacks among the sequents in Example 1 and the argumentation framework induced by the corresponding derivation are the following:

Definition 6 is a logic-based representation of argumentation frameworks, which according to Dung [1995] are pairs AF = 〈Args, Attack〉, where Args is a denumerable set of elements, called arguments, and Attack is a relation on Args × Args, whose instances are called attacks.

Given a framework AF, a key issue in its understanding is the question what combinations of arguments can collectively be accepted in AF. This is determined as follows:

Definition 7. Let AF = 〈Args, Attack〉 be an argumentation framework, and let E ⊆ Args.

• E attacks an argument A if there is an argument B ∈ E that attacks A (i.e., (B,A) ∈ Attack). The set of arguments that are attacked by E is denoted by E +.
• E defends A if E attacks every argument that attacks A.
• E is conflict-free if it does not attack any of its elements (i.e., E + ∩ E = ∅), E is admissible if it is conflict-free and defends all of its elements, and E is complete if it is admissible and contains all the arguments that it defends.
• E is a stable extension of AF if it is conflict-free and E ∪E + = Args. E is a grounded extension of AF if it is ⊆-minimal among the complete extensions of AF.

The next results show the close relations between derivations in annotated calculi (Definition 2) and stable, respectively grounded semantics of argumentation frameworks.

Proposition 4. If D is coherent, then Accept(D) is a stable extension of AF(D).

Outline of proof. We show that Accept(D) is conflict-free in AF(D) and attacks any eliminated sequent. The former follows from the coherence of D. To see the latter, let r be an eliminated sequent. If r is [retrospectively] attacked by s in a derivation step, then by coherence the status of s is [i], thus s ∈ Accept(D). If r is attacked by s during the status revision process, then it is easy to verify that the statuses of r and s must interchange. Since r is eliminated, s ∈ Accept(D).

Note 1. The coherence requirement in Proposition 4 is necessary. Consider the derivation D in Figure 2. Step 3 in Stage II is not coherent, as the attacker s3 is eliminated. Thus, Accept(D) = {s2}, but AF(D) has no stable extensions.

Example 5. In Example 4, if the last [retrospective] attack of p⇒p on ¬p⇒¬p is performed after the last [retrospective] attack of ¬p ⇒ ¬p on p ⇒ p, then for the corresponding derivation D we have Accept(D) = {⇒p∨¬p, q⇒q, p⇒p}. This is indeed a stable extension of AF(D). If the mutual attacks of p⇒p and ¬p⇒¬p are performed in a reversed order, then Accept(D) = {⇒ p ∨ ¬p, q ⇒ q, ¬p ⇒ ¬p}, which again is a stable extension of AF(D).

Definition 8. An S-derivation D is saturated if Final(D) is exhaustive in D: i.e., the final acceptability rules are applied to every derived sequent in D to which it can be applied. 13

Proposition 5. If D is saturated, then Final(D) is the (unique) grounded extension E ⊆ Derived(D) of AF(D).

Proof. We show that Final(D) = E. Let 〈s1[!], . . . , sn[!]〉 be the ordered set of all [!]-annotated sequents derived in D, in the order in which they occur in D.

"⊆". We prove inductively that si[!] ∈ E for i = 1, . . . , n. Base case. Since s1[!] is derived by an application of a final applicability rule and it is the first sequent in D with this property, it has no attackers. Since E is complete, s1 ∈ E. Inductive step. Suppose the sequent si+1[!] was derived by a final acceptability rule calling upon the [!]-annotated sequents sj1 [!], . . . , sjm [!]. Then j1, . . . , jm < i + 1 and by the inductive hypothesis, sj1 , . . . , sjm ∈ E. Also, the sequents sj1 , . . . , sjm attack all attackers of si+1, so si+1 is defended by E and by the completeness of E, si+1 ∈ E.

"⊇". We show that Final(D) is complete in AF(D). Since E is ⊆-minimal complete, then E ⊆ Final(D). We show conflict-freeness inductively by showing that for each i = 1, . . . , n there is no k ≤ i such that sk attacks si. Base case. Trivial, since s1 doesn't have attackers. Inductive step. Suppose there is a k ≤ i s.t. sk attacks si+1. By the final acceptability rule there is a j ≤ i s.t. sj attacks sk, which contradicts the inductive hypothesis. Suppose now that si+1 attacks itself. By the final acceptability rule there is a k ≤ i such that sk attacks si+1 which we have already excluded.

For admissibility, suppose that s ∈ Derived(D) \ Final(D) attacks some si. Then by the application of the final acceptability rule that produces si[!] ∈ D, there is a k < i such that sk attacks s. For completeness, let s ∈ Derived(D) be defended by Final(D). Then we can apply final applicability rule to derive s[!]. Since D is saturated, s[!] ∈ Final(D).

13 For a finite S this is a decidable property.

Proposition 6. For a derivation D, let S = ⋃{∆ | ∆ ⇒ φ ∈ D}. Let AF(S) = 〈Args(S), Attack〉 where Args(S) = {Γ ⇒ ψ | Γ ⊆ S and Γ ⊢ ψ} and Attack = {(s, t) | s = ∆ ⇒ φ, t = Γ ⇒ ψ ∈ Args and φ ⊢ ¬∧Γ}. Let E be the grounded extension of AF(S). For every s ∈ E, there is an S-based derivation D′ of s[!] without attack rules.

Proof. We note that for each r ∈ Args(S) there is an S-based derivation Dr concluding r[i]. Since D is finite, E = ⋃i≥1 Ei where E0 = ∅ and Ei+1 = {s ∈ Args | Ei defends s} [Dung, 1995]. Let s ∈ E. We prove by induction on i, that for each s ∈ Ei (i = 1, . . . , n) there is an S-based derivation D′s of s[!] without attacks. Base case. Since s ∈ E1, s has no attackers. Let D′s be the extension of Ds by an application of the final acceptibility rule that concludes s[!]. Inductive step. Let s ∈ Ei+1. For each attacker r of s there is an s′ ∈ ⋃ij=1 Ej that attacks r. By the IH there are derivations D′s′ for each such defending s′ . We obtain D′s by concatenating the proofs Dr of each attacker, the proofs D′s′ for each defender, and applying the final acceptability rule to conclude s[!].

5 RelatedWork and Conclusion

Annotated versions of sequent calculi have been introduced in, e.g., [Doˇsen, 1985; Indrzejczak, 1997]. However, those calculi significantly deviate from ours and have different motivations and purposes (we discuss this in future work).

There are a variety of reasoning methods for abstract and structured (or, more specifically, logical) argumentation frameworks. We refer to [Cerutti et al., 2017] and [Besnard et al., 2020] for two extensive surveys on this subject. Most of the approaches mentioned in these review papers are based on CSP/SAT/ASP/QBF-solvers, and as such, the reasoning engine is encapsulated in the solvers and/or limited to specific base logics. Our approach extends standard sequent calculi using the same notions (sequents, inference rules, etc), augmented with primary concepts from argumentation theory for a better handling of conflicts among the sequents. Some other notions, such as final acceptability are borrowed from proof systems for adaptive logics [Batens, 2007; Straßer, 2014]. Altogether, this results in a modular paraconsistent method for reasoning with arguments based on different underlying logics and attack rules.

A different approach with a similar motivation is presented in [Arieli and Straßer, 2019]. The formalism introduced in this paper has some advantages: First, in our case all inference rules may be chained, so in particular conclusions of attack rules may serve as conditions of other rules. Second, rules for final acceptability are based on the available derivation and not on its potential extensions, as in [Arieli and Straßer, 2019], or in adaptive logics. Last, by including sequent annotations, the machinery for updating the statuses of derived sequents is included in the derivation itself and does not require an external evaluation procedure. By allowing inference rules to reason about the acceptability statuses of arguments, our approach integrates meta-argumentative reasoning [Jakobovits and Vermeir, 1999; Boella et al., 2009].

Acknowledgements

Ofer Arieli is partially supported by the Israel Science Foundation (Grant No. 550/19). Kees van Berkel is supported by the projects WWTF MA16-028 and FWF W1255-N23.