Competition Format and Rules
The competition will be feature seven main tracks, one for each semantics. Each of these tracks is composed of 4 (resp. 2 for single-status semantics) tasks, one for each reasoning task. A special track, Dung's Triathlon, will be conducted in order to have a reasoning task including several semantics.
Each solver participating in the competition can support, i.e. compete in, an arbitrary set of tasks. If a solver supports all tasks of a track, it also participates in the track.
Tasks
A task is a reasoning problem under a particular semantics. Following ICCMA'15 we consider four different problems:
- DC-σ: Given F=(A,R), a ∈ A decide whether a is credulously accepted under σ.
- DS-σ: Given F=(A,R), a ∈ A decide whether a is skeptically accepted under σ.
- SE-σ: Given F=(A,R) return some set E ⊆ A that is a σ-extension.
- EE-σ: Given F=(A,R) enumerate all sets E ⊆ A that are σ-extensions.
for the seven semantics σ ∈ {CO,PR,ST,SST,STG,GR,ID}. For single-status semantics (GR and ID) only the problems SE and DC are considered.
The combination of problems with semantics amounts to a total number of 24 tasks. Each solver participating in a task will be queried with a fixed number of instances corresponding to the task with a timeout of 10 minutes each. For each instance, the solvers get
- 1 point, if it delivers the correct result;
- −5 points, if it delivers an incorrect result;
- 0 points otherwise.
The terms correct and incorrect for the different reasoning problems are defined as follows.
- DC-σ (resp. DS-σ): if the queried argument is credulously (resp. skeptically) accepted in the given AF under σ, the result is correct if it is YES and incorrect if it is NO; if the queried argument is not credulously (resp. skeptically) accepted in the given AF under σ, the result is correct if it is NO and incorrect if it is YES.
- SE-σ: the result is correct if it is a σ-extension of the given AF and incorrect if it is a set of arguments that is not a σ-extension of the given AF. If the given AF has no σ-extensions, then the result is correct if it is NO and incorrect if it is any set of arguments.
- EE-σ: the result is correct if it is the set of all σ-extensions of the given AF and incorrect if it contains a set of arguments that is not a σ-extension of the given AF.
Intuitively, a result is neither correct nor incorrect (and therefore gets 0 points) if (i) it is empty (e.g.\ the timeout was reached without answer) or (ii) it is not parsable (e.g.\ some unexpected error message). For EE-σ there is also the case that the result (iii) contains only σ-extensions, but not all of them.
The score of a solver for a particular task is the sum of points over all instances. The ranking of solvers for the task is then based on the scores in descending order. Ties are broken by the total time it took the solver to return correct results.
For semi-stable and stage semantics, we recall that those semantics coincide with stable for AFs that possess at least one stable extension. Benchmarks will be selected such that the majority of AFs does not have a stable extension.
Tracks
All tasks for a particular semantics constitute a track. The ranking of solvers for a track is based on the sum of scores over all tasks of the track. Again, ties are broken by the total time it took the solver to return correct results. Note that in order to make sure that each task has the same impact on the evaluation of the track, all tasks for one semantics will have the same number of instances.
The winner of each track will be awarded.
Dung's Triathlon
In this special track, the solver is required to deal with the following problem: D3: Given F=(A,R) enumerate
- all sets E ⊆ A that are GR-extensions, followed by
- all sets E ⊆ A that are ST-extensions, followed by
- all sets E ⊆ A that are PR-extensions.
For scoring and ranking the same method as for single tasks is applied, except that the timeout for each instance is 30 minutes.
The result of D3 is correct if it is the set of all GR-extensions, followed by the set of all ST-extensions, followed by the set of all PR-extensions, and incorrect if the first set contains a set of arguments that is not the GR-extension, the second set contains a set of arguments that is not a ST-extension, or the third set contains a set of arguments that is not a PR-extension.
The winner of Dung's Triathlon will be awarded.