Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)

T0 review · 3 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The calculus chosen for EL reasoning decides the proof's shape.

desk verdict The directed cutwidth algorithm is solid and worth refereeing; the empirical shape comparison is a useful pipeline but the headline conclusions are not yet supported because of the single-trace bias. read the letter →

arxiv 2507.21851 v1 pith:CA2WWD5W submitted 2025-07-29 cs.LO

Christian Alrabbaa , Stefan Borgwardt , Philipp Herrmann , Markus Krötzsch This is my paper · ORCID
classification cs.LO MSC 68R1068T27
keywords descriptionlogicsELfamilyconsequence-basedreasoningproofexplanationNemoruleenginedirectedcutwidthshapeontology
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

When a description logic ontology entails something, the proof you see depends not only on the ontology but on the reasoning calculus that derives it. This paper demonstrates that point for three calculi in the EL family—Elk, Envelope, and Textbook—by implementing all three uniformly on top of the Nemo rule engine, translating execution traces back into OWL proofs, and measuring 1,573 benchmark entailments. The measurements show Textbook proofs are the shallowest and most bushy, while Elk proofs are the smallest and use the least complex inference steps, with Envelope in between. These differences matter for proof explanation and visualization: a user who wants to scroll less vertically should get Textbook-style proofs, while a user who wants to understand each step quickly should get Elk-style proofs. The paper also contributes a polynomial-time algorithm for directed cutwidth on trees, the metric used to quantify how linear a proof is.

What carries the argument

Two mechanisms carry the paper. First, the translation of all three calculi into existential rules with stratified negation, executed by the Datalog-based engine Nemo, lets the same tracing machinery produce derivations for each calculus from a shared normalisation stage; traces are then mapped back to DL axioms, with auxiliary blank nodes expanded into the complex concepts they denote, and minimized. Second, the directed cutwidth metric is made practical by the standard serialization of a rooted tree, defined inductively by ordering child subtrees in increasing order of their cutwidths; Theorem 1 shows this serialization already achieves the optimal cutwidth, enabling bottom-up polynomial computation. The paper also introduces a bushiness score (size divided by depth plus one) to capture how non-linear a proof is.

What would settle it

For the empirical claim, rerun a sample of benchmark tasks with Nemo modified to enumerate all traces (or to randomize rule scheduling across many runs) and recompute depth and bushiness for Textbook; if Textbook proofs are not systematically shallower and bushier than Elk and Envelope over the full trace distribution, the central comparison fails. For the algorithmic claim, brute-force all serializations of random trees up to ten nodes and compare the minima with the cutwidth of the standard serialization; any mismatch would refute Theorem 1.

Watch

Extended reading notes

Core claim

The central claim is that the shape of a proof is a property of the calculus, not just of the entailment. Using the same normalisation and proof-extraction pipeline for all three calculi, the paper observes that the Textbook calculus yields proofs with higher directed cutwidth and bushiness scores and lower depth than the other two; the Elk calculus yields smaller proofs with lower average step complexity; and Envelope offers no consistent advantage. In addition, Theorem 1 states that for every tree the directed cutwidth equals the cutwidth of its standard serialization, so this metric can be computed in polynomial time by a simple bottom-up procedure. The paper treats these as empirical findings plus a proved theorem, and interprets them as a basis for choosing a calculus to match a target explanation format.

Load-bearing premise

The comparison assumes the single execution trace Nemo happens to return for each reasoning task is representative of what the calculus as such produces; Section 6.1 admits this trace is biased toward smaller depth.

Editorial extensions

