{"id":"bd6eabba-06a6-47c1-a52c-2ca30ba6c82f","arxiv_id":"2507.21851","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"An empirical comparison of three EL calculi shows proof shape varies predictably with rule design, with an accompanying new algorithm for directed cutwidth on trees.","lead":"This paper compares the proofs generated by three description logic calculi by encoding them in a rule engine and shows that the shape of a proof depends on the calculus, one producing small simple proofs and another producing shallow bushy proofs. It also contributes a polynomial algorithm for measuring directed cutwidth on proof trees.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The comparative claim is not supported because Nemo returns a single, depth-biased trace per task; Section 6.1 admits this, so the reported Textbook/Elk shape differences may be an artifact of trace selection rather than of the calculi.","rationale":"The reader's weakest assumption correctly identifies the load-bearing issue: the comparison depends on a single trace per task, and the paper itself discloses that Nemo's traces are systematically biased toward smaller depth. The Textbook-vs-Elk differences in depth, bushiness, and cutwidth are exactly the metrics most likely to be distorted by that bias, so the main empirical conclusion is conditional. The directed cutwidth algorithm is a separate contribution with a self-contained proof and available code, and I see no internal flaw there; the concern is specifically about the empirical attribution of proof shape to the calculus. Since the paper already states the limitation in Section 6.1 and the authors plan to revisit it when multi-trace support is available, the appropriate verdict remains CONDITIONAL. My stress-test does not move the reader's verdict, so no change is needed.","tokens_in":15051,"tokens_out":13188,"duration_ms":174495,"concrete_test":"For a random sample of ~100 benchmark tasks, enumerate all non-redundant proofs (or all proofs up to the minimal size) for each of the three calculi using an independent proof search, and compute the full distribution of depth, bushiness score, and directed cutwidth. Then check whether the Nemo-selected trace lies inside that distribution and whether the Textbook-vs-Elk ordering under Nemo's default trace is reproduced by the median or by a random draw from the distribution. If the ordering flips or the Nemo trace is an outlier, the Section 7 conclusion is an artifact of trace selection; if the ordering is stable across the whole proof space, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central conclusion in Section 7 is that the Textbook calculus produces more bushy and shallower proofs and that Elk yields smaller, less complex proofs. The evidence for this is one Nemo trace per benchmark task. Section 6.1 concedes that Nemo always computes only one trace and that there is a systematic bias in the resulting proofs, specifically that Nemo traces seem to be biased towards smaller depth. Since depth, bushiness, and directed cutwidth are exactly the metrics on which Textbook is declared superior, the default trace-selection heuristic is entangled with the outcome. A single trace is not a draw from the proof space: without knowing the within-calculus variance of proof shapes or Nemo's selection distribution, the large pairwise differences (e.g., Textbook shallower in 1,503 cases, higher cutwidth in 1,486/1,381 cases) cannot be attributed to rule design. The size and step-complexity results are less vulnerable because proofs are minimized after extraction and the metric is less shape-dependent, but the headline shape conclusion is not established. The directed cutwidth theorem, by contrast, is independent of this issue and appears sound; the weakness is empirical, not algorithmic.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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).","tokens_in":15297,"tokens_out":9326,"duration_ms":97853,"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":[{"comment":"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.","section":"Section 6 and 6.1"},{"comment":"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.","section":"Section 2, 'Proofs' and modifications"},{"comment":"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.","section":"Section 5.2"}],"minor_comments":[{"comment":"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.","section":"Section 2"},{"comment":"The parenthetical counts in Figures 7-11 (e.g., 'Elk(8) Envelope(188)') are not explained in the captions; state what these numbers represent.","section":"Section 6"},{"comment":"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.","section":"Section 6.1"},{"comment":"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.","section":"Section 3"},{"comment":"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.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper is suited to the DL workshop venue. The main concern is whether the empirical comparison can be fixed within a revision: the authors could re-run the experiments with a modified Nemo that can produce multiple traces, or provide evidence that the current trace selection does not affect relative rankings. The algorithmic part is solid and could be extracted if the empirical part cannot be fully remedied. The tools and benchmark originate from the authors' own group, which is not itself a problem, but it means the trace-selection bias is within their control and should be addressed explicitly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: The directed cutwidth algorithm is the real contribution, and it appears sound. The comparative calculus story is a good idea but the empirical support is weaker than the conclusion section claims, and the authors' own limitation paragraph basically says why.\n\nWhat's new: The polynomial-time algorithm for directed cutwidth on trees (Theorem 1) via the standard serialization, with Lemma 1 proved in the appendix, is clean and useful. That alone merits publication. The Nemo-to-DL proof translation pipeline and the benchmark of 1,573 tasks are also carefully built, and the code and data are available.\n\nWhere it gets soft: The headline claim that Textbook produces bushier, shallower proofs rests on a single Nemo trace per task. Section 6.1 admits Nemo's traces are systematically biased toward smaller depth. Since depth, bushiness, and cutwidth are exactly the metrics where Textbook is declared superior, the observed differences may be an artifact of Nemo's trace selection rather than the calculi. The size and step-complexity results are less exposed because the proofs are minimized after extraction, but the shape conclusions are not established. The authors are transparent about this, so it isn't a hidden flaw, but the conclusion section overstates what the data can show.\n\nAlso note: the benchmark and tools come from the authors' own group, which is fine for a measurement study but adds a mild dependency.\n\nBottom line: The algorithmic result deserves serious refereeing, and the empirical pipeline is a useful foundation. The paper should be accepted only if the comparative claims are tempered or supported by a sampling over multiple traces. As is, the conclusion needs revision, but the core work is sound. For peer review: yes, worth sending out.","headline":"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.","tokens_in":15793,"tokens_out":2710,"would_cite":true,"duration_ms":28793,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68R10","68T27"],"pacs":[],"model":"deepseek-v4-flash","headline":"The calculus chosen for EL reasoning decides the proof's shape.","keywords":["description logics","EL family","consequence-based reasoning","proof explanation","Nemo rule engine","directed cutwidth","proof shape","ontology reasoning"],"falsifier":"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.","tokens_in":14868,"feed_emoji":"🌳","tokens_out":6287,"duration_ms":65411,"temperature":0.7,"pith_summary":"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.","feed_headline":"The EL calculus you choose shapes the proof you get","feed_subtitle":"On 1,573 reasoning tasks, Textbook proofs run shallow and bushy; Elk proofs come out smallest and simplest.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["[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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the Envelope calculus, one of the three rule sets compared.","marker":"[2]"},{"why":"Supplies the Elk calculus and its optimized inference rules, the baseline reasoner.","marker":"[5]"},{"why":"Supplies the Textbook calculus, the third rule set, from the description logic textbook.","marker":"[13]"},{"why":"Provides the Nemo rule engine and its trace output, the implementation substrate for all three calculi.","marker":"[16]"},{"why":"Provides the benchmark of 1,573 reasoning tasks and the notion of non-redundant proofs used throughout.","marker":"[11]"},{"why":"Supplies the ORE 2015 ontologies from which the benchmark tasks are extracted.","marker":"[17]"},{"why":"Defines cutwidth and shows computing it is NP-complete in general, motivating the tree algorithm.","marker":"[18]"},{"why":"Gives the earlier polynomial algorithm for cutwidth on trees that the paper's directed version simplifies.","marker":"[24]"},{"why":"Defines the cognitive step-complexity measure used to compare inference steps.","marker":"[19]"},{"why":"Provides the proof-minimization technique used to clean the translated traces.","marker":"[22]"}],"fun_headline_variants":["Proof shape is set by calculus, not just entailment","Textbook proofs: shallow and bushy; Elk: small and simple","Three EL calculi, three distinct proof shapes","Which EL calculus gives simplest proofs? Elk study says","Directed cutwidth: fast to compute for tree-shaped proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Proof shape is set by calculus, not just entailment","Textbook proofs: shallow and bushy; Elk: small and simple","Three EL calculi, three distinct proof shapes","Which EL calculus gives simplest proofs? Elk study says","Directed cutwidth: fast to compute for tree-shaped proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000186,"raw_usage":{"total_tokens":1271,"prompt_tokens":836,"completion_tokens":435,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":452,"completion_tokens_details":{"reasoning_tokens":354}},"tokens_in":452,"tokens_out":435,"duration_ms":5943,"temperature":1.0,"reasoning_tokens":354,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T12:17:34.259150+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Baader, S","cited_arxiv_id":null,"evidence_quote":"Supplies the Envelope calculus, one of the three rule sets compared."},{"cited_title":"Kazakov, M","cited_arxiv_id":null,"evidence_quote":"Supplies the Elk calculus and its optimized inference rules, the baseline reasoner."},{"cited_title":"Ivliev, L","cited_arxiv_id":null,"evidence_quote":"Provides the Nemo rule engine and its trace output, the implementation substrate for all three calculi."},{"cited_title":"Alrabbaa, F","cited_arxiv_id":null,"evidence_quote":"Provides the benchmark of 1,573 reasoning tasks and the notion of non-redundant proofs used throughout."},{"cited_title":"Parsia, N","cited_arxiv_id":null,"evidence_quote":"Supplies the ORE 2015 ontologies from which the benchmark tasks are extracted."},{"cited_title":"Yannakakis, A polynomial algorithm for the min-cut linear arrangement of trees, J","cited_arxiv_id":null,"evidence_quote":"Gives the earlier polynomial algorithm for cutwidth on trees that the paper's directed version simplifies."},{"cited_title":"Horridge, S","cited_arxiv_id":null,"evidence_quote":"Defines the cognitive step-complexity measure used to compare inference steps."},{"cited_title":"Alrabbaa, F","cited_arxiv_id":null,"evidence_quote":"Provides the proof-minimization technique used to clean the translated traces."}],"review_version":1}