SESAME

SEmantics Specification for Abstract arguMEntation

Introducing SESAME

Sesame logo 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.
SESAME has been developped at IRIT (Institut de Recherche en Informatique de Toulouse), in the context of the AMANDE project, funded by the French National Research Agency (ANR) as ANR-13-BS02-004 and the Fondation de Recherche pour l'Aéronautique et l'Espace (FRAE).

SESAME - example 1
S is conflict-free and satisfies both admissibility and reinstatement In short: S is a complete extension
SESAME - example 2
S is conflict-free and A ⊆(S ∪ ℜ⁺(S)) In short: S is a stable extension
SESAME - example 3
S is a minimal subset satisfying reinstatement
SESAME - example 4
For all bℜa, if a ∈ S then either there exists cℜb such that c ∈ S or there exists bℜb such that b ∈ A In short: Each argument that attacks S but is not attacked by S is self-attacking

Documents

SESAME – A System for Specifying Semantics in Abstract Argumentation Philippe Besnard, Sylvie Doutre, Van Hieu Ho and Dominique Longin In: First International Workshop on Systems and Algorithms for Formal Argumentation (SAFA'16), 2016
Encoding Argument Graphs in Logic Philippe Besnard, Sylvie Doutre, and Andreas Herzig In: 15th International Conference on Information Processing and Management of Uncertainty in Knowledge-Based Systems (IPMU'14), pp. 345--354, 2014 ​
Checking the acceptability of a set of arguments Philippe Besnard and Sylvie Doutre In: 10th International Workshop on Non-Monotonic Reasoning (NMR 2004) ​

FAQ

(1) What are the grammatical rules for specifying a semantics?

<semantics> ::= <principle>

<principle> ::= <classical-principle>
 | it isn't the case that <principle>
 | <principle> and <principle>
 | <principle> or <principle>
 | if <principle> then <principle>
 | there exists <quantified-upon> such that <principle>
 | for all <quantified-upon>, <principle>
 | <set> is the intersection of all subsets of A that satisfy <principle>
 | <set> is maximal w.r.t. <principle>
 | <set> is minimal w.r.t. <principle>
 | <complex-set> is a subset of <complex-set>
 | <argument> is in <domain>

<classical-principle> ::= <set> is conflict-free
 | <set> satisfies admissibility
 | <set> satisfies reinstatement

<quantified-upon> ::= <argument> ℜ <argument>
 | <argument> in <set>
 | <set> subset of <set>

<complex-set> ::= <domain>
 | <complex-set> union <complex-set>
 | <complex-set> intersection <complex-set>
 | A \ <complex-set>
 | ℜ⁺ <set>
 | ℜ⁻ <set>

<domain> ::= <set>
 | ℜ⁺ <argument>
 | ℜ⁻ <argument>

<set> ::= A | S | S1 | S2 | S3 | ...

<argument> ::= a | b | c | ... | x | y | z

<semantics> ::= <principle>


(2) At some point, not all symbols a, b, c,..., x, y, z or S1, S2, S3,...
are available to choose from?

S1, S2, S3,... are variables denoting sets of arguments.

So, they should only occur quantified.

When <principle> is developed into "<argument> is in <domain>", the scroll menu therefore only allows to choose between variables that are currently quantified.

By contrast, A and S are not variables (hence they can always be chosen to expand <set>).
 

(3) There is a warning pop-up "Would you really want to use ...?

When <quantified-upon> is developed, if a variable chosen for <argument> or <set> is already quantified, then there is a warning pop-up:
The user must decide whether the new occurrence of the variable introduces a new quantification, in which case the user must choose a fresh variable.

Example:
Assume that "For all a in S, there exists <quantified-upon> such that <principle>" is expanded by developing <quantified-upon> into "<argument> ℜ <argument>".
Assume further that the user chooses "b" to develop the first <argument> and chooses "a" to develop the second <argument>.
There is a warning pop-up "Would you really want to use a?".
If the user answers yes, then the result "For all a in S, there exists bℜa such that <principle>" means "For all a in S, there exists b of the kind bℜa such that <principle>".
In this case, the results means that for all a in S, an argument x satisfying aℜx must exist such that <principle> (parameterized by a, x) holds.
If the user answers no, then after the user chooses an alternative variable -say c- instead of a, the result will be "For all a in S, there exists bℜc such that <principle>".
Here, the result means that for all a in S, two arguments x and y satisfying xℜy must exist such that <principle> (parameterized by a, x, y) holds.

Download

January 30, 2017

Compiled version of SESAME:
  • Windows 32/64 bits  Download
  • MacOS 64 bits  Download
    Launch it by the following command line :
    java -jar -XstartOnFirstThread <app_path>/Sesame_osx.jar

Contact