If this is right

  • Proof explanation tools can pick a calculus to match the display: Elk for compact, linear-friendly proofs; Textbook for shallow, bushy trees that scroll less vertically.
  • The directed cutwidth of proof trees can be computed in polynomial time, so this metric becomes usable at scale without a dedicated solver.
  • Because all three calculi are encoded uniformly as existential rules, a new calculus can be compared by changing only the rule set, not the proof extraction pipeline.
  • For users who want to understand individual inference steps, Elk's lower average step complexity is preferable; for users who want an overview, Textbook's shallow proofs help.
  • Envelope shows no specific advantage over the other two calculi on the measured proof shape, so it is a weaker candidate for explanation-oriented reasoning.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • [Editorial inference] If Nemo were extended to enumerate all traces rather than one, the exact magnitudes might change, but the direction of the Textbook versus Elk contrast could persist or even strengthen, since the reported bias is toward shallow traces, which favors Textbook.
  • [Editorial inference] The directed-cutwidth theorem likely generalizes to any rooted tree with edges pointing away from the root, so it applies beyond proof trees to any tree-shaped dependency structure.
  • [Editorial inference] The observed comparison suggests a trade-off principle: smaller proof size and step complexity come at the cost of greater depth, so an ideal explanation system may need a hybrid calculus rather than a single one.
  • [Editorial inference] The same experimental design could be applied to consequence-based calculi for more expressive logics such as ALC, as the paper itself plans for future work.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper compares the shape of proofs produced by three consequence-based calculi for the EL family of description logics: the Elk calculus, the Textbook calculus, and the Envelope calculus. The calculi are encoded as existential rules with stratified negation and executed using the Nemo rule engine; the resulting traces are translated into DL proofs, minimized, and compared on five metrics: size, depth, directed cutwidth, bushiness score, and average step complexity. The evaluation on 1,573 reasoning tasks from ORE 2015 reports that Textbook proofs are more bushy and shallower, while Elk proofs are smaller with less complex inference steps. The paper also contributes a polynomial-time algorithm and proof for computing the directed cutwidth of a tree (Theorem 1 and Lemma 1).

Significance. The question of how the choice of reasoning calculus affects proof shape is relevant for proof explanation and visualization. If established, the empirical results could guide tool builders in selecting a calculus matched to a visualization format. The algorithmic result in Section 4 is a clean and useful contribution that appears correct and fills a gap in the literature. The paper is generally well written, and the implementation and benchmark data are shared. The main weakness is that the comparative conclusions rest on a single trace per task, a limitation the authors explicitly concede in Section 6.1; because this limitation is in the same direction as the headline shape claims, the empirical evidence does not as written support the central conclusion.

major comments (3)
  1. [Section 6 and 6.1] The shape comparison is based on exactly one trace per task returned by Nemo. Section 6.1 states: 'Nemo always computes only one trace... there is a systematic bias in the resulting proofs... Nemo traces seem to be biased towards smaller depth.' The headline claims in Section 7 that Textbook produces 'more bushy and more shallow proofs' rely on the depth, bushiness, and directed cutwidth metrics, all of which are directly affected by this bias. Since the bias is in the same direction as the observed effect, the pairwise differences (e.g., Textbook has lower depth in 1,503 cases) could be artifacts of Nemo's trace-selection algorithm rather than of the calculi. To support the comparative conclusion, the paper should either sample multiple traces per task and report the within-calculus variance, or demonstrate that Nemo's selection does not alter the relative ordering of the calculi on the shape metrics. The size and step-complexity results are less affected because proofs are minimized after extraction and those metrics are less shape-dependent, but the headline shape comparison is not established as written.
  2. [Section 2, 'Proofs' and modifications] The translation of the original calculi into DL proofs drops init(C) statements and side conditions of the form 'X occurs negatively in T', adds rules for deriving role-hierarchy axioms, and replaces C r->E with C⊑∃r.E. The paper asserts that these changes do not change the comparative shape of proofs (paragraph after the example in Figure 4), but this is not supported by an argument or an experiment. Since the comparison is intended to reflect properties of the three calculi, the transformation could introduce shape differences that are not intrinsic to the rule design. For example, the additional role-hierarchy rules might increase depth in some calculi more than in others. A sensitivity analysis on a subset of tasks, or a formal statement of the shape preservation property, would be needed to justify the comparison.
  3. [Section 5.2] After translating Nemo traces, the proofs are minimized using MinimalProofExtractor to eliminate redundant inferences and unnecessary tautologies. The paper reports that this reduces size, but it also applies the minimization before measuring depth, cutwidth, and bushiness. The effect of this post-processing on the shape metrics is not discussed. Since the paper uses these metrics to compare calculi, it is possible that minimization changes the relative order. The paper should report metrics before and after minimization for a sample of tasks, or otherwise argue that minimization preserves the relative ordering on the shape metrics.
