Sylvie Doutre

Andreas Herzig

Laurent Perrussel

A dynamic logic framework for abstract argumentation (long version)

We provide a logical analysis of abstract argumentation frameworks and their dynamics. Following previous work, we express attack relation and argument status by means of propositional variables and define acceptability criteria by formulas of propositional logic. We here study the dynamics of argumentation frameworks in terms of basic operations on these propositional variables, viz. change of their truth values. We describe these operations in a uniform way within a well-known variant of Propositional Dynamic Logic PDL: the Dynamic Logic of Propositional Assignments, DL-PA. The atomic programs of DL-PA are assignments of propositional variables to truth values, and complex programs can be built by means of the connectives of sequential and nondeterministic composition and test. We start by showing that in DL-PA, the construction of extensions can be performed by a DL-PA program that is parametrized by the definition of acceptance. We then mainly focus on how the acceptance of one or more arguments can be enforced and show that this can be achieved by changing the truth values of the propositional variables describing the attack relation in a minimal way.

Introduction

Argumentation is a reasoning model based on the construction and on the evaluation of arguments. The seminal approach by Dung [START_REF] Dung | On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games[END_REF] represents an argumentation framework AF as a set of abstract arguments, the structure and origin of which are left unspecified, along with an attack relationship between arguments. Dung and his followers have defined semantics for the evaluation of the acceptability of arguments (see [START_REF] Baroni | Semantics of abstract argument systems[END_REF] for a comprehensive overview). We focus in this paper on extension-based semantics, that define collectively acceptable sets of arguments, called extensions.

Dung's AF has already been represented in various logics, notably in propositional logic, starting with [START_REF] Besnard | Checking the acceptability of a set of arguments[END_REF]. There, AF is described by means of a boolean formula in a logical language whose propositional variables represent the attacks (the attack variables). Furthermore, extensions of the AF under a given semantics σ can also be described by means of boolean formulas constraining valuations to correspond to the extensions under the semantics. This is done in an extension of the language of attack variables by variables representing argument acceptance.

Based on such a logical representation, several authors have recently investigated the dynamics of the AF, such as [START_REF] Baumann | What does it take to enforce an argument? minimal change in abstract argumentation[END_REF][START_REF] Booth | A logical theory about dynamics in abstract argumentation[END_REF][START_REF] Bisquert | Enforcement in Argumentation is a kind of Update[END_REF][START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF]. They start by distinguishing several kinds of modification of the AF, such as the addition or the removal of attacks, or the enforcement of the acceptability of an argument a (e.g. such that a is part of at least one extension). All these papers build on previous work in belief change, either referring to AGM theory [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF], such as [START_REF] Booth | A logical theory about dynamics in abstract argumentation[END_REF][START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF], or to KM theory [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF], such as [START_REF] Bisquert | Enforcement in Argumentation is a kind of Update[END_REF]. They express the modification as a logical formula describing some goal, i.e., a property that AF should satisfy: the task is to revise/update AF so that this formula is true.

The above papers do not provide a single framework encompassing at the same time AF, the logical definition of the enforcement constraint and the change operations: there is usually one language for representing AF and another language for representing constraints, plus some definitions in the metalanguage connecting them. This has motivated us to provide a general, unified logical framework for the representation and the update of argumentation frameworks. We make use of a flexible yet simple logic: Dynamic Logic of Propositional Assignments, abbreviated DL-PA [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]. DL-PA is a simple instantiation of Propositional Dynamic Logic PDL [START_REF] Harel | Dynamic logic[END_REF][START_REF] Harel | Dynamic Logic[END_REF] whose atomic programs are assignments of propositional variables to either true or false. Complex programs are built then from atomic programs by the standard PDL program operators of sequential composition, nondeterministic composition, and test. We here moreover add a less frequently considered PDL program operator, namely the converse operator. The language of DL-PA has formulas of the form π ϕ and [π]ϕ, where π is a program and ϕ is a formula. The former expresses that ϕ is true after some possible execution of π, and the latter expresses that ϕ is true after every possible execution of π. It is shown in [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF] that every DL-PA formula can be reduced to an equivalent propositional formula. The reduction extends to the converse operator in a straight-forward manner and provides a syntactical representation of the modified belief base.

We start by showing that the construction of extensions under a given semantics can be performed by a DL-PA program that is parametrized by the formula describing the semantics. Then we consider modifications of the attack relation and/or of the extensions. Modifications of the extensions are enforced by changing the attack relation only (addition or removal of attacks between the existing arguments). This can be achieved by changing the truth values of the attack variables. More precisely, to every input formula A describing the desired modification we associate a DL-PA program π A implementing the update by A. We can then check whether a formula C is true in all (resp. in some) extensions of (the argumentation framework resulting from) the update AF by the goal A.

The paper is organized as follows. In the next section we recall the definitions of an argumentation framework and of various semantics as well as their encoding in propositional logic. We then introduce DL-PA and show how to use it to construct extensions, before applying it to the modification of the attack relation and of the extensions. After that, we discuss several ways to extend our framework in order to capture other kinds of modifications. The last section discusses related work and concludes. 1

Representing argumentation frameworks

In the present section we set the stage for our paper: we recall the definition of argumentation frameworks and provide a logical language to reason about them. An argumentation framework AF can be represented in propositional logic as follows. First, a set of attack variables is associated to the set of arguments A:

Argumentation frameworks

ATT A = {Att a,b : (a, b) ∈ A × A} Let L Att
be the set of all formulas that are built from attack variables. Theory of AF = (A, R) is the boolean formula

Th AF =         (a,b)∈R Att a,b         ∧         (a,b) R ¬Att a,b         Example 1. Consider the set of arguments A 1 = {a, b} and the two argumentation frameworks AF 1 = (A 1 , R 1 ) and AF 2 = (A 1 , R 2 ), with R 1 = {(a, b)} and R 2 = {(a, b), (b, a)}.
They are depicted in Figure 1.

AF 1 and AF 2 are described by the theories Argumentation semantics Many semantics have been defined for acceptability. Some of them are extension-based, some others are labelling-based. In this paper we only consider the first: they prevail in the literature, and moreover equivalent extension-based formulations of labelling-based semantics are available [START_REF] Baroni | Semantics of abstract argument systems[END_REF]. For a given AF, a semantics identifies sets of acceptable arguments, called extensions. There may be none, one or several such extensions. In order to characterize extensions we associate to A a second set of propositional variables:

Th AF 1 = Att a,b ∧ ¬Att b,a ∧ ¬Att a,a ∧ ¬Att b,b Th AF 2 = Att a,b ∧ Att b,a ∧ ¬Att a,a ∧ ¬Att b,b
IN A = {In a : a ∈ A}
where In a stands for "argument a belongs to an extension".

