8, Dialectic proof procedures for assumption-based, admissible argumentation

Notes taken from ‘Dialectical Proof Procedures For Assumption-Based, Admissible Argumentation’ (2005), by P. M. Dung, R. A. Kowalski, F. Toni

“We have presented three, successive refinements of dialectic proof procedures for the admissibility semantics of assumption-based frameworks. The proof procedures search for a winning strategy for a proponent, who argues to establish the admissibility of a belief, against an opponent, who attacks in every possible way the initial and defending arguments of the proponent…”

1, Introduction

Stable Semantics: Sanctions a belief if the belief is the conclusion of an argument whose set of supporting assumptions can be extended to a set of assumptions that both attacks every assumption not in the set, and does not attack itself.

Admissibility Semantics: Sanctions a belief if it is the conclusion of an argument whose set of supporting assumptions can be extended to a set of defending assumptions, which both counter-attacks every attack, and does not attack itself.

Because different agents can hold contrary beliefs the admissibility semantics is said to be credulous, rather than sceptical.

2, Admissibility for assumption-based argumentation frameworks

2.1, Deductive system: A pair (L, R) where…
2.2, Deduction of a conclusion ‘alpha’ based on a set of premises P: A sequence ‘beta1’, …, ‘betaM’ of sentences in L, where m>0 and ‘alpha’ = ‘betaM’, such that…

Flat frameworks: Assumptions do not occur as conclusions of inference rules.

2.3, Assumption-based framework: A tuple (L, R, A, ~) where…
2.4, Argument: A deduction whose premises are all assumptions.

2.5, The only way to attack an argument is to attack one of its assumptions:
- An argument ‘a’ attacks an argument ‘b’ iff ‘a’ attacks an assumption in the set of assumptions on which ‘b’ is based.
- An argument ‘a’ attacks an assumption ‘alpha’ iff the conclusion of a is the contrary ‘~alpha’ of ‘alpha’.

2.6, A set of assumptions A attacks a set of assumptions B iff there exists an argument ‘a’ based upon a set of assumptions A’ (that is a subset of A) which attacks an assumption in B.

“Rebuttal” attacks (where an argument attacks another argument by contradicting its conclusion) are reduced to “undermining” attacks (that depend solely on sets of assumptions)…

2.7, The attack relationship is the basis of the admissibility semantics for argumentation:
- A set of assumptions A is admissible iff (1) A attacks every set of assumptions that attacks A, and (2) A does not attack itself.
- A belief ‘alpha’ is admissible iff there exists an argument for ‘alpha’ based on a set of assumptions A0, and A0 is a subset of an admissible set A.

3, Simplified frameworks for assumption-based argumentation

We use simplified assumption-based frameworks of the form (L, R, A, ~) where:
- All sentences in L are atoms p, q, … or negations of atoms p, q, … (i.e. L is a set of literals).
- The set of assumptions A is a subset of the set of all literals that do not occur as the conclusion of any inference rule in R.
- The contrary of any assumption p is p; the contrary of any assumption p is p.

4, Tight arguments

4.1, Given a selection function, a backward argument of a conclusion ‘alpha’ based on (or supported by) a set of assumptions A is a sequence of multi-sets S1, …, Sm, where S1 = {alpha}, Sm = A, and for every 1 <= i < m…

Because all steps in a backward argument are relevant to the conclusion by construction, we also call backward arguments tight arguments.

A set of assumptions A is admissible iff:
1. for every tight argument ‘a’ that attacks A there exists a tight argument supported by A’ (that is a subset of A) that counter-attacks ‘a’, and
2. no A’ (that is a subset of A) supports a tight argument that attacks an assumption in A.

5, Abstract dispute trees

An abstract dispute tree can be viewed as an and-tree (“and” because it includes all attacks by the opponent against all proponent arguments in the tree).

The search space can be viewed as an and-or-tree (“or” because it includes all the alternative counter-attacks by the proponent against the opponent’s attacks).

5.1, An abstract dispute tree for an initial argument ‘a’ is a (possibly infinite) tree T such that…

Defence set of T: The set of all assumptions belonging to the proponent nodes in T.

5.2, An abstract dispute tree T is admissible iff no culprit in the argument of an opponent node belongs to the defence set of T.

If the opponent can attack the proponent using only the proponent’s own assumptions, then the proponent loses the dispute, because then the proponent attacks itself. However, to win the dispute, the proponent needs to identify and counter-attack in every attack of the opponent some culprit that does not belong to the proponent’s own defence.

Soundness: The defence set of an admissible dispute tree is admissible.

(Strong form of) Completeness: For any initial argument ‘a’ whose support set is contained in an admissible set A of assumptions, there exists a dispute tree for ‘a’ whose defence set A’ is contained in A.

Any dispute tree that has no infinitely long branches is an admissible dispute tree.

5.3, A framework is stratified iff there exists no infinite sequence of arguments ‘a1’, …, ‘an’, …, where for every n >= 1, ‘an+1’ attacks ‘an’.

6, Concrete dispute trees

6.1, Given a selection function, a concrete dispute tree for a sentence ‘alpha’ is a (possibly infinite) tree T such that…

6.2, A concrete dispute tree T for a sentence ‘alpha’ is admissible iff no culprit of an opponent belongs to the defence set of T.

“… our proof procedures generalise negation as failure in logic programming…”

Patient selection functions: Always choose non-assumption sentences in preference to assumptions… they wait until a complete argument has been constructed before beginning to attack it.

For every admissible concrete dispute tree constructed by means of a patient selection function, there exists a corresponding admissible abstract dispute tree with the same defence set. Conversely as well…

6.3, A framework is acyclic if there is a well-ordering of all sentences in the language of the framework such that, whenever a sentence belongs to the premise of an inference rule, then the sentence is lower in the ordering than the conclusion of the inference rule.

7, Dispute derivations

Dispute derivations are to dispute trees what backward arguments are to proof trees…

… Different selections give rise to different derivations, but do not affect completeness, because they simply represent different ways of generating the same dispute tree.

The frontier of a dispute tree is a set of proponent and opponent nodes labelled by multi-sets of sentences, representing steps of potential arguments. A dispute derivation represents the current state of this frontier, together with the set of defence assumptions Ai and culprits Ci generated so far, as a quadruple: [Pi, Oi, Ai, Ci]. The sets Ai and Ci are used to filter arguments…

7.1, Given a selection function, a dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples [P0, O0, A0, C0], …, [Pi, Oi, Ai, Ci], …, [Pn, On, An, Cn] where…”

For every dispute tree derivation of a defence set A for a sentence ‘alpha’, the defence set is admissible, and there exists some A’ (that is a subset of A) that supports an argument for ‘alpha’.

8, Algorithmic issues…

9, Related Work
Our assumption-based approach has the following features, which distinguish it from all the abstract approaches:
- tight arguments are generated by reasoning backwards from conclusions to assumptions,
- partially constructed, potential arguments can be attacked before they are completed,
- the same counter-argument can be used to attack different arguments sharing the same assumption.

10, Conclusion…