Welcome to the system page of UNREAL, the realizability-tool for abstract argumentation. The development of UNREAL is supported by the project Abstract Dialectical Frameworks: Advanced Tools for Formal Argumentation.
UNREAL is a system based on answer set programming for deciding realizability of a given set of interpretations. It supports Dung's well-known abstract argumentation frameworks (AFs), abstract dialectical frameworks (ADFs), the subclass of bipolar ADFs (BADFs), and frameworks with sets of attacking arguments (SETAFs). For each of these formalisms, realizability can be tested for the main semantics, namely admissible, complete, preferred and two-valued models (stable semantics for (SET)AFs). More specifically, given a set of interpretations V, a formalism F and a semantics σ, UNREAL computes all knowledge bases κ of type F; having σ(κ) = V. Optionally, the output can be converted into the format readable by ASPARTIX or DIAMOND.
We provide an archive containing all encodings together with an executable shell-script. Moreover, the individual encodings are available below.
UNREAL requires the installation of an ASP solver supporting clingo 4 syntax (see potassco). Using the shell-script in the bundled archive even requires clingo to be executable.
The input file has to specify the set of interpretations that shall be realized. This is done by specifying the statements (s) and the interpretations (in). An interpretation is given as a list of Boolean assignments to statements; unspecified statements are assigned truth value u.
The following input encoding specifies a set of four interpretations over the three statements. It includes the interpretations mapping two statements to t and the other to u and the interpretation mapping all statements to u.
s(a).s(b).s(c). in((t(a),(t(b),(f(c),nil)))). in((t(a),(f(b),(t(c),nil)))). in((f(a),(t(b),(t(c),nil)))). in(nil).
Running this input encoding with UNREAL will reveal that only a few combinations of semantics and formalism will be able to realize this set of interpretations.
After downloading the bundled archive, the script can be used in the following way:
./unreal.sh [OPTION]... inputfile Options: -s --semantics Semantics among {adm,com,prf,mod} Default: prf -f --formalism Formalism among {af,setaf,badf,adf} Default: adf -t --translate Way of translation among {diamond,aspartix,none} diamond (default): Output diamond-instances aspartix: Output aspartix-instances (only compatible with formalism af) none: Output just the characterizations
The answer set solver has to be invoked with the input encoding, the main encoding, a semantics encoding and a formalism encoding (none is necessary if the formalism is ADF). If the σ-characerizations shall be returned then show.lp has to be included, for output in DIAMOND-format (resp. ASPARTIX-format) 2diamond.lp (resp. 2aspartix.lp has to be included. Note that a translation to ASPARTIX is only possible if AF is the selected formalism.
For computing all BADFs which realize the set of interpretations specified by input.lp under preferred semantics and returning them in DIAMOND-format, the respective call of clingo looks as follows:
> clingo -n 0 input.lp main.lp prf.lp badf.lp 2diamond.lp