minor comments (5)
  1. [Section 2] Figure 3 appears to include rules CR1 and CR2 even though the text says 'We also add CR1 and CR2 to the Envelope calculus'; clarify whether the figure shows the original or the modified version.
  2. [Section 6] The parenthetical counts in Figures 7-11 (e.g., 'Elk(8) Envelope(188)') are not explained in the captions; state what these numbers represent.
  3. [Section 6.1] The sentence 'In this case, Nemo traces seem to be biased towards smaller depth, which allows us to observe the differences between the calculi and confirms our initial intuitions' reads as if the bias is a helpful feature, whereas it is a threat to validity; please rephrase.
  4. [Section 3] The claim that justification size 'does not depend on the reasoning calculus' seems too strong, since different proofs may use different sets of axioms; if justification size is defined as the number of distinct leaf axioms, it can vary across proofs.
  5. [Throughout] Minor typos: 'Our experiment do not show' in Section 6 should be 'Our experiments do not show'; in the abstract 'the calculus of the ELK reasoner' should be 'the ELK reasoner's calculus' or similar.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation chain; the empirical comparison and the cutwidth theorem are independently computed, though the evaluation relies heavily on the authors' own tools and a single trace per task.

full rationale

The paper's central claims are derived from running three concrete calculi in Nemo and measuring proof metrics on the resulting traces. No parameter is fitted to the reported outcomes, and no metric is defined in terms of the hypotheses. The directed cutwidth result (Theorem 1) is proved from Lemma 1 with explicit assumptions and an appendix proof that does not presuppose the theorem; it is mathematically self-contained. Section 6.1 candidly states that Nemo computes only one trace per task and that its traces are biased toward smaller depth. That admission undermines the generality of the empirical comparison, but it is a stated limitation about trace-selection bias, not a circular step: the bias is not constructed from the measured metrics, and the paper does not define Textbook's shallowness into the evaluation. The authors do cite and reuse their own prior work for the benchmark, Evee, and Nemo encodings, but the implementations are available, the traces are freshly generated, and the cited results are not invoked as unverified premises. Thus there is no reduction of the conclusions to their inputs, and the mild self-dependency does not amount to circularity.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No free parameters are fitted in the paper. The central comparative claim depends on the correctness of the three cited calculi and on the adequacy of the Nemo trace translation. The side-condition omission is an ad hoc modeling choice that could affect proof shape, so it is listed as an axiom of the analysis.

assumptions (4)
  • standard math Standard description logic semantics for ELH_bot, including role compositions, as given in [2, 5, 13].
    Used throughout Section 2 to define proofs and inference steps.
  • domain assumption The three calculi are sound and complete for their respective fragments.
    Correctness is cited from the original papers (Kazakov et al. 2014, Baader et al. 2017, Baader et al. 2005), not reproved in this paper.
  • domain assumption The Nemo trace plus the Java translation produces a correct minimal DL proof.
    Section 5.2 gives an informal argument and relies on the MinimalProofExtractor; no formal verification is provided.
  • ad hoc to paper Side conditions and init statements can be dropped without changing the comparative shape of proofs.
    Section 2 removes 'occurs negatively' side conditions and init(C), and Section 5.2 maps non-DL atoms to bottom-top; this is a design choice specific to producing OWL-only proofs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Shape of $\mathcal{EL}$ Proofs: A Tale of Three Calculi (Extended Version)." pith.science (2026). https://pith.science/paper/CA2WWD5W

@misc{pith2026250721851,
  author       = {Pith},
  title        = {Pith review of: The Shape of $\mathcalEL$ Proofs: A Tale of Three Calculi (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CA2WWD5W}},
  note         = {Machine review of arXiv:2507.21851}
}
abstract

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 $\mathcal{EL}$ family of DLs, each of which gives rise to proofs of different 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 effective 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 different aspects of their complexity.

Figures

Figures reproduced from arXiv: 2507.21851 by the authors.

