User Guide

1) Inputting a Logic Program

The LABAS Justifier takes an extended logic program as input, either through uploading a .lp file containing the logic program, or via the textbox.
Every clause in the logic program has to be of one of the two forms:

• a.
("a" is a fact)
• a :- a1, a2, -b, d, not p, not -m.
(a clause with head "a", atoms "a1", "a2", and "d", negated atom "-b", and NAF literals "not p" and "not -m")

Note that, currently, the LABAS Justifier cannot handle variables, so all body literals have to be atoms (start with lower case letters). It also does not support integritiy constraints, aggregates, and other advanced constructs.

2) Building a Justification

Inputting a logic program and uploading it, will take you to the main interface of the LABAS Justifier.
On the right, the logic program and its answer sets are displayed. On the left, you can choose which literal you want to justify and which type of justification should be computed.

a) LABAS Justifications or Attack Trees?

By default, the LABAS Justifier will compute LABAS Justifications. If you want to compute Attack Trees instead, click the Attack Trees button on the left.

b) Which Answer Set?

Choose with respect to which Answer Set you want to justify a literal, using the Select Answer Set dropdown menu (numbers are as shown in the "Answer Sets" box on the right). By default, the first Answer Set is selected.

c) How many justifications?

By default, all justifications (LABAS or Attack Tree) are computed. You can choose a maximum number of justifications to be computed by selecting a different value (1, 5, 10, or 20) from the Generate all dropdown menu.

d) Skip justifications?

Consecutively computed justifications can be very similar. You can thus choose to only compute every second justification (with either even or odd index) using the Generate odd and even dropdown menu.

e) Which literal?

Choose which literal you want to justify using the CHOOSE LITERAL input box on the bottom left.

f) Build justifications!

Finally, hit the Build button to compute the justifications with the chosen parameters.

3) Displaying a Justification

After hitting the "Build" button, the first computed justification (either LABAS or Attack Tree) is displayed below the main interface.

LABAS Justification

The top part of the justification provides some basic information about the displayed LABAS Justification, in particular, which literal is being justified with respect to which Answer Set, how many LABAS Justifications were computed, and which LABAS Justicication is currently displayed (by default, the first justification is displayed).
The Select LABAS Justification to display dropdown menu is used to select which of the computed justifications should be displayed.

The nodes in a LABAS Justification can be dragged horizontally (except for the top node). In order to return to the initial layout of the justification, press the Reset Tree button.

Attack Tree

As for LABAS Justifications, the top part of the Attack Tree view provides the respective basic information, and the Select Attack Tree to display dropdown menu is used to select which of the computed Attack Trees should be displayed.

In contrast to LABAS Justifications, the nodes in Attack Trees cannot be dragged. However, when clicking on a node in the Attack Tree, it collapses. A collapsed node can be expanded by clicking on it again. In order to return to the initial layout of the Attack Tree, press the Reset Tree button.