Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the ℰℒ family of DLs, each of which gives rise to proofs of diferent shapes. Here, we study three such calculi and the proofs they produce on a benchmark based on the OWL Reasoner Evaluation. The calculi are implemented using a translation into existential rules with stratified negation, which had already been demonstrated to be efective for the calculus of the Elk reasoner. We then use the rule engine Nemo to evaluate the rules and obtain traces of the rule execution. After translating these traces back into DL proofs, we compare them on several metrics that reflect diferent aspects of their complexity.
Consequence-based reasoning for DLs has a long tradition, starting from the first reasoning algorithms
for ℰ ℒ with general concept inclusions [
We follow an approach to encode DL reasoning into (an extension of) Datalog rules [14, 15, 16]. To execute these rules, we use Nemo, a Datalog-based rule engine that is easy to use and ofers many advanced features, such as datatypes, existential rules, aggregates, and stratified negation [ 16]. This has already been demonstrated to be efective for the reasoning calculus of Elk, including pre-processing of the ontology in OWL format,1 which essentially implements an ℰ ℒ⊥+ reasoner by existential rules with stratified negation [ 16]. The advantage of this approach is that one can relatively quickly implement new reasoning procedures with low efort.
In this paper, we also consider two other calculi for ℰ ℒ-based logics from the literature: the original
ℰ ℒ++ calculus, denoted by Envelope [
init() ⊤ ⊑ ⊤ : ⊤ occurs negatively in
R∃+ →− ⊑ ∃. ⊑ : ∃ ⊑.* occurs negatively in extracted from the 2015 OWL Reasoner Evaluation (ORE) [17]. After encoding them into rules as for the Elk calculus, we use the tracing capabilities of Nemo to compute proofs for the derived consequences. However, since Nemo traces are based on translated rules and may include statements not expressible as DL axioms (e.g., side conditions), we must still transform them to obtain DL proofs suitable for inspection by ontology engineers. Finally, we compare the shape of the resulting proofs using several measures, such as the size, depth, directed cutwidth [18], and cognitive complexity of inference steps [19].
+ Let NC and NR be two disjoint, countably infinite sets of concept- and role names, respectively. ℰ ℒ⊥ concepts are defined by the grammar , ::= ⊤ | ⊥ | | ⊓ | ∃., where ∈ NC and ∈ NR.
+ axioms are either concept inclusions of the form ⊑ or complex role inclusions of the form ℰ ℒ⊥ 1 ∘ · · · ∘ ⊑ +, wthhaetroenly1,a.l.l o.w,ss,im∈pleNrRo.leAinncℰluℒs⊥+ionTsBoofxtihseafofinrimte se⊑tof. Wℰ ℒe+⊥assauxmioemtsh.eℰrℒeaℋd⊥eritsothbee fragment of ℰ ℒ⊥ familiar with the semantics of these logics, in particular the definition of entailment of an axiom from a TBox , written |= [13]. + that are tailored towards classification , Calculi. We consider three inference calculi for fragments of ℰ ℒ⊥ i.e., computing all entailments of the form |= ⊑ for , ∈ NC. + TBoxes. Side conditions are
Figure 1 shows the inference rules used in the reasoner Elk for ℰ ℒ⊥ marked in gray, where “ occurs negatively” means that occurs within a concept on the left-hand side of some axiom in , and ⊑
* denotes the precomputed role hierarchy, i.e., the transitive closure
over simple role inclusions. Furthermore, complex role inclusions are assumed to be in the normal
form 1 ∘ 2 ⊑ , using only binary role composition. Axioms with longer role compositions can be
normalized with the help of fresh role names. Then, |= ⊑ holds if either ⊑ or ⊑ ⊥ can
be derived by these rules from init() [
Figure 2 shows the Textbook classification rules for ℰ ℒ from [13] with a slight modification to rule CR5 and the addition of a variant of R⊥ from Elk, in order to support ℰ ℒℋ⊥. Here, all input and derived concept inclusions are required to be of one of the forms ⊑ , 1 ⊓ 2 ⊑ , ⊑ ∃. or ∃. ⊑ , where , 1, 2, are concept names from , ⊤ or ⊥, which is again without loss of generality. This calculus is correct in the same sense as the Elk calculus above, but, instead of the init() statement, it is initialized with all axioms of the input TBox .
+ from [
Figure 3 shows the Envelope rules for ℰ ℒ⊥ concrete domains. For a consistent representation, we translate the statements “ ∈ ()” and “(, ) ∈ ()” from the original paper into ⊑ and ⊑ ∃., respectively. Note that and must be concept names from , ⊤ or ⊥. This calculus requires the concept and role inclusions in to be in normal form, and is correct in the same sense as for the other calculi, but stars only from the tautologies ⊑ and ⊑ ⊤ for all concept names from .
⊑ ⊥ CR1 ⊑⊑ : ⊑ ∈
CR2 ⊑ 1 ⊑ ⊑ 2 : 1 ⊓ 2 ⊑ ∈ CR3 ⊑⊑∃. : ⊑ ∃. ∈
CR4 ⊑ ∃.1⊑ 1 ⊑ 2 : ∃.2 ⊑ ∈ CR5 ⊑ ∃.⊑ ⊥ ⊑ ⊥
⊑ ∃. : ⊑ ∈
CR10 ⊑ ∃. CR11 ⊑ ∃1.⊑ ∃.⊑ ∃2. : 1 ∘ 2 ⊑ ∈
Proofs. Following the notion introduced in [
Consider, for example, the TBox = { ⊑ , ⊑ ∃., ⊑ , ∃. ⊑ , ⊑ , ⊑ } and the entailment |= ⊑ . Since proofs are to be inspected by ontology engineers, they are restricted to DL axioms. This means, however, that they cannot include side conditions and statements that are not DL axioms (e.g., init()). Thus, we have to adapt the calculus rules before we can use them as inference steps in proofs.
We treat side conditions of the form ⊑ ∈ as ordinary premises ⊑ , since they are DL axioms. However, this does not mean that R⊑ from Elk is now equivalent to CR3 from Textbook, since the second premise in the former is still restricted to axioms from .
Similarly, we treat side conditions ⊑* as premises ⊑ . However, to obtain a valid proof, we also have to derive these axioms from the TBox. For both the Elk and the Textbook calculus, we ⊑ ⊑ ∃. ⊑
⊑ ⊑ ∃. ⊑ ⊑ ⊑ ⊑ ∃. ⊑ ⊑ ⊑ ∃. ∃. ⊑ ⊑ ∃. ⊑ ∃. ⊑ ⊑ ⊑ ⊑ ⊑ ∃. ⊑ ∃.
⊑ ⊑ ∃. ⊑
⊑ ⊑ ∃. ⊑ ∃. ⊑ ⊑ therefore add the following two rules: ⊑ : ∈ NR occurs negatively in ⊑ : ⊑ ∈ ⊑
Next, we replace statements of the form →− in the Elk calculus by ⊑ ∃., which preserves
the soundness of the inference rules, and is similar to the treatment of “(, ) ∈ ()” in the Envelope
calculus. We also omit init() statements, meaning that R0 and R1 from Elk become similar to CR1
and CR2 from Textbook, but they may only appear in a proof if init() was actually derived by the
original rules. We also add CR1 and CR2 to the Envelope calculus to express the initialization step,
which does not correspond to explicit rules in [
⊑ However, this violates non-redundancy since ⊑ has multiple non-isomorphic proofs. In such cases, we keep only a subproof of minimal size (in the example, only the leaf ⊑ ). This also applies to other inference rules, for example, R∃− , which now trivially derives ⊑ ∃. from ⊑ ∃.. Thus, due to the above simplification, this rule will never appear in a proof.
We also omit the side conditions of the form “ occurs negatively in ”. To represent them in our proofs, we could add the axiom in which occurs negatively as a premise; however, this axiom is not logically necessary for the inference step, and may be confusing because it has no connection to the inference other than the occurrence of . For example, consider the following application of R+, which ∃ also requires that ∃. occurs negatively in : ⊑ ∃.
⊑ ⊑ ∃. ⊑ We could add ∃. ⊑ as a premise to express the side condition, but this axiom is not required to derive ⊑ ∃.. Moreover, since ∃. ⊑ is also used in the subsequent application of R⊑, having it appear in two consecutive steps—while only being necessary for one—may be unnecessarily confusing.
The proofs resulting from all these considerations can be seen in Figure 4, where we draw them as trees to emphasize their shape, which we analyze in the following. Despite the transformations and simplifications we applied, the three calculi can still result in substantially diferent proofs, even for such a simple entailment. justification size depth
cutwidth
We evaluate the shape of proofs by several measures from the literature, which reflect diferent aspects
of how ontology engineers can inspect a proof in diferent representations (see Figure 5).
Size. The size of a proof [
Depth. The depth of a proof [22] is the length of the longest path from a leaf to the root. This is related to the task of finding an error in the ontology based on an erroneous inference. In this case, ontology engineers would rather inspect the proof only along the “most suspicious-looking” branch (or a few such branches), and thus the time they may need in the worst case depends on the length of the longest branch. The depth is also proportional to the height of a more traditional proof-tree representation, as used in Evonne [21].
The width of such a tree visualization, assuming that adjacent subtrees are non-overlapping in the sense that nodes from one subtree are not positioned vertically above nodes from another subtree, can be expressed as a function of the number of leafs in the proof, which is also called its justification size [23]. However, we do not consider the justification size in this paper, since it does not depend on the reasoning calculus.
Cutwidth. The (directed) cutwidth of a graph tries to measure how linear it is [18]. Given a linear vertical arrangement of a proof’s nodes [21], the cutwidth is the maximal number of edges that would be afected when cutting the graph horizontally between any two consecutive nodes (see Figure 5). The cutwidth of the graph is then the minimum of the cutwidths of all possible such linear arrangements. Hence, it is proportional to the maximal number of intermediate axioms an ontology engineer needs to keep in memory when reading the proof in such an (optimal) linear representation from top to bottom. Bushiness Score. We developed another score to measure how “bushy” (non-linear) a proof is. It is computed as the ratio between the size of the proof and its depth (+1 for the root). Hence, it can be interpreted as the average number of vertices per level (see Figure 5). A completely linear proof in which all inference steps have only one premise results in a bushiness score of 1 (not bushy at all), and the full binary tree with five levels gets a score of 351 = 6.2 (very bushy).
Step Complexity. Finally, we consider a measure based on the cognitive complexity of inference steps, which has been proposed in the context of justifications, and has been evaluated in user studies [ 19]. It reflects multiple aspects of the syntactical structure of the argument, such as the depth of involved concepts, how many constructors and axiom types are used, or whether it uses the triviality of a concept name (i.e., being equivalent to ⊥ or ⊤). Here, we consider the average of the step complexities of the individual inference steps in the proof.
Computing cutwidth is NP-complete in general [18], and the general-purpose implementations we tried could not compute the metric for our complete evaluation set in a feasible time. The problem becomes polynomial on trees [24], but the algorithm is complicated, and we are not aware of any implementation. Directed cutwidth on trees, however, admits a far simpler algorithm, which we now introduce and prove to be correct, since we could not find any publication that establishes this result.
Consider a tree = ⟨, ⟩ with vertices and directed edges pointing towards the leafs.2 A serialization of is a word ∈ * that contains each vertex ∈ at a unique position ∈ {1, . . . , | |} such that ⟨, ⟩ ∈ implies < . For ∈ {1, . . . , | | − 1}, the number of edges cut in the th gap between vertices in is cut() = |{⟨, ⟩ ∈ | ≤ < }|. The cutwidth cw() of is max1≤ <| | cut(), and the directed cutwidth cw( ) of is the minimal cutwidth of any serialization of . The out-degree of any vertex in is a lower bound for its directed cutwidth, though it can be higher (e.g., for a full binary tree , cw( ) is depth + 1). We omit directed below, since we consider no other kind of cutwidth on trees.
Definition 1. The standard serialization ( ) of a tree = ⟨, ⟩ is defined inductively. If = {}, then ( ) := . If | | > 1, then let be the root of and let 1, . . . , ℓ be its direct subtrees, ordered such that < implies cw(()) ≤ cw(( )); then ( ) := (1) · · · (ℓ).
For non-singleton trees , each of the sub-sequences () has ℓ − “overarching” edges from the root to the roots of later , > (see also Figure 5). Therefore, if the root of has ℓ children, cw(( )) = max({ℓ} ∪ {cw(()) + ℓ − | 1 ≤ ≤ ℓ}). It is easy to compute ( ) and cw(( )) in a bottom-up fashion. To do this in small steps, after computing () and cw(()) for all child trees of a vertex , we can add the children to one by one, in an order of non-decreasing cutwidth. The following lemma is the key to showing that this recursive procedure yields, for each partial subtree (with only some child trees added yet), the exact cutwidth. Its proof can be found in the extended version of the paper [25].
Lemma 1. For ∈ {1, 2}, let be a tree with root and cutwidth = cw() = cw() for an optimal serialization . Assume that 1, . . . , ℓ are the direct child trees below 1 in an order of non-decreasing cutwidth, and that 2 ≥ cw() for all 1 ≤ ≤ ℓ. Then the tree obtained from 1 by adding 2 as an additional direct child tree below 1 has cutwidth cw( ) = max(1 + 1, 2), and an optimal serialization is 12.
Now we can perform an easy induction over the structure of to show that the recursive computation of cw(( )) produces cw( ). The induction base are single-node trees (leafs), and the step is Lemma 1. Theorem 1. For trees , cw( ) = cw(( )), which can thus be computed in polynomial time.
We now describe the encoding of the calculi into existential rules with stratified negation in Nemo syntax, and the subsequent translation of rule-based reasoning traces into DL proofs. We have implemented this in the DL explanation library Evee.3
The implementation of the Elk calculus in existential rules with stratified negation is split into three stages [16]. The first stage consists of RDF import and normalization. Here, the input OWL ontology is translated into facts over several predicates with the prefix nf. These facts serve as the input for the calculus, e.g., nf:subClassOf(A,B) for ⊑ ∈ .4 The normalization takes advantage of the 2This edge direction is more intuitive for this section, but our results are readily applied to proof trees with edges oriented the other way (see Figures 4 and 5). Indeed, directed cutwidth is the same for the dual ordering. 3See https://github.com/de-tu-dresden-inf-lat/evee/tree/nemo-extractor/evee-nemo-proof-extractor 4More precisely, concept names are identified by IRIs, e.g., <http://example.org/iriA>, but we omit them here. OWL RDF encoding, which already contains a blank node for each complex concept that can be used as an auxiliary concept name identifying that concept. For example nf:exists(?C,?R,?D) states that ?C is an auxiliary concept name representing the existential restriction with role ?R and filler concept ?D. All such auxiliary concept names are marked by the predicate auxClass, which allows identifying the named concepts occurring in the input ontology using the rule
nf:isMainClass(?X) :- class(?X), ∼ auxClass(?X) .
Auxiliary role names are treated similarly. Since there can be multiple blank nodes denoting the same complex concept, there are additional existential rules that create unique representatives for these concepts, in order to avoid redundant computations. Additionally, the normalization stage precomputes the role hierarchy ⊑
* in the predicate nf:subProp.
The second stage consists of the actual inference rules of the Elk calculus, which derive additional facts over predicates with the prefix inf. Due to the normalization, the implementation of these rules is straightforward and close to the original calculus, for example for the rule R⊑:
inf:subClassOf(?C,?E) :- inf:subClassOf(?C,?D), nf:subClassOf(?D,?E) .
In the third stage, the interesting entailments, namely subsumptions between concept names, are extracted with the help of the inf:subClassOf and nf:isMainClass predicates. Modifications. We slightly adapted these rules for our purposes. All modifications are confined to the normalization and extraction; the inference rules of the calculus are not afected.
To the normalization stage, we added an inference rule that derives ⊥ ⊑ for each concept name
in the input, which ensures that ⊑ is inferred for any concept with |= ⊑ ⊥. Such reasoning
with the ⊥-concept is handled outside the calculus of Kazakov et al. [
Next, we updated the precomputation of the role hierarchy, which is recursively computed in a top-down manner, starting with the largest role in a set of connected role inclusions, rather than in a bottom-up fashion (as in the original rules).
directSubProp(?R,?S) :- TRIPLE(?R,rdfs:subPropertyOf,?S) . nf:subProp(?R,?R) :- nf:exists(?C,?R,?D), nf:isSubClass(?C) .
nf:subProp(?R,?T) :- directSubProp(?R,?S), nf:subProp(?S,?T) . For example, starting from ⊑ , ⊑ , ⊑ , we first derive ⊑ and then ⊑ . This modification is necessary, because the original implementation did not compute the role hierarchy correctly. It started from roles occurring negatively in (using nf:isSubClass as above), but only computed the role hierarchy above , the opposite of what is needed by R+. ∃
We also added support for transitivity and domain axioms by introducing two rules that translate domain(, ) into ∃.⊤ ⊑ and trans() into ∘ ⊑ . Moreover, we support the current OWL 2 encoding of role chains, i.e., owl:propertyChainAxiom, including role chains with more than two role names. Finally, we added the possibility to prove equivalence axioms ≡ directly from ⊑ and ⊑ .
Other Calculi. The same normalization is also utilized in the implementation of the Textbook and Envelope calculi. Additionally, we added the normalization predicates nf:subClassConj(?C,?D,?E) for ⊓ ⊑ , nf:subClassEx(?R,?C,?D) for ∃. ⊑ , and nf:supClassEx(?C,?R,?D) for ⊑ ∃., according to the normal forms expected by these calculi. The main inference rules of both calculi are implemented as expected, for example inf:subClassOf(?C,?F) :- inf:supClassEx(?C,?R,?D),
inf:subClassOf(?D,?E), nf:subProp(?R,?S), inf:subClassEx(?S,?E,?F) . for CR5′ from the Textbook calculus, and
R(?C,?R,?E) :- S(?C,?D), nf:supClassEx(?D,?R,?E)
for CR3 from the Envelope calculus, where we used the original names and [
Nemo allows us to obtain a trace of how a particular entailment, e.g., inf:subClassOf(A,B), was obtained using the rules. Such a trace is similar to a DL proof, but the vertices are labeled with ground facts instead of DL axioms. In the Java class NemoProofParser, we implemented a translation from such traces into valid DL proofs, which reads a Nemo trace in JSON format into an IProof<String> object, where each String represents a fact, and outputs an IProof<OWLAxiom> object5 that can be further processed or again saved in JSON format.
The abstract class AbstractAtomParser, instantiated for each of the three calculi, translates facts into DL axioms, e.g., inf:subClassOf(A,B) into ⊑ and nf:supClassEx(A,r,B) into ⊑ ∃.. Any fact that does not have a corresponding DL axiom, e.g., inf:init(A), is translated into ⊥ ⊑ ⊤, which indicates that the atom is skipped and will not appear in the final proof (see Section 2). In particular, traces contain many normalization steps that use various auxiliary predicates, which do not show up in the final DL proof.
Auxiliary concept names that are represented by blank nodes (either from the RDF encoding or from existential rules) need special treatment, since they would not make sense in the translated proof. Instead, we replace them by the concepts they denote. Since a fact containing a blank node, such as inf:subClassOf(A,_:61), does not contain information about the complex concept the blank node identifies, we need to collect other relevant facts from the trace. For example, nf:exists(_:61,t,D) encodes that _:16 stands for ∃.. If D is also a blank node, then we have to recursively consider more facts until we can construct the final concept.
However, this approach fails for complex role inclusions with auxiliary role names. For example, if ∘ ∘ ⊑ is normalized into nf:subPropChain(r,s,_:5) and nf:subPropChain(_:5,t,u), we cannot simply replace _:5 by ∘ , as this would yield ∘ ⊑ ∘ , which is not expressible in OWL due to ∘ on the right-hand side. Still, this axiom is a tautology, and can be omitted without afecting the correctness of the inference. During reasoning, auxiliary roles can appear in existential restrictions, e.g., in inf:supClassEx(C,_:5,D), which we translate into multiple nested existential restrictions: ⊑ ∃.∃..
Lastly, after translating the inference steps in the described manner, we minimize the size of the resulting OWL proof using the MinimalProofExtractor class, which eliminates redundant inferences and unnecessary tautologies [22]. In particular, this removes all occurrences of ⊥ ⊑ ⊤. As a result, we obtain a correct and complete DL proof from the Nemo reasoning trace.
We compared the proofs resulting from the three calculi on a benchmark of 1,573 reasoning tasks that
were extracted from the ORE 2015 ontologies [
From the structure of the calculi, we expected proofs of the Textbook calculus to be less linear and shallower, i.e., have larger directed cutwidth, larger bushiness score and smaller depth, because it does not restrict any premises of the inference rules to be from the input TBox (see also Figure 5), and therefore allows for more balanced proof trees. This was confirmed in the experiments, with the directed cutwidth of Textbook proofs being higher in 1,486 and 1,381 cases compared to Elk and Envelope, respectively, and never lower. Similarly, the bushiness score is higher for 1,534 and 1,512 proofs, and lower in only 12 and 23 cases, respectively. Conversely, the depth is lower for 1,503 proofs, and higher in only 8 cases, compared to both other calculi. We conjecture that the depth of the Textbook proofs is 5OWLAxiom is part of the Java OWL API [26]. approximately logarithmic in the depth of the corresponding Elk or Envelope proofs, and that the relationship for directed cutwidth and bushiness score is exponential. On the same three measures, the Elk and Envelope proofs behave very similarly, with Envelope proofs having slightly higher directed cutwidth and bushiness score, but nearly identical depth, compared to the Elk proofs.
We also compared directed cutwidth and bushiness score, since they both try to measure how linear proofs are. We observe that there is indeed a correlation between them; however, whereas directed cutwidth is always a natural number, bushiness score allows a more fine-grained comparison of proofs, and also tends to increase faster than the directed cutwidth.
For the remaining measures of size and average step complexity, the Elk calculus is the outlier, with both lower size (in 1,025 and 584 cases compared to Envelope and Textbook, respectively) and lower average step complexity (1,281 and 1,062 proofs, respectively). Here, Envelope and Textbook obtain very similar results, with slightly lower values for Textbook.
There is no clear winner across all the measures we considered. However, depending on specific use cases, proofs generated using certain calculi may be more preferable. Overall, proofs generated with the Elk calculus seem to be the better choice for providing explanations of entailments, since they are smaller and rely on simpler inferences. Additionally, Elk proofs have lower cutwidth and bushiness scores, indicating that axioms are used as soon as possible in the proof, which can be an advantage when reading the proofs in a linear format (see Figure 5). Conversely, the low depth of Textbook proofs may be a better option for other types of visualizations, since it can reduce the amount of vertical or horizontal scrolling required, which also allows users to inspect the proof in a more linear manner. Our experiment do not show a specific advantage for proofs generated using the Envelope calculus over the other two.
+ proofs, mainly for two reasons. First, the
The benchmarks are not fully representative of general ℰ ℒ⊥
benchmark does not contain all possible justifications and entailments from the ORE 2015 ontologies,
since for some cases it was too costly to compute all justifications [
We compared the proofs obtained from three reasoning calculi for the ℰ ℒ family of DLs. This was
facilitated by Nemo, a powerful rule engine that allowed us to quickly implement the calculi without
having to develop a dedicated reasoner. As expected, the Textbook calculus [13] indeed produces
more bushy and more shallow proofs, and it turns out that the Elk calculus [
This work was supported by BMFTR and DAAD in project 57616814 (SECAI, School of Embedded and Composite AI), and by DFG in grant 389792660 (TRR 248: CPEC, https://perspicuous-computing.science).
During the preparation of this work, the authors used ChatGPT 4 in order to: Paraphrase and reword, and grammar and spelling check. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. (LPAR’20), volume 73 of EPiC Series in Computing, EasyChair, 2020, pp. 32–67. doi:10.29007/ nhpp. [12] C. Alrabbaa, S. Borgwardt, T. Friese, A. Hirsch, N. Knieriemen, P. Koopmann, A. Kovtunova, A. Krüger, A. Popovic, I. S. R. Siahaan, Explaining reasoning results for OWL ontologies with Evee, in: P. Marquis, M. Ortiz, M. Pagnucco (Eds.), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR 2024), 2024. doi:10.24963/KR. 2024/67. [13] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge
University Press, 2017. URL: http://dltextbook.org/. doi:10.1017/9781139025355. [14] M. Krötzsch, Eficient rule-based inferencing for OWL EL, in: T. Walsh (Ed.), Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI’11), IJCAI/AAAI, 2011, pp. 2668–2673. doi:10.5591/978-1-57735-516-8/IJCAI11-444. [15] D. Carral, I. Dragoste, M. Krötzsch, Reasoner = logical calculus + rule engine, Künstliche Intell. 34 (2020) 453–463. doi:10.1007/S13218-020-00667-6. [16] A. Ivliev, L. Gerlach, S. Meusel, J. Steinberg, M. Krötzsch, Nemo: Your friendly and versatile rule reasoning toolkit, in: P. Marquis, M. Ortiz, M. Pagnucco (Eds.), Proceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning (KR’24), 2024. doi:10.24963/KR.2024/70. [17] B. Parsia, N. Matentzoglu, R. S. Gonçalves, B. Glimm, A. Steigmiller, The OWL reasoner evaluation (ORE) 2015 competition report, J. Autom. Reason. 59 (2017) 455–482. doi:10.1007/ S10817-017-9406-8. [18] H. L. Bodlaender, M. R. Fellows, D. M. Thilikos, Derivation of algorithms for cutwidth and related graph layout parameters, J. Comput. Syst. Sci. 75 (2009) 231–244. doi:10.1016/J.JCSS.2008. 10.003. [19] M. Horridge, S. Bail, B. Parsia, U. Sattler, Toward cognitive support for OWL justifications, Knowl.
Based Syst. 53 (2013) 66–79. doi:10.1016/j.knosys.2013.08.021. [20] Y. Kazakov, P. Klinov, A. Stupnikov, Towards reusable explanation services in Protege, in: A. Artale, B. Glimm, R. Kontchakov (Eds.), Proceedings of the 30th International Workshop on Description Logics (DL’17), volume 1879 of CEUR Workshop Proceedings, CEUR-WS.org, 2017. URL: http://ceur-ws.org/Vol-1879/paper31.pdf. [21] J. Méndez, C. Alrabbaa, P. Koopmann, R. Langner, F. Baader, R. Dachselt, Evonne: A visual tool for explaining reasoning with OWL ontologies and supporting interactive debugging, Computer Graphics Forum (2023). doi:https://doi.org/10.1111/cgf.14730. [22] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding good proofs for description logic entailments using recursive quality measures, in: A. Platzer, G. Sutclife (Eds.), Proceedings of the 28th International Conference on Automated Deduction (CADE’21), volume 12699 of LNCS, Springer, 2021, pp. 291–308. doi:10.1007/978-3-030-79876-5_17. [23] C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, On the complexity of finding good proofs for description logic entailments, in: S. Borgwardt, T. Meyer (Eds.), Proceedings of the 33rd International Workshop on Description Logics (DL 2020), volume 2663 of CEUR Workshop Proceedings, CEUR-WS.org, 2020. URL: http://ceur-ws.org/Vol-2663/paper-1.pdf. [24] M. Yannakakis, A polynomial algorithm for the min-cut linear arrangement of trees, J. ACM 32 (1985) 950–988. doi:10.1145/4221.4228. [25] C. Alrabbaa, S. Borgwardt, P. Herrmann, M. Krötzsch, The shape of ℰℒ proofs: A tale of three calculi (extended version), 2025. doi:10.48550/arXiv.2507.21851. [26] M. Horridge, S. Bechhofer, The OWL API: A Java API for OWL ontologies, Semantic Web 2 (2011) 11–21. doi:10.3233/SW-2011-0025. [27] C. Alrabbaa, S. Borgwardt, P. Herrmann, M. Krötzsch, The shape of EL proofs: A tale of three calculi - DL25 - Resources, 2025. doi:10.5281/zenodo.16320822.