As proposed in [START_REF] Besnard | Checking the acceptability of a set of arguments[END_REF]) and as extensively discussed in [START_REF] Gabbay | Dungs argumentation is essentially equivalent to classical propositional logic with the peircequine dagger[END_REF], several semantics can be captured in propositional logic. Among such semantics, we consider at first the well-known stable, admissible and complete semantics. 2We write the propositional formulas capturing these semantics in a language that is built from the set of propositional variables P = ATT A ∪ IN A by means of the boolean connectives in the usual way. Let L Att , ,In be our language of Boolean formulas.

A stable extension of AF = (A, R) is a set S ⊆ A such that it does not exist two arguments a and b in S such that (a, b) ∈ R (that is, S is conflict-free), and for each argument b S , there exists a ∈ S such that (a, b) ∈ R (any argument out of the extension is attacked by the extension). This can be rephrased in propositional logic as follows [START_REF] Besnard | Checking the acceptability of a set of arguments[END_REF]:

Stable A = a∈A         In a ↔ ¬ b∈A (In b ∧ Att b,a )        
An admissible set of AF = (A, R) is a conflict-free set S ⊆ A that defends all its elements: for all a ∈ S , if there exists b such that (b, a) ∈ R, then there is some argument c ∈ S such that (c, b) ∈ R.

Adm A = a∈A         In a → b∈A (Att b,a → (¬In b ∧ c∈A (In c ∧ Att c,b )))        
A complete extension of AF = (A, R) is an admissible set S ⊆ A that contains all the arguments it defends, that is: if an argument a is such that, for all b such that (b, a) ∈ R, there exists some c ∈ S such that (c, b) ∈ R, then a ∈ S .

Complete A = a∈A         (In a → ¬ b∈A (In b ∧ Att b,a )) ∧ (In a ↔ b∈A (Att b,a → c∈A (In c ∧ Att c,b )))        
The justification state of an argument [START_REF] Baroni | Semantics of abstract argument systems[END_REF] depends on the extensions it belongs to; basically, an argument is credulously justified (resp. skeptically justified) under a given semantics, if it belongs to at least one of (resp. all) the extensions under the semantics.

Extensions and valuations Argumentation frameworks and semantics being encoded in propositional logic, computing the extensions under the semantics consists in finding the models of the formulas representing the argumentation system and the semantics. A valuation is a subset of the set of propositional variables P = ATT A ∪ IN A . The set of all valuations is 2 P . We use v, v 1 , v 2 , etc. to denote valuations. A given valuation determines the truth value of the boolean formulas of the language L Att , ,In in the usual way. The set of valuations where A is true is called the set of models of A or the set of A-valuations and is noted ||A||.

The following proposition, adapted from [START_REF] Besnard | Checking the acceptability of a set of arguments[END_REF]

Th AF 1 ∧ Stable A 1 → In a ∧ ¬In b Th AF 1 ∧ Adm A 1 → ¬In b Th AF 1 ∧ Complete A 1 → In a ∧ ¬In b

DL-PA: Dynamic Logic of Propositional Assignments

We have just seen that looking for the extensions of an argumentation framework AF with respect to some semantics σ amounts to looking for the models of the formulas representing AF and σ. We now consider a way to build these models in a logic which makes operations on valuations, namely the Dynamic Logic of Propositional Assignments DL-PA [START_REF] Herzig | A dynamic logic of normative systems[END_REF][START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]. DL-PA is based on Propositional Dynamic Logic PDL [START_REF] Harel | Dynamic logic[END_REF][START_REF] Harel | Dynamic Logic[END_REF]. Just as PDL, it has operators of sequential and nondeterministic composition of programs, test and iteration (the Kleene star), which enable reasoning about programs. The atomic programs of DL-PA are assignments of truth values to propositional variables, such as assigning true or false to p, respectively written p←⊤ and p←⊥. The formulas of DL-PA can express how valuations are modified by programs so that after this modification stage, some property holds. In our context, they express how to build the valuations representing the extensions of AF w.r.t. σ. Before showing this we define syntax and semantics of DL-PA and state complexity results.

We here base our work on the star-free version of DL-PA of [START_REF] Herzig | A dynamic logic of normative systems[END_REF]), that we extend by the operator of converse execution of programs. We keep on calling that logic DL-PA.

Language The language of DL-PA is defined by the following grammar:

π p←⊤ | p←⊥ | ϕ? | π; π | π ∪ π | π - ϕ p | ⊤ | ⊥ | ¬ϕ | ϕ ∨ ϕ | π ϕ
where p ranges over P. Key formulas are: [π]ϕ which stands for "after every execution of the program π formula ϕ holds" and π ϕ which stands for "after some execution of the program π formula ϕ holds". The formula [π]ϕ abbreviates ¬ π ¬ϕ.

The atomic program p←⊤ makes p true and p←⊥ makes p false. The operators of sequential composition (";"), nondeterministic composition ("∪") and test ("(.)?") are familiar from PDL. The operator "(.) -" is the converse operator: formula [π -]ϕ stands for "before every execution of the program π formula ϕ was true" and π -ϕ stands for "before some execution of the program π formula ϕ was true".

The length of a formula ϕ, noted |ϕ|, is the number of symbols used to write down ϕ, without " ", " ", and parentheses. For example, |¬(q ∨ ¬r)| = 1+(1+1+2) = 5 and | q←⊤ (q ∨ r)| = 3+3 = 6. The length of a program π, noted |π|, is defined in the same way. For example, |p←⊥; p?| = 3+1+2 = 6.

Conjunction (∧), implication (→) and equivalence (↔) are considered with their usual meaning. We also make use the exclusive disjunction ϕ ⊕ ψ which abbreviates (ϕ∧¬ψ) ∨ (¬ϕ∧ψ). Furthermore, several program abbreviations are familiar from PDL. First, skip abbreviates ⊤? ("nothing happens"). Second, for n ≥ 0, we define inductively π n and π ≤n as follows:

π n = skip if n = 0 π; π n-1 if n ≥ 1 π ≤n = skip if n = 0 (skip ∪ π); π ≤n-1 if n ≥ 1 ||p←⊤|| = {(v 1 , v 2 ) : v 2 = v 1 ∪ {p}} ||p←⊥|| = {(v 1 , v 2 ) : v 2 = v 1 \ {p}} ||ϕ?|| = {(v, v) : v ∈ ||ϕ||} ||π; π ′ || = ||π|| • ||π ′ || ||π ∪ π ′ || = ||π|| ∪ ||π ′ || ||π -|| = ||π|| -1 ||p|| = {v : p ∈ v} ||⊤|| = 2 P ||⊥|| = {} ||¬ϕ|| = 2 P \ ||ϕ|| ||ϕ ∨ ψ|| = ||ϕ|| ∪ ||ψ|| || π ϕ|| = v : there is v ′ s.t. (v, v ′ ) ∈ ||π|| and v ′ ∈ ||ϕ||
Table 1: Interpretation of the DL-PA connectives

