Answer Set Programming (ASP) is one of the most widely used non-monotonic reasoning paradigms, allowing to efficiently compute solutions to problems.
A problem is represented in terms of a logic program, that is if-then clauses containing negation-as-failure (NAF) literals which express exception conditions for the applicability of clauses.
The solutions to the problem are then given by the declarative answer set semantics for the logic program.
The LABAS Justifier uses two methods for justifying literals with respect to an answer set of a consistent logic program
by applying Argumentation Theory, another widely used technique in the field of non-monotonic reasoning.
The first justification approach, an Attack Tree, expresses how to construct an argument for the literal in question (the supporting argument)
as well as which arguments attack the argument for the literal in question (the attacking arguments);
the same information is provided for all arguments attacking the attacking arguments, and so on.
An Attack Tree is a (possibly infinite) tree with nodes holding arguments, where the argument held by a child node attacks the argument held by the parent node.
The second justification approach, a Labelled ABA-Based Answer Set (LABAS) Justification, represents the same information as an Attack Tree,
but expressed in terms of literals rather than arguments.
A LABAS Justification comprises facts and NAF literals necessary to derive the literal in question (the ``supporting literals'')
as well as information about literals which are in conflict with the literal in question (the ``attacking literals'').
The same information is provided for all supporting and attacking literals of the literal in question, for all their supporting and attacking literals, and so on.
A LABAS Justification is the flattened version of an Attack Tree,
containing literal-pairs which express the different parent-child relations expressed in an Attack Tree.
The relation between arguments in the Attack Tree is represented in terms of literal-pairs which are in an attack relation;
the relation between components of an argument is represented in terms of literal-pairs which are in a support relation.
A LABAS Justification can be interpreted as a graph, where every literal occurring in a pair forms a node in the graph.
The graph has a support edge between two literal-nodes if these two literals occur as a literal-pair in a support relation in the LABAS Justification.
Analogously, the graph has an attack edge between two literal-nodes if these two literals occur as a literal-pair in an attack relation in the LABAS Justification.
For formal details about Attack Trees and LABAS Justifications, please refer to the paper:
Justifying Answer Sets using Argumentation (Schulz & Toni, 2016)
(the paper on arXiv)
The LABAS Justifier was developed and is maintained by Claudia Schulz.
If you encounter any problems, or have questions or comments, please email Claudia.