Figure 1
Figure 1. Optimized Elk calculus [5]. CR1 𝐶 ⊑ 𝐶 CR2 𝐶 ⊑ ⊤ 𝐶 ⊑ 𝐷1 𝐶 ⊑ 𝐷2 𝐷1 ⊓ 𝐷2 ⊑ 𝐸 CR4 𝐶 ⊑ 𝐸 𝐶 ⊑ 𝐷 𝐷 ⊑ 𝐸 CR3 𝐶 ⊑ 𝐸 𝐶 ⊑ ∃𝑟.𝐷1 𝐷1 ⊑ 𝐷2 ∃𝑠.𝐷2 ⊑ 𝐸 CR5′ : 𝑟 ⊑* 𝒯 𝑠 𝐶 ⊑ 𝐸 𝐶 ⊑ ∃𝑟.𝐸 𝐸 ⊑ ⊥ R ′ ⊥ 𝐶 ⊑ ⊥ [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Textbook calculus [13] with a modified CR5 and added variant of R⊥. 𝐶 ⊑ 𝐷 CR1 : 𝐷 ⊑ 𝐸 ∈ 𝒯 𝐶 ⊑ 𝐸 𝐶 ⊑ 𝐷1 𝐶 ⊑ 𝐷2 CR2 : 𝐷1 ⊓ 𝐷2 ⊑ 𝐸 ∈ 𝒯 𝐶 ⊑ 𝐸 𝐶 ⊑ 𝐷 CR3 : 𝐷 ⊑ ∃𝑟.𝐸 ∈ 𝒯 𝐶 ⊑ ∃𝑟.𝐸 𝐶 ⊑ ∃𝑟.𝐷1 𝐷1 ⊑ 𝐷2 CR4 : ∃𝑟.𝐷2 ⊑ 𝐸 ∈ 𝒯 𝐶 ⊑ 𝐸 𝐶 ⊑ ∃𝑟.𝐷 𝐷 ⊑ ⊥ CR5 𝐶 ⊑ ⊥ 𝐶 ⊑ ∃𝑟.𝐸 CR10 : 𝑟 ⊑ 𝑠 ∈ 𝒯 𝐶 ⊑ ∃𝑠.𝐸 𝐶 ⊑ ∃𝑟1.𝐷 𝐷 ⊑ ∃𝑟2.𝐸 CR11 : 𝑟1 ∘ 𝑟2 ⊑ 𝑠 ∈ 𝒯 𝐶 ⊑ ∃𝑠.𝐸 [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Envelope calculus [2], restricted to ℰℒ+ ⊥. 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 𝒯 . Finally, [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Example proofs based on Elk (top left), Textbook (top right), and Envelope (bottom) 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…
Figure 5
Figure 5. Figure 5: Different visual representations of a proof: nested list (left), linear (middle), proof tree (right). that, despite the transformations and simplifications we applied, the three calculi can still result in substantially different proofs, even for such a simple entailme…
Figure 6
Figure 6. Figure 6: Relation between bushiness score and directed cutwidth 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 Elk (8) Envelope (188) Directed Cutwidth 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 Elk (0) Textbook (1486) Directed Cutwidth 0 1 2 3 4 5 6 7 0 1 2 3 4 5 6 7 Envelope (0) Textbook (1381) Direct…
Figure 7
Figure 7. Figure 7: Directed cutwidth. Circle area is scaled proportionally to the number of corresponding proofs. 0 1 2 3 4 5 6 7 8 9 10 11 0 1 2 3 4 5 6 7 8 9 10 11 Elk (53) Envelope (1042) Bushiness Score 0 1 2 3 4 5 6 7 8 9 10 11 0 1 2 3 4 5 6 7 8 9 10 11 Elk (12) Textbook (1534) Bush…
Figure 8
Figure 8. Figure 8: Bushiness score [PITH_FULL_IMAGE:figures/full_fig_p016_8.png]
Figure 9
Figure 9. Figure 9: Depth 0 60 120 180 240 300 360 420 0 60 120 180 240 300 360 420 Elk (82) Envelope (1281) Average Step Complexity 0 60 120 180 240 300 360 420 0 60 120 180 240 300 360 420 Elk (202) Textbook (1062) Average Step Complexity 0 60 120 180 240 300 360 420 0 60 120 180 240 30…
Figure 10
Figure 10. Figure 10: Average step complexity 0 15 30 45 60 75 90 105 120 135 0 15 30 45 60 75 90 105 120 135 Elk (27) Envelope (1025) Tree Size 0 15 30 45 60 75 90 105 120 135 0 15 30 45 60 75 90 105 120 135 Elk (607) Textbook (584) Tree Size 0 15 30 45 60 75 90 105 120 135 0 15 30 45 60 …
Figure 11
Figure 11. Figure 11: Tree Size [PITH_FULL_IMAGE:figures/full_fig_p017_11.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$

    cs.AI 2026-08 conditional novelty 7.0 of 10 partial

    Moose compiles OWL 2 EL ontologies into a Lean-verified differentiable weighted-model-counting layer and uses it to learn latent concept labels under partial supervision, beating propositional neuro-symbolic baselines...

Reference graph

Works this paper leans on

28 extracted references · 23 canonical work pages · cited by 1 Pith paper

  1. [1]

    Brandt, Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else?, in: R

    S. Brandt, Polynomial time reasoning in a description logic with existential restrictions, GCI axioms, and—what else?, in: R. L. de Mántaras, L. Saitta (Eds.), Proceedings of the 16th European Conference on Artificial Intelligence (ECAI’04), IOS Press, 2004, pp. 298–302. URL: https://www.frontiersinai.com/ecai/ecai2004/ecai04/p0298.html

    work page 2004

  2. [2]

    Baader, S

    F. Baader, S. Brandt, C. Lutz, Pushing the EL envelope, in: L. P. Kaelbling, A. Saffiotti (Eds.), Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI’05), Professional Book Center, 2005, pp. 364–369. URL: http://ijcai.org/Proceedings/ 05/Papers/0372.pdf

    work page 2005

  3. [3]

    Tena Cucala, B

    D. Tena Cucala, B. Cuenca Grau, I. Horrocks, Consequence-based reasoning for description logics with disjunction, inverse roles, number restrictions, and nominals, in: J. Lang (Ed.), Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI’18), ijcai.org, 2018, pp. 1970–1976. doi:10.24963/IJCAI.2018/272

    work page doi:10.24963/ijcai.2018/272 2018

  4. [4]

    Tena Cucala, B

    D. Tena Cucala, B. Cuenca Grau, I. Horrocks, 15 years of consequence-based rea- soning, in: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (Eds.), Description Logic, Theory Combination, and All That: Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, volume 11560 of LNCS, Springer, 2019, pp. 573–587. doi:10.1007/978-3-030-22102-7_27

    work page doi:10.1007/978-3-030-22102-7_27 2019

  5. [5]

    Kazakov, M

    Y. Kazakov, M. Krötzsch, F. Simančík, The incredible ELK: From polynomial procedures to efficient reasoning withℰℒ ontologies, J. Autom. Reason. 53 (2014) 1–61. doi:10.1007/ s10817-013-9296-3

    work page 2014

  6. [6]

    Steigmiller, T

    A. Steigmiller, T. Liebig, B. Glimm, Konclude: System description, J. Web Semant. 27-28 (2014) 78–85. doi:10.1016/J.WEBSEM.2014.06.003

    work page doi:10.1016/j.websem.2014.06.003 2014

  7. [7]

    A. Bate, B. Motik, B. Cuenca Grau, D. Tena Cucala, F. Simančík, I. Horrocks, Consequence- based reasoning for description logics with disjunctions and number restrictions, J. Artif. Intell. Res. 63 (2018) 625–690. doi:10.1613/JAIR.1.11257

    work page doi:10.1613/jair.1.11257 2018

  8. [8]

    Kazakov, P

    Y. Kazakov, P. Klinov, Goal-directed tracing of inferences in EL ontologies, in: P. Mika, T. Tudorache, A. Bernstein, C. Welty, C. A. Knoblock, D. Vrandečić, P. Groth, N. F. Noy, K. Janowicz, C. A. Goble (Eds.), Proceedings of the 13th International Semantic Web Conference (ISWC’14), volume 8797 of LNCS, Springer, 2014, pp. 196–211. doi:10.1007/ 978-3-319...

    work page 2014

Show all 28 references
  1. [9]

    Horridge, B

    M. Horridge, B. Parsia, U. Sattler, Justification oriented proofs in OWL, in: P. F. Patel- Schneider, Y. Pan, P. Hitzler, P. Mika, L. Zhang, J. Z. Pan, I. Horrocks, B. Glimm (Eds.), Proceedings of the 9th International Semantic Web Conference (ISWC’10), volume 6496 of LNCS, Sp...

    2010 doi

  2. [10]

    Schlobach, Explaining subsumption by optimal interpolation, in: J

    S. Schlobach, Explaining subsumption by optimal interpolation, in: J. J. Alferes, J. A. Leite (Eds.), Proceedings of the 9th European Conference on Logics in Artificial Intel- ligence (JELIA’04), volume 3229 of LNCS, Springer, 2004, pp. 413–425. doi: 10.1007/ 978-3-540-30227-8_35

    2004

  3. [11]

    Alrabbaa, F

    C. Alrabbaa, F. Baader, S. Borgwardt, P. Koopmann, A. Kovtunova, Finding small proofs for description logic entailments: Theory and practice, in: E. Albert, L. Kovács (Eds.), Proceedings of the 23rd International Conference on Logic for Programming, Artificial Intelligence and...

    2020 doi

  4. [12]

    Alrabbaa, S

    C. Alrabbaa, S. Borgwardt, T. Friese, A. Hirsch, N. Knieriemen, P. Koopmann, A. Kov- tunova, 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 ...

    2024 doi

  5. [13]

    Baader, I

    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

    2017 doi

  6. [14]

    Krötzsch, Efficient rule-based inferencing for OWL EL, in: T

    M. Krötzsch, Efficient 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

    2011 doi

  7. [15]

    Carral, I

    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

    2020 doi

  8. [16]

    Ivliev, L

    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

  9. [17]

    Parsia, N

    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

    2017

  10. [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

    2009 doi

  11. [19]

    Horridge, S

    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

    2013 doi

  12. [20]

    Kazakov, P

    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,

  13. [21]

    Méndez, C

    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

    2023 doi

  14. [22]

    Alrabbaa, F

    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. Sut- cliffe (Eds.), Proceedings of the 28th International Conference on Automated Deduc- tion (CADE’21), ...

    2021

  15. [23]

    Alrabbaa, F

    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 W...

    2020

  16. [24]

    Yannakakis, A polynomial algorithm for the min-cut linear arrangement of trees, J

    M. Yannakakis, A polynomial algorithm for the min-cut linear arrangement of trees, J. ACM 32 (1985) 950–988. doi:10.1145/4221.4228

    1985

  17. [25]

    Horridge, S

    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

    2011 doi

  18. [26]

    Alrabbaa, S

    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. A. Proof of Lemma 1 Lemma 1. For 𝑖∈{ 1, 2}, let 𝑇𝑖 be a tree with root 𝑟𝑖 and cutwidth 𝑤𝑖 = cw(𝑇𝑖) = cw(𝑆𝑖) for an optima...

    2025 doi

  19. [28]

    We abbreviate 𝑤𝑠 1 = cw(𝑆′ 1), and note that 𝑤𝑠 1≥ 𝑤1 = cw(𝑇 )

    = max({ℓ}∪{ cw(𝐶𝑖) + ℓ− 𝑖| 1≤ 𝑖≤ ℓ}). We abbreviate 𝑤𝑠 1 = cw(𝑆′ 1), and note that 𝑤𝑠 1≥ 𝑤1 = cw(𝑇 ). Case (A): If 𝑤𝑠 1 = ℓ, since 𝑤1≥ ℓ and cw(𝑇 )≥ ℓ + 1 (cutwidth≥ out-degree), we get 𝑤1 = ℓ and cw(𝑇 )≥ 𝑤1 + 1, contradicting cw(𝑇 ) = 𝑤1. Case (B): There is 𝑚∈{ 1, . . . , ℓ} ...

  20. [2017]

    URL: http://ceur-ws.org/Vol-1879/paper31.pdf

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.