Let us now introduce assignments of literals to variables by way of the following abbreviations: p←q = (q?; p←⊤) ∪ (¬q?; p←⊥) p←¬q = (q?; p←⊥) ∪ (¬q?; p←⊤)

The former assigns to p the truth value of q, while the latter assigns to p the truth value of ¬q. So p←p does nothing and p←¬p flips the truth value of p. Note that both abbreviations have constant length, viz. 14.

Semantics Models of DL-PA are nothing but models of classical propositional logic, i.e., subsets of the set of propositional variables P, alias valuations. We sometimes write v(p) = 1 when ∈ v and v(p) = 0 when v. DL-PA programs are interpreted by means of a (unique) relation between valuations. For instance, suppose P = {p} and consider the atomic program π = p←⊤, and the two valuations v 1 = {} and v 2 = {p}. The execution of π relates v 1 to v 2 , and v 2 to itself. In other words, π is interpreted as

||π|| = {(v 1 , v 2 ), (v 2 , v 2 )}.
Atomic programs of the form p←⊤ and p←⊥ are interpreted as update operations on valuations, and complex programs are interpreted just as in PDL by mutual recursion. Table 1 gives the interpretation of the DL-PA connectives.

Two formulas ϕ 1 and ϕ 2 are formula equivalent

if ||ϕ 1 || = ||ϕ 2 ||. Two programs π 1 and π 2 are program equivalent if ||π 1 || = ||π 2 ||.
In that case we write π 1 ≡ π 2 . For example, the program equivalence π; skip ≡ π holds.

An expression is a formula or a program. When we say that two expressions are equivalent we mean program equivalence if we are talking about programs, and formula equivalence otherwise. Equivalence is preserved under replacement of a sub-expression by an equivalent expression [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF].

Eliminating the modal operators DL-PA formulas being interpreted through classical propositional logic valuations, modal operators can be eliminated. In order to do this, we (ϕ?) -≡ ϕ?

(π 1 ; π 2 ) -≡ π - 2 ; π - 1 (π 1 ∪ π 2 ) -≡ π - 1 ∪ π - 2 p←⊤ -≡ p?; (skip ∪ p←⊥) ≡ p? ∪ (p?; p←⊥) p←⊥ -≡ ¬p?; (skip ∪ p←⊤) ≡ ¬p? ∪ (¬p?; p←⊤)
p←q -≡ p←p if p = q p↔q?; (p←⊤ ∪ p←⊥) otherwise p←¬q -≡ p←¬p if p = q p⊕q?; (p←⊤ ∪ p←⊥) otherwise
Proposition 2. For every DL-PA formula ϕ there is an equivalent DL-PA formula ϕ ′ such that ϕ ′ is without (.) -and such that the length of ϕ ′ is linear in the length of ϕ.

Next, we remind the following key result: for conversefree DL-PA, every formula is equivalent to a boolean formula [START_REF] Herzig | A dynamic logic of normative systems[END_REF][START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF]. With Proposition 2 we obtain the following result for our present language with converse. Theorem 1. For every DL-PA formula there is an equivalent boolean formula.

For example, for different propositional variables r and p, the formula p←⊥ (p ∨ r) is successively equivalent to p←⊥ p ∨ p←⊥ r, to ⊥ ∨ r, and to r.

Note that the boolean formula might be exponentially longer than the original formula.

Validity and complexity results

A formula ϕ is DL-PA valid if it is equivalent to ⊤, i.e., if ||ϕ|| = 2 P . It is DL-PA sat- isfiable if it is not a formula equivalent to ⊥, i.e., if ||ϕ|| {}.
For example, the formulas p←⊤ ⊤ and p←⊤ ϕ ↔ ¬ p←⊤ ¬ϕ are DL-PA valid.

Due to Proposition 2, the complexity results of [START_REF] Herzig | A dynamic logic of normative systems[END_REF]) transfer to our extension with the converse operator: both model checking and satisfiability checking are PSPACE complete for our language.

Constructing extensions with DL-PA

Let us first show how the extensions of an argumentation framework can be constructed by means of DL-PA programs. Remember that such programs modify valuations: our aim is to define a program which sets the truth values of the variables representing the acceptance of an argument so that after the execution of that program, the formula characterizing the semantics holds. We first present a few definitions that will help us to define that program.

Sorting variables of L Att , ,In formulas For every L Att , ,In formula A we consider two sets: the set of attack variables occurring in A, noted ATT(A), and the set of accept variables occurring in A, noted IN(A). For example,

ATT(¬Att a,b ∨ In a ) = {Att a,b } and IN(¬Att a,b ∨ In a ) = {In a }.
It is the modifications of ATT(A) that will be minimized in order to construct the extensions, while the modifications of the set IN(A) will not be minimized: given the truth values of the attack variables, the semantics determines the truth values for the accept variables (or rather, the possible combinations of accept variables, because there may be several extensions).

Evaluating the difference between valuations The symmetric difference between two valuations v 1 , v 2 ⊆ P is the number of variables whose truth values differ, formally defined as

v 1 -v 2 = (v 1 \ v 2 ) ∪ (v 2 \ v 1 ) So v 1 -v 2 is the set of all those p such that v 1 (p) v 2 (p).
The Hamming distance between two valuations v 1 , v 2 ⊆ P is the cardinality of their symmetric difference: v 1 -v 2 is the number of all those p such that v 1 (p) v 2 (p). Example 3. Suppose two valuations: {p, q} and {q, r, s}. Their symmetric difference is {p, r, s} and their Hamming distance is 3.

Changing variables through DL-PA programs Let us consider the two following DL-PA programs that can change the truth value of one or more propositional variables in the finite subset P = {p 1 , . . . , p n } of the set of propositional variables P = ATT A ∪ IN A .

vary(P) = (p 1 ←⊤ ∪ p 1 ←⊥); • • • ; (p n ←⊤ ∪ p n ←⊥) flip1(P) = p 1 ←¬p 1 ∪ • • • ∪ p n ←¬p n
The intuitive meaning of program vary(P) is "the program is composed of a sequence of n steps and at each step i, the value of variable p i is nondeterministically set to either to true or false"; one may also say that vary(P) forgets the values of the variables in P. Second, program flip1(P) should be read as "one variable from P is randomly chosen and is nondeterministically set to either true or false". Observe that the programs vary(P) and flip1(P) ≤n are equivalent.

Note that the length of each program is linear in the cardinality of P.

The following lemma characterises the behaviour of the two programs in semantic terms. Lemma 1. The following hold:

1. (v 1 , v 2 ) ∈ ||vary(P)|| iff v 1 -v 2 ⊆ P 2. (v 1 , v 2 ) ∈ ||flip1(P)|| iff v 1 -v 2 = {p k } for some p k ∈ P
Given an L Att , ,In formula A, P A is defined as the set of variables from P occurring in A. The first item of Lemma 1 hence tells us that the program vary(P A ); A? accesses all relevant A-valuations (where 'relevant' means that only those A-valuations are accessed which keep constant the truth values of variables not occurring in A).

