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 parameterized propositional formula. When applied to a subset S of a given argumentation 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.
1. Introduction
This paper is a report on SESAME (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 [
The principle of such an encoding was introduced in [
Let us consider e.g. the stable semantics [
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, 8 a 2 S 8 bRa
b 26 S 8 a 2 A ✓ a 26 S ) 9 bRa b 2 S
◆
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
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.
Actually, the formula encoding stable extensions can be rewritten in many ways, e.g.
2Logical encoding of a statement “the argument b is in the set X” is denoted j (b2 X) in [
^ ✓ ◆ 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: ^ ✓ a2 A ¬a ! _ b bRa ◆! There remains to introduce the set F S 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 a2 A
¬a ! ^ ^ ¬b a2 S bRa _ b bRa !
^ R+(a) d=ef {b 2 A | aRb}; R (a) d=ef {b 2 A | bRa}.
s (A ,R),S =
^
a2 S
0
and all this leads us to a formula encoding stable extensions:
s (A ,R),S =
^ ^ ¬b
a2 S bRa
!
^
^ ✓
a2 A
¬a !
_ b
bRa
◆!
^
^ F S
Thus, the system requires the user to input an argumentation semantics as a combination
of principles (see [
V a ^ V ¬b a2 S b2 R (a)
}| ⌘{ (d ^ ¬ f ) ^ (e ^ > ) ^ z ⇣ ¬d ! f ^
V a2 A ¬a ! W b2 R (a) }| ¬e ! ? ^ ! b ¬ f ! (e _ f )
V{¬a | a 2 A \S} { ⌘ ^ z⇣ }| ⌘{ ¬ f
W b2 R (e) junction where > (resp. ? ) results from the empty conjunction
V b2 R (e) b) because no argument in A attacks e.
¬b (resp. the empty dise f
d
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 SESAME 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. 3The non-terminals are the phrases enclosed between h and i (see the grammar).
4It 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. 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 ^ h principlei.
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 5Even 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. 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 h seti hclassical-principlei ::= hseti is conflict-free | hseti satisfies admissibility | hseti satisfies reinstatement hattack-quantificationi ::= hquantifieri hargumenti ¬ hargumenti hmembership-quantificationi ::= hquantifieri hargumenti 2 h seti hinclusion-quantificationi ::= hquantifieri hseti ✓ h seti hoperatori ::= ^ | _ | ! hquantifieri ::= V | W 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 . 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. quant ifier V attack quantif ication
¬ argu ment a argu ment
a This decomposition tree (not visible by the user!) produces the formula Va¬ a Wb¬ a j (b2 S) and corresponds to an appropriate sequence of clicking upon development buttons: principle quant ifier W argu ment b attack quantif ication
¬
principle argu ment b 2 set S
development button hprinciplei hquantified-uponi hargumenti hargumenti At this point the current output is: development button hprinciplei hquantified-uponi hargumenti hargumenti At this point the current output is: ! ! ! ! choice from the scroll menu for all hquantified-uponi, hprinciplei h argumenti ¬ hargumenti a a choice from the scroll menu there exists hquantified-uponi such that hprinciplei h argumenti ¬ hargumenti b a 9. 10. 11. 12.
development button hprinciplei hargumenti hdomaini hseti At this point the output is final: s (A ,R),S (where j (b2 S) encodes the statement “b is in S”, see footnote 2) is the formula:6 ^ _ j (b2 S) ^ a¬ a b¬ a
^ F S 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: 6Let us repeat that V F S is not part of the user’s specification. Moreover, following the generic notation, F S = {j (a2 S) | a 2 S} [ {¬j (a2 S) | a 2 A \ S}. 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 [ h complex-seti hcomplex-seti \ h complex-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 h seti or hseti ✓ h seti. 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). 4.3. The ‘undo’ and ‘redo’ Buttons Immediately above the main white frame there is a series of buttons, of which the leftmost 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). 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 [
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 [
Moreover, we plan to extend the functionalities of the system so that, for example,
recursive semantics of various kinds [