=Paper=
{{Paper
|id=Vol-1207/paper_2
|storemode=property
|title=Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
|pdfUrl=https://ceur-ws.org/Vol-1207/paper_2.pdf
|volume=Vol-1207
|dblpUrl=https://dblp.org/rec/conf/ore/Ludwig14
}}
==Just: a Tool for Computing Justifications w.r.t. ELH Ontologies==
https://ceur-ws.org/Vol-1207/paper_2.pdf
Just: a Tool for Computing Justifications
w.r.t. ELH Ontologies
Michel Ludwig?
Theoretical Computer Science, TU Dresden, Germany
michel@tcs.inf.tu-dresden.de
Abstract. We introduce the tool Just for computing justifications for
general concept inclusions w.r.t. ontologies formulated in the description
logic EL extended with role inclusions. The computation of justifications
in Just is based on saturating the input axioms under all possible infer-
ences w.r.t. a consequence-based calculus. We give an overview of the im-
plemented techniques and we conclude with an experimental evaluation
of the performance of Just when applied on several practical ontologies.
1 Introduction
Users or authors of ontologies are often interested in understanding why a con-
sequence α logically follows from a given ontology T . As the ontologies that are
typically used in practice consist of several thousand axioms, it can be helpful
to compute a small subset of T which entails the consequence α for analysing
why α logically follows from T . A minimal such subset is called a justification of α
w.r.t. T . Furthermore, when α represents an erroneous consequence that should
be fixed, it becomes necessary to compute all the justifications of α w.r.t. T to
ensure that all the relevant axioms of T are taken into account when changing
the ontology in such a way that α is no longer entailed.
Previous approaches described in the literature for computing all the justi-
fications of an ontology w.r.t. a consequence can broadly be classified into the
following two categories. “Black-box” algorithms use off-the-shelf reasoners solely
to check whether a concept inclusion follows from an ontology while searching for
candidate subsets of the ontology that can serve as justifications [4,8,9]. “Glass-
box” approaches, on the other hand, typically rely on intricate modifications to
a pre-existing reasoner implementation to keep track of which axioms were used
during the classification of an ontology. This information can then be used to
construct a justification [2, 5, 11]. In this paper we follow such a “glass-box” ap-
proach as well. Generally speaking, the transformation of a reasoner into a tool
capable of computing all justifications is not an easy task as one goal of efficient
reasoners is to avoid generating duplicate inferences for the same consequence.
We present the tool Just that is designed from the ground up for computing
either one, or all the justifications for general concept inclusions w.r.t. ontolo-
gies formulated in the description logic EL extended with role inclusions. We
?
The author was supported by the German Research Foundation (DFG) within the
Cluster of Excellence ‘Center for Advancing Electronics Dresden’ (cfAED).
first give a brief overview of the implemented techniques, and we conclude the
paper with an experimental evaluation of its performance on several practical
ontologies. The tool and proofs establishing its correctness and completeness are
available from http://lat.inf.tu-dresden.de/~michel/software/just/
2 Preliminaries
We assume the reader to be familiar with basic notions of description logics [1].
An ELH-ontology, or ELH-TBox T , is a finite set of axioms of the form C v D or
r v s, where C, D are EL-concepts and r, s are roles names. An EL-concept C is
either a concept name, or a concept that makes use of the concept constructors
>, u, ∃r.D only, where r is a role name and D an EL-concept. We assume
standard set-theoretic semantics.
We now formally introduce the main notion relevant for our tool.
Definition 1. Let T be an ELH-TBox and let C, D be EL-concepts. A justifi-
cation1 for T |= C v D is a subset M ⊆ T such that M |= C v D, and for
every M0 ( M it holds that M0 6|= C v D. The set of all the justifications for
T |= C v D will be denoted by JustT (C v D).
Example 1. Let T = {A v X, A v Y, X v ∃r.Y, ∃r.Y v B, Y v B, Y v
Y 0 , Y 0 v Y }. Then the set JustT (A v B) consists of the two sets {A v X, X v
∃r.Y, ∃r.Y v B} and {A v Y, Y v B}.
Note that there can exist exponentially many justifications for a given TBox T
and a concept inclusion C v D. Hence, unlike with standard reasoning in ELH,
it is not possible to compute all justifications in polynomial time w.r.t. the size of
the TBox in every case [2]. It is however still (theoretically) possible to compute
one justification in polynomial time.
3 Tool Overview & Computation Techniques
Just v 0.1 is implemented in Java and it takes an ELH-TBox T and two EL
concepts C, D as input. The default operation mode of Just is then to compute
and output the set JustT (C v D). Alternatively, the tool can be instructed to
search for one justification for T |= C v D only.
We first focus on describing how the computation of justifications for inclu-
sions between concept names w.r.t. normalised TBoxes is performed in Just. A
TBox Tdis said to be in normal form if every axiom of T is of one of the following
n
forms: i=1 Ai v B, A v ∃r.X̄, ∃r.X̄ v B, or r v s, where n ≥ 0, A, B are
concept names, and an expression of the form X̄ stands either for the concept
name X or for the >-concept.
The computation of justifications for inclusions between concept names w.r.t.
a normalised TBox T is performed by a saturation procedure that computes all
the (minimal) derivations for inclusions of the form A v B, > v A, or > v >, for
1
Justifications are also known as MinAs in the literature.
(Ax) (AxTop) (RoleAx)
Ā v Ā Av> rvr
rvs
(RoleSucc)
rvt if s v t ∈ T
X̄ v Ȳ rvs
(Ex)
Ā v B
if Ā v ∃r.X̄ ∈ T and ∃s.Ȳ v B ∈ T
Ā v X1 ... Ā v Xn
(Conj)
Ā v B
if X1 u . . . u Xn v B ∈ T with n ≥ 0
Ā v X̄ X̄ v B̄
(Merge)
Ā v B̄
Fig. 1. Calculus T
concept names A and B, using the calculus T depicted in Fig. 1. The calculus T is
related to calculi used for consequence-based reasoning [6]. Note that expressions
of the form Ā must be consistently instantiated (either with concept names or
>) in the premise and the conclusion of inference rules.
The axioms used in the application of the inference rules for generating a
derivation for X v Y yield a subset of T from which the consequence X v Y
logically follows. The minimal such axiom sets resulting from all the (minimal)
derivations for X v Y are therefore the justifications for X v Y w.r.t. T .
Example 2. Let T be defined as in Example 1. Then, for instance, the following
two derivations ∆1 and ∆2 for the inclusion A v B can be generated w.r.t. T
using the calculus T. We associate with each derivation ∆i a set Axioms(∆i )
which consists of the axioms of T that were used in the inference rule applications
occurring in ∆i . First, ∆1 is given as follows:
(Ax) (Ax)
AvA Y vY
(Conj) (Conj)
AvY Y vB
(Merge)
AvB
We have Axioms(∆1 ) = {A v Y, Y v B}. The derivation ∆2 can be depicted as
(Ax) (Ax)
Y vY Y0 vY0
(Conj) (Conj)
Y vY0 Y0 vY
(Ax) (Merge)
AvA Y vY
(Conj) (Conj)
AvY Y vB
(Merge)
AvB
with Axioms(∆2 ) = {A v Y, Y v B, Y v Y 0 , Y 0 v Y } ) Axioms(∆1 ).
Following the example of derivation ∆2 , it is possible to construct infinitely
many derivations for the inclusion A v B from the TBox T (as defined in
Example 1). However, one can prove that for finding all justifications it is suf-
ficient to construct so-called admissible derivations ∆ only in which every sub-
derivation ∆0 of an inclusion α does not contain an occurrence of α as a premise
in ∆0 . It is easy to see that there can only exist finitely many admissible deriva-
tions w.r.t. a normalised TBox T for a given inclusion α.
To compute justifications w.r.t. general TBoxes, Just keeps track of which
original axiom corresponds to which normalised axiom. The justifications for a
consequence C v D w.r.t. a general TBox T are then generated from the justifi-
cations for C v D w.r.t. the normalisation of T by successively replacing every
normalised axiom with all the axioms from which it originates. The minimal sets
obtained in that way are the justifications w.r.t. the general TBox.
Example 3. Let T = {A v B u ∃r.>, A v B u ∃s.>} and let TN = {A v B, A v
∃r.>, A v ∃s.>} be the normalisation of T . Then JustTN (A v B) = {{A v B}}.
As the axiom A v B in TN originates from both axioms in T , we obtain that
JustT (A v B) consists of the two sets {A v B u ∃r.>} and {A v B u ∃s.>}.
The computation of justifications for inclusions of the form C v D w.r.t. T ,
where C and D are not necessarily concept names, can be done analogously by
computing justifications for AC v AD w.r.t. T ∪ X , where X = {AC v C, D v
AD } for fresh concept names AC and AD . The justifications for C v D are then
the minimal sets obtained from the justifications for AC v AD after removing
the axioms contained in X .
Example 4. Let T = {A v B} and let X = {AC v A u Y, B v AD }. Then
JustT ∪X (AC v AD ) = {{AC v A u Y, B v AD , A v B}} and JustT (A u Y v
B) = {{A v B}}.
Similarly to [9], Just extracts a reachability-based module for X v Y first
before starting to compute all the (minimal) derivations for X v Y . Moreover, we
used techniques from resolution-based theorem provers to obtain an acceptable
performance of our tool in practice. In particular, whenever a derivation Γ 0 for
an inclusion α was generated, another derivation Γ for α had been obtained
previously, and all the axioms associated with Γ were contained in the set of
axioms associated with Γ 0 , then Γ 0 was discarded. Such a deletion strategy
corresponds to forward subsumption deletion in resolution theorem provers. We
also employed a technique equivalent to backward subsumption deletion.
The computation of a single justification is currently implemented by stop-
ping the saturation process after a derivation for the target inclusion has been
found.2 As the axioms occurring in this derivation might not represent a justifi-
cation yet, superfluous axioms are identified by checking for each axiom whether
the target inclusion still follows (using the reasoner ELK [7]) after the considered
axiom has been removed.
2
Note that in Just v 0.1 the saturation step is not guaranteed to finish in polynomial
time w.r.t. the size of the input TBox, even when only one justification is computed.
Table 1. Metrics of the Ontologies Used in the Experiments
Ontology # Axioms # Concept Names # Role Names
NCI 117 583 105 105 92
SNOMED CT 354 601 291 144 57
GALEN-OWL 46 457 23 136 949
4 Experimental Evaluation
For our experiments we picked three ontologies that are typically considered to
pose different challenges to DL reasoners and that are expressed mainly in ELH:
version 13.12e of the NCI thesaurus,3 the January 2010 international release
of SNOMED CT, and the GALEN-OWL ontology.4 In the case of NCI all the
152 axioms that fell outside the considered ELH fragment were first removed
from the ontology. The number of axioms, concept names, and role names in
the resulting ontologies is shown in Tbl. 1. For each of the three ontologies T
we then randomly selected 1000 inclusions between concept names, A v B, such
that T |= A v B holds. In a first set of experiments we used Just and the algo-
rithm for computing all justifications implemented in the OWL-API [3,4] (using
the reasoner FaCT++5 [10]) to compute all the justifications for each selected
inclusion w.r.t. the respective ontology. In a second series of experiments we in-
structed Just to only search for one justification for each considered inclusion.
All experiments were conducted on a PC equipped with an Intel i5-2500K CPU
running at 3.30GHz and with 16 GiB of main memory. An execution timeout of
10 CPU minutes was imposed on each problem.
The results obtained for computing all justifications are shown in Tbl. 2.
The first column indicates which ontology was used. The next five columns then
show the results obtained with Just, whereas the last two columns refer to
the OWL-API implementation. More precisely, the second and seventh column
indicate the number of successful computations within the given time limit by
the respective implementations. The average and the maximal number, as well
as the maximal size of the justifications as computed by Just are shown in the
next three columns. The sixth and eighth columns contain the average CPU time
3
http://evs.nci.nih.gov/ftp1/NCI_Thesaurus
4
http://owl.cs.manchester.ac.uk/research/co-ode/
5
Note that at the time of writing it was not possible to use the reasoner ELK in
combination with the OWL-API implementation for computing justifications.
Table 2. Results Obtained for Computing All Justifications
Just OWL-API
Ontology # Success. Avg. # Max. # Max. Size Time (s) # Success. Time (s)
NCI 954/1000 1.165 32 10 34.895 577/1000 231.532
SNOMED CT 876/1000 2.622 127 28 57.405 16/1000 395.882
GALEN-OWL 511/1000 1.315 4 16 8.740 0/1000 -
Table 3. Results Obtained for Computing One Justification using Just
Ontology # Success. Max. Size Time (s)
NCI 972/1000 10 36.827
SNOMED CT 951/1000 28 53.473
GALEN-OWL 978/1000 22 71.759
required by the respective implementations for the successful computations over
each considered set of inclusions.
Regarding the computation of all justifications with Just, the lowest number
of successful computations were observed for GALEN-OWL, despite it being the
smallest ontology of the corpus. The largest size, average & maximal number of
justifications, as well as the longest average computation times involving Just,
were found for SNOMED. No computation succeeded within the allocated time
for experiments involving GALEN-OWL using the OWL-API implementation.
In general, we observed fewer timeouts and shorter average computation times
with Just than with the OWL-API.
The results obtained for computing only one justification using Just are
given in Tbl. 3. Analogously to Tbl. 2, the number of successful computations
and the maximal size of the computed justifications are given in the second
and third columns. The last column shows the average CPU time required to
compute one justification.
One can see that fewer timeouts occurred when only one instead of all jus-
tifications were computed with Just. The least number of successful computa-
tions was now observed for SNOMED, whereas only 22 computations involving
GALEN-OWL did not succeed within the given time limit. The longest average
computation times were reported for GALEN-OWL, and the largest justification
was again computed for SNOMED CT.
In all the successful computations Just required at most 14.13 GiB of main
memory.
5 Conclusion
We presented the tool Just for computing either one, or all the justifications
for general concept inclusions w.r.t. ontologies formulated in ELH. Our exper-
imental evaluation showed that Just is capable of finding all the justifications
for consequences in many practical cases within a reasonable time, even when a
large number of justifications exist.
As future work we aim to implement an extended calculus which would allow
it to compute justifications for more expressive description logics. Our tool could
also benefit from a more goal-oriented construction of derivations and from an
improved module extraction procedure that yields smaller modules. It would
also be interesting to implement an incremental computation of justifications,
which would permit it to generate as many justifications as requested by the user.
Finally, we also plan to perform a more extensive comparison of the performance
of our tool against other approaches for computing justifications.
References
1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applica-
tions. Cambridge University Press, 2nd edn. (2007)
2. Baader, F., Peñaloza, R., Suntisrivaraporn, B.: Pinpointing in the description logic
EL+ . In: Proceedings of the 30th Annual German Conference on AI (KI 2007).
Lecture Notes in Computer Science, vol. 4667, pp. 52–67. Springer (2007)
3. Horridge, M., Bechhofer, S.: The OWL API: A Java API for OWL ontologies.
Semantic Web 2(1), 11–21 (2011)
4. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL
DL entailments. In: Proceedings of the 6th International Semantic Web Conference
& 2nd Asian Semantic Web Conference (ISWC 2007 & ASWC 2007). Lecture Notes
in Computer Science, vol. 4825, pp. 267–280. Springer (2007)
5. Kalyanpur, A., Parsia, B., Sirin, E., Hendler, J.A.: Debugging unsatisfiable classes
in OWL ontologies. Journal of Web Semantics 3(4), 268–293 (2005)
6. Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In: Proceed-
ings of the 21st International Joint Conference on Artificial Intelligence (IJCAI’09).
pp. 2040–2045 (2009)
7. Kazakov, Y., Krötzsch, M., Simancik, F.: The incredible ELK: From polynomial
procedures to efficient reasoning with EL ontologies. Journal of Automated Rea-
soning 53(1), 1–61 (2014)
8. Suntisrivaraporn, B.: Finding all justifications in SNOMED CT. ScienceAsia 39(1),
79–90 (2013)
9. Suntisrivaraporn, B., Qi, G., Ji, Q., Haase, P.: A modularization-based approach to
finding all justifications for OWL DL entailments. In: Proceedings of the 3rd Asian
Semantic Web Conference (ASWC 2008). Lecture Notes in Computer Science, vol.
5367, pp. 1–15. Springer (2008)
10. Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: System description.
In: Proceedings of the Third International Joint Conference on Automated Rea-
soning (IJCAR 2006). Lecture Notes in Computer Science, vol. 4130, pp. 292–297.
Springer (2006)
11. Zhou, Z., Qi, G., Suntisrivaraporn, B.: A new method of finding all justifications in
OWL 2 EL. In: Proceedings of the 2013 IEEE/WIC/ACM International Confer-
ences on Web Intelligence (WI 2013). pp. 213–220. IEEE Computer Society (2013)