Example 4. Consider the formula A = In a ∧ ¬In b . The set of variables of A is P A = {In a , In b }. The models of A can be built by, first, varying the truth values of the variables of the formula (vary(P A )), and second, by testing which of the resulting valuations satisfy the formula, and by keeping them only (A?). vary(P A ) is here:

(In a ←⊤ ∪ In a ←⊥); (In b ←⊤ ∪ In b ←⊥)
Its execution relates each valuation for P A , i.e., each of {}, {In a }, {In b }, and {In a , In b }, to every other, including itself. Among the couples of valuations making up that relation, there is only one relating the model of A (that is, {In a }) to itself. So the execution of the test A? only keeps this pair in the relation. So the pair ({In a }, {In a }) is a possible execution of the program vary(P A ); A?.

Our example illustrates that the satisfiability of a boolean formula A can be expressed in DL-PA as the existence of valuation that is accessible by the program vary(P A ); A?, i.e., by means of the formula vary(P A ); A? ⊤ The formula says that there is a way of changing the truth value of some variables of A so that A is true afterwards. Lemma 2. Let A be a propositional formula. A is (propositionnally) satisfiable iff vary(P A ); A? ⊤ is DL-PA valid.

Defining extensions in DL-PA Let us now show how a DL-PA program can express in a concise and natural way the construction of extensions of an argumentation framework AF under a semantics σ. The program makeExt σ A below constructs the valuations representing extensions w.r.t. a semantics σ, of argumentation frameworks over the set of arguments A. Remember that the set of attack variables is ATT A , that the set of accept variables is IN A , and that σ is either stable, complete, or admissible acceptability semantics. We define the DL-PA program makeExt σ A as follows:

makeExt σ A = vary(IN A ); Semantics σ A ?
The following result says that if v 1 completely describes the attack relation then the set of accept variables of the valuations v 2 such that (v 1 , v 2 ) ∈ ||makeExt σ A || characterises the extensions of AF w.r.t. semantics σ. It is a consequence of Corollary 1 and Lemma 2. Lemma 3. Let AF be an argumentation framework. Let σ be either the stable, complete or admissible semantics. Let v 1 be a model of

Th AF . Then (v 1 , v 2 ) ∈ ||makeExt σ A || iff v 2 is a model of Th AF ∧ Semantics σ A .
Lemma 3 entails that we can construct all the extensions of a given argumentation system w.r.t. some semantics by means of a DL-PA program. Proposition 3. Let AF = (A, R) be an argumentation framework and let C be a boolean formula. The boolean formula Th AF ∧ Semantics σ A → C is propositionally valid if and only if the DL-PA formula Th AF → [makeExt σ A ]C is valid. Moreover, the equivalence

Th AF ∧ Semantics σ A ↔ (makeExt σ A ) -Th AF is DL-PA valid.

According to Proposition 3, given a description of the attack relation, program makeExt σ

A can construct valuations where the formula describing the semantics is true, and so in a way such that only acceptance variables are changed, while the attack variables do not change. Note that the equivalence takes care of situations where there is no extension. Let the L Att , ,In formula A be a goal, i.e., a boolean formula that should be satisfied by the extensions of some AF. By means of the program makeExt σ A one can check what has been called σ-consistency in (Coste-Marquis et al. 2013): whether there exists an argumentation framework AF such that some or every extension w.r.t. σ satisfies A. Adopting the standard terms for characterizing a justification state, we distinguish the notions of credulous and skeptical consistency.

Definition 1 (σ-consistency). Let AF = (A, R) be an argumentation framework, let σ be either the stable, admissible, or complete semantics. The L Att , ,In formula A is σ-

credulously-consistent for A iff makeExt σ A A is satisfiable; A is σ-skeptically-consistent for A iff [makeExt σ A ]A is sat- isfiable.
Example 5. Consider the set of arguments A 2 = {a, b} and the goal A = ¬In a ∧ ¬In b ∧ ¬Att a,a . Then makeExt σ A A is unsatisfiable; in particular, it is false in every valuation for Th AF 2 of Example 1. Therefore the formula A is stablecredulous inconsistent for A 2 .

To sum it up, we have shown how extensions can be constructed through programs modifying propositional variables. In the next section we show how to modify an argumentation framework and its extensions.

Modifying an argumentation framework

We start by discussing several kinds of modifications of an argumentation framework AF and then focus on the most involved family of operations: modifications enforcing a goal either in all extensions or in some extension of AF.

Generally speaking, when we want to incorporate a new piece of information A into a belief base B then we want to build a new belief base that retains as much as possible the initial beliefs of B while entailing A. Neither AGM theory [START_REF] Alchourrón | On the logic of theory change: Partial meet contraction and revision functions[END_REF] nor KM [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF] theory provide a single, concrete belief change operation: they rather constrain the set of 'reasonable' belief change operations by means of a set of postulates. Several concrete belief change operations satisfying the AGM or KM postulates have been defined in the literature. Among the most prominent are Winslett's 'possible models approach' (PMA) [START_REF] Winslett | Reasoning about action using a possible models approach[END_REF][START_REF] Winslett | Updating Logical Databases[END_REF]), Forbus's update operation [START_REF] Forbus | Introducing actions into qualitative simulation[END_REF]), Winslett's standard semantics (WSS) [START_REF] Winslett | Updating logical databases[END_REF], and Dalal's revision operation [START_REF] Dalal | Investigations into a theory of knowledge base revision: preliminary report[END_REF]; see [START_REF] Herzig | Propositional belief base update and minimal change[END_REF][START_REF] Lang | Belief update revisited[END_REF]) for an overview. According to Katsuno and Mendelzon's distinction between update and revision operations [START_REF] Katsuno | On the difference between updating a knowledge base and revising it[END_REF], the first three are update operations, usually written ⋄, while Dalal's is a revision operation, usually written * .

Kinds of change Several kinds of modifications of a given argumentation framework AF = (A, R) have been distinguished (Cayrol, Dupin de Saint Cyr Bannay, and Lagasquie-Schiex 2010):

1. One may modify the set of arguments A by adding or removing an argument.

2. One may modify the attack relation R by adding or removing an edge between two arguments.

3. One may wish to modify the extensions of AF.

The first kind of operation, viz. adding an argument to the set of arguments A or removing it, requires more linguistic resources than our language L Att , ,In provides; we will sketch a way of implementing it in DL-PA in an augmented language in the end of the paper.

Addition and removal of an attack edge between two arguments a, b ∈ A are rather simple operations: we just add or subtract (a, b) from R. In our logical representation, these operations correspond to making propositional variables true or false: the addition of (a, b) to R can be implemented by the update of Th AF by Att a,b , and the removal of (a, b) from R can be implemented by the update of Th

