A justification is a type of explanation for an entailment (inference). More specifically, a justification for an entailment in an ontology, is a minimal subset of the ontology that is sufficient for the entailment to hold. Justifications operate on the level of asserted axioms. For this reason, it may be the case that not all of the parts of axioms in a justfication are required for an entailment to hold. In other words, justifications may contain axioms that contain superfluous parts. These superfluous parts can distract users when they try to understand justifications, and they can also cause over-repair of ontologies (more information may be removed from an ontology than necessary when attempting to break the entailment that the justification supports). For these reasons, we have defined two new classes of fine-grained justifications: Laconic Justifications, which are justifications whose axioms do not contain any superfluous parts, and Precise Justifications, which are Laconic Justifications where each axiom represents a minimal part of the justification. For more details on this work, see “Laconic and Precise Justifcations in OWL“, which was presented at the International Semantic Web Conference 2008, where it won the award for Best Paper.
As part of my PhD I have developed tools that can compute these types of justifications. This software requires a special build of Protege 4 – the build of Protege 4 containing the workbench plugin can be downloaded here. The Explanation Workbench is a plugin for Protege-4 that can compute regular and Laconic Justications. A screen-shot of the Explanation Workbench is shown below. The workbench allows entailments to be selected and then the justifications for these entailments to be viewed and compared.
The explanation workbench is split into two main areas. The left handside shows a list of entailments. Entailments automatically get added to this list when the “Explain inference” button is pressed in the Protege 4 user interface (see screeshot below). The workbench can also be invoked by selecting the “Explanation workbench…” item from the “Tools” menu. Multiple entailments can be selected, and the justifications for the selected entailments will appear on the right hand side of the workbench.
Justifications are presented as lists of ordered and indented axioms. An example justification is shown below. This justification is for the entailment Director subClassOf Employee, which holds in the univ-benchontology. The first line in the justification shows the entailment. The remaining lines show the axioms in the justification. In the example below there are four axioms. From the first, second and third axioms we know that a Director is a Person that worksFor and Organization (since headOf is a sub-property of worksFor and Program is a subclass of Organisation). Since from axiom 4, Person that worksFor anOrganisation is an Employee this means that Director is a subclass of Employee
Laconic Justifications are justifications whose axioms do not contain any superflous parts. There are two modes for computing Laconic Justifications in the Explanation Workbench. The first mode can be used to compute a snapshot of a Laconic version of a justification. To display a laconic version of a justification the “Show laconic justification” checkbox should be checked.
The second mode of working with Laconic Justifications is to view Laconic Justification on a “global” view. To work in this mode, the “Show Laconic Justifications” radio button (located at the top of the workbench window) should be selected. This will compute all Laconic Justifications for an entailment
Consider the justification for ReseachAssistant subClassOf Employee, as shown below.
After checking the “Display laconic explanation” checkbox the following Laconic Justification is revealed.
The Laconic version of the justification only contains the parts of the axioms that are responsible for the entailment in question. Notice that the 2nd, 3rd, 5th and 7th axioms in the Laconic version of the justification are smaller and only contain parts of the original axioms – the superfluous parts have been removed. This includes the parts of the equivalent classes axioms that aren’t necessary to support the entailment (e.g. in the 2nd axiom, only one direction of the implication is required and the restriction is also not required), fillers of existential restrictions (e.g. in the 3rd axiom it isn’t necessary that the filler of the restriction is ResearchGroup), and parts of inverse property axioms (e.g. the 5th axiom)
One aspect of Justifications that is not particularly desirable is that masking can occur – axioms in regular justifications can mask further justifications for an entailment. The only regular justification for Employee subClassOf Person is shown below.
Selecting “Show Laconic Justifications” radio button at the top of the Explanation Workbench displays all of the Laconic justifications for the entailment. Where as there is only one regular justification for the entailment Employee subClassOf Person, there are two Laconic justicifications for this entailment – the additional justification is masked by the regular justification. The additional justification is shown below. In this case, part of the first axiom masks the second justification. If the “Employee subClassOf Person” part of the axiom is disregarded, the remainder of the axiom forms part of a second laconic justification.