=Paper=
{{Paper
|id=Vol-1672/paper_4
|storemode=property
|title=SESAME - A System for Specifying Semantics in Abstract Argumentation
|pdfUrl=https://ceur-ws.org/Vol-1672/paper_4.pdf
|volume=Vol-1672
|authors=Philippe Besnard,Sylvie Doutre,Van Hieu Ho,Dominique Longin
|dblpUrl=https://dblp.org/rec/conf/comma/BesnardDHL16
}}
==SESAME - A System for Specifying Semantics in Abstract Argumentation==
https://ceur-ws.org/Vol-1672/paper_4.pdf
S ESAME – A System for Specifying
Semantics in Abstract Argumentation
Philippe BESNARD a , Sylvie DOUTRE b,1 , Van Hieu HO c and Dominique LONGIN a
a IRIT, CNRS
b IRIT, University of Toulouse 1
c IRIT, University of Toulouse 3
Abstract. This is a report on an implemented system that allows the user to specify
an argumentation semantics and that returns a logical encoding in the form of a pa-
rameterized propositional formula. When applied to a subset S of a given argumen-
tation graph G, the instantiated formula is satisfiable if and only if S is an extension
for G according to the argumentation semantics specified by the user.
Keywords. Abstract argumentation, argumentation semantics, logical encoding.
1. Introduction
This paper is a report on S ESAME (SEmantics Specification for Abstract arguMEntation),
a system that allows the user to specify an argumentation semantics and that returns a
logical encoding in the form of a parameterized propositional formula [1]. When applied
to a given argumentation graph G = (A , R), for S ✓ A , the instantiated formula is
satisfiable if and only if S is an extension for G according to the argumentation semantics
specified by the user.
The principle of such an encoding was introduced in [1] (see also [2,3], see [4] for
an ASP variant) where a propositional formula s(A ,R),S is defined that turns out to be
satisfiable if and only if S is a s -extension of the argumentation graph (A , R). That is,
the formula s(A ,R),S encodes the argumentation semantics s .
Let us consider e.g. the stable semantics [5] and construct s(A ,R),S for s = stable.
Definition 1. Given an argumentation graph G = (A , R), a stable extension S ✓ A is
a set that satisfies the following two conditions:
1. there does not exist two arguments a and b in S such that aRb;
2. for each argument a 62 S, there exists b 2 S such that bRa.
That a set of arguments S satisfies the first condition amounts to: for all a in S, for
all b attacking a, it is not the case that b is in S. In symbols,
8a 2 S 8bRa b 62 S
1 Corresponding Author: Sylvie Doutre, University of Toulouse 1, Toulouse, France; E-mail:
sylvie.doutre@irit.fr.
40
The statement b 2 S can be encoded2 through identifying b with a propositional symbol
(letting the propositional symbol b to be read “b is in S”), hence an encoding for the
statement that S satisfying condition 1. is
^ ^
¬b (1)
a2S bRa
As to the second condition for S to be a stable extension, it can be expressed by: for all a
in A , if a is not in S then there exists some b attacking a such that b is in S.
✓ ◆
8a 2 A a 62 S ) 9bRa b 2 S
The statement b 2 S is again to be encoded via identifying b with a propositional symbol,
and, similarly, a 2 S is encoded as a. Hence, an encoding for the statement that S satisfies
condition 2. is
✓ ◆
^ _
¬a ! b (2)
a2A bRa
Conjoining (1) and (2), we obtain a subformula (of s(A ,R),S ) expressing that S meets
conditions 1. and 2. for being a stable extension:
! ✓ ◆!
^ ^ ^ _
¬b ^ ¬a ! b (3)
a2S bRa a2A bRa
There remains to introduce the set FS of literals expressing that all elements of S are in
S and that all elements not in S fail to be in S, as follows
def
FS = {a | a 2 S} [ {¬a | a 2 A \ S}
and all this leads us to a formula encoding stable extensions:
! ✓ ◆!
^ ^ ^ _ ^
s(A ,R),S = ¬b ^ ¬a ! b ^ FS (4)
a2S bRa a2A bRa
Thus, the system requires the user to input an argumentation
V
semantics as a combination
of principles (see [6] for the notion) —excluding FS which is transparent to the user.
Notation. Quantifying over attacks relative to an argument can easily be turned into
quantifying over membership in R+ (·) and R (·) according to the next definition:
def
R+ (a) = {b 2 A | aRb};
def
R (a) = {b 2 A | bRa}.
Actually, the formula encoding stable extensions can be rewritten in many ways, e.g.
s(A ,R),S =
0 1 0 1
^ ^ ^ _ ^
@a ^ ¬bA ^ @¬a ! bA ^ {¬a | a 2 A \ S} (5)
a2S b2R (a) a2A b2R (a)
2 Logical encoding of a statement “the argument b is in the set X” is denoted j
(b2X) in [3] for genericity.
41
2. Logical Encoding of Argumentation Semantics
For a given semantics, s(A ,R),S represents a class of formulas each of which is induced
from s(A ,R),S by considering a particular argumentation graph (A , R) and S ✓ A .
It just takes to unfold s(A ,R),S according to the actual values taken by A , R and S.
Example 1. As to s =stable, for A = {d, e, f } with {eR f , f Rd, f R f } (see Figure 1),
for the case S = {d, e} which is a stable extension, instantiating s(A ,R),S (using the
version of Equation (5) for readability reasons) yields the satisfiable formula:
! !
V V V W
a^ ¬b ¬a ! b V
{¬a | a 2 A \S}
a2S b2R (a) a2A b2R (a)
z⇣ }| ⌘{ z⇣ }| ⌘{ z⇣ }| ⌘{
(d ^ ¬ f ) ^ (e ^ >) ^ ¬d ! f ^ ¬e ! ? ^ ¬ f ! (e _ f ) ^ ¬ f
V
where > (resp. ?) results from the empty conjunction ¬b (resp. the empty dis-
b2R (e)
W
junction b) because no argument in A attacks e.
b2R (e)
e f d
Figure 1. The argumentation graph (A , R) of Example 1
In s(A ,R),S , all the atomic formulas encode a statement of the form “the argument
a is in the set X” where a is a variable denoting an argument of A and X is a variable
denoting a subset of A . These are the only primitive statements that can appear in the
semantics specified by the user. In the semantics s , such statements can be conjuncted,
negated, etc, arguments can be quantified over, sets of arguments can be maximized, etc.
Most importantly, S denotes a distinguished set: S denotes the subset of A to be
tested for being a s -extension.
3. Introducing the System
The main step in specifying an argumentation semantics via S ESAME is developing
a decomposition tree (from the grammar given in Section 3.1). This can be done by
the user, by clicking upon the buttons in the left part of the screen (they are called
development buttons – see Figure 2). When the user clicks upon one of these buttons,
the current non-terminal3 is expanded according to the derivation labelling the button.
As an illustration, when the user clicks upon the button hprinciplei, a scroll menu is
displayed that indicates what chains are available to replace hprinciplei, namely “it isn’t
the case that hprinciplei” or “hprinciplei and hprinciplei” or . . . (see Figure 3).
After the user has selected her choice, the system updates the current expression
(in semi-natural language) of the decomposition tree displayed in the main white frame.
The formula4 to be generated (it is displayed in the lower white frame) is duly updated.
3 The non-terminals are the phrases enclosed between h and i (see the grammar).
4 It is rather a pseudo-formula containing items such as hprinciplei as long as the user is not finished with
specifying the argumentation semantics of hers.
42
Figure 2. The home screen
Figure 3. The principle ‘It is not the case that’ is selected
43
Figure 4. After a principle has been selected, the corresponding formula (lower white frame) is updated
For example, “it is not the case that hprinciplei” gives rise to the formula ¬ hprinciplei
(see Figure 4) and “hprinciplei and hprinciplei” gives rise to hprinciplei ^ hprinciplei.
Assume for example that the current non-terminal is hclassical-principlei. As the
user clicks upon the development button labelled hclassical-principlei, a scroll menu is
displayed (see Figure 7) which indicates that hclassical-principlei can be replaced by
“hseti is conflict-free” or “hseti satisfies admissibility” or “hseti satisfies reinstatement”.
After choosing one of these three options, the user will eventually have to specify hseti
by clicking upon the development button labelled hseti (see Figure 2) etc.
3.1. Grammar
The range of argumentation semantics that the user can specify is given by means of the
grammar below. Moreover, the way the user can specify an argumentation semantics is
constrained as discussed in Section 2: The grammar only accepts primitive statements of
(non-)membership in X for some variable X denoting a set of arguments. An example is
for all a and b such that aRb, if a is in S then b is not in S.
A counter-example is the same semantics, when expressed as follows:
for all a in S, if b is in S then aRb fails.
The latter does not conform with the grammar since it resorts to a statement (i.e. aRb)
that fails to be a membership statement as required.5 Let us repeat that all the primitive
5 Even when aRb is expressed as b 2 R+ (a) or as a 2 R (b) because neither R+ (a) nor R (b) is a variable.
44
Figure 5. The principle ‘classical-principle’ is selected
statements to be encoded must be of the kind a is in X where a is a variable referring to
an argument and X is either A or S or a variable referring to a subset of the arguments.
hsemanticsi ::= hprinciplei
hprinciplei ::= hclassical-principlei
| ¬ hprinciplei
| hprinciplei hoperatori hprinciplei
| hattack-quantificationi hprinciplei
| hmembership-quantificationi hprinciplei
| hinclusion-quantificationi hprinciplei
| hargumenti 2 hseti
hclassical-principlei ::= hseti is conflict-free
| hseti satisfies admissibility
| hseti satisfies reinstatement
hattack-quantificationi ::= hquantifieri hargumenti ¬ hargumenti
hmembership-quantificationi ::= hquantifieri hargumenti 2 hseti
hinclusion-quantificationi ::= hquantifieri hseti ✓ hseti
hoperatori ::= ^ | _ | !
V W
hquantifieri ::= |
hseti ::= A | S | S1 | S2 | . . .
hargumenti ::= a | b | c | . . . | x | y | z
A and S are parameters, all the other non-logical terminals in the grammar are variables:
a, b,. . . , y, z, S1 , S2 ,. . . In particular, a, b, . . . , y, z is not a list of arguments of A .
45
Figure 6. A classical-principle must be chosen
The user is to input her argumentation semantics by clicking upon development buttons
so as to construct a decomposition tree for the grammar. Assume e.g. that the user is to
define the principle that every self-attacking argument is attacked by an argument of S.
principle
attack principle
quantif
ication
attack principle
quant argu ¬ argu quantif
ifier ment ment ication argu 2 set
V ment
a a S
quant argu ¬ argu
b
ifier ment ment
W
b a
V W
This decomposition tree (not visible by the user!) produces the formula a¬a b¬a j(b2S)
and corresponds to an appropriate sequence of clicking upon development buttons:
46
development button choice from the scroll menu
1. hprinciplei ! for all hquantified-uponi, hprinciplei
2. hquantified-uponi ! hargumenti ¬ hargumenti
3. hargumenti ! a
4. hargumenti ! a
At this point
the current
output is:
development button choice from the scroll menu
5. hprinciplei ! there exists hquantified-uponi such that hprinciplei
6. hquantified-uponi ! hargumenti ¬ hargumenti
7. hargumenti ! b
8. hargumenti ! a
At this point
the current
output is:
47
development button choice from the scroll menu
9. hprinciplei ! hargumenti 2 hdomaini
10. hargumenti ! b
11. hdomaini ! hseti
12. hseti ! S
At this point
the output is
final:
s(A ,R),S (where j(b2S) encodes the statement “b is in S”, see footnote 2) is the formula:6
^ _ ^
j(b2S) ^ FS
a¬a b¬a
4. Features of the System
4.1. Scroll Menus for Development Buttons
As development buttons correspond to non-terminals of the grammar, the items in the
scroll menu attached to the button are the grammar rule(s) expanding the non-terminal.
For instance, the scroll menu for hargumenti displays the list a, b, . . . , y, z and the scroll
menu for hseti displays an initial series of the list S1 , S2 , . . . Also, the scroll menu for
hclassical-principlei displays three items (see Figure 7).
As an exception, not all options in the scroll menu for hprinciplei are grammar rules
expanding hprinciplei. The extra options can be viewed as macros explicited in order to
help the user. For instance, the grammar allows the user to specify that a subset of A
is maximal for satisfying hprinciplei. A casual user is not expected to figure out how to
express this through the grammar. So, the scroll menu for hprinciplei includes the items:
6 Let us repeat thatV
FS is not part of the user’s specification. Moreover, following the generic notation,
FS = {j(a2S) | a 2 S} [ {¬j(a2S) | a 2 A \ S}.
48
Figure 7. A classical-principle is being chosen
hseti is maximal wrt hprinciplei
hseti is minimal wrt hprinciplei
hseti is the intersection of all subsets of A that satisfy hprinciplei
The grammar allows the user to specify ¬+ (a) ✓ ¬ (b)[(A \S) and other set-inclusion
statements but only in a convoluted way. The system is to alleviate the burden on the user
by providing her with appropriate items. Hence the scroll menu for hprinciplei includes:
hcomplex-seti is a subset of hcomplex-seti
This is why there is a development button labelled hcomplex-seti whose scroll menu is:
hdomaini
A \ hcomplex-seti
hcomplex-seti [ hcomplex-seti
hcomplex-seti \ hcomplex-seti
and there is a development button labelled hdomaini whose scroll menu displays:
hseti
¬+ hargumenti
¬ hargumentti
Also, the scroll menu for hprinciplei factors the three cases hattack-quantificationi,
hset-quantificationi, and hinclusion-quantificationi by means of the two items “for all
hquantified-uponi” and “there exists hquantified-uponi” where hquantified-uponi is to be
expanded to either hargumenti ¬ hargumenti or hargumenti 2 hseti or hseti ✓ hseti.
49
4.2. Current Non-terminal: Highlighted Development Button
At any time, the non-terminal to be developed next is highlighted (blue inverse video).
By default, the order in which the non-terminals are developed is depth-first, left to right.
However, the browsing buttons (see Figure 8) allow the user to override the default order
and to freely choose the next non-terminal to be developed. Also, depending on which
non-terminal is highlighted, a development button is enabled but the other development
buttons are disabled (shadow display).
Figure 8. The buttons allowing to browse among non-terminals of the main white frame
4.3. The ‘undo’ and ‘redo’ Buttons
Immediately above the main white frame there is a series of buttons, of which the left-
most two are undo and redo (see Figure 9). They allow the user to navigate through any
step between the current state of the decomposition tree and its initial state. Of course,
undo goes backward one step and redo goes forward one step (up to the current state).
Figure 9. The ‘undo’ and ‘redo’ buttons
4.4. Output Files Menu
The File button offers a pull-down menu with an import item and various export options.
The first option stores an output file .txt with the content of the main white frame
(that is, an expression of the user’s argumentation semantics in semi-natural language).
The second option stores an output file .tex with the LATEX source of the content of the
lower main frame (i.e., the formula s(A ,R),S in LATEX). The third option stores an output
file .jpg of the image of the LATEX display of s(A ,R),S . An option stores an output file
.sesame with s(A ,R),S in internal format —that the import item of the menu downloads.
Lastly, there is an option that stores an output file .touistl of s(A ,R),S in the format
of TouIST [7] which is a front-end for various SAT solvers. Indeed, a future version of
our system will have a procedure permitting the user to input an argumentation graph
(A , R) and S ✓ A (also possibly varying (A , R) and S while still considering the same
semantics s ) so that s(A ,R),S gets instantiated by A , R, S and fed to a SAT solver,
thereby automatically informing the user whether the set S is a s -extension of (A , R).
4.5. A Semantics . . . or not?
The system achieves syntactical checking as it ensures that the specification entered by
the user conforms with the grammar (e.g., the system makes it impossible that the input
involves a statement of the form “the subset X of A is in the argument a”). Yet, there is no
semantical check and it is largely possible for the user to input some dubious semantics
(e.g., a “semantics” requiring that all self-attacking arguments are in S).
50
5. Conclusion and Perspectives
We have shortly described S ESAME, a system (see www.irit.fr/SESAME) implemented
in Java. It allows the user (guided by a simple BNF grammar) to specify an argumentation
semantics s , for which the system generates a propositional formula s(A ,R),S that turns
out to be satisfiable if and only if S is a s -extension of the argumentation graph (A , R).
Such an argumentation semantics must conform to the grammar, and this may require
some ingenuity from the user. The reason is that there are usually many ways to specify
an argumentation semantics but the user must find out how to express hers in a way
accepted by the grammar. To some extent, the system alleviates the burden on the user
by allowing the user not to conform strictly to the rules of the grammar (but the system
ensures that the user conforms with the language generated by the grammar).
When instantiated by a specific argumentation graph (A , R) and set S, the formula
generated by SESAME may be fed to a SAT solver. Of course, such an approach is not
meant to compete with optimized systems e.g. from ICCMA [8]. However, the ICCMA
argumentation graphs benchmark may provide interesting instantiations allowing new
semantics to be tested on a wide and diverse range of small argumentation graphs.
Moreover, we plan to extend the functionalities of the system so that, for example,
recursive semantics of various kinds [9] can be specified (as to now, classical semantics
captured by S ESAME include grounded, complete, preferred, semi-stable, stage, ideal).
Acknowledgements. This work benefited from the support of the AMANDE project
(ANR-13-BS02-0004) of the French National Research Agency (ANR).
References
[1] Philippe Besnard and Sylvie Doutre, Checking the Acceptability of a Set of Arguments, Proc. of the 10th
Int. Workshop on Non-Monotonic Reasoning (NMR’04), James Delgrande and Torsten Schaub (editors),
pp. 59–64, Whistler, B.C., Canada, 2004.
[2] Michal Walicki and Sjur Dyrkolbotn, Finding Kernels or Solving SAT, Discrete Algorithms, 10 (2012),
146–164.
[3] Philippe Besnard, Sylvie Doutre, and Andreas Herzig, Encoding Argument Graphs in Logic, Proc. of the
15th Int. Conference on Information Processing and Management of Uncertainty in Knowledge-Based
Systems (IPMU’14), Anne Laurent, Olivier Strauss, Bernadette Bouchon-Meunier and Ronald Yager
(editors), volume 443 of Communications in Computer and Information Science, pp. 345–354 (Part II),
Montpellier, France, 2014.
[4] Uwe Egly, Sarah Gaggl, and Stefan Woltran, Answer-Set Programming Encodings for Argumentation
Frameworks, Argument and Computation, 1, (2010), 147–177.
[5] Phan Minh Dung, On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Rea-
soning, Logic Programming and n-person Games, Artificial Intelligence, 77 (1995), 321–357.
[6] Pietro Baroni and Massimiliano Giacomin, On Principle-based Evaluation of Extension-based Argu-
mentation Semantics, Artificial Intelligence, 171, (2007), 675–700.
[7] Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba, Olivier Lezaud,
Frédéric Maris, and Maël Valais, Twist your Logic with TouIST, Proc. of the 4th Int. Congress on Tools
for Teaching Logic (TTL’15), Antonia Huertas, João Marcos, Marı́a Manzano, Sophie Pinchinat and
François Schwarzentruber (editors), Rennes, France, 2015.
[8] Matthias Thimm and Serena Villata (editors), Systems Descriptions of the 1st Int. Competition on Com-
putational Models of Argumentation (ICCMA’15), 2015. ArXiv:1510.05373.
[9] Pietro Baroni and Massimiliano Giacomin, Semantics of Abstract Argument Systems, in Argumentation
in Artificial Intelligence, Guillermo Simari and Iyad Rahwan (editors), pp. 25–44, 2009, Springer.
[10] Günther Charwat, Wolfgang Dvorák, Sarah Alice Gaggl, Johannes Peter Wallner, Stefan Woltran, Meth-
ods for Solving Reasoning Problems in Abstract Argumentation –A Survey, Artificial Intelligence, 220,
(2015), 28-63.
51