Th AF ⋄ Att a,b = Att a,b ←⊤ -Th AF Th AF ⋄ ¬Att a,b = Att a,b ←⊥ -Th AF
where ⋄ is any of the above belief change operations. Once Th AF has been updated by some Att a,b or ¬Att a,b , the extensions of the resulting framework can be obtained by conjoining the result with Semantics σ A . Adding an argument to extensions or removing it is more involved because it has to be achieved indirectly, by changing the underlying attack relation of AF (or by changing the set of arguments, but as we said, we disregard this option for the time being). Moreover, when an argumentation framework has several extensions, one may wish to change the justification status of a, so that it be skeptically justified (that is, added in all the extensions), or credulously justified (added in at least one extension), or credulously justified but not skeptically justified (added in at least one extension, but removed from at least one), or even not credulously justified (removed from all extensions).

While the distinction between update and revision was irrelevant for the modification of the attack relation, it gets important when it comes to the modification of extensions: which operation should we apply? We dedicate the next section to the problem of modifying an extension.

The modification of extensions In order to discuss which change operation is the most appropriate, let us consider again the above argumentation framework AF 2 = (A 2 , R 2 ) and the stable semantics. AF 2 has two stable extensions E a = {a} and E b = {b}. We have seen that the associated boolean formula Th AF 2 ∧ Stable A 2 has two L Att , ,In models:

v a = {Att a,b , Att b,a , In a } v b = {Att a,b , Att b,a , In b }
Suppose we wish to modify AF 2 such that a is in none of its stable extensions. What we have to do is to adapt the attack relation of AF 2 in a way that is minimal and that guarantees that a does not occur in any of its extensions, while guaranteeing that a is rejected. We view minimality as minimality of the number of modifications of the attack relation; in contrast, the current extensions may be modified in a nonminimal way. This policy agrees with [START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF], where the minimization of the changes on the attack relation is considered to be secondary.

What we do is to modify the models of Th AF 2 ∧ Stable A 2 one by one so that In a holds: we minimally modify the attack variables such that the result is stable. As we can see, enforcing a constraint is similar to update and we will hereafter commit to this reading.

To sum up, enforcing A consists in minimally updating the attack relation of an initial argumentation framework AF = (A, R) with respect to some goal A in a way such that A holds in all of the extensions of the resulting AF ′ = (A, R ′ ). Another perspective is however possible, too, where enforcing consists in minimally modifying the attack relation such that A holds in some of the extensions of the resulting AF ′ = (A, R ′ ). This operation seems to be closer in spirit to a revision operation. So 'enforcement' can be understood in two different ways, leading to two different definitions. In both cases, there is a key difference with standard revision and update operations: in classical belief change, output is limited to one belief set, while here, several AF ′ may be produced by the enforcement operations. Let AF ⋄ Cred,σ A denote the credulous enforcement of property A in AF w.r.t. semantics σ, and let AF ⋄ Skep,σ A denote the skeptical enforcement of property A in AF. We consider that both⋄ Cred,σ and ⋄ Skep,σ are operations mapping an argumentation framework and an L Att , ,In formula to a set of argumentation frameworks.

In line with the definitions of classical revision and update operations, we now define some postulates that 'reasonable' operations ⋄ should satisfy. They are mainly inspired by [START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF].

We have shown above that both attack relations and σconsistency can be captured by DL-PA formulas. As moreover the goal A is an L Att , ,In formula, too, our postulates can be formulated in terms of DL-PA formulas.

Definition 2 (enforcement postulates). Let ⋄ be an operation mapping an argumentation framework and an L Att , ,In formula to a set of argumentation frameworks. Let σ be either the stable, admissible, or complete semantics. The operation ⋄ is a credulous enforcement operation iff it satisfies the following postulates:

E1.C For all AF ′ ∈ AF ⋄ σ A, | = Th AF ′ → makeExt σ A A. E2.C If | = Th AF ∧ Semantics σ A → makeExt σ A A then AF ⋄ σ A = {AF}. E3 If | = A 1 ↔ A 2 then for every AF 1 ∈ AF ⋄ σ A 1 there exists AF 2 ∈ AF ⋄ σ A 2 such that | = Th AF 1 ↔ Th AF 2 .
The operation ⋄ is said to be a skeptical enforcement operation iff it satisfies postulate E3 plus the following:

E1.S For all AF ′ ∈ AF ⋄ σ A, | = Th AF ′ → [makeExt σ A ]A. E2.S If | = Th AF ∧ Semantics σ A → [makeExt σ A ]A then AF ⋄ σ A = {AF}.
The postulates E1.C and E1.S say that success in required for credulous and skeptical enforcement E2 represents a minimal change principle: it states that if A already holds then AF is unchanged. Postulate E3 is the postulate of syntax independence: enforcement should be based on the content of a goal and not on its syntax.

Additional postulates may be formulated; see [START_REF] Bisquert | Enforcement in Argumentation is a kind of Update[END_REF][START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF]) for more details. A key difference is that we do not consider postulates based on the expansion operation. The main reason is that this operation is actually useless: first, if an attack has to be changed then expansion cannot be used because, as we have seen above, Th AF is complete for L Att . Now consider that an argument has to be enforced in a credulous way. We face two cases: (i) either the argument is already credulously acceptable and there is no reason to change the argumentation framework, or (ii) the argument is not credulously acceptable. Then as all possible extensions are considered, some attacks must be changed so that new extensions can be constructed (and A will then hold). The same reasoning can be made for skeptical acceptance.

Let us now show how DL-PA helps us to reason about enforcement.

Expressing extension modification in DL-PA

The aim of this section is to show how modification programs can be defined. These programs should satisfy the enforcement postulates that we have defined. Second, they should only minimally change the attack relations of an initial argumentation framework. As previously mentioned, enforcement is close to update, and we will root our programs in the update operations that guarantee minimal change. One of the most popular is Forbus's update operation [START_REF] Forbus | Introducing actions into qualitative simulation[END_REF], where minimal change involves counting how many variables have been changed. Our solution is strongly connected to it.

The Hamming distance predicate Let us define the DL-PA formula h(A, ≥m), where A is an L Att , ,In formula, P is a set of propositional variables, and m ≥ 0 is an integer:

h(A, P, ≥m) = ⊤ if m = 0 ¬ flip1(P) ≤m-1 A if m ≥ 1
We call h(A, P, ≥m) the Hamming distance predicate w.r.t. the set of variables P: it is true at a valuation v exactly when the A-valuations v ′ that are closest to v in the sense of the Hamming distance differ in at least m variables from v, where the computation of the distance only considers variables from the set P, while the other variables in P \ P keep their value. Proposition 4. Let v a valuation, A a boolean formula, P some set of propositional variables, and m ≥ 0. Then 1. v ∈ ||h(A, P, ≥m)|| iff the A-valuations that are closest to v w.r.t. P have Hamming distance at least m, i.e., iff

