13.4-13.5, Computing ideal sceptical argumentation

Notes taken from ‘Computing ideal sceptical argumentation’ by P. M. Dung, Paolo Mancarella and F. Toni (2006)

4, Computing ideal beliefs for assumption-based argumentation

… Our proof procedure for computing ideal beliefs for assumption-based frameworks is defined in terms IB-dispute derivations, adapted from (a variant of) the dispute derivations of the paper ‘Dialectic proof procedures for assumption-based, admissible argumentation’ for computing admissible beliefs, that we refer to here as AB-dispute derivations…

By virtue of relying upon potential attacks, dispute derivations thus actually construct concrete dispute trees, that may correspond to one, no or multiple dispute trees.

Note that all our dispute derivations will be of finite length. This is because our ultimate goal is to develop effective proof procedures that can be used to support practical applications.

Computing admissible beliefs

The efficient construction of admissible dispute trees for assumption-based argumentation frameworks can be obtained via AB-dispute derivations… These are variants of the dispute derivations of ‘Dialectic proof procedures for assumption-based, admissible argumentation’, that improve upon them by being “more complete”… GB-dispute derivations (which compute grounded beliefs) can be seen as an initial step between dispute trees and the actual, final form of AB-dispute derivations, in that they are correct, but highly incomplete and inefficient…

4.1, Let ABF be an assumption-based argumentation framework, and AF be the corresponding abstract framework. Given a dispute tree T for AF,
- for any opponent node labelled by an argument ‘b’ with child a proponent node labelled by an argument ‘a’ if ‘a’ attacks some assumption ‘alpha’ in the set supporting ‘b’ then ‘alpha’ is said to be the culprit in ‘b’;
- the set of all assumptions supporting the arguments in the defence set of T is referred to as the assumption-defence set of T.

(Theorem 4.1) … Given a dispute tree T for AF, T is admissible iff no culprit in the argument of an opponent node belongs to the assumption-defence set of T.

In GB-dispute derivations:
- the set of culprits Ci is used to filter potential defence arguments…
- the set of defence assumptions Ai is used to filter potential culprits…
so that the final assumption-defence set constructed by the derivation does not attack itself (theorem 4.1).

4.2… Given a selection function, a GB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…

(Theorem 4.2) Given a GB-dispute derivation of a defence set A for a sentence ‘alpha’:
- A is admissible and it is contained in the grounded set of assumptions;
- There exists A’ (a subset of A) and an argument A’ |- alpha.

Note that GB-dispute derivations succeed in many cases where other procedures for computing grounded beliefs fail. However, GB-dispute derivations are “highly incomplete” for admissibility, in that they fail to compute admissible sets in many cases, corresponding to infinite dispute trees.

AB-dispute derivations incorporate a filtering by defence assumptions so that they can (finitely) compute infinite admissible dispute trees… Moreover, AB-dispute derivations incorporate a filtering by culprit assumptions so that they can be more efficient…

4.3… Given a selection function, a AB-dispute derivation of a defence set A for a sentence ‘alpha’ is a finite sequence of quadruples (P0, O0, A0, C0), …, (Pi, Oi, A, Ci), …, (Pn, On, An, Cn) where…

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

4.4, An assumption-based framework AF is positively acyclic (or p-acyclic for short) if the dependency graph of AF+ is acyclic. (AF+ is the framework obtained by deleting all assumptions appearing in the premises of the inference rules of R.)

(Lemma 4.1) Given an assumption based framework, let an infinite partial deduction be an infinite sequence of steps defined as in Definition 2.4. Given a p-acyclic framework, there exists no infinite partial deduction.

Computing ideal beliefs

… Like AB-dispute derivations, IB-dispute derivations are sequences of tuples, but these tuples are of the form (Pi, Oi, Ai, Ci, Fi). Fi a novel component intuitively holding all potential attacks against the proponent: by virtue of theorem 3.3 IB-dispute derivations need to make sure that no admissible set of assumptions containing any attack in Fi exists. This check is ultimately performed by a new kind of (subsidiary) dispute derivations, that we call Fail dispute derivations…

(Notation 4.2) Let S be a set of sentences in L. By Fail(S) we mean that there exists no admissible set E of assumptions such that E ||- S.

IB-dispute derivations are sequences of tuples of the form (Pi, Oi, Ai, Ci, Fi) where
- the new component Fi holds all multisets S for which we want to prove that Fail(S) (these are the potential attacks S dealt with in step 2 of AB-dispute derivation)
- Pi, Oi, Ai, Ci are as in AB-dispute derivations, except that sentences occurring in the multisets in Oi may be marked.

Intuitively, IB-dispute derivations compute an admissible support for the given sentence ‘alpha’ while trying to check that no admissible set attacks it. As soon as a (potential) attack is found, this is stored in the F component of the tuple to check that this fails to be become/admissible. Whenever a potential culprit is ignored in a potential attack, this is marked so that it will not be selected again. Selected elements in the potential attacks in the O component are chosen amongst the unmarked elements. Thus, we will impose that, given a multisets S in Oi, the selection function will only select unmarked sentences in Su. (Su is the set of unmarked sentences in S.)

4.5… Given a selection function, an IB-dispute derivation of an ideal support A for a sentence alpha is a finite sequences of tuples (P0, O0, A0, C0, F0), …, (Pi, Oi, A, Ci, Fi), …, (Pn, On, An, Cn, Fn) where…

(Theorem 4.5) If there exists an IB-dispute derivation for ‘alpha’, then ‘alpha’ is an ideal belief.

(Theorem 4.6) Given a p-acyclic framework with an underlying finite language, if ‘alpha’ is an ideal belief then there exists an IB-dispute derivation for ‘alpha’.

4.6… Given a selection function, a Fail-dispute derivation of a multiset of sentences S is a sequence D0, …, Dn such that each Di is a set of quadruples of the form (P, O, A, C) where…

(Theorem 4.7) If there exists a Fail-dispute derivation for a multiset of sentences S then Fail(S) holds.

(Corollary 4.2) If there exists an IB-dispute derivation for ‘alpha’ in which Fail-dispute derivations are used to check whether Fail holds, then ‘alpha’ is an ideal belief (i.e. the derivations are sound).

Fail-dispute derivations are complete if AB-dispute derivations are complete for the admissibility semantics. Thus:

(Theorem 4.8) For p-acyclic frameworks with a finite underlying language, if there exists no admissible argument supporting S then there is a Fail-dispute derivation for S.

(Corollary 4.3) For p-acyclic frameworks with a finite underlying language, IB-dispute derivations in which Fail-dispute derivations are used to check Fail, are complete.

5, Conclusion…