{"id":"a73da33e-684d-48e8-95da-75a9331ac0e6","arxiv_id":"2608.12961","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":4,"one_line_summary":"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 on relational and role-chain MNIST regimes.","lead":"Moose turns OWL 2 EL ontologies, the logic behind SNOMED CT and the Gene Ontology, into a differentiable exact-inference layer, so a neural network can learn hidden labels from partial observations plus logical constraints. Its correctness proofs are machine-checked in Lean, and it reports large accuracy gains on relational and role-chain tasks, though its own ablation ties those gains to added closure axioms rather than to the EL logic alone.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The role-pinning ABox encoding of existentials as universal Horn clauses breaks the exactness of the supervision channel: the NF3/NF4 grounding of E⊑∃R.C enforces a universal reading and omits any existence clause, so the Stage-7 SDD's model set can differ from the ontology's ABox models, and…","rationale":"I read the paper in good faith. The authors state their formal results precisely, disclose the role-pinning caveat in Stage 7, in Table 5, and in the Limitations section, and they are careful to call the ABox encoding a Moose-specific choice rather than an ELK theorem. The Lean verification covers the TBox-level compilation and the DISPONTE correspondence for subsumption entailment, not the production ABox grounding. The reader's weakest assumption identifies the same spot: the transfer from cmp(O,C,D) to the grounded SDD is unproven and, on close inspection, the NF3 encoding is not merely unproven but actually unsound as a model-preserving translation of existential restrictions. A minimal ontology with one existential exposes both directions of the mismatch: the clause set admits E(a) with no R-witness, and it forbids E(a) when a named R-successor is not in C even if an alternative witness exists. Pinning role atoms by evidence removes uncertainty about role values but does not repair the missing existence clause or the overconstraint from multiple named R-successors. Since the WMC layer is used as the training loss and as the posterior computation, this is load-bearing for the paper's central claim of an exact supervision channel. However, the empirical headline gains are not solely dependent on this formal exactness: the MNIST experiments use role atoms that are observed, and the closure ablation shows that Φclos, not the existential encoding, carries most of the learning signal. The paper's own conditional framing and honest reporting mean the proper verdict is still CONDITIONAL, not reject or accept outright. I agree with the reader's weakest assumption and would keep the verdict unchanged while requiring the ABox soundness question to be settled or explicitly scoped out of the exactness claims.","tokens_in":46331,"tokens_out":6363,"duration_ms":80044,"concrete_test":"Construct the Stage-7 SDD for the minimal ontology O={E⊑∃R.C} over ∆={a,b}, with E(a) observed true and R(a,b) latent at weight 1/2, and compare model sets by brute-force enumeration: (i) assignments M satisfying the ontology in the finite-domain sense (there exists z with M(R(a,z))=1 and M(C(z))=1) versus (ii) assignments satisfying Γ = {¬E(a)∨¬R(a,b)∨C(b)} from Algorithm 1. If, as expected, the assignment E(a)=1, R(a,b)=0, C(b)=0 is in Γ's model set but not in the ontology's model set, the ABox encoding is not model-preserving, and the exactness claim for the learning pipeline fails without an added existence clause such as E(a) → ⋁_{b∈∆} (R(a,b)∧C(b)). This check can be done with a 4-variable exhaustive count or as a Lean theorem about the grounded clause set.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The load-bearing premise is the transfer of the verified TBox-level compilation (Theorems 1–4) to the production ABox encoding of Stage 6–7. The Links extractor emits, for each derived link (E,R,C), the clause ¬E(a)∨¬R(a,b)∨C(b) over named pairs a≠b, plus an NF4 reverse clause when the witness concept is unique. This is a universal reading: it says every named R-successor of an E-instance must be in C. EL++ existential semantics says only that at least one R-successor must be in C. Moreover, no clause enforces existence at all: an assignment with E(a)=true, R(a,b)=false, C(b)=false satisfies the Horn clause vacuously but is not a model of E⊑∃R.C over a closed domain. The paper's own Stage-7 remark concedes that soundness depends on role atoms over Sig_o_R being pinned by evidence and that this is 'a Moose-specific encoding choice for the finite-named-domain regime, not an ELK theorem.' Table 5 similarly concedes that unobserved role witnesses are not hypothesized. Because the same SDD is the sole training-signal channel, the claim that the WMC is an exact distribution-semantics marginal for the learning pipeline is not covered by Theorem 2, which concerns WMC_Q(cmp(O,C,D),w) over axiom-selection worlds for C⊑D entailment, not over ABox assignments. This is not an internal inconsistency: the paper discloses the caveat. It is a scope gap in the central exactness claim, and it is exactly the assumption that would have to hold for the compiled SDD to be an exact supervision channel.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"Moose compiles an EL++ ontology and a finite ABox domain into a Sentential Decision Diagram (SDD) and uses the SDD's weighted model count as a differentiable supervision signal for learning per-individual classifiers over latent concept atoms. The paper's formal core is a set of four theorems: a verified SDD encoding of the ELK saturation, a rational DISPONTE distribution-semantics correspondence, and SCC-compositional factorizations at the Sat and WMC levels, all claimed to be machine-checked in Lean 4. The empirical part introduces an MNIST-with-ontology benchmark in three supervision regimes (atomic, relational, role-chain) plus a Pizzaiolo transfer track, and reports gains over propositional NeSy, fuzzy, and ontology-embedding baselines, together with a reasoning-shortcut analysis using BEARS and NeSyDM wrappers.","tokens_in":46597,"tokens_out":8732,"duration_ms":93516,"significance":"If the claims hold, the contribution is substantial: a formally verified compilation of an OWL profile into a tractable circuit, a distribution-semantics correspondence for probabilistic ontology reasoning, and the first reasoning-shortcut analysis in an ontology setting. The paper is unusually transparent and careful in several respects: it ships a Lean 4 library with a stated audit-clean axiom footprint, an explicit assumptions table (Table 5), a closure ablation (Section F.10), paired significance tests over 20 seeds (Section F.8), an inductive held-out-edge split (Section F.9), and reproducible code and data. These are genuine strengths. The central caveat, however, is that the four verified theorems concern the TBox-level circuit cmp(O,C,D) over axiom-selection worlds, while the production learning signal is the Stage 6-7 ABox encoding whose soundness rests on an unproven role-pinning assumption that the paper itself labels 'not an ELK theorem.' Because the exactness of the supervision channel is the paper's main claimed advantage over fuzzy and embedding alternatives, this gap is load-bearing.","major_comments":[{"comment":"The four verified theorems certify the TBox-level circuit cmp(O,C,D) over axiom-selection worlds, not the Stage 6-7 ABox encoding used for learning. Stage 6 grounds a saturation link (E,R,C) as the universal Horn clause ¬E(a)∨¬R(a,b)∨C(b), plus an NF4 reverse clause when the witness concept is unique; this is a universal reading of an existential axiom and omits any existence clause. The manuscript itself concedes in Stage 7 and in Limitations (iii) that soundness depends on role atoms over Sig_o_R being pinned by evidence and that this is 'a Moose-specific encoding choice for the finite-named-domain regime, not an ELK theorem.' Section D.2 then asserts without proof that soundness of the four-extractor encoding follows from Theorem 5 under role-pinning. The consequence is load-bearing: the entailment oracle of Eq. (13) can return a false positive because an assignment with E(a)=true and all R(a,b) false is a model of the Horn clauses but not of E⊑∃R.C over a closed domain. Theorem 2, which concerns WMC_Q(cmp(O,C,D),w) for axiom weights, does not cover the ABox-atom weights of Table 1. The paper should either prove a dedicated soundness/completeness theorem for the Stage 6-7 encoding under explicit assumptions (including existence witnesses), or weaken the exactness claims and characterize the approximation error.","section":"§3.2 (Stage 7), §D.2, Eq. (13)"},{"comment":"Section 3.1 invokes Theorem 2 to assert that the WMC layer's output is a probability under the per-atom product distribution defined by Table 1. But Theorem 2's formal statement is about a different object: cmp(O,C,D) with rational weights on ontology axioms, measuring entailment over axiom-selection worlds. The learning pipeline's weights in Table 1 are per ground ABox atom C(a), R(a,b), and the two WMCs coincide only if a further equivalence is proved. This is not a notation issue: TBox-level worlds index subsets of axioms, while ABox worlds assign truth to ground atoms. The paper should state and prove a transfer lemma for the ABox encoding, or explicitly limit the 'formal contract' claim to the probabilistic-ontology-reasoning use case and describe the learning signal as an approximation.","section":"§3.1, Theorem 2, Table 1"},{"comment":"The role-pinning assumption is not satisfied in one of the reported benchmarks. Experiment 1 uses |∆|=1 with no role evidence, so succ(a,a) and plus_two(a,a) receive weight 1/2 under Table 1. The Stage 6 Links clauses for the ten successor existentials are therefore active in the compiled SDD under the universal reading, and neither Theorem 5 nor Theorem 2 certifies that the resulting WMC equals the distribution-semantics marginal for the Exp-1 training signal. This is not a merely theoretical concern: the paper's own Table 5 concedes that 'unobserved role witnesses are not hypothesized.' The exactness claims should be scoped to regimes in which role-pinning provably holds, with Experiment 1 either excluded from the exactness claim or supplied with a separate argument.","section":"§5.1, Experiment 1, Table 1"},{"comment":"The abstract and contribution list claim 'polynomial intermediate sizes' as part of the formal contribution, but Section 3.3 states that the polynomial saturation-closure bound of Theorem 6 applies to the EL Horn fragment only and does not transfer to ΓEL∪Φclos, and Section D.5 gives an exponential worst case for SDD compilation under rising treewidth. Since the headline MNIST results use the closure-augmented variant and the closure ablation (Section F.10) shows that most of the empirical gain comes from Φclos, the 'polynomial intermediate sizes' phrasing overstates what is proved for the shipped system. The claims should be qualified so that the reader can see that the polynomial bound applies to the EL fragment and that the closure-augmented pipeline has only an empirical complexity statement.","section":"Abstract, §3.3, §D.5"}],"minor_comments":[{"comment":"The DeepProbLog rows on Pizza tracks A-C are not separate runs, as Section F.6 explains, yet the Table 2 caption does not say so. A reader comparing rows could mistakenly attribute independent performance to DeepProbLog; the caption should carry the same ‡ note as Table 9.","section":"Table 2 caption and §F.6"},{"comment":"There is an inconsistency in the use of the label 'NF7.' Table 4 lists BBL normal form NF7 as ⊥⊑A, while Section F.2 calls the role-chain axiom succ◦succ⊑plus_two 'NF7.' This notation collision should be corrected, for example by using 'role-chain axiom' instead of NF7 in the experimental section.","section":"§F.2 and Table 4"},{"comment":"Theorem 5's completeness is conditional on OWL2ELFragment (branches (a)-(e)), and Section A states that the branches are not jointly compatible. The main text should state this condition alongside the theorem, not only in the appendix, to avoid the impression that full EL++ completeness is verified in all cases.","section":"§D.1, Theorem 5"},{"comment":"Table 9 notes that RScons and F1macro on Track A are computed on the in-distribution eval block, not on the OOD harness. The main text should state this restriction where Track A is discussed, so the reader does not interpret those columns as OOD metrics.","section":"Table 9, Pizza Track A"},{"comment":"The discussion of family-argmax accuracy on Pizza Track B would be clearer if Table 10 appeared earlier in the main text: the current presentation in Section F.7 argues convincingly that AccF is uninformative there, and that argument belongs next to the definition of the Pizza metrics.","section":"§5.3, Table 10"}],"recommendation":"major_revision","confidential_remarks":"The formal TBox-level results are impressive and the authors are unusually transparent about assumptions, including the role-pinning caveat and the closure-axiom scope. The blocker is the unproven transfer from cmp(O,C,D) to the production ABox encoding: the exactness of the supervision channel is the central claim, and it currently rests on an assumption the paper itself labels as not an ELK theorem. I would support a major revision that either proves a dedicated ABox-level soundness theorem under explicit hypotheses and verifies those hypotheses in every reported regime, or rewrites the exactness claims as approximate with a quantified error. I would also ask that the DeepProbLog rows on Pizza be clearly labeled as reproductions of the Moose WMC values."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Two things to know. The formal part is the real contribution: a Lean-checked compilation from EL++ saturation to SDDs, with a rational DISPONTE correspondence and a clean statement of what is verified. That is new and it is solid. The second thing is that the paper's headline exactness claim about the learning signal is not covered by those theorems. The ABox encoding grounds an existential E⊑∃R.C as a universal Horn clause over named pairs, and it omits the existence condition entirely. If a role atom is not pinned by evidence, the SDD's models include assignments that violate the ontology. The authors disclose this in Stage 7 and in the limitations, so it is not hidden, but the abstract still says the SDD's models \"coincide with ABox interpretations satisfying the entailments,\" which is only true under a role-pinning assumption that the experiments only partially satisfy.\n\nWhat the paper does well: the Lean mechanization is substantial and audit-clean, the compilation pipeline with role chains and role hierarchies closes a real capability gap, the reasoning-shortcut analysis is the first in an OWL EL setting, and the empirical reporting is unusually honest—paired tests, a closure ablation, and a clear statement of what is not covered. The closure ablation is especially useful: it shows the MNIST gains are largely due to the non-EL closure clauses, not to the EL compilation alone. That is a scope limitation, not a flaw.\n\nSoft spots, in proportion. The role-pinning issue is the most serious: it means the WMC layer is not an exact distribution-semantics marginal for the learning pipeline, only an approximation with a disclosed caveat. This should be fixed either by adding existence clauses or by restricting the exactness claims to the pinned-role regime. The empirical scale is tiny—|∆|=2, with a 40x compile-time jump at |∆|=4—so the ontology-scale motivation is not yet demonstrated. The Pizzaolo result is weaker than the MNIST story: plain Moose equals DeepProbLog by construction there, and LTN matches or beats it on Track C. Also, the public artifacts are promised but no commit hash is given, so the machine-checked claims cannot yet be independently re-run.\n\nWho this is for: anyone working on neuro-symbolic learning with description logics or on verified knowledge compilation. It deserves a serious referee, but the referee should push on the ABox soundness gap and on the role-pinning assumption before the exactness claims are accepted.","headline":"Lean-verified EL compilation is the real contribution; the ABox-level exactness claim is narrower than the abstract suggests, and the role-pinning caveat deserves a major revision rather than a desk reject.","tokens_in":47334,"tokens_out":3903,"would_cite":true,"duration_ms":48223,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Moose compiles OWL 2 EL ontologies into an exact differentiable reasoning layer, enabling latent concept learning from partial ABox evidence.","keywords":["OWL 2 EL","description logic","neuro-symbolic learning","knowledge compilation","sentential decision diagram","weighted model counting","latent concept learning","reasoning shortcuts"],"falsifier":"Take the ontology with a single axiom $E \\sqsubseteq \\exists R.C$ and domain $\\Delta=\\{a,b\\}$, with evidence $E(a)=\\mathrm{true}$, $\\neg C(a)$, $\\neg C(b)$, and no role atom for $R$ asserted. Under EL++ semantics no model exists because the existential witness for $E(a)$ can be neither $a$ nor $b$, so the correct marginal probability is zero. Moose's grounded clause set is satisfied by setting $R(a,b)=\\mathrm{false}$, giving a nonzero weighted model count and violating the claimed WMC/entailment correspondence on this instance.","tokens_in":2030,"feed_emoji":"🧠","tokens_out":2398,"duration_ms":113705,"temperature":0.7,"pith_summary":"Moose tries to establish that OWL 2 EL ontologies, the description-logic profile behind SNOMED CT and the Gene Ontology, can be compiled into an exact and differentiable reasoning layer rather than approximated by embeddings or fuzzy relaxations. The paper compiles a finite EL++ ontology into a sentential decision diagram whose weighted model count equals the distribution-semantics marginal of the ontology, making the circuit a faithful supervision channel for learning latent concept classifiers from partial ABox evidence. On relational and role-chain MNIST regimes, the closure-augmented variant reaches 74.6 and 96.1 percent family-argmax accuracy, against 38.9 and 59.6 for a propositional neuro-symbolic baseline, and it reports the first reasoning-shortcut analysis for OWL EL. A reader should care because production ontologies use EL, and existing neuro-symbolic learners accept only propositional theories or Datalog, not ontology axioms with role chains.","feed_headline":"EL++ ontology logic becomes an exact training signal","feed_subtitle":"Weighted model counting over the compiled ontology lifts relational latent-concept accuracy by tens of points.","key_machinery":"The central object is a sentential decision diagram (SDD), a tractable Boolean circuit whose smooth, decomposable, and deterministic structure makes weighted model counting linear in circuit size. The construction first saturates the ontology with consequence-based completion rules, then extracts only the ABox-relevant consequences: atomic subsumptions, disjointness clauses, unsatisfiable concepts, and existential role links, adding a reverse clause when the witness concept is unique. Those clauses, together with optional closure clauses over exhaustive families, are compiled into the SDD; neural perception outputs become the per-atom literal weights, and the training objective is the negative log weighted model count of the diagram with observed evidence clamped.","core_discovery":"At the TBox level, the paper's central mathematical discovery is the compilation identity stated in Theorem 2: for every EL++ ontology $O$, every pair of concepts $C,D$, and every rational weight function $w$, the weighted model count of the compiled sentential decision diagram equals the rational distribution-semantics marginal, $\\mathrm{WMC}_{\\mathbb{Q}}(\\mathrm{cmp}(O,C,D),w)=P_{\\mathbb{Q}}(O,C,D,w)$. That identity makes the circuit an exact and differentiable oracle for entailment, so one diagram supports a training loss, a conditional posterior, and a perception-free entailment query. At the ABox level, the pipeline grounds the saturated consequence set as Horn clauses over the finite named domain, adds optional closure clauses on modeller-declared exhaustive families, and learns per-individual classifiers for latent concept atoms by maximizing the weighted model count of the evidence. The paper claims that this pipeline outperforms propositional neuro-symbolic baselines by tens of points on relational and role-chain tasks, and that the gain separates cleanly: the EL-aware grounding propagates evidence across individuals, while closure clauses render the latent signal learnable when no exhaustive family is otherwise constrained.","pith_inferences":["Editorial: the cleanest extension is latent-role learning: if unobserved role atoms are freed from the uniform one-half weight and predicted from perception, the same weighted-model-count layer could supervise role assertions, an open direction the paper itself names.","Editorial: the role-pinning caveat draws a sharp boundary for exactness: the method is exact precisely when all observably used witness roles are pinned by evidence, so ontologies with genuinely latent existential witnesses may require explicit witness variables or lifted reasoning.","Editorial: because the large MNIST gains depend on closure axioms outside the EL profile, applying the approach to open-world biomedical ontologies requires deciding which families are exhaustive; the reported advantage may track that modelling choice as much as the EL compilation itself.","Editorial: scaling to SNOMED-sized knowledge bases is blocked by circuit growth, since the SDD size scales empirically as roughly the square of the domain size with a sharp compile-time jump at four individuals; lifted weighted model counting would be needed."],"forward_implications":["Any OWL 2 EL ontology with a finite named ABox can supervise latent concept learning without a hand-written propositional translation, preserving role hierarchies and role chains.","The weighted-model-count and distribution-semantics identity means training gradients are exact rather than sampled or relaxed, and inference on the SDD is linear in its node count.","On the MNIST-style relational and role-chain regimes, the closure-augmented variant beats the propositional baseline by 35.7 and 36.5 points in family-argmax accuracy, but the ablation shows that removing the closure clauses collapses accuracy to near chance.","Reasoning-shortcut mitigations transfer from propositional settings to OWL EL: under symbolic ambiguity, ensemble diversification favors accuracy while diffusion-style distributions favor calibration, whereas plain Moose is best when forward subsumption pins the latent vector.","The same compiled circuit serves as training loss, posterior estimator, and entailment oracle through one linear-time traversal, so the learned perception and the exact reasoner share a single artifact."],"supporting_citations":[{"why":"Supplies the consequence-based saturation calculus whose soundness and completeness the compilation relies on.","marker":"[26]"},{"why":"Defines the neural-probabilistic marginal loss that the method generalizes and equates on the Horn theory.","marker":"[39]"},{"why":"Supplies the semantic-loss objective, the negative log weighted model count used as the training loss.","marker":"[51]"},{"why":"Defines sentential decision diagrams and their compilation and weighted-model-counting properties.","marker":"[20,17]"},{"why":"Defines the DISPONTE distribution semantics whose rational marginal is equated to the SDD's weighted model count.","marker":"[44]"},{"why":"Establishes the reasoning-shortcut phenomenon and its root causes, which the EL-based analysis port.","marker":"[41]"},{"why":"Proves that per-atom independence is incompatible with reasoning-shortcut awareness, motivating the mitigation wrappers.","marker":"[29]"},{"why":"Contributes the ensemble-diversification mitigation evaluated in the reasoning-shortcut experiments.","marker":"[40]"},{"why":"Contributes the masked discrete-diffusion concept distribution evaluated in the reasoning-shortcut experiments.","marker":"[30]"},{"why":"Defines the EL++ profile and the normal forms used throughout the encoding.","marker":"[5]"}],"fun_headline_variants":["Exact entailment oracle turns EL++ into a differentiable loss","Moose: SDD-weighted EL++ gives exact gradients for latent concepts","First reasoning-shortcut-aware learner for OWL EL ontologies","Compile EL++ to SDD: exact entailment as a training signal","EL++ exactness lifts latent-concept accuracy by tens of points"],"cache_read_input_tokens":49024,"weakest_assumption_plain":"The load-bearing premise is that every observable role atom within the finite named domain is pinned by evidence, so that encoding an existential axiom $E \\sqsubseteq \\exists R.C$ as the universal Horn clause $\\neg E(a) \\lor \\neg R(a,b) \\lor C(b)$ preserves the ontology's models; when a witnessing role is unobserved, the compiled circuit can admit models the ontology does not have.","fun_headline_variants_meta":{"raw":{"variants":["Exact entailment oracle turns EL++ into a differentiable loss","Moose: SDD-weighted EL++ gives exact gradients for latent concepts","First reasoning-shortcut-aware learner for OWL EL ontologies","Compile EL++ to SDD: exact entailment as a training signal","EL++ exactness lifts latent-concept accuracy by tens of points"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000308,"raw_usage":{"total_tokens":1797,"prompt_tokens":1016,"completion_tokens":781,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":632,"completion_tokens_details":{"reasoning_tokens":689}},"tokens_in":632,"tokens_out":781,"duration_ms":6940,"temperature":1.0,"reasoning_tokens":689,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:43:53.970604+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take the ontology with a single axiom $E \\sqsubseteq \\exists R.C$ and domain $\\Delta=\\{a,b\\}$, with evidence $E(a)=\\mathrm{true}$, $\\neg C(a)$, $\\neg C(b)$, and no role atom for $R$ asserted. Under EL++ semantics no model exists because the existential witness for $E(a)$ can be neither $a$ nor $b$, so the correct marginal probability is zero. Moose's grounded clause set is satisfied by setting $R(a,b)=\\mathrm{false}$, giving a nonzero weighted model count and violating the claimed WMC/entailment correspondence on this instance.","supporting_citations":[{"cited_title":"In: Advances in Neural Informa- tion Processing Systems 31 (NeurIPS)","cited_arxiv_id":null,"evidence_quote":"Defines the neural-probabilistic marginal loss that the method generalizes and equates on the Horn theory."},{"cited_title":"In: Proceedings of the 35th International Conference on Machine Learning (ICML)","cited_arxiv_id":null,"evidence_quote":"Supplies the semantic-loss objective, the negative log weighted model count used as the training loss."},{"cited_title":"Semantic Web6(5), 477–501 (2015)","cited_arxiv_id":null,"evidence_quote":"Defines the DISPONTE distribution semantics whose rational marginal is equated to the SDD's weighted model count."},{"cited_title":"In: Advances in Neural Information Processing Systems 36 (NeurIPS)","cited_arxiv_id":null,"evidence_quote":"Establishes the reasoning-shortcut phenomenon and its root causes, which the EL-based analysis port."},{"cited_title":"In: Proceedings of the 41st International Conference on Machine Learning (ICML)","cited_arxiv_id":null,"evidence_quote":"Proves that per-atom independence is incompatible with reasoning-shortcut awareness, motivating the mitigation wrappers."},{"cited_title":"In: Advances in Neural Information Processing Systems 39 (NeurIPS) (2025)","cited_arxiv_id":null,"evidence_quote":"Contributes the masked discrete-diffusion concept distribution evaluated in the reasoning-shortcut experiments."},{"cited_title":"In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI)","cited_arxiv_id":null,"evidence_quote":"Defines the EL++ profile and the normal forms used throughout the encoding."}],"review_version":1}