card(v -v ′ ) ≥ m for every v ′ ∈ ||A|| s.t. v -v ′ ⊆ P. 2. (v, v ′ ) ∈ ||h(A, P, ≥m)?; flip1(P) m ; A?|| iff v ′ is one of the A-valuations that is closest to v w.r.t. P, i.e., iff v ′ ∈ ||A|| and card(v -v ′ ) = m for every v ′ ∈ ||A|| s.t. v -v ′ ⊆ P.
It follows from the first item of Proposition 4 that when P equals P A then v ∈ ||h(A, P A , ≥m)|| iff the A-valuations that are closest to v have Hamming distance at least m, i.e., iff card(v -v ′ ) ≥ m for every v ′ ∈ ||A||. This is used in Forbus's udpate operation.

Forbus's update operation Forbus's update operation is based on minimization of the Hamming distance. First, the Forbus update of a valuation v by A is the set of those Avaluations whose Hamming distance to v is minimal. Second, the Forbus update of a belief base B by A collects the Forbus updates of all B-valuations by A.

The following DL-PA program performs Forbus's update operation:

forbus(A) = m≤card(P A ) h(A, P A , ≥m)?; flip1(P A ) m ; A?
The program nondeterministically chooses an integer m, checks if the Hamming distance to A-valuations is at least m and flips m of the variables of A. Finally, the test A? only succeeds for A-valuations.

Proposition 5. The formula C is true after the Forbus update of B by A if and only if B → [forbus(

A)]C is DL-PA valid.
Argumentation framework update The update of argumentation frameworks has some specificities: first, we are going to modify only the attack variables while leaving the accept variables unchanged; second, the target formula is not going to be a boolean formula, but a formula saying that A will be the case after building extensions. Let us define the program credEnf(A) modifying AF w.r.t. some semantics σ such that the boolean formula A ∈ L Att , ,In becomes true in some σ-extensions:

credEnf(A) = m≤card(ATT A ) h makeExt σ A A, ATT A , ≥m ?; flip1(ATT A ) m ; makeExt σ A A?
The following program enforces a constraint in a skeptical way.

skepEnf(A) = m≤card(ATT A ) h [makeExt σ A ]A, ATT A , ≥m ?; flip1(ATT A ) m ; [makeExt σ A ]A?
The length of these two programs is polynomial in the cardinality of A. (The cardinality of the set ATT A is quadratic in that of A and the length of (flip1(ATT A ) m is quadratic in that of A.)

To check whether C is true in all extensions of AF modified by A (for A, C ∈ L Att , ,In ) can then be done by checking whether the DL-PA formula Th AF → [skepEnf(A)]C is valid. In particular we have the following proposition which states that if there is a chance to get A by modifying the attack variables then the enforcement will succeed: Proposition 6.

| = [credEnf(A)] makeExt σ A A | = [skepEnf(A)][makeExt σ A ]A
The second key property is that an argumentation framework is unchanged if the goal already holds. Proposition 7. For every goal A that is credulously justified, the credulous update program does not change anything: )]C For every goal A that is skeptically justified, the skeptical update program does not change anything:

| = (Th AF ∧ makeExt σ A A ∧ C) → [credEnf(A
| = (Th AF ∧ [makeExt σ A ]A ∧ C) → [skepEnf(A)]C
The modified argumentation frameworks can be extracted from the formulas credEnf(A) -Th AF and skepEnf(A) -Th AF representing it in DL-PA (or rather, their reduction) by forgetting the accept variables, as proposed in [START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF]. This operation can be implemented in our framework by the program vary(IN A ). Definition 3 (⋄ σ,enf ). Let σ be either the stable, admissible, or complete semantics. Let enf be either the skepEnf or the credEnf program. Let ⋄ σ,enf be an operation mapping an argumentation framework and an L Att , ,In formula to a set of argumentation frameworks. The update of AF by A under σ and enf is

AF ⋄ σ,enf A = (A, R v ) : v ∈ || (enf(A)) -Th AF ||
where R v is the attack relation extracted from v, defined as

R v = {(a, b) : Att a,b ∈ v}.
The two preceding propositions guarantee that our enforcement operations satisfy the postulates. Theorem 2. Operation ⋄ σ,credEnf satisfies E1.C and E2.C. Operation ⋄ σ,skepEnf satisfies E1.S and E2.S. Both operations ⋄ σ,credEnf and ⋄ σ,skepEnf satisfy E3.

This result is actually not a surprise, given that our tool for enforcement is a variant of Forbus's update operation. Example 6. Let us take up the argumentation framework AF 2 of Example 1. Remember that AF 2 = (A 1 , R 2 ), with A 1 = {a, b} and R 2 = {(a, b), (b, a)} and that Th AF 2 = Att a,b ∧ Att b,a . Let us consider the stable semantics and suppose our goal is to enforce that a is always acceptable (skeptical enforcement). We disregard self-attacks for the sake of simplicity. The nondeterministic part m≤card(ATT A ) (. . .) of the program SkepEnf(In a ) changes one variable from Th AF 2 , either Att a,b or Att b,a . This corresponds to two candidate extensions: one where a only attacks b and one where b only attacks a. Only the former case gives valuations where a is always acceptable. Hence:

AF ⋄ Stable,skepEnf In a = (A 1 , {(a, b)})

Going Further

We have illustrated how DL-PA offers a fruitful framework for representing argumentation framework and reasoning about them. We now sketch several ways of extending our account.

Other argumentation semantics Our exposition focused on the stable, admissible, and complete semantics. This can however be generalized to every semantics Σ whose extensions can be characterized by a propositional formula Σ A built from the set of attack variables ATT A and the set of accept variables IN A . In the previous sections we have given DL-PA programs modifying valuations (that represent argumentation frameworks) in a minimal way and producing (representations of) extensions. Therefore all minimizationbased semantics can be handled in an elegant way, as well as all maximization-based semantics. Semantics such as the grounded semantics can then be described in terms of programs minimizing valuations.

Other update semantics The modification programs that we have defined in the present paper basically applies Forbus's update operation to the attack variables. It is possible to use other such operations, such as Winslett's Possible Models Approach (PMA) [START_REF] Winslett | Reasoning about action using a possible models approach[END_REF], or revision operations such as [START_REF] Dalal | Investigations into a theory of knowledge base revision: preliminary report[END_REF].

Other kinds of change Up to now we did not cover addition and removal of some argument from an argumentation framework. Let us sketch how this could be done in a fairly straightforward way in the framework of DL-PA. First of all, we have to add a further ingredient to argumentation frameworks: let us consider triples AF = (A 0 , A, R) where A ⊆ R×R as before, and moreover A 0 is a (possibly infinite) set such that A ⊆ A 0 . We think of A 0 as the background set of all possible arguments, while A is the set of all arguments that are currently under consideration. We have to modify the logical language L Att , ,In accordingly. First, we suppose that there are propositional variables Att a,b and In a for every a, b in the background set A 0 . Second, we add propositional variables Cons a , one per argument a ∈ A 0 , where Cons a reads "a is considered". Let us denote the resulting language by L Att , ,In,Cons . Then the theory of AF = (A 0 , A, R) is the boolean formula

Cons a       
So Th AF does not say anything about the arguments that are currently not under consideration: the models of Th AF have arbitrary truth values for Att a,b , Att b,a , In a , and Cons a as soon as a A.

The semantic definitions have to be adapted, too, and should only quantify over arguments in A, and not over those in A 0 . For stable semantics we get:

Stable A = a∈A         Cons a → In a ↔ ¬ b∈A (In b ∧ Att b,a )        
In this setting, the mere addition or deletion of an argument a can be achieved straightforwardly, viz. by changing the status of a from 'disregarded' to 'considered' by means of the assignments Cons a ←⊤ and Cons a ←⊥. Subsequently, the attack relation can be modified as sketched above: one has to first delete all the Att a,b and Att b,a such that b ∈ A, and then add the attack relation as desired.

Conclusion

The main result of this paper is the encoding of argumentation frameworks and their dynamics in DL-PA. More precisely, our contribution is threefold.

First, as long as argument acceptability can be expressed in propositional logic, finding acceptable arguments and enforcing acceptability can be done in DL-PA. Other logical frameworks allow capturing and computing argument acceptability (see [START_REF] Charwat | Implementing abstract argumentation a survey[END_REF]) for an overview), but few of them allow capturing and computing acceptability change as well.

Second, as DL-PA formulas can be rewritten as propositional logic formulas, the result of the modification of an argumentation framework is described by a propositional formula from the models of which one may retrieve the modified argumentation frameworks. Our proposal is hence more 'operational' than those of [START_REF] Bisquert | Enforcement in Argumentation is a kind of Update[END_REF][START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF]) because we use a formal logic encompassing the representation of change operations. Moreover, we consider not only credulous acceptability changes, as most of the current approaches do [START_REF] Baumann | What does it take to enforce an argument? minimal change in abstract argumentation[END_REF][START_REF] Coste-Marquis | On the revision of argumentation systems: Minimal change of arguments status[END_REF]), but skeptical acceptability change as well.

Third, our framework takes advantage of the complexity results for DL-PA: both model checking and satisfiability checking are in PSPACE. A closer look at the formulas expressing the modifications shows that the alternation of quantifications is bounded, which typically leads to complexity bounds at the second level of the polynomial hierarchy.

The richness of our framework makes it expandable to other kinds of changes, other update semantics, and other argumentation semantics beyond those that are detailed in the present paper. We plan to investigate this research avenue in future work. Proposition 2. For every DL-PA formula ϕ there is an equivalent DL-PA formula ϕ ′ such that ϕ ′ is without (.) -and such that the length of ϕ ′ is linear in the length of ϕ.

Proof. Given a formula ϕ, we choose some innermost converse operator (such that no other converse operator is in its scope) and apply the reduction axioms of Table 2 from the left to the right: the first three of them 'push the converse operator down' until it reaches an atomic program; in the final stage, we eliminate these atomic programs p←⊤ -and p←⊥ -by the last two reduction axioms.

Theorem 1. For every DL-PA formula there is an equivalent boolean formula.

Proof. Let ϕ be a DL-PA formula. By Proposition 2 there is an equivalent formula ϕ ′ without the converse operator. Then there is a boolean formula ϕ ′′ that is equivalent to ϕ ′ by Theorem 2 of [START_REF] Balbiani | Dynamic logic of propositional assignments: a well-behaved variant of PDL[END_REF].

Lemma 1. The following hold:

1. (v 1 , v 2 ) ∈ ||vary(P)|| iff v 1 -v 2 ⊆ P 2. (v 1 , v 2 ) ∈ ||flip1(P)|| iff v 1 -v 2 = {p k } for some p k ∈ P Proof.
For Item 1, if the set P = {p 1 , . . . , p n } is empty then ||vary(P)|| = ||skip|| and we are done. If it is a singleton then we have

||{p 1 }|| = ||p 1 ←⊤ ∪ p 1 ←⊥|| = ||p 1 ←⊤|| ∪ ||p 1 ←⊥|| = (v 1 , v 2 ) : v 2 = v 1 ∪ {p} ∪ (v 1 , v 2 ) : v 2 = v 1 \ {p} = (v 1 , v 2 ) : v 2 = v 1 -v 2 ⊆ {p}
Then the result for the general case of an arbitrary set of variables P should be clear (but the proof is a bit lengthy to spell out). For Item 2, if P is empty then ||flip1(P)|| = ||skip||. For a single flip we have: Proof. Suppose vary(P A ); A? ⊤ is DL-PA valid. Let v be some valuation. By the interpretation of the dynamic operator there exists a valuation v ′ such that (v, v ′ ) ∈ ||vary(P A ); A?||. This means that there exists a valuation v ′′ such that (v, v ′′ ) ∈ ||vary(P A )|| and (v ′′ , v ′ ) ∈ ||A?||. The latter means that v ′ ∈ ||A||: we have found a valuation where A is true.

The other way round, suppose A is propositionnally satisfiable, i.e., there is some A-valuation v A . Let v be an arbitrary valuation. Let v ′ A be the valuation which interprets the variables of A in the same way as v A and interprets the other variables in the same way as v: The other way round, let v 1 be a model of Th AF and suppose v 2 is a model of Th AF ∧ Semantics σ A . As Th AF is a complete theory for the ATT A variables, v 1 and v 2 give the same values to the ATT A variables. By Item 1 of Lemma 1, the set of valuations that can be accessed from v 1 via the program vary(IN A ) is made up of valuations which cover all possible variations of the truth values of the IN A variables, while giving the same truth values to the remaining variables, i.e., the ATT A variables. Proof. For Item 1, things are clear for m = 0, and we only consider the case m > 1.

From the left to the right, suppose v is a model of h(A, P, ≥m), i.e., of ¬ flip1(P) ≤m-1 A. Then there is no Avaluation v ′ such that (v, v ′ ) ∈ ||flip1(P)|| k , for some k < m. So by Lemma 1, for every valuation v ′ ∈ ||A|| such that v -v ′ ⊆ P we must have card(v -v ′ ) ≥ m.

From the right to the left, suppose for every valuation v ′ ∈ ||A|| such that v -v ′ ⊆ P we have card(v -v ′ ) ≥ m. Then by Lemma 1, there cannot be a v ′ such that (v, v ′ ) ∈ ||flip1(P)|| k for some k < m and v ′ ∈ ||A||. Therefore v must be a model of ¬ flip1(P) ≤m-1 A.

Item 2 then follows from Item 1 and Lemma 1.

  An abstract argumentation framework as defined by Dung in (Dung 1995) is a pair AF = (A, R) where A is a finite set of abstract arguments and R ⊆ A × A is a binary relation on A, called the attack relation: (a, b) ∈ R means that a attacks b. So an argumentation framework is a directed graph with arguments as vertices and attacks as edges.

Figure 1 :

 1 Figure 1: AF 1 (on the left) and AF 2 (on the right)

  AF by ¬Att a,b . 3 In DL-PA, the update of Th AF by Att a,b can be implemented by the program Att a,b ←⊤, and the update by ¬Att a,b by Att a,b ←⊥. Indeed, we have:

  ||p k ←¬p k || = ||(p k ?; p k ←⊥) ∪ (¬p k ?; p k ←⊤)|| = ||p k ?; p k ←⊥|| ∪ ||¬p k ?; p k ←⊤|| = {(v 1 , v 2 ) : p k ∈ v 1 and p k v 2 } ∪ {(v 1 , v 2 ) : p k v 1 and p k ∈ v 2 } = {(v 1 , v 2 ) : v 1 -v 2 = {p k }} Therefore ||flip1(P)|| = 1≤k≤n ||p k ←¬p k || = {(v 1 , v 2 ) : v 1 -v 2 = {p k } for some p k ∈ P} Lemma 2.Let A be a propositional formula. A is (propositionnally) satisfiable iff vary(P A ); A? ⊤ is DL-PA valid.

  v ′A = (v A ∩ P A ) ∪ (v ∩ (P \ P A )) This is clearly also an A-valuation. (Indeed, for every p that does not occur in ϕ we havev ∪ {p} ∈ ||ϕ|| iff v \ {p} ∈ ||ϕ||.) As v -v ′ A ⊆ P A we have (v, v ′ A ) ∈ ||vary(P A )|| by Item 1 of Lemma 1. And as v ′ A is an A-valuation we have (v ′ A , v ′ A ) ∈ ||A?||. So (v, v ′A ) ∈ ||vary(P A ); A?||, from which it follows that v ∈ || vary(P A ); A? ⊤||. As v was arbitrary, vary(P A ); A? ⊤ is DL-PA valid.Lemma 3 Let AF be an argumentation framework. Let σ be either the stable, complete or admissible semantics. Let v 1 be a model ofTh AF . Then (v 1 , v 2 ) ∈ ||makeExt σ A || iff v 2 is a model of Th AF ∧ Semantics σ A . Proof. Let v 1 be a model of Th AF and suppose (v 1 , v 2 ) ∈ ||makeExt σ A ||.Therefore there is a valuation that is accessible from v 1 via the relation ||vary(IN A ); Semantics σ A ?|| and from which v 2 can be accessed via ||Semantics σ A ?||. As the test program Semantics σ A ? does not modify any truth value that valuation must be v 2 itself, which moreover must be a model of Semantics σ A . By Item 1 of Lemma 1, v 2 differs from v 1 only by the truth values of the IN A variables and has the same truth values for the ATT A variables. Therefore v 2 is also a model of Th AF .

we denote the associated propositional formula describing the semantics by Semantics σ . Corollary 1. Let AF = (A, R) be an argumentation frame- work. Let σ be a semantics. Let C ∈ L Att , ,In be a formula describing some property of A. All extensions of AF have property C if and only if Th AF ∧ Semantics σ

  , connects extensions and valuations.

	Proposition 1. Let AF = (A, R) be an argumentation
	framework and let E ⊆ A. Consider the valuation v E =
	{Att a,b : (a, b) ∈ R} ∪ {In a : a ∈ E}.
	1. E is a stable extension of AF if and only if v E is a model
	of Th AF ∧ Stable A .
	2. E is an admissible set of AF if and only if v E is a model
	of Th AF ∧ Adm A .
	3. E is an complete extension of AF if and only if v E is a
	model of Th AF ∧ Complete A .
	Given a definition of a semantics σ (either stable, admis-
	sible, or complete), A → C is valid.
	Example 2. Let us consider again Example 1. AF 1 has a
	single stable extension {a}, two admissible extensions {} and
	{a}, and one complete extension {a}; that is:

Table 2 :

 2 Reduction axioms for the converse operator first eliminate the converse operator. Table2lists the relevant program equivalences (aka reduction axioms). Iterating their application we can eliminate the converse operator with only linear increase in program size. For example, for assignments of variables to literals we have:

  Proofs Proposition 1. Let AF = (A, R) be an argumentation framework and let E ⊆ A. Consider the valuation v E = {Att a,b : (a, b) ∈ R} ∪ {In a : a ∈ E}. 1. E is a stable extension of AF if and only if v E is a model of Th AF ∧ Stable A . 2. E is an admissible set of AF if and only if v E is a model of Th AF ∧ Adm A . 3. E is an complete extension of AF if and only if v E is a model of Th AF ∧ Complete A . Let AF = (A, R) be an argumentation framework. Let σ be a semantics. Let C ∈ L Att , ,In be a formula describing some property of A. All extensions of AF have property C if and only if Th AF ∧ Semantics σ A → C is valid. Proof. According to Proposition 1, C is true in all extensions of AF if and only if C is true in every model of Th AF ∧ Semantics σ A , i.e., if and only if Th AF ∧ Semantics σ A → C is valid in classical propositional logic.

	Proof. These three items are propositions 5, 6, and 8 in
	(Besnard and Doutre 2004).
	Corollary 1.

  Therefore (v 1 , v 2 ) ∈ ||vary(IN A )||. And as v 2 is a model of Semantics σ A , we have (v 2 , v 2 ) ∈ ||Semantics σ A ?||. Putting things together, we have proved that (v 1 , v 2 ) ∈ ||vary(IN A ); Semantics σ A ?||. Proposition 4. Let v a valuation, A a boolean formula, P some set of propositional variables, and m ≥ 0. Then 1. v ∈ ||h(A, P, ≥m)|| iff the A-valuations that are closest to v w.r.t. P have Hamming distance at least m, i.e., iff card(v -v ′ ) ≥ m for every v ′ ∈ ||A|| s.t. v -v ′ ⊆ P. 2. (v, v ′ ) ∈ ||h(A, P, ≥m)?; flip1(P) m ; A?|| iff v ′ is one of the A-valuations that is closest to v w.r.t. P, i.e., iff v ′ ∈ ||A|| and card(v -v ′ ) = m for every v ′ ∈ ||A|| s.t. v -v ′ ⊆ P.

Admissibility is usually considered to be a building brick of other, stronger semantics, but we consider it here as a semantics on its own, the construction of admissible sets following the same process as the construction of extensions.

We note that the question whether this is an update or a revision does not really play a role here because we are in a simple situation: as far as the language L Att is concerned, the formula Th AF is complete (it has a unique model), and the update of complete theories by literals leads to the same result for all the belief change operations that we have mentioned, WSS, PMA, Forbus, and Dalal, be they update or revision operations.