Paper deep dive
Moose: Latent concept learning with reasoning-shortcut awareness in $\mathcal{EL}^{++}$
Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho, Robert Hoehndorf
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 8/14/2026, 5:40:47 AM
Summary
The paper introduces Moose, a neuro-symbolic learning method that compiles OWL 2 EL++ ontologies (TBox and ABox) into Sentential Decision Diagrams (SDDs) to enable differentiable weighted model counting. It addresses latent concept learning under partial supervision, overcoming the limited expressivity of EL++ by adding closure clauses. The method is validated for termination, soundness, and completeness, and evaluated on MNIST-with-ontology and Pizzaïolo datasets, showing improvements over propositional neuro-symbolic, fuzzy-logic, and ontology embedding baselines. It also provides the first reasoning-shortcut analysis in an OWL EL setting.
Entities (13)
Relation Signals (12)
Moose → processes → OWL 2 EL
confidence 95% · We present Moose, a method that compiles an EL++ TBox and finite ABox...
Moose → uses → Sentential Decision Diagram
confidence 95% · We present Moose, a method that compiles an EL++ TBox and finite ABox to a Sentential Decision Diagram (SDD).
Moose → analyzes → Reasoning Shortcut
confidence 90% · ...presents the first reasoning-shortcut analysis in an OWL EL setting.
Moose → evaluateson → MNIST-with-ontology
confidence 90% · ...evaluate Moose on MNIST-with-ontology and Pizzaïolo.
Moose → evaluateson → Pizzaïolo
confidence 90% · ...evaluate Moose on MNIST-with-ontology and Pizzaïolo.
OWL 2 EL → usedin → SNOMED CT
confidence 90% · The OWL 2 EL profile is used in some of the largest production ontologies, including the Gene Ontology and SNOMED CT.
OWL 2 EL → usedin → Gene Ontology
confidence 90% · The OWL 2 EL profile is used in some of the largest production ontologies, including the Gene Ontology...
Moose → improvesover → propositional-NeSy
confidence 88% · Moose improves over propositional-NeSy, fuzzy-logic, and ontology embedding baselines...
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The OWL 2 EL profile is used in some of the largest production ontologies, including the Gene Ontology and SNOMED CT. Existing neuro-symbolic (NeSy) learning methods accept propositional theories or Datalog, and reasoning-shortcut (RS) awareness has not been investigated in ontology settings. We present Moose, a method that compiles an $\mathcal{EL}^{++}$ TBox and finite ABox to a Sentential Decision Diagram (SDD). The SDD acts as a differentiable weighted-model-counting layer, and we add closure clauses outside the $\mathcal{EL}^{++}$ profile on declared exhaustive families to overcome the limited expressivity of $\mathcal{EL}^{++}$ under partial supervision. We show termination, soundness, completeness, and polynomial intermediate sizes, and validate the proofs in Lean. We then define the first formal partial-supervision latent-concept-learning task over an OWL EL ontology, i.e., learning per-individual classifiers for latent concepts from observed ABox literals, and evaluate Moose on MNIST-with-ontology and Pizzaïolo. Moose improves over propositional-NeSy, fuzzy-logic, and ontology embedding baselines, and presents the first reasoning-shortcut analysis in an OWL EL setting.
Tags
Links
- Source: https://arxiv.org/abs/2608.12961v1
- Canonical: https://arxiv.org/abs/2608.12961v1
Trouble viewing inline? Open PDF directly →
Full Text
181,743 characters extracted from source content.
Expand or collapse full text
Moose: Latent concept learning with reasoning-shortcut awareness in ℰℒ++EL^++ Olga Mashkova OrcID: 0000-0002-4916-1660 Affiliation: Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia Asaad Mohammedsaleh OrcID: 0009-0007-3160-8819 Affiliation: Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia Affiliation: E-mail first_name.last_name@kaust.edu.sa Fernando Zhapa-Camacho and Robert Hoehndorf OrcID: 0000-0002-0710-2259 OrcID: 0000-0001-8149-5890 Affiliation: Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia Affiliation: Computer Science Program, Computer, Electrical, and Mathematical Sciences & Engineering Division, King Abdullah University of Science and Technology, Thuwal 23955, Saudi Arabia Abstract The OWL 2 EL profile is used in some of the largest production ontologies, including the Gene Ontology and SNOMED CT. Existing neuro-symbolic (NeSy) learning methods accept propositional theories or Datalog, and reasoning-shortcut (RS) awareness has not been investigated in ontology settings. We present Moose, a method that compiles an ℰℒ++EL^++ TBox and finite ABox to a Sentential Decision Diagram (SDD). The SDD acts as a differentiable weighted-model-counting layer, and we add closure clauses outside the ℰℒ++EL^++ profile on declared exhaustive families to overcome the limited expressivity of ℰℒ++EL^++ under partial supervision. We show termination, soundness, completeness, and polynomial intermediate sizes, and validate the proofs in Lean. We then define the first formal partial-supervision latent-concept-learning task over an OWL EL ontology, i.e., learning per-individual classifiers for latent concepts from observed ABox literals, and evaluate Moose on MNIST-with-ontology and Pizzaïolo. Moose improves over propositional-NeSy, fuzzy-logic, and ontology embedding baselines, and presents the first reasoning-shortcut analysis in an OWL EL setting. Keywords: OWL 2 EL neuro-symbolic learning knowledge compilation weighted model counting reasoning shortcuts. 1 Introduction The OWL 2 EL profile underpins some of the largest and most widely-used ontologies, such as the Gene Ontology with ∼ 50K classes and ∼ 8M annotations [3, 49], SNOMED CT [22], and most of the OBO Foundry ontologies [45, 25], because EL trades expressivity for polynomial-time reasoning on subsumption, instance checking, and consistency [5, 26]. Neuro-symbolic (NeSy) learning combines neural perception with symbolic constraints; several families coexist. Fuzzy / t-norm methods replace propositional truth with continuous operators on [0,1][0,1] [7]; embedding methods score entities and relations in a continuous geometry [36, 15, 16]; knowledge-compilation methods compile the constraint to an arithmetic circuit whose weighted model count (WMC) is differentiable in the inputs [39, 51, 43, 1]. The knowledge-compilation family retains an exact WMC of the constraint as its training signal under partial supervision. The task we address, ABox-supervised latent concept learning, takes the following form. Each training instance supplies one perceptual input per named individual (e.g. an image of a digit) together with a partial set of ABox literals over an observable signature; the truth values of atoms over a separate latent signature are never directly supervised. The objective is to learn per-individual classifiers for the truth values of latent concept atoms. A WMC layer over a circuit compiled from the ontology supplies the training signal: evaluated with the perception’s per-atom outputs and clamped on the observed evidence, the layer scores how compatible the perception’s predictions are with the ontology, and the gradient steers the perception toward configurations that the constraints admit. When several latent configurations satisfy the same evidence, no method can recover the true labels from supervision alone; per-atom-independent predictors fail to recognize this and collapse to high confidence on a single arbitrary configuration rather than spreading mass over the satisfying ones [39, 41, 29]. Existing knowledge-compilation NeSy frameworks accept propositional formulas, Datalog programs, or finite-domain rules [39, 51, 43, 1], but not OWL ontologies directly. Two recent works target description logics: a domino-style reduction of ℒℐALCI to a probabilistic circuit [37] that treats the circuit as a regulariser under full label supervision, and a fuzzy approximation of ℰℒ++EL^++ via Goguen-implication semantics [53] that targets knowledge-base completion without exact WMC or compilation soundness; neither performs partial-supervision concept learning over OWL EL. Embedding methods such as ELEmbeddings and OWL2Vec∗ [36, 15] map ontology structure to a continuous geometry (via geometric model-theoretic constraints or graph walks respectively), trading exact entailment for differentiability. A separate body of work on reasoning shortcuts (RS) [41, 40, 29, 31, 30, 9] formally proves that conditional independence among predicted concepts is incompatible with RS-awareness, and develops mitigation strategies (BEARS ensembles, neuro-symbolic diffusion); these results are stated entirely in propositional or Datalog NeSy. OWL 2 EL underpins many production ontologies, so the RS phenomena documented in propositional settings translate directly into uncertainty-modeling failures in deployed ontology-driven systems. Translations of OWL EL into other formalisms are well established: it is Datalog-rewritable [33, 11], and probabilistic [12, 13] and fuzzy [53, 8] variants have been studied at length. However, a rewriting yields a reasoning procedure rather than a learning signal, and the probabilistic and fuzzy variants relax or re-specify the model-theoretic semantics rather than compiling it. Here we present Moose, a method that compiles an ℰℒ++EL^++ ontology and a finite ABox domain into a Sentential Decision Diagram [20, 17] whose models coincide with ABox interpretations satisfying the entailments of the input ontology, paired with a learning framework that uses the differentiable circuit as the sole supervision channel for latent concept atoms and provides the first RS analysis in an OWL EL setting. Our contributions are: 1. End-to-end OWL 2 EL compilation with full proofs. We compile the EL profile, including role chains R1∘R2⊑SR_1 R_2 S and role hierarchies (the constructs that distinguish SNOMED CT and the Gene Ontology from a propositional or ℒℐALCI setting), via ELK-style saturation [26] to an SDD supporting WMC. The four formal contributions are a verified SDD encoding (Theorem 4.1), the rational DISPONTE [44] distribution-semantics correspondence (Theorem 4.2), and SCC-compositional factorizations at the Sat and WMC levels (Theorems 4.3 and 4.4). All four are mechanized in Lean 4 (no Moose-specific axioms; Appendices 0.D and 0.D.10), along with the supporting Lean libraries for ELK saturation, soundness/completeness on ℰℒ++EL^++ [26], and SDD knowledge compilation, which to our knowledge are the first such formalizations (Section 0.D.1). The closure-augmented variant is correct (Theorem 0.D.3) and inference is linear in the SDD (Theorem 0.D.4). 2. ABox-supervised latent concept learning under partial axiom observation. We pose a learning task in which a subset of ABox literals over the observable signature is given as evidence (with truth values written true and false, so that they are not confused with the ℰℒ++EL^++ concepts ⊤ and ⊥ ), and the goal is to learn per-individual classifiers for the truth values of latent concept atoms (role atoms are observed or marginalized, never classified), to our knowledge the first such formulation over an OWL EL ontology, generalizing DeepProbLog [39] and Semantic Loss [51] to description logic constraints with role chains and role hierarchies. 3. Reasoning-shortcut analysis transposed to OWL EL. We compute family-argmax accuracy, expected calibration error (ECE), and the RS-consistency rate under Moose and two plug-in mitigations (Moose+BEARS [40] and Moose+NeSyDM [30]), and isolate a calibration-vs-accuracy trade-off: BEARS leads on family-argmax accuracy via ensemble diversification on RS-suspect inputs, NeSyDM leads on calibration (ECE) under symbolic ambiguity. 4. A benchmark suite. A single MNIST-with-ontology benchmark covering three supervision regimes (atomic, relational, and role-chain), together with a fourth experiment on the Pizzaïolo synthetic-image dataset [10] that transfers the method to a real expert-authored OWL EL ontology. 2 Background and related work 2.1 Preliminaries: OWL EL, knowledge compilation, partial-supervision NeSy The OWL 2 EL profile. ℰℒ++EL^++ [5] is the description logic basis of OWL 2 EL (syntax and semantics in Table 4). Concepts are built from atomic names, ⊤ , ⊥ , conjunction C⊓DC D, and existential restriction ∃R.C∃ R.C; an ontology O contains GCIs C⊑DC D, role inclusions R⊑SR S, and role chains R1∘R2⊑SR_1 R_2 S, with subsumption, instance checking, and consistency decidable in time polynomial in |||O|. ELK [26] realizes this bound through a consequence-based saturation closure under ten completion rules [48]. ℰℒ++EL^++ is moreover Datalog-rewritable: consequence-based reasoning can be recast as the evaluation of a Datalog program [33, 11], and Stage 2 of our pipeline (§3.2) uses precisely this view, treating the ELK saturation as a monotone Datalog program. Such a rewriting yields a reasoning procedure, not a differentiable one. Probabilistic ℰℒ++EL^++ [12, 13, 24] attaches weights via Bayesian-network encodings; fuzzy ℰℒ++EL^++ [53, 8] replaces model-theoretic semantics with a t-norm-based approximation. Knowledge compilation, WMC, and SDDs. For a propositional formula φ and literal weights w(ℓ)≥0w( )≥ 0, the weighted model count is (φ,w)=∑M⊧φ∏ℓ∈Mw(ℓ) WMC( ;w)= _M _ ∈ Mw( ) [14]. With arbitrary non-negative weights WMC is a generic algebraic quantity; it acquires a probabilistic reading precisely when the weights are per-variable normalized, i.e. w(X)+w(¬X)=1w(X)+w( X)=1 for every variable X. Under that condition the weights specify a product distribution over truth assignments, and (φ,w) WMC( ;w) is exactly the probability that a sample from this distribution satisfies φ : it lies in [0,1][0,1] and (φ,w)+(¬φ,w)=1 WMC( ;w)+ WMC( ;w)=1 [14]. Moose enforces this normalization by construction (§3.1, Table 1), and Theorem 4.2 establishes the resulting WMC/distribution-semantics identity for the compiled circuit. When the per-variable weights are produced by a neural network, WMC is differentiable in the network’s outputs. Knowledge compilation translates φ to a circuit whose structural properties (smoothness, decomposability, determinism) make WMC linear in circuit size and reduce probabilistic queries to circuit traversals [21]. A Sentential Decision Diagram (SDD) [20, 17] is one such circuit and supports polynomial-time conjunction, disjunction, conditioning, and weighted model counting; exact definitions are in Appendix 0.D, and Section 0.C.3 shows a small example. Knowledge-compilation NeSy and partial supervision. A predictor composes a neural concept extractor pθ(∣)p_θ(c ) with a symbolic constraint φ and trains by maximizing the marginal pθ(∣)=∑pθ(∣) 1[φ()=],p_θ(y )= _cp_θ(c )\,1[ (c)=y], (1) the standard objective across this family [39, 51, 1, 43, 30]. DeepProbLog [39] grounds φ as probabilistic Datalog with neural-network annotated facts; Semantic Loss [51] adds −log(φ)- WMC( ) on propositional constraints; Semantic Probabilistic Layers [1] combine exact probabilistic inference with logical constraints in a single tractable circuit; Scallop [38] compiles differentiable Datalog with provenance semirings; NeurASP [52] embeds neural perception inside answer-set programs; and A-NeSI [32] amortizes the intractable WMC marginal with a neural surrogate. A partial-supervision instance reveals labels for a subset of y-atoms only; the latent concept vector c is recovered through the WMC gradient (Definition 1). None of the existing frameworks accepts an OWL ontology directly: the user must hand-translate existentials, role hierarchies, and role chains, losing the soundness, completeness, and polynomial-time saturation guarantees of consequence-based EL reasoning [26] in the process. 2.2 The independence assumption and reasoning shortcuts Knowledge-compilation NeSy predictors almost universally factorize pθ(∣)=∏ipθ(ci∣)p_θ(c )= _ip_θ(c_i ). Marconato et al. [41] show that this can attain optimal log-likelihood while learning unintended concept semantics, i.e., a reasoning shortcut (RS), and identify four root causes (knowledge structure, ground-truth concept distribution, objective, extractor architecture); RSBench [9] quantifies RS rates across NeSy architectures. [29, 31] prove that the independence factorization is incompatible with RS-awareness: placing non-trivial probability mass on every constraint-consistent latent assignment. Two mitigations are available: BEARS [40] keeps the independent extractor and trains a K-encoder ensemble whose members commit to distinct shortcut explanations; NeSyDM [30] replaces independence with a masked discrete-diffusion concept distribution. Every published RS result is propositional, Datalog, or finite-domain relational; no OWL fragment has been studied through this lens. Related work on description logic compilation [37, 53], refinement [19, 4], and ontology embeddings [36, 15, 16] is reviewed in Appendix 0.G. 3 Methods Figure 1: End-to-end Moose workflow on MNISTO_ MNIST at Δ=a,b =\a,b\. The TBox is compiled once via ELK saturation → shape-aware extractors →ΓEL→ _EL (+Φclos+ _clos when supplied) → SDD α. The differentiable WMC layer evaluates (α,pθ(),) WMC(α;p_θ(x),e) for the training loss, the conditional posterior, and the entailment query. 3.1 Task and ground vocabulary Given an ℰℒ++EL^++ ontology O and a finite ABox domain Δ=a1,…,am =\a_1,…,a_m\, the ground vocabulary is Δ:=C(a):C∈C,a∈Δ∪R(a,b):R∈R,a,b∈ΔV_O :=\C(a):C∈ Sig_C,a∈ \∪\R(a,b):R∈ Sig_R,a,b∈ \. The modeller partitions each signature into observable and latent names, C=Co⊎Cℓ Sig_C= Sig^o_C Sig _C and R=Ro⊎Rℓ Sig_R= Sig^o_R Sig _R. A training instance (Δ,,)( ,x,e) comprises a per-individual input tuple =(xa)a∈Δx=(x_a)_a∈ with each xa∈x_a and a partial set of ABox literals e over the observable ground vocabulary (Definition 1, Appendix 0.B). We learn a weight-shared per-individual classifier fθ:→[0,1]|Cℓ|f_θ:X→[0,1]^| Sig _C| that approximates the marginal of each latent atom under ∪O . The differentiable WMC layer evaluates (α,w,) WMC(α;w,e) under the literal-weight map w that assigns fθ(xa)f_θ(x_a) to each latent concept atom C(a)C(a), its observed truth value to each observed atom, 12 12 to each unobserved observable and to each latent role atom, and 1−w(X)1-w(X) to each negative literal ¬X X, where X ranges over the ground atoms of ΔV_O (Table 1). Because w(X)+w(¬X)=1w(X)+w( X)=1 for every X by construction, the map is per-variable normalized: it defines a product distribution over the ground atoms whose per-atom marginal is w, and (α,w,) WMC(α;w,e) is the probability under this distribution that a sample satisfies α and the evidence e (§2.1; Theorem 4.2). This product form encodes the per-atom independence factorization pθ(∣)=∏ipθ(ci∣)p_θ(c )= _ip_θ(c_i ) shared by knowledge-compilation NeSy predictors (§2.2). We make the assumption explicit here because it is the object of study rather than an incidental choice: it is exactly the factorization that induces reasoning shortcuts, which contribution 3 quantifies via RSconsRS_cons and which the BEARS and NeSyDM variants (§3.4) are designed to mitigate. Table 1: Literal-weight map w; the two weights of each variable sum to 11. Literal Weight Literal Weight C(a)C(a), C∈CℓC∈ Sig _C fθ(xa)[C]f_θ(x_a)[C] C(a)C(a), C∈CoC∈ Sig^o_C unobs. 12 12 C(a)∈C(a) 11 R(a,b)R(a,b), R∈RoR∈ Sig^o_R obs. 11 or 00 from e ¬C(a)∈ C(a) 00 R(a,b)R(a,b) latent or unobs. 12 12 ¬X X for any atom X: 1−1-weight of X 3.2 Compilation algorithm The algorithm (full pseudocode in Algorithm 1, Appendix 0.C) compiles an ℰℒ++EL^++ ontology and a finite ABox domain to an SDD over ΔV_O in seven stages; the SDD is built once at startup and reused across every training step. Stage 1 runs the ELK saturation, which derives all entailed subsumptions and role links and records the grounded rule instances that justify each derivation. Stages 2–5 build a propositional encoding of the full saturation closure, including deeply nested existential derivations and cyclic dependency chains, via Clark completion, strongly-connected-component (SCC) detection, time-stamped unrolling, and conjunctive normal form (CNF) conversion. Stages 6–7 ground the saturation onto the finite ABox domain and compile the resulting clauses into the SDD that the differentiable WMC layer evaluates. The two groups of stages operate at different abstraction levels and serve complementary purposes. Stages 2–5 produce a TBox-level propositional theory whose variables are concept-level atoms such as xC⊑Dx_C D and xE→Cx_E RC, including derived complex concepts (e.g. C⊑∃R.∃S.DC ∃ R.∃ S.D); the input axiom variables αi _i in this theory are free, so the theory supports probabilistic ontology reasoning: assigning a weight pip_i to each αi _i and computing the WMC gives P(query entailed)P(query entailed). Stages 6–7 operate on the ground vocabulary ΔV_O whose variables are ABox atoms C(a)C(a) and R(a,b)R(a,b); for NeSy learning all ontology axioms are certain and the WMC literal weights come from a neural network’s per-atom outputs (Table 1), so the input-axiom tracking of Stages 2–5 is not consumed. In the NeSy learning use case, Stages 6–7 return to the Stage 1 saturation output and extract the subset relevant for ABox grounding: subsumptions, disjointness, and role links between named concepts. Deeply nested existential derivations that Stages 2–5 process, including those that create cyclic SCCs requiring time-stamped unrolling, have no ABox-level counterpart: the complex concepts produced during saturation (e.g. ∃R.C∃ R.C or ∃R.∃S.D∃ R.∃ S.D) do not lie in the named signature C() Sig_C(O), and the shape-aware extractors of Stage 6 correctly filter them out. Stages 2–5 still serve a diagnostic and validation role: the Clark completion, SCC structure, and CNF size characterize the TBox complexity and verify that the Stage 6 filter captures every ABox-relevant consequence. We summarize each stage below. Stage 1: ELK saturation. Saturate(,E)(O,E) runs the ten ELK completion rules [26] and returns the saturation pair (Σ,Λ)( , ), where Σ is the set of derived subsumptions C⊑DC D and Λ the set of derived role links E→CE RC, sound and complete with respect to O [26]. We write Sat():=Σ∪Λ Sat(O):= ∪ for the saturation closure. For each derived atom the saturation records all grounded rule instances that can derive it (there may be multiple justifications), and these form the input to Stage 2. When the ontology contains existential restrictions or role chains, the saturation may derive non-atomic concepts (e.g. ∃R.C∃ R.C, ∃R.∃S.D∃ R.∃ S.D); these are internal to the completion and are consumed by Stages 2–5 but filtered out by the shape-aware extractors of Stage 6. Algorithmic details are in Appendix 0.C, and Section 0.C.3 works one axiom end-to-end through the algorithm. Stages 2–5: TBox-level encoding. The saturation of Stage 1 can be viewed as a monotone Datalog program [18]. Stages 2–5 turn it into a propositional TBox theory: Clark completion [18] replaces each derived atom’s justifications with a biconditional, Tarjan’s algorithm [47] isolates cyclic strongly-connected components, these are broken by SCC-local time-stamped unrolling, and the Tseitin transformation [50] yields an equisatisfiable CNF. With all input-axiom variables true this theory has Sat() Sat(O) as its unique model; when the axioms carry weights it supports probabilistic ontology reasoning. For NeSy learning these stages are diagnostic: the deeply nested and cyclic derivations they handle lie outside the named signature and are filtered by the Stage 6 extractors, so the ABox grounding of Stages 6–7 consumes only the Stage-1 saturation. The construction and its equations are given in Appendix 0.C. Stage 6: shape-aware extractors and ABox grounding. Stage 6 extractors return to the Stage 1 saturation output (Σ,Λ)( , ) and select the subset that maps to ground ABox atoms over ΔV_O . AtomSub emits ¬A(a)∨B(a) A(a) B(a) for every subsumption A⊑BA B in Σ where both A and B are named concepts in C() Sig_C(O); Disj emits ⋁i¬Ai(a) _i A_i(a) for n-ary atomic disjointness A1⊓⋯⊓An⊑⊥A_1 … A_n (flattened from any parenthesization); Unsat emits ¬A(a) A(a) for atomic A⊑⊥A ; Links emits the NF3-forward clause ¬E(a)∨¬R(a,b)∨C(b) E(a) R(a,b) C(b) per saturation-derived atomic link (E,R,C)∈Λ(E,R,C)∈ (i.e. E⊑∃R.CE ∃ R.C with E,C∈C()E,C∈ Sig_C(O)), plus an NF4-reverse clause ¬R(a,b)∨¬C(b)∨E(a) R(a,b) C(b) E(a) when L(E,R):=C:(E,R,C)∈ΛL(E,R):=\C:(E,R,C)∈ \ is a singleton (so the NF4 direction is deterministic). The union of the clauses produced by these extractors is the propositional Horn program Γ over ΔV_O ; the saturation closure is polynomial by Theorem 0.D.2 and grounding multiplies it by at most |Δ|2| |^2 (Section 0.D.4). Stage 7: SDD compilation. Γ is compiled bottom-up into an SDD α that is smooth, decomposable, and deterministic [17, 21]. The role-pinning caveat applies to the Links clause: ELK derives E⊑∃R.CE ∃ R.C (existential, “some witness”); Moose encodes the propositional clause E(a)∧R(a,b)→C(b)E(a) R(a,b)→ C(b), which is universal on the named pair. Soundness depends on Δ being closed and on role atoms over Ro Sig^o_R being pinned by evidence (a Moose-specific encoding choice for the finite-named-domain regime, not an ELK theorem). The differentiable WMC layer traverses α and evaluates (α,w) WMC(α;w) by the standard smooth/decomposable/deterministic recursion (Equation 8 in Appendix 0.C), with literal weights w read from Table 1. Decomposability factors the product at each decision node; determinism makes the prime/sub pairs mutually exclusive, so the sum is plain rather than an inclusion–exclusion. Conditioning on e clamps the literal weight of every observed atom to 00 or 11. 3.3 Closure axioms outside the EL profile OWL EL is open-world and lacks both right-hand-side disjunction and cardinality constructors [5], so the covering axiom ⊤⊑D0⊔⋯⊔DK−1 D_0 … D_K-1 on an exhaustive family is unstatable in EL. Under partial supervision the WMC gradient on unobserved members of such a family vanishes at every all-False extension (e.g. on MNIST, observing Even(a) Even(a) without closure leaves the digit posterior uninformative). We therefore optionally append a finite set of closure axioms Φclos _ clos to ΓEL _ EL on each modeller-declared exhaustive family ℱF: pairwise disjointness, the covering clause ⋁iDi(a) _iD_i(a), and (when each DiD_i carries a distinguishing property profile πi _i) profile-keyed reverse implications. We write these three jointly manipulated components as Φclos=Φmutex∪Φcover∪Φprofile _ clos= _ mutex∪ _ cover∪ _ profile. Two of the three are outside the EL profile but are standard OWL-DL machinery; Moose’s contribution is the ELK-via-SDD infrastructure that absorbs Φclos _ clos at the propositional level, so the same compilation yields αEL _ EL or αclos _ clos with no method change. This absorption is free at the CNF level (Φclos _ clos adds at most (K2)m+(K+1)m K2m+(K+1)m clauses per declared family: (K2)m K2m mutex, m covering, and up to KmKm profile-keyed reverse implications), but the polynomial saturation-closure bound of Theorem 0.D.2 applies to the EL Horn fragment only and does not transfer to ΓEL∪Φclos _ EL∪ _ clos: covering disjunctions can raise the primal-graph treewidth, and SDD compilation is worst-case exponential in |Γ|| | with a O(|Γ|⋅2w)O(| |· 2^w) bound under treewidth w (Section 0.D.5); inference remains O(|α|)O(|α|) in the SDD node count regardless (Theorem 0.D.4). Whether closure is needed is ontology- and regime-dependent: a forward-only EL hierarchy under factorized perception leaves the all-false latent assignment consistent with any property evidence, so the WMC gradient is uninformative and closure restores a non-trivial gradient (an architectural softmax head encoding mutex+covering, as DeepProbLog uses via n(⋅) n(·), achieves the same effect by other means); when forward subsumption alone pins the latent vector, no closure is added. The choice is orthogonal to RS-awareness, which targets the cross-atom factorization at the perception output [41, 29] and is implemented by the BEARS / NeSyDM wrappers of §3.4. Section 0.B.1 summarizes the assumptions introduced by each pipeline component and what each concedes against open-world semantics. 3.4 Inference and RS-aware variants The differentiable WMC layer supports three inference operations on the same SDD (training loss, conditional posterior, and entailment query), varying only literal weights and evidence. The training loss is L(θ,,)=−log(α,pθ(),)L(θ;x,e)=- WMC(α;p_θ(x),e) [51], which coincides with the DeepProbLog marginal loss on this Horn theory by Proposition 1. The conditional posterior Pθ(C(a)∣,)P_θ(C(a) ,e) is the ratio of two WMCs with C(a)C(a) clamped vs. left free; the perception-free entailment query ∪⊧C(a)O C(a) holds iff (α;w1/2,∪C(a):=)=0 WMC(α;w_1/2,e∪\C(a):= false\)=0 (the 12 12-weighted SDD acts as a satisfiability oracle). All three run in O(|α|)O(|α|) (Theorem 0.D.4, Equations 11, 12 and 13 in Section 0.E.1). The compilation algorithm is independent of the perception’s output distribution, so RS-aware methods (§2.2) plug in by replacing pθ()p_θ(x) in w without modifying α. Moose+BEARS [40] trains a K-encoder ensemble diversified by Kullback–Leibler (KL) divergence against the running ensemble average; Moose+NeSyDM [30] replaces ∏ipθ(ci∣) _ip_θ(c_i ) with a masked discrete-diffusion qθq_θ, evaluated with both the REINFORCE leave-one-out (RLOO) estimator [28] and an exact-WMC gradient estimator. Wrapper losses with hyperparameters are in Section 0.E.3. 4 Correctness and complexity This section states the four theorems that constitute the formal contribution of Moose: a verified SDD encoding of the ELK-derived saturation, the unconditional rational DISPONTE correspondence, and the SCC-compositional factorizations at the Sat and WMC levels. Each theorem is mechanized in Lean 4; the infrastructure on which they rest (ELK soundness/completeness on ℰℒ++EL^++ and polynomial-time Sat decidability [26]) is reused unchanged from the ELK literature and re-mechanized in our Lean library (Section 0.D.1). Proofs, Lean theorem names, and audit-surface details are deferred to Appendices 0.D and 0.D.10. Notation. O ranges over ℰℒ++EL^++ ontologies (OWL 2 EL minus datatype properties and concrete domains). (,C,D) Sat(O,C,D) holds iff ELK derives C⊑DC D from O [26]. A world M:→0,1M:O→\0,1\ selects the sub-ontology (,M):=α∈:M(α)=1 sel(O,M):=\α :M(α)=1\ (sel short for selectedAxioms in the Lean library). For a weight w:×0,1→ℚw:O×\0,1\ , the rational DISPONTE marginal [44] is ℚ(,C,D,w):=∑M:→0,1[((,M),C,D)]⋅∏α∈w(α,M(α)); P^Q(O,C,D,w)\;:=\; _M:O→\0,1\1[\, Sat( sel(O,M),C,D)\,]· _α w(α,M(α)); (,C,D,w) P(O,C,D,w) denotes the natural-valued analogue when w takes values in ℕN. (,C,D) cmp(O,C,D) (cmp short for compileSat) is the verified Shannon-tree SDD produced by the algorithm of §3.2, and ℚ(t,w) WMC^Q(t,w) is its rational weighted model count. Theorem 4.1 (Verified SDD encoding) For every ℰℒ++EL^++ ontology O and concepts C,DC,D, there exists an SDD tree t such that 1. model(t,M)⇔((,M),C,D)model(t,M) Sat( sel(O,M),C,D) for every world M:→0,1M:O→\0,1\; 2. for every weight w, (t,w)=(,C,D,w) WMC(t,w)= P(O,C,D,w); 3. |t|= 2||+1−1|t|\,=\,2^|O|+1-1. Theorem 4.1 is the formal contract of Moose’s compilation step: the SDD’s models are exactly the worlds whose selected sub-ontology ELK-entails C⊑DC D, the SDD’s WMC is the DISPONTE marginal under arbitrary weights, and the worst-case size is the explicit 2||+1−12^|O|+1-1 bound of the Shannon expansion (Section 0.D.5). Lean proof: see Appendix 0.D. Theorem 4.2 (Rational DISPONTE correspondence) For every ℰℒ++EL^++ ontology O, every concepts C,DC,D, and every rational weight w, ℚ((,C,D),w)=ℚ(,C,D,w). WMC^Q\! ( cmp(O,C,D),\,w )\;=\; P^Q(O,C,D,w). (2) The identity holds unconditionally on rational weights: no distributional assumption is required. It is the formal warrant of the standard entailment-as-WMC-zero phrasing of probabilistic DLs [44] (at the uniform prior w≡12w≡ 12, ℚ=0 WMC^Q=0 iff no world’s sub-ontology entails C⊑DC D), and lifts that phrasing from the propositional encoding to the verified compiled circuit. Lean proof: see Appendix 0.D. Theorem 4.3 (SCC compositional theorem, Sat level) Let =1⊎2O=O_1 _2 with disjoint signatures, both components nominal-free and range-chain-safe, 2O_2 consistent (¬(2,⊤,⊥) \, Sat(O_2, , )), and C,DC,D nominal-free with C,DC,D in the signature of 1O_1. Then (1⊎2,C,D)⇔(1,C,D). Sat(O_1 _2,C,D)\; \; Sat(O_1,C,D). The result formalizes the intuition that an inferentially irrelevant SCC cannot affect Sat-derivability inside the relevant component, provided the irrelevant component is itself consistent. SCC-wise compilation follows: each SCC can be saturated and compiled in isolation, and the joint posterior recovered by combination. Range-chain safety rules out interactions between role chains and range axioms that would block the SCC factorization. It holds vacuously when neither component has range axioms (the case for both experimental ontologies); for chain-and-range ontologies, mechanized syntactic range-elimination [6] reduces to this case under a side condition that is automatically satisfied by reflexive role-inclusion propagation. Lean proofs, theorem names, and side-condition details: Appendices 0.D and 0.D.10. Theorem 4.4 (Per-SCC posterior equivalence) Under the hypotheses of Theorem 4.3, for any uniform per-axiom prior w≡cw≡ c with c>0c>0, the per-SCC and joint DISPONTE posteriors coincide. In the unnormalized counting case w≡1w≡ 1, ℚ(1⊎2,C,D,w)=ℚ(1,C,D,w)⋅2|2|. P^Q(O_1 _2,C,D,w)\;=\; P^Q(O_1,C,D,w)· 2^|O_2|. (3) The multiplicative 2|2|2^|O_2| from the irrelevant SCC cancels under posterior normalization, and the same cancellation extends the identity to any c>0c>0 after factoring out c|1|+|2|c^|O_1|+|O_2|. This is the WMC-level analogue of Theorem 4.3: per-SCC compilation is posterior-faithful. Lean proof: Appendices 0.D and 0.D.10. The closure-augmented variant of the SDD (which materializes the per-individual partition constraints on declared exhaustive families) satisfies an analogous correctness theorem (Theorem 0.D.3, appendix). Inference is linear in |(,C,D)|| cmp(O,C,D)| [17, 21] (Theorem 0.D.4, appendix). All proofs and the DeepProbLog equivalence Proposition 1 are in Appendix 0.D; the implementation index in Section 0.D.10 cross-references every paper claim with its formalized counterpart. 5 Research questions and experiments We evaluate Moose on two benchmarks: the MNIST-with-ontology benchmark we developed for this work (Example 1), instantiated under three supervision regimes (atomic property literals, relational ∃R.C∃ R.C evidence, and role-chain evidence); and the Pizzaïolo dataset [10] of 4,8004,800 synthetic pizza images generated to conform to the published OWL pizza ontology [46], which lets us test transfer to a third-party ontology and a different image distribution. Within each benchmark, the experiments share the ontology and differ only in the observable signature, the domain size |Δ|| |, and the supplied evidence. We address five research questions. RQ1–RQ3 test latent digit recovery on MNISTO_ MNIST as the supervision signal grows from a single individual with unary property literals (RQ1), to a pair of individuals connected by an observed r(a,b)r(a,b) role literal under an ∃R.C∃ R.C axiom (RQ2), to a pair connected by observed role literals only through an ELK-derived role-chain consequence (RQ3). RQ4 tests transfer to the pre-existing third-party OWL pizza ontology, restricted to its EL fragment (Pizzaïolo, §5.2). RQ5 asks which RS-mitigation regime works under which conditions: with encoder, ontology, and compiled SDDs fixed, we vary only the output-distribution treatment: an independent per-atom baseline (no logical structure), Moose on the EL theory alone (the DPL surface, Proposition 1), Moose with closure Φclos _ clos, and the BEARS / NeSyDM wrappers, across factorized relational, tied symmetric, and high-arity disjunctive ambiguity. The independent baseline (binary cross-entropy, BCE, on observed atoms) is a lower-bound reference that cannot propagate evidence through subsumption, disjointness, or role axioms and so cannot beat chance on latent atoms [41, 29]. 5.1 The MNIST ontology and supervision regimes A single OWL EL ontology MNISTO_ MNIST (1414 concepts, 22 roles, 7676 axioms; full listing in Section 0.F.2) is used in all three MNIST experiments; the experiments differ only in |Δ|| | and the evidence regime, never in the TBox. ELK saturation derives the chain consequence Di⊑∃plus_two.D(i+2)mod10D_i ∃ plus\_two.\,D_(i+2) 10 from the axiom succ∘succ⊑plus_two succ succ plus\_two at compile time. The compiled SDD has 14m+2m214m+2m^2 ground atoms. A small convolutional neural network (CNN) fθf_θ (22 conv blocks + 22 fully-connected layers, weight-shared across individuals; Section 0.F.3) maps each image to per-atom probabilities; training minimizes ℒ(θ)=−log(αclos,pθ(),)L(θ)=- WMC( _clos;p_θ(x),e) with Adam, batch 3232, 55 seeds; per-regime learning rates and epoch counts are in Section 0.F.4. EL-only ablations omit Φclos _ clos and train against αEL _EL, recovering the DPL loss (Proposition 1). Exp. 1 (atomic, RQ1) uses Δ=a =\a\ with nobs∈1,2,3n_obs∈\1,2,3\ unary literals over Co=Even,Odd,Prime,Composite Sig^o_C=\ Even, Odd, Prime, Composite\. Exp. 2 (relational, RQ2) uses Δ=a,b =\a,b\ with the role atom succ(a,b) succ(a,b) asserted (digits satisfy digit(b)=(digit(a)+1)mod10 digit(b)=( digit(a)+1) 10) plus nobs∈1,2,3n_obs∈\1,2,3\ primality literals. Exp. 3 (role chain, RQ3) flips the asserted role to plus_two(a,c) plus\_two(a,c) and widens the unary pool to parity and primality; the only chain from a to c is the NF7-derived consequence above. The digit family is declared exhaustive at every individual; Φclos _ clos supplies pairwise disjointness, covering, and reverse-implication clauses. Some property profiles uniquely identify the latent digit (e.g. Even(a)∧Prime(a) Even(a) Prime(a) pins D2D_2), while others leave it ambiguous (e.g. Even(a) Even(a) alone admits D0,D2,D4,D6,D8\D_0,D_2,D_4,D_6,D_8\); RScons_cons on the ambiguous cases measures confident commitment to a wrong digit. 5.2 Experiment 4: Pizzaïolo (RQ4) Pizzaïolo [10] provides 4,8004,800 synthetic pizza images. The canonical pizza ontology contains non-EL constructs (universal restrictions on hasTopping, complement-based definitions such as VegetarianPizza≡Pizza⊓¬∃hasTopping.MeatTopping⊓¬∃hasTopping.FishTopping VegetarianPizza≡ Pizza ∃ hasTopping. MeatTopping ∃ hasTopping. FishTopping, and cardinality on NumberedPizza); we use only its EL-expressible fragment, restating the four-pizza recipes and property classes as conjunctive subsumption and disjointness axioms, and treating classes whose canonical definitions fall outside EL (e.g. VegetarianPizza) as atomic concepts whose truth values come from the dataset labels rather than from non-EL closure. The method targets the four-pizza subset Mushroom,Cajun,Capricciosa,FourSeasons\ Mushroom, Cajun, Capricciosa, FourSeasons\ over 1616 topping concepts, with conjunctive per-pizza axioms (e.g. Capricciosa⊑Ham⊓Anchovy⊓Olive⊓Peperonata Capricciosa Ham Anchovy Olive Peperonata), pairwise pizza disjointness, and disjointness axioms P⊓T⊑⊥P T for every topping T outside P’s recipe. EL forward subsumption plus these disjointness axioms pin the topping vector once pizza identity is observed; no out-of-profile closure is added. Track A reveals pizza identity; toppings are latent. We test distribution shift via an OOD split: the four training pizzas all carry Anchovy and Olive together, so a network can score well on the in-distribution split by coupling the two atoms; we hold out five tie-breaker pizzas (Fiorentina, Giardiniera, LaReine, Soho, Veneziana) whose recipes break this co-occurrence. Track B reveals one of four property-class atoms (NonVegetarianPizza, SpicyPizza, RealFrenchPizza, VegetarianPizza); revealing NonVegetarianPizza leaves Cajun,Capricciosa,FourSeasons\ Cajun, Capricciosa, FourSeasons\ indistinguishable (a 3-way RS over pizza identity). Track C (the is_spicy task in the codebase) adds four axioms Ti⊑SpicyToppingT_i SpicyTopping for Ti∈Jalapeno,Peperonata,PeperoniSausage,PrawnT_i∈\ Jalapeno, Peperonata, PeperoniSausage, Prawn\ together with SpicyTopping≡SpicyPizza SpicyTopping≡ SpicyPizza (two GCIs; here SpicyTopping acts as a label-class denoting “pizza with a spicy topping”). Symbolic supervision SpicyPizza(a) SpicyPizza(a) forces SpicyTopping(a) SpicyTopping(a) but the EL theory leaves the witness ambiguous over 24=162^4=16 topping subsets (the multi-witness regime BEARS/NeSyDM target). We train the perception CNN from scratch with batch size 3232, 55 seeds, and 6060 epochs on Tracks A and B (Track C uses 1515 epochs); per-method hyperparameters and the NeSyDM (γc,γh)( _c, _h) sweep results are in Section 0.F.4. 5.3 Baselines, metrics, and results We compare Moose against seven baselines. Independent (BCE on observed atoms) is the NeSy-free lower bound. Semantic Loss [51] shares the −log- WMC objective but compiles only the directly-stated NF1/NF2 atomic axioms, dropping NF3/NF4/NF7 and ELK saturation, isolating the EL-aware method of §3.2. DeepProbLog [39] hand-codes each MNIST regime as a ProbLog program with one n(⋅) n(·) digit directive; by Proposition 1 DPL and Moose compute the same loss on the same Horn theory, though that directive is an annotated disjunction, so DPL is not closure-free. Moose+BEARS [40] keeps the factorized perception and αclos _clos but replaces the single encoder with K=5K=5 diversified encoders. Moose+NeSyDM [30] replaces the factorized extractor with a masked-diffusion concept distribution; we evaluate both RLOO and exact-WMC gradient estimators. LTN [7] substitutes a fuzzy product T-norm; ELEmbeddings [36, 54] embeds the EL ontology into ball geometries with a classifier head; both are detailed in Section 0.E.4. Metrics. The headline tables Tables 2 and 3 report the regime’s principal accuracy and ECE, the expected calibration error binned by predicted confidence [23]. The two ontologies do not admit the same accuracy metric. On MNIST the digit family is declared exhaustive and we report AccFAcc_F, family-argmax accuracy: per individual, the argmax of the WMC posterior over that family. On Pizzaïolo we report AccCAcc_C, per-atom accuracy on the latent slice, since Track C declares no exhaustive family and the decode degenerates on the other two (Section 0.F.7). The full per-regime breakdown (Table 9, Section 0.F.6) additionally reports the negative log-likelihood (NLL), the mean per-atom Bernoulli loss on the latent signature; the RS-consistency rate RS=consConf⋅(1−AccF)_cons=Conf·(1-Acc_F) on the latent family-argmax (higher = more confident commitment to a wrong shortcut; on Pizzaïolo the complement uses AccCAcc_C, and on Track C it is not applicable); per-atom accuracy AccatomAcc_atom on the latent signature; and the macro-averaged per-concept F1, F1macroF1_macro. A paired significance analysis of the headline comparisons over 2020 seeds is given in Section 0.F.8, and a learning-rate sensitivity analysis in Section 0.F.5. Table 2: Principal accuracy (%, mean ± s.d. over 55 seeds. MNIST Experiments 1–3 (Section 5.1), Pizzaïolo Tracks A–C (Section 5.2); Track A is the out-of-distribution split. Metric: AccFAcc_F (family-argmax) on MNIST, AccCAcc_C (per-atom, latent slice) on Pizzaïolo; compare only within a column (Section 0.F.7). Operative theory: ΓEL+Φclos _ EL+ _ clos for the Moose rows on MNIST, ΓEL _ EL elsewhere, none for Independent (§3.3). Bold = column-best; † = highest but not significant (Section 0.F.8); DeepProbLog on Pizzaïolo is not a separate run (Section 0.F.6). Full AccatomAcc_atom, NLL, RScons_cons, and F1macroF1_macro in Table 9. MNIST Pizzaïolo Method Exp 1 Exp 2 Exp 3 Pz A Pz B Pz C Independent 13.2 ± 7.9 08.8 ± 4.5 12.2 ± 7.3 21.7 ± 9.7 25.0 ± 0.0 48.9 ± 5.6 DeepProbLog 42.1 ± 1.3 38.9 ± 3.2 59.6 ± 13.6 68.1 ± 0.3 84.5 ± 2.1 81.0 ± 3.0 LTN 25.9 ± 6.5 14.5 ± 4.9 11.0 ± 7.9 22.1 ± 5.2 32.5 ± 20.9 84.8 ± 0.4† ELEm/mOWL 34.9 ± 4.2 34.8 ± 3.6 27.4 ± 7.1 25.7 ± 7.3 25.0 ± 0.0 75.4 ± 6.6 Moose 48.1 ± 10.1 74.6 ± 0.3 96.1 ± 7.2 68.1 ± 0.3 84.5 ± 2.1 81.0 ± 3.0 +BEARS 50.1 ± 5.2† 76.5 ± 5.9† 89.2 ± 7.2 68.6 ± 0.3 87.9 ± 0.9 84.2 ± 3.6 +NeSyDM (RLOO) 46.6 ± 2.1 58.2 ± 1.4 62.7 ± 2.9 72.2 ± 1.3 78.5 ± 0.8 63.9 ± 3.7 +NeSyDM (exact) 49.4 ± 9.7 62.6 ± 6.1 60.1 ± 5.7 67.4 ± 1.4 84.7 ± 2.2 80.1 ± 1.5 Table 3: Expected calibration error ECE (%, mean ± s.d.). Lower is better. Same baselines, seed counts, operative theories, and metric conventions as Table 2; bold = column-best per regime, not significance-tested. Per-regime AccatomAcc_atom, NLL, RScons_cons, and F1macroF1_macro alongside ECE are in Table 9 (Section 0.F.6). MNIST Pizzaïolo Method Exp 1 Exp 2 Exp 3 Pz A Pz B Pz C Independent 09.3 ± 4.5 13.4 ± 3.6 09.0 ± 8.2 58.3 ± 15.4 26.4 ± 17.1 22.1 ± 9.2 DeepProbLog 10.3 ± 0.9 12.3 ± 0.9 08.0 ± 2.9 30.8 ± 0.7 15.5 ± 2.1 15.3 ± 1.4 LTN 16.1 ± 6.7 10.0 ± 0.0 10.0 ± 0.0 52.7 ± 21.8 39.3 ± 17.4 14.1 ± 0.5 ELEm/mOWL 03.9 ± 0.4 07.2 ± 0.1 06.3 ± 0.1 49.7 ± 10.2 16.1 ± 0.2 11.8 ± 3.8 Moose 10.6 ± 1.8 04.9 ± 0.3 01.1 ± 1.5 30.8 ± 0.7 15.5 ± 2.1 15.3 ± 1.4 +BEARS 03.9 ± 1.0 04.0 ± 1.2 05.6 ± 1.1 28.2 ± 1.5 12.3 ± 1.0 11.3 ± 3.4 +NeSyDM (RLOO) 06.0 ± 0.6 07.3 ± 0.7 04.6 ± 0.8 07.5 ± 1.2 02.6 ± 0.9 08.9 ± 1.5 +NeSyDM (exact) 05.1 ± 1.5 07.4 ± 1.2 07.9 ± 1.1 30.8 ± 3.2 15.3 ± 2.2 06.9 ± 2.2 Findings on Experiments 1–3 (RQ1–3, RQ5). At |Δ|=1| |=1 (Exp. 1) Moose leads DeepProbLog on AccFAcc_F (48.148.1 vs. 42.142.1). Independent stays near random (AccF=13.2Acc_F=13.2). BEARS cuts ECE from 10.610.6 to 3.93.9 at no cost to accuracy; at |Δ|=1| |=1 there is little diversifiable structure left for the ensemble to exploit. NeSyDM matches Moose on AccFAcc_F (46.646.6 and 49.449.4 for the RLOO and exact estimators vs. 48.148.1). On the relational and role-chain regimes (Exps. 2–3) Moose dominates DeepProbLog by tens of points on AccFAcc_F (74.674.6 vs. 38.938.9 on Exp. 2; 96.196.1 vs. 59.659.6 on Exp. 3): the EL-aware Links extractor propagates evidence across the |Δ|=2| |=2 ground individuals, but the closure clauses Φclos _ clos are what make this signal learnable. The ablation in Section 0.F.10 shows the base WMC objective falling to 17.417.4 and 9.49.4 (near chance) once Φclos _ clos is removed, so the EL compilation supplies the structure and Φclos _ clos the identifying constraint, with reasoning-shortcut mitigations partially substituting for the latter (Table 13). BEARS reduces RScons_cons (Table 9, Section 0.F.6) but gives up a few points of accuracy on Exp. 3 (89.289.2 vs. 96.196.1); NeSyDM lags even at tuned (γc,γh)( _c, _h). LTN and ELEmbeddings under-perform on AccFAcc_F (14.514.5 and 34.834.8 on Exp. 2): LTN’s ECE saturates near the uniform prior (10.010.0, information-vacuous), while ELEmbeddings’ lower ECE on Exps. 2–3 (7.27.2, 6.36.3) does not translate into accuracy. An inductive held-out-edge split, in which query individuals appear only in relational configurations never supervised, leaves Moose’s accuracy essentially unchanged while NeSyDM collapses to near-chance (Section 0.F.9). Findings on Experiment 4 (RQ4–5). Track A is an OOD generalization test on five held-out tie-breaker pizzas whose recipes break the Anchovy,Olive\ Anchovy, Olive\ co-occurrence admissible on the four training pizzas; on the in-distribution split most methods reach near-perfect topping accuracy, but on the OOD split the Moose family clusters around 6767–7272% on AccCAcc_C (Table 2). Track B is the canonical RS test (3-way symbolic ambiguity: a property-class observation leaves three pizzas indistinguishable). Plain Moose-WMC commits to a single constraint-consistent latent (“Mechanism A” of [41]); BEARS lifts AccCAcc_C from 84.584.5 to 87.987.9 via ensemble diversification on RS-suspect pizzas, and NeSyDM (RLOO) trades a few points of accuracy (78.578.5) for the lowest ECE of any row (2.62.6). Track C (is_spicy disjunction) is the multi-witness regime NeSyDM was designed for: among the Moose variants BEARS leads on AccCAcc_C (84.284.2 vs. 81.081.0 for plain Moose-WMC) and NeSyDM (exact) leads on ECE (6.96.9, the column best); LTN matches BEARS on accuracy (84.884.8, the highest value in the column but not significantly so, Section 0.F.8) at higher ECE (14.114.1). On both Track B and Track C the Moose-family results separate along an argmax-vs-calibration axis (BEARS leads accuracy, NeSyDM leads ECE). These mitigation effects are sizeable rather than marginal: paired over 2020 seeds, BEARS significantly exceeds plain Moose-WMC on both Track B and Track C, and NeSyDM significantly exceeds it on the Track A OOD split (Section 0.F.8). In the symbolically ambiguous regimes it is therefore the RS-mitigation wrapper, not the exact base layer, that is the stronger configuration; the mitigation is doing substantive work, not fine-tuning. This reverses the relational regime (Exps. 2–3), where forward subsumption already pins the latent vector, no residual reasoning shortcut remains to remove, and plain Moose is best; mitigation helps precisely where symbolic ambiguity leaves an RS to exploit. Whether this generalizes beyond the regimes tested here is left to future work. 6 Conclusion and outlook Moose compiles OWL 2 EL into a Lean 4-verified weighted-model-counting layer with native role chains and role hierarchies, and supplies the first end-to-end formally verified circuit for an OWL profile together with the first reasoning-shortcut analysis in OWL EL. Empirically, the closure-augmented variant dominates propositional NeSy baselines by tens of points on relational and role-chain regimes, where the EL-aware grounding propagates evidence that propositional encodings cannot and the closure clauses render the resulting signal learnable (Section 0.F.10); under symbolic ambiguity BEARS and NeSyDM separate along an argmax-vs-calibration axis. Limitations. Three assumptions bound the present results. (i) Scale. Our experiments use |Δ|=2| |=2; the compiled SDD grows empirically as ≈|Δ|2.9≈| |^2.9 with a 40×40× compile-time jump at |Δ|=4| |=4 (Section 0.D.5). Saturation and grounding are polynomial and the compilation is exact, but we do not demonstrate ontology-scale ABoxes such as SNOMED CT or the Gene Ontology; that regime requires lifted WMC and is the principal open problem. (i) Finite named domain. Moose learns over a given finite ABox of named individuals (Definition 1); this defines the ABox-supervised task rather than weakening it, but it does not by itself perform open-domain inference over unnamed individuals. (i) Role-pinning. Soundness of the Links encoding treats an existential as universal on the named pair, assuming role atoms over Ro Sig^o_R are pinned by evidence (§3.2, Stage 7), a Moose-specific choice for the finite-named-domain regime, not an ELK theorem. The theoretical contribution, a Lean-verified exact compilation and the RS analysis, stands independently of the scaling outcome: it is the learned-perception pipeline at ontology scale, not the correctness result, that the scalability question concerns. Open directions include lifted WMC [37] for larger ABox domains, ℒALC rewriting that would extend the same encoding to existential-on-the-left axioms, and evaluation on biomedical ontologies such as SNOMED CT and the Gene Ontology, and link prediction over latent role assertions: the role atoms R(a,b)R(a,b) that the weight map (Table 1) currently fixes at 12 12 when unobserved would instead be predicted from perception, extending the same WMC layer from latent-concept learning to latent-role learning. Acknowledgements This work was supported by funding from King Abdullah University of Science and Technology (KAUST), through the KAUST Center of Excellence for Smart Health (KCSH), under award number 5932, and the KAUST Center of Excellence for Generative AI, under award number 5940. Supplemental Material Statement: Source code, MNISTO_ MNIST, the Pizzaïolo subset, seeds, per-seed JSON, the Lean 4 proof library, and pseudocode are at https://github.com/bio-ontology-research-group/moose-iswc/; full proofs are given in Appendix 0.D. Declaration of use of Generative AI. A large language model assisted with copy-editing and with Lean 4 transcription of the proofs in Appendix 0.D. All technical content (definitions, theorem statements, proof structure, algorithms, experimental design and results) was authored, verified, and approved by the authors, and every mechanized statement was checked by the Lean type checker. References [1] Ahmed, K., Teso, S., Chang, K.W., Van den Broeck, G., Vergari, A.: Semantic probabilistic layers for neuro-symbolic learning. In: Advances in Neural Information Processing Systems 35 (NeurIPS). p. 29944–29959 (2022). https://doi.org/10.52202/068431-2171 [2] Alrabbaa, C., Borgwardt, S., Herrmann, S., Krötzsch, M.: The shape of EL proofs: A tale of three calculi. In: Proceedings of the 38th International Workshop on Description Logics (DL 2025) (2025), https://arxiv.org/abs/2507.21851 [3] Ashburner, M., Ball, C.A., Blake, J.A., Botstein, D., Butler, H., Cherry, J.M., Davis, A.P., Dolinski, K., Dwight, S.S., Eppig, J.T., Harris, M.A., Hill, D.P., Issel-Tarver, L., Kasarskis, A., Lewis, S., Matese, J.C., Richardson, J.E., Ringwald, M., Rubin, G.M., Sherlock, G.: Gene ontology: tool for the unification of biology. Nature Genetics 25(1), 25–29 (2000). https://doi.org/10.1038/75556 [4] Aspis, Y., Broda, K., Lobo, J., Russo, A.: Embed2Sym: Scalable neuro-symbolic reasoning via clustered embeddings. In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (KR). p. 421–431 (2022). https://doi.org/10.24963/kr.2022/44 [5] Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence (IJCAI). p. 364–369 (2005). https://doi.org/10.25368/2022.144 [6] Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope further. In: Proceedings of the OWLED 2008 DC Workshop on OWL: Experiences and Directions (2008) [7] Badreddine, S., Garcez, A.d., Serafini, L., Spranger, M.: Logic tensor networks. Artificial Intelligence 303, 103649 (2022). https://doi.org/10.1016/j.artint.2021.103649 [8] Bobillo, F., Straccia, U.: Fuzzy ontology representation using OWL 2. International Journal of Approximate Reasoning 52(7), 1073–1094 (2011). https://doi.org/10.1016/j.ijar.2011.05.003 [9] Bortolotti, S., Marconato, E., Carraro, T., Morettin, P., van Krieken, E., Vergari, A., Teso, S., Passerini, A.: A neuro-symbolic benchmark suite for concept quality and reasoning shortcuts. In: Advances in Neural Information Processing Systems 38 (NeurIPS), Datasets and Benchmarks Track (2024). https://doi.org/10.52202/079017-3679 [10] Bourguin, G., Lewandowski, A.: Pizzaïolo dataset: Des images synthétiques ontologiquement explicables. https://hal.science/hal-04401953 (2024), dataset DOI: https://doi.org/10.5281/zenodo.10165941 [11] Carral, D., González, L., Koopmann, P.: From Horn-SRIQ to Datalog: A data-independent transformation that preserves assertion entailment. Proceedings of the AAAI Conference on Artificial Intelligence 33(01), 2736–2743 (2019). https://doi.org/10.1609/aaai.v33i01.33012736 [12] Ceylan, İ.İ., Peñaloza, R.: Bayesian description logics. In: Proceedings of the 27th International Workshop on Description Logics (DL). CEUR Workshop Proceedings, vol. 1193, p. 447–458 (2014) [13] Ceylan, İ.İ., Peñaloza, R.: The bayesian ontology language ℬℰℒBEL. Journal of Automated Reasoning 58(1), 67–95 (2017). https://doi.org/10.1007/s10817-016-9386-0 [14] Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artificial Intelligence 172(6-7), 772–799 (2008) [15] Chen, J., Hu, P., Jimenez-Ruiz, E., Holter, O.M., Antonyrajah, D., Horrocks, I.: OWL2Vec*: embedding of OWL ontologies. Machine Learning 110(7), 1813–1845 (2021). https://doi.org/10.1007/s10994-021-05997-6 [16] Chen, J., Mashkova, O., Zhapa-Camacho, F., Hoehndorf, R., He, Y., Horrocks, I.: Ontology embedding: A survey of methods, applications and resources. IEEE Transactions on Knowledge and Data Engineering 37(7), 4193–4212 (2025). https://doi.org/10.1109/TKDE.2025.3559023 [17] Choi, A., Darwiche, A.: Dynamic minimization of sentential decision diagrams. In: Proceedings of the 27th AAAI Conference on Artificial Intelligence (2013). https://doi.org/10.1609/aaai.v27i1.8690 [18] Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, p. 293–322. Plenum Press (1978). https://doi.org/10.1007/978-1-4684-3384-5_11 [19] Daniele, A., van Krieken, E., Serafini, L., van Harmelen, F.: Refining neural network predictions using background knowledge. Machine Learning 112(9), 3293–3331 (2023). https://doi.org/10.1007/s10994-023-06310-3 [20] Darwiche, A.: SDD: A new canonical representation of propositional knowledge bases. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI). p. 819–826 (2011). https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-143 [21] Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research 17, 229–264 (2002). https://doi.org/10.1613/jair.989 [22] Donnelly, K.: SNOMED-CT: The advanced terminology and coding system for eHealth. Studies in Health Technology and Informatics 121, 279–290 (2006) [23] Guo, C., Pleiss, G., Sun, Y., Weinberger, K.Q.: On calibration of modern neural networks. In: Proceedings of the 34th International Conference on Machine Learning (ICML). p. 1321–1330 (2017) [24] Gutiérrez-Basulto, V., Jung, J.C., Lutz, C., Schröder, L.: A closer look at the probabilistic description logic Prob-EL. In: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence (AAAI). p. 197–202 (2011). https://doi.org/10.1609/aaai.v25i1.7856 [25] Jackson, R.C., Matentzoglu, N., Overton, J.A., Vita, R., Balhoff, J.P., Buttigieg, P.L., Carbon, S., Courtot, M., Diehl, A.D., Dooley, D.M., Duncan, W.D., Harris, N.L., Haendel, M.A., Lewis, S.E., Natale, D.A., Osumi-Sutherland, D., Ruttenberg, A., Schriml, L.M., Smith, B., Stoeckert, C.J., Vasilevsky, N.A., Walls, R.L., Zheng, J., Mungall, C.J., Peters, B.: OBO Foundry in 2021: operationalizing open data principles to evaluate ontologies. Database 2021, baab069 (2021). https://doi.org/10.1093/database/baab069 [26] Kazakov, Y., Krötzsch, M., Simčík, F.: The incredible ELK: From polynomial procedures to efficient reasoning with ℰℒEL ontologies. Journal of Automated Reasoning 53(1), 1–61 (2014). https://doi.org/10.1007/s10817-013-9296-3 [27] Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. In: Proceedings of the 3rd International Conference on Learning Representations (ICLR) (2015) [28] Kool, W., van Hoof, H., Welling, M.: Buy 4 REINFORCE samples, get a baseline for free! In: Workshop on Deep Reinforcement Learning Meets Structured Prediction (ICLR Workshop) (2019) [29] van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: On the independence assumption in neurosymbolic learning. In: Proceedings of the 41st International Conference on Machine Learning (ICML). PMLR, vol. 235 (2024) [30] van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: Neurosymbolic diffusion models. In: Advances in Neural Information Processing Systems 39 (NeurIPS) (2025) [31] van Krieken, E., Minervini, P., Ponti, E.M., Vergari, A.: Neurosymbolic reasoning shortcuts under the independence assumption. In: Proceedings of the 19th Conference on Neurosymbolic Learning and Reasoning (NeSy). Proceedings of Machine Learning Research, vol. 284, p. 1–18 (2025) [32] van Krieken, E., Thanapalasingam, T., Tomczak, J.M., van Harmelen, F., ten Teije, A.: A-NeSI: A scalable approximate method for probabilistic neurosymbolic inference. In: Advances in Neural Information Processing Systems 36 (NeurIPS) (2023). https://doi.org/10.52202/075280-1069 [33] Krötzsch, M.: Efficient Inferencing for OWL EL, p. 234–246. Springer Berlin Heidelberg (2010). https://doi.org/10.1007/978-3-642-15675-5_21 [34] Kulmanov, M., Guzmán-Vega, F.J., Duek Roggli, P., Lane, L., Arold, S.T., Hoehndorf, R.: Protein function prediction as approximate semantic entailment. Nature Machine Intelligence 6, 220–228 (2024). https://doi.org/10.1038/s42256-024-00795-w [35] Kulmanov, M., Hoehndorf, R.: DeepGOZero: improving protein function prediction from sequence and zero-shot learning based on ontology axioms. Bioinformatics 38(Supplement_1), i238–i245 (2022). https://doi.org/10.1093/bioinformatics/btac256 [36] Kulmanov, M., Liu-Wei, W., Yan, Y., Hoehndorf, R.: EL embeddings: Geometric construction of models for the description logic EL++. In: Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI). p. 6103–6109 (2019). https://doi.org/10.24963/ijcai.2019/845 [37] Lazzari, N., Presutti, V., Vergari, A.: To neuro-symbolic classification and beyond by compiling description logic ontologies to probabilistic circuits. CoRR abs/2601.14894 (2026). https://doi.org/10.48550/arXiv.2601.14894 [38] Li, Z., Huang, J., Naik, M.: Scallop: A language for neurosymbolic programming. In: Proceedings of the ACM on Programming Languages (PLDI) (2023). https://doi.org/10.1145/3591280 [39] Manhaeve, R., Dumančić, S., Kimmig, A., Demeester, T., De Raedt, L.: DeepProbLog: Neural probabilistic logic programming. In: Advances in Neural Information Processing Systems 31 (NeurIPS). p. 3753–3763 (2018) [40] Marconato, E., Bortolotti, S., van Krieken, E., Passerini, A., Teso, S., Vergari, A.: BEARS make neuro-symbolic models aware of their reasoning shortcuts. CoRR abs/2402.12240 (2024). https://doi.org/10.48550/arXiv.2402.12240 [41] Marconato, E., Passerini, A., Teso, S., Vergari, A.: Not all neuro-symbolic concepts are created equal: Analysis and mitigation of reasoning shortcuts. In: Advances in Neural Information Processing Systems 36 (NeurIPS). p. 72507–72539 (2023). https://doi.org/10.52202/075280-3170 [42] Mishra, A., Tahar, S.: VEL: A formally verified reasoner for OWL2 EL profile. arXiv preprint abs/2412.08739 (2024), https://arxiv.org/abs/2412.08739 [43] Pryor, C., Dickens, C., Augustine, E., Albalak, A., Wang, W.Y., Getoor, L.: NeuPSL: Neural probabilistic soft logic. In: Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI). p. 4145–4153 (2023). https://doi.org/10.24963/ijcai.2023/461 [44] Riguzzi, F., Bellodi, E., Lamma, E., Zese, R.: Probabilistic description logics under the distribution semantics. Semantic Web 6(5), 477–501 (2015). https://doi.org/10.3233/SW-140154 [45] Smith, B., Ashburner, M., Rosse, C., Bard, J., Bug, W., Ceusters, W., Goldberg, L.J., Eilbeck, K., Ireland, A., Mungall, C.J., Leontis, N., Rocca-Serra, P., Ruttenberg, A., Sansone, S.A., Scheuermann, R.H., Shah, N., Whetzel, P.L., Lewis, S.: The OBO Foundry: coordinated evolution of ontologies to support biomedical data integration. Nature Biotechnology 25(11), 1251–1255 (2007). https://doi.org/10.1038/nbt1346 [46] Stevens, R., Drummond, N., Rector, A.: The pizza ontology. https://github.com/owlcs/pizza-ontology, manchester University tutorial OWL ontology [47] Tarjan, R.: Depth-first search and linear graph algorithms. SIAM Journal on Computing 1(2), 146–160 (1972). https://doi.org/10.1137/0201010 [48] Tena Cucala, D., Cuenca Grau, B., Horrocks, I.: 15 years of consequence-based reasoning. In: Description Logic, Theory Combination, and All That, Lecture Notes in Computer Science, vol. 11560, p. 573–587. Springer (2019). https://doi.org/10.1007/978-3-030-22102-7_27 [49] The Gene Ontology Consortium: The gene ontology knowledgebase in 2023. Genetics 224(1), iyad031 (2023). https://doi.org/10.1093/genetics/iyad031 [50] Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers on Computational Logic 1967–1970, p. 466–483. Springer (1983). https://doi.org/10.1007/978-3-642-81955-1_28 [51] Xu, J., Zhang, Z., Friedman, T., Liang, Y., Van den Broeck, G.: A semantic loss function for deep learning with symbolic knowledge. In: Proceedings of the 35th International Conference on Machine Learning (ICML). PMLR, vol. 80, p. 5498–5507 (2018) [52] Yang, Z., Ishay, A., Lee, J.: NeurASP: Embracing neural networks into answer set programming. In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI) (2020). https://doi.org/10.24963/ijcai.2020/243 [53] Zhao, Y.: Fast and faithful: Scalable neuro-symbolic learning and reasoning with differentiable fuzzy EL++. In: Proceedings of the 34th ACM International Conference on Information and Knowledge Management (CIKM) (2025). https://doi.org/10.1145/3770854.3780220 [54] Zhapa-Camacho, F., Kulmanov, M., Hoehndorf, R.: mOWL: Python library for machine learning with biomedical ontologies. Bioinformatics 39(1), btac811 (2023). https://doi.org/10.1093/bioinformatics/btac811 Appendix 0.A ℰℒ++EL^++ syntax, semantics, and ELK calculus This appendix collects the formal foundations on which Moose is built: the syntax and semantics of the ℰℒ++EL^++ profile of OWL 2 EL, the Baader–Brandt–Lutz (BBL) normal-form rules NF1–NF7 [5], and the ELK saturation calculus [26] that drives Stage 1 of the compilation pipeline. Every construct, normal form, and rule listed here is also formalized in the Lean 4 library introduced below; Appendix 0.D contains the full proofs of §4. The Lean library. All formalized statements cited in this paper live in the Lean 4 library ELKSDD, distributed with the supplementary release at https://github.com/bio-ontology-research-group/moose-iswc/. Theorems are organized into namespaces: ELKSDD.ELpp (the bulk of the OWL 2 EL stack (syntax, semantics, the ELK saturation calculus, canonical-model completeness, the SCC compositional results, the DISPONTE correspondence, and the paper-citation theorems), ELKSDD.SDD (sentential decision diagrams and weighted model counting), ELKSDD.RangeNorm (the syntactic range-elimination of [6]), and the ELKSDD.EL and ELKSDD.MiniEL fragments for testing purposes. The DeepProbLog equivalence layer lives in a companion library under namespace Moose. Inline references of the form <namespace>.<theorem> point to a specific theorem; the index in Section 0.D.10 cross-references every paper claim with its mechanized counterpart. Every theorem listed in Section 0.D.10 is audit-clean: its proof depends only on the standard Lean foundation propext,Classical.choice,Quot.sound\ propext,\, Classical.choice,\, Quot.sound\ and the formalization contains zero sorry or admit. An audit pass in each library runs #print axioms on every paper-cited theorem at build time and reports its dependency set. Syntax. Fix countably infinite, pairwise-disjoint vocabularies of atomic concept names N_C, role names N_R, and individual names N_I. ℰℒ++EL^++ concepts are built by the grammar C,D::=⊤∣⊥∣A∣a∣C⊓D|∃R.C,C,D\;::=\; A \a\ C D ∃ R.C, where A∈A∈ N_C, a∈a∈ N_I, and R∈R∈ N_R. An ontology O is a finite set of axioms of one of the following shapes (Table 4): general concept inclusions C⊑DC D, role inclusions R⊑SR S, role chains R1∘R2⊑SR_1 R_2 S, range restrictions range(R)⊑Crange(R) C, reflexive-role declarations Ref(R)Ref(R), local-reflexivity ∃R.∃ R. Self, and key axioms HasKey(C,R1,…,Rn)HasKey(C,R_1,…,R_n). The ground vocabulary of O over a finite individual set Δ is Δ:=A(a):A∈C(),a∈Δ∪R(a,b):R∈R(),a,b∈ΔV_O :=\A(a):A∈ Sig_C(O),\,a∈ \∪\R(a,b):R∈ Sig_R(O),\,a,b∈ \. Semantics. An interpretation ℐ=(Δℐ,⋅ℐ)I=( ^I,·^I) comprises a non-empty domain Δℐ ^I and a mapping ⋅ℐ·^I that sends each A∈A∈ N_C to Aℐ⊆ΔℐA^I ^I, each R∈R∈ N_R to Rℐ⊆Δℐ×ΔℐR^I ^I× ^I, and each a∈a∈ N_I to aℐ∈Δℐa^I∈ ^I. Concept and axiom semantics extend ⋅ℐ·^I to compound concepts and constraints as in Table 4. ℐI is a model of O, written ℐ⊧I , if it satisfies every axiom in O; ⊧C⊑DO C D means Cℐ⊆DℐC^I D^I in every model ℐI of O. Table 4: ℰℒ++EL^++ syntax and semantics. Together with role inclusion, role chain, and range axioms, plus the ABox-style constructs (nominals, Self, HasKeyHasKey), this is the OWL 2 EL profile minus datatype properties. Construct Syntax Semantics top ⊤ Δℐ ^I bottom ⊥ ∅ atomic concept A Aℐ⊆ΔℐA^I ^I nominal a\a\ aℐ\a^I\ conjunction C⊓DC D Cℐ∩DℐC^I∩ D^I existential ∃R.C∃ R.C a∣∃b:(a,b)∈Rℐ,b∈Cℐ\a ∃ b:\,(a,b)∈ R^I,\,b∈ C^I\ local reflexivity ∃R.∃ R. Self a∣(a,a)∈Rℐ\a (a,a)∈ R^I\ GCI C⊑DC D Cℐ⊆DℐC^I D^I role inclusion R⊑SR S Rℐ⊆SℐR^I S^I role chain R1∘R2⊑SR_1 R_2 S R1ℐ∘R2ℐ⊆SℐR_1^I R_2^I S^I range restriction range(R)⊑Crange(R) C ∀(a,b)∈Rℐ:b∈Cℐ∀(a,b)∈ R^I:\,b∈ C^I reflexive role Ref(R)Ref(R) (a,a)∈Rℐ(a,a)∈ R^I for all a∈Δℐa∈ ^I key HasKey(C,R1,…,Rn)HasKey(C,R_1,…,R_n) shared RiR_i-fillers force individual identity BBL normal forms NF1–NF7. Baader, Brandt, and Lutz [5] show every ℰℒ++EL^++ ontology can be transformed into one whose GCIs have one of seven shapes by introducing fresh atomic names, with the transformation conservative for atomic subsumptions: NF1, A1⊓⋯⊓An⊑BA_1 … A_n B (atomic conjunctive LHS); NF2, ∃R.A⊑B∃ R.A B (atomic existential LHS); NF3, A⊑∃R.BA ∃ R.B (atomic existential RHS); NF4, A⊑⊥A (atomic unsat); NF5, A⊑BA B (atomic-atomic); NF6, ⊤⊑A A (top-LHS); NF7, ⊥⊑A A (vacuous). Our Lean formalization (namespace ELKSDD.Normalize) covers all seven rules via the canonical-extension construction of BBL 2005, §3.1. ELK saturation calculus. Kazakov, Krötzsch, and Simančík [26] give a saturation procedure that decides Sat-derivability (,C,D) Sat(O,C,D) for the full OWL 2 EL profile (minus datatypes) in time O(||4)O(|O|^4). The calculus operates on a finite collection of atomic subsumptions and links E→DE RD, closed under a fixed rule set: R0R_0 (A⊑A A), R⊤R_ (A⊑⊤A ), R⊑R_ (transitivity along axioms), R⊓−R^-_ and R⊓+R^+_ (conjunction), R⊥R_ (unsatisfiability propagation), R∃+R^+_∃ and R⊥-∃R_ -∃ (existential constructors), role-side rules RrincR_rinc, RrchainR_rchain for role inclusions and chains, plus specialized rules for ranges, reflexive roles, Self, the nominal-handling rules of [26, §3], and the merging canonical-model construction of [26, §6] for shapes 1–4 of nominals together with HasKeyHasKey. Saturation terminates because all derivable atoms are over the finite vocabulary of ()∪() Sub(O)∪ Roles(O); the resulting closure has size O(n2r)O(n^2r) for n=|()|n=| Sub(O)| and r=|()|r=| Roles(O)| [26, Thm. 1]. Our formalization (namespace ELKSDD.ELpp) mechanizes the same calculus, sound and complete on the nominal-free fragment (with ranges, reflexive roles, Self, role inclusions, and role chains) and on the LHS-nominal and shallow-exist-RHS-nominal extensions; shapes 2/4 (RHS-nominal GCIs C⊑aC \a\, a⊑b\a\ \b\) and HasKeyHasKey are handled by the merging canonical-model construction of [26, §6], fully mechanized as ELKSDD.ELpp.complete_via_mergedCanon_regular and ELKSDD.ELpp.complete_via_mergedCanon_nom (both audit-clean), under the shallow concept restriction of [26, §6]: concepts may not contain deep existentials with non-nominal targets. The unified completeness theorem ELKSDD.ELpp.complete_owl2el cases on a fragment witness to invoke the appropriate canonical-model construction; together with ELKSDD.ELpp.sound_owl2el, it gives Sat ⇔ Entails on every ontology meeting at least one of its five branch preconditions. Every individual ℰℒ++EL^++ construct (nominals, ranges, role chains, reflexive, Self, HasKeyHasKey) is supported in some branch, but the branches are not jointly compatible: shapes 2/4 (RHS-nominal GCIs C⊑aC \a\, a⊑b\a\ \b\) combined with deep non-nominal existentials, and the merging fragment combined with role chains or ranges, hit the case-disabling preconditions of [26, §6] (an ontology may have a model where C is empty and another where C is forced into the a\a\-class; a single canonical construction must pick one); the supported shapes follow the consequence-based reasoning literature [48, 2]. The concurrent verified-reasoner effort VEL [42] mechanizes BBL 2005 ℰℒ++EL^++ in Coq but covers strictly less than our unified completeness theorem (no nominals, no RHS-nominal GCIs, no ranges, no role chains, no HasKey). The exact closure-size bound |L|≤5n3(r+1)|L|≤ 5n^3(r+1) that includes ranges, reflexive, and Self is ELKSDD.ELpp.sat_closure_total_polynomial_bound. Appendix 0.B Task formalism and MNIST instantiation Definition 1 (ABox-supervised latent concept learning) A training instance is a triple (Δ,,)( ,x,e) where =(xa)a∈Δx=(x_a)_a∈ with each xa∈x_a and e is a set of literals (truth-tagged ground atoms) over the observable ground vocabulary; ground atoms not in e are unobserved. The task is to learn a weight-shared per-individual classifier fθ:→[0,1]|Cℓ|f_θ:X→[0,1]^| Sig _C| such that fθ(xa)[C]f_θ(x_a)[C] approximates the marginal probability of C(a)C(a) given O and e, for every C∈CℓC∈ Sig _C and a∈Δa∈ . A negative literal ¬C(a)∈ C(a) encodes the polarity of a ground variable in ΔV_O (ℰℒ++EL^++ itself has no concept negation); role atoms are not classified by fθf_θ, and latent role atoms are marginalized at the uniform prior. A boolean assignment M:Δ→0,1M:V_O →\0,1\ induces an ABox interpretation ℐM=(Δ,⋅M)I_M=( ,·^M) via CM:=a:M(C(a))=1C^M:=\a:M(C(a))=1\ and RM:=(a,b):M(R(a,b))=1R^M:=\(a,b):M(R(a,b))=1\. The differentiable WMC layer evaluates (α,w,) WMC(α;w,e) where the literal-weight map w is the unique extension of fθ()f_θ(x) and e that makes the training-loss, posterior, and entailment-query operations of §3.4 three settings of the same SDD traversal: The literal-weight map itself is now inlined in §3.1 as Table 1. Example 1 (MNIST instantiation) Definition 1 instantiates on MNIST as follows. The TBox is MNISTO_ MNIST over C=D0,…,D9,Even,Odd,Prime,Composite Sig_C=\D_0,…,D_9,\, Even, Odd, Prime, Composite\ and R=succ,plus_two Sig_R=\ succ, plus\_two\ (full listing in Section 0.F.2). The observable signature is Co=Even,Odd,Prime,Composite Sig^o_C=\ Even, Odd, Prime, Composite\; the latent signature is Cℓ=D0,…,D9 Sig _C=\D_0,…,D_9\ (the digit class is never revealed). A training instance places one MNIST image xax_a at each named individual and supplies one or two property literals as evidence, e.g. =Even(a),¬Prime(a)e=\ Even(a),\, Prime(a)\ for an image of digit 44. An independent per-atom baseline matching its predictions to the observed literals provably cannot disambiguate the latent atoms when several digits share the property profile (e.g. D3,D5,D7D_3,D_5,D_7 are all Odd⊓Prime Odd Prime) [39, 41, 29]. 0.B.1 Summary of pipeline assumptions Table 5 collects the assumptions that the pipeline introduces beyond the source ontology, one per component, and states for each what it concedes relative to the open-world semantics that OWL EL is designed for. The assumptions are not defects of the implementation but scoping choices that define the ABox-supervised learning task (Definition 1); the right-hand column makes explicit what a user gives up by adopting them. Table 5: Assumptions introduced by each component of the Moose pipeline and their departure from open-world semantics. Component Assumption Departure from open-world semantics EL fragment Background axioms lie in the ℰℒ++EL^++ profile: conjunction and existentials, no right-hand-side disjunction or cardinality. Exhaustiveness and counting are not natively expressible; they must be supplied as closure axioms rather than read from the ontology. Closed domain Learning and inference range over a given finite set of named individuals. No certain answers are produced over anonymous or unnamed individuals; entailment over the anonymous domain is not performed. Role-pinning An existential ∃R.C∃ R.C is scored on the observed role pair, with role atoms over Ro Sig^o_R fixed by the evidence. Unobserved role witnesses are not hypothesized; existential import over the anonymous domain is dropped. Declared families Mutual exclusion and covering hold only on families the modeller declares exhaustive. The closed-world reading is local and opt-in; outside declared families the open-world reading is retained. Factorized perception The predictor factorizes pθ(∣)=∏ipθ(ci∣)p_θ(c )= _ip_θ(c_i ): atoms independent given the image. Joint perceptual correlations among atoms are not modeled; this is the reasoning-shortcut source, mitigated but not removed by BEARS and NeSyDM. Appendix 0.C Compilation algorithm and worked example This appendix gives the seven-stage compilation pseudocode (Algorithm 1) and works a concrete two-axiom ontology through it (Section 0.C.3). 0.C.1 Pseudocode Algorithm 1 gives the full pseudocode of the seven-stage compilation algorithm summarized in §3.2. Stages 2–5 (Clark completion of the saturation output, SCC detection via Tarjan’s algorithm, SCC-local time-stamped unrolling, and Tseitin CNF conversion) operate on the TBox-level derived atoms and produce a propositional CNF that exactly characterizes the ELK canonical model. For acyclic ontologies (all SCCs are trivial), Stages 3–4 are no-ops and the Clark biconditionals compile directly to CNF. Two implementation choices are essential for the soundness, completeness, and termination arguments. The first is the signature side condition on the existential-introduction rule R∃+R^+_∃: the rule fires only on existentials already in () Sub(O) (line 1 of the algorithm). This is the standard ELK rule [26, §5] and is what keeps saturation finite on ontologies with cyclic role inclusions. The second is uniform super-role materialization under the role-composition rule R∘R_ : the implementation routes every link insertion through a helper that records the link for the base role and, recursively, for every strict super-role. Without this step, an ontology with R1∘R2⊑SR_1 R_2 S and S⊑TS T produces the S-link from the chain rule but silently loses the T-link, breaking ELK completeness (Theorem 0.D.1) on chain heads with a super-role. Algorithm 1 Moose: ℰℒ++EL^++ ontology to SDD over ground atoms 1: Ontology O as a set of GCIs C⊑DC D, role inclusions R⊑SR S, role chains R1∘R2⊑SR_1 R_2 S. Finite ABox domain Δ . 2: SDD α over ΔV_O (Theorem 4.1). 3: 4: [Stage 1: ELK saturation] 5: ℰ∃←∃R.D∣∃R.D∈()E_∃←\∃ R.D ∃ R.D∈ Sub(O)\ ⊳ signature side condition on R∃+R^+_∃ 6: (Σ,Λ)←Saturate(,ℰ∃)( , )← Saturate(O,E_∃) ⊳ Σ : subsumptions C⊑DC D; Λ : links E→CE RC 7: 8: [Stages 2–5: Clark completion, SCC, unrolling, CNF] 9: for each derived atom h∈Σ∪Λh∈ ∪ do 10: Clark(h)←h↔⋁j(⋀b∈j(h)b) Clark(h)← h _j( _b _j(h)b) ⊳ Stage 2: Clark completion 11: end for 12: SCCs←Tarjan(DepGraph(Clark)) SCCs← Tarjan( DepGraph( Clark)) ⊳ Stage 3: SCC detection 13: for each non-trivial SCC S of size T=|S|T=|S| (|S|>1|S|>1 or self-loop) do ⊳ Stage 4: time-stamped unrolling 14: for each h∈Sh∈ S do 15: emit xh(0)↔⊥x_h^(0) ; xh↔xh(T)x_h x_h^(T) 16: end for 17: for each h∈Sh∈ S, t=0,…,T−1t=0,…,T-1 do 18: emit xh(t+1)↔xh(t)∨⋁j(⋀bxb(t))x_h^(t+1) x_h^(t) _j( _bx_b^(t)) 19: end for 20: end for 21: CNF←Tseitin(all formulas) CNF← Tseitin(all formulas) ⊳ Stage 5: CNF conversion 22: 23: [Stages 6–7: ABox grounding and SDD compilation] 24: AtomSub←(X,Y)∈Σ:X,Y∈C(),X≠Y AtomSub←\(X,Y)∈ :X,Y∈ Sig_C(O),\ X≠ Y\ 25: Disj←flatten(C):(C⊑⊥)∈Σ,C atomic conjunction Disj←\ flatten(C):(C )∈ ,\ C atomic conjunction\ 26: Unsat←X∈Σ:X⊑⊥,X∈C() Unsat←\X∈ :X ,\ X∈ Sig_C(O)\ 27: Links←(X,R,Y)∈Λ:X,Y∈C() Links←\(X,R,Y)∈ :X,Y∈ Sig_C(O)\ 28: Γ←∅ ← 29: for (X,Y)∈AtomSub,a∈Δ(X,Y)∈ AtomSub,\ a∈ do Γ∪=¬X(a)∨Y(a) \;∪\!=\;\ X(a) Y(a)\ 30: end for 31: for (X1,…,Xn)∈Disj,a∈Δ(X_1,…,X_n)∈ Disj,\ a∈ do Γ∪=⋁i¬Xi(a) \;∪\!=\;\ _i X_i(a)\ 32: end for 33: for X∈Unsat,a∈ΔX∈ Unsat,\ a∈ do Γ∪=¬X(a) \;∪\!=\;\ X(a)\ 34: end for 35: for (X,R,Y)∈Links,(a,b)∈Δ2,a≠b(X,R,Y)∈ Links,\ (a,b)∈ ^2,\ a≠ b do 36: Γ∪=¬X(a)∨¬R(a,b)∨Y(b) \;∪\!=\;\ X(a) R(a,b) Y(b)\ ⊳ NF3 forward 37: if |Y′:(X,R,Y′)∈Links|=1|\Y :(X,R,Y )∈ Links\|=1 then 38: Γ∪=¬R(a,b)∨¬Y(b)∨X(a) \;∪\!=\;\ R(a,b) Y(b) X(a)\ ⊳ NF4 reverse 39: end if 40: end for 41: return SDDCompile(Γ) SDDCompile( ) ⊳ PySDD bottom-up 0.C.2 Stages 2–5: the TBox-level encoding This subsection expands the Stage 2–5 block of Algorithm 1, which turns the Stage-1 saturation into a propositional TBox theory. For NeSy learning these stages are diagnostic (§3.2); they are the compilation path used for probabilistic ontology reasoning, where the input-axiom variables carry weights. Stage 2: Clark completion. The saturation of Stage 1 can be viewed as a monotone Datalog program [18]: each derived atom h has one or more grounded rule body 1,…,kbody_1,…,body_k that can derive it. The Clark completion replaces these defining clauses with a biconditional h⟷1∨2∨⋯∨k,h\; \;body_1\; \;body_2\; \;·s\; \;body_k, (4) asserting that h holds if and only if at least one of its justifications holds. Each jbody_j is a conjunction of previously derived atoms and input axiom variables αi _i representing ontology axioms. The input variables are free (not defined by any biconditional) and represent whether each axiom is active: in standard reasoning all αi _i are true; in probabilistic reasoning each carries a weight. When the dependency graph is acyclic, Clark completion has the Datalog least fixed point as its only model for each assignment to the input variables [18]. For recursive monotone Datalog, however, completion alone can also admit supported non-least fixed points. Stages 3–4 therefore identify recursive strongly connected components and replace their circular definitions by time-stamped unrolling from the all-false interpretation. The completed and unrolled theory, rather than Clark completion alone, has exactly one model; with all αi _i true, that model is exactly the set of atoms ELK derives from O, i.e. the saturation closure Sat() Sat(O) [26]. When the ontology contains axioms with existential restrictions, derived atoms can have heads that contain nested existentials, e.g. xDi⊑∃R.∃R.Dkx_D_i ∃ R.∃ R.D_k. For NeSy training, the Clark completion is restricted to atoms whose head is an atomic concept, a conjunction of atomic concepts, ⊤ , or ⊥ (the groundable atoms); all other atoms are filtered out. This keeps Stages 3–5 tractable without losing any ABox-relevant consequence, because the filtered atoms have no corresponding ground variable in ΔV_O . Stage 3: SCC detection. The dependency graph among derived atoms may contain cycles. For example, a cyclic successor chain D0⊑∃succ.D1⊑∃succ.∃succ.D2⊑⋯⊑D0D_0 ∃ succ.D_1 ∃ succ.∃ succ.D_2 ·s D_0 (through the existential derivations) produces circular dependencies among the derived concept-level atoms. Plain biconditionals have circular definitions in this case. We apply Tarjan’s algorithm [47] to find strongly connected components (SCCs) of the dependency graph. Acyclic atoms (trivial SCCs) can use the plain biconditional of Equation 4 directly. Non-trivial SCCs (size >1>1, or self-loops) require time-stamped unrolling in Stage 4. Stage 4: propositional compilation with time-stamped unrolling. For acyclic atoms the biconditional of Equation 4 is directly expressible in propositional logic. For cyclic SCCs we break the circularity by introducing time-stamped copies xh(0),xh(1),…,xh(T)x_h^(0),x_h^(1),…,x_h^(T) of each atom h within the SCC and defining: xh(0) x_h^(0) ⟷⊥, \; \; , (5) xh(t+1) x_h^(t+1) ⟷xh(t)∨⋁j(⋀b∈j(h)xb(t)), \; \;x_h^(t)\; \; _j ( _b _j(h)x_b^(t) ), (6) xh x_h ⟷xh(T), \; \;x_h^(T), (7) where the local bound T=|S|T=|S| (the SCC size) suffices because each iteration of the monotone operator must derive at least one new atom or the fixed point is already reached. Only atoms within the same non-trivial SCC receive time-stamped copies; atoms from other SCCs (already computed in topological order) use their plain variable. This gives total cost ∑S|S|2 _S|S|^2 instead of ||2|V|^2 for global unrolling. Stage 5: CNF conversion. The Tseitin transformation [50] converts the nested propositional formulas from Stage 4 into equisatisfiable conjunctive normal form (CNF) by introducing an auxiliary variable for each sub-formula φ and adding clauses that enforce the auxiliary to equal φ . The resulting CNF is linear in the size of the Stage 4 output and encodes the full TBox-level propositional theory. In the probabilistic ontology reasoning use case, this CNF is the input to an SDD compiler that produces a circuit over the input-axiom variables; in the NeSy learning use case, the CNF serves a diagnostic role (characterizing the TBox complexity) and the ABox grounding of Stage 6 produces its own clause set over ΔV_O . WMC recursion. The differentiable WMC layer of Stage 7 traverses the compiled SDD α and evaluates (α,w)=w(ℓ)if α=ℓ is a literal node,0if α=⊥,1if α=⊤,∑(pi,si)∈α(pi,w)⋅(si,w)if α is a decision node, WMC(α;w)\;=\; casesw( )&if α= is a literal node,\\ 0&if α= ,\\ 1&if α= ,\\ _(p_i,s_i)∈α WMC(p_i;w)· WMC(s_i;w)&if α is a decision node, cases (8) with literal weights w read from Table 1. 0.C.3 Worked example Consider the two-axiom fragment 5:=D5⊑Odd,D5⊑PrimeO_5:=\D_5 Odd,\,D_5 Prime\ on Δ=a =\a\, drawn from MNISTO_ MNIST (§5.1). Stage 1 runs the ELK rule R⊑R_ over 5O_5 and adds the two input axioms to Σ as atomic subsumptions; no role axioms, so Λ=∅ = . Stages 2–5 (Clark completion, SCC detection, propositional compilation, CNF conversion) produce a propositional theory over the derived atoms; for this acyclic two-axiom fragment no time-stamped unrolling is needed (both atoms are in trivial SCCs). Stage 6 applies the four extractors to (Σ,Λ)( , ): both subsumptions match the AtomSub shape (atomic-atomic, X≠YX≠ Y), so AtomSub=(D5,Odd),(D5,Prime) AtomSub=\(D_5, Odd),\,(D_5, Prime)\; the other extractors produce nothing. The extractors ground each (X,Y)∈AtomSub(X,Y)∈ AtomSub on every a∈Δa∈ , emitting Γ=¬D5(a)∨Odd(a),¬D5(a)∨Prime(a) =\\, D_5(a) Odd(a),\; D_5(a) Prime(a)\,\ over 5aV_O_5^\a\. Stage 7 compiles Γ into an SDD whose models are exactly the assignments in which D5(a)=1D_5(a)=1 implies Odd(a)=1 Odd(a)=1 and Prime(a)=1 Prime(a)=1. The full MNISTO_ MNIST extends 5O_5 with the analogous property axioms for the remaining digits, the 4545 pairwise digit disjointness axioms (handled by Disj), the 1010 NF3 successor existentials, and the NF7 role chain (Section 0.F.2); the SDD is 155155 nodes over 1414 atoms and compiles in under a quarter of a second (Section 0.F.1). Appendix 0.D Full proofs This part of the appendix contains the full proofs of the §4 theorems (Theorems 4.1, 4.2, 4.3 and 4.4), the ELK mechanization of the reused infrastructure (Theorems 0.D.1 and 0.D.2, Section 0.D.1), and the closure-augmented and inference-time variants (Theorems 0.D.3 and 0.D.4). The final subsection (Section 0.D.10) cross-references each paper claim with its Lean module and theorem identifier. We use the notation introduced in §4. Mechanized statements. The Lean library ELKSDD (Appendix 0.A) proves every prior-work result it relies on rather than admitting it as an axiom: ELK soundness/completeness [26] is proved end-to-end in namespaces ELKSDD.EL and ELKSDD.ELpp; SDD compilation correctness [21, 17] and the WMC-correctness theorem underlying Theorem 0.D.4(c) are proved structurally in namespace ELKSDD.SDD; the four ELK extractors are concrete noncomputable defs with proven membership and size theorems; the Manhaeve 2018 distribution-semantics step of the DPL-equivalence proof is closed both qualitatively (Iff.rfl) and quantitatively ([21] SDD-WMC correctness, by structural induction). Running #print axioms on every paper-cited theorem at build time confirms that the dependency set is exactly propext,Classical.choice,Quot.sound\ propext, Classical.choice, Quot.sound\. 0.D.1 Reused ELK infrastructure: soundness, completeness, and polynomial Sat decision The two results below are restatements of the standard ELK soundness/completeness theorem and the polynomial-time Sat decision procedure of Kazakov, Krötzsch, and Simančík [26]. They are reused unchanged in §4 but re-mechanized in our Lean library so that Theorems 4.1, 4.2, 4.3 and 4.4 can be proved within the same audit-clean foundation. OWL2ELFragment abbreviates the syntactic fragment witness selecting the canonical-model construction used for completeness on (,C,D)(O,C,D): (a) nominal-free with C,DC,D in the signature of O and range-chain-safe; (b) the ABox-style LHS-nominal extension; (c) the shallow-exist RHS-nominal extension; (d) the strict fragment without ranges or chains; (e) the merging canonical model [26, §6] for shapes 1–4 of nominals and HasKeyHasKey, restricted to Shallow concepts (no deep existentials with non-nominal targets). The disjunction is the inductive predicate ELKSDD.ELpp.OWL2ELFragment; together with OWL2ELFragment the unified completeness theorem ELKSDD.ELpp.complete_owl2el covers any ontology meeting at least one branch precondition (a)–(e). Every individual ℰℒ++EL^++ construct is supported in some branch; the residual unmechanized cases (shapes 2/4 (RHS-nominal GCIs) combined with deep non-nominal existentials, and the merging fragment combined with ranges or chains) correspond to the case-disabling preconditions of [26, §6] and constitute open work in the ELK literature itself rather than gaps in the Lean formalization (see Appendix 0.A for discussion of a 2019 survey, a 2025 proof-theoretic study, and the concurrent VEL effort, none of which extend the canonical-model coverage). The atomic-shape vocabulary ΔV_O used by the SDD encoding (§3.2) is a separate, deliberate scope choice: nested existentials produce ELK-internal derivations but have no ground counterpart in the SDD; ELK Sat-completeness via the unified completeness theorem holds over all concepts, the SDD-encoding completeness holds over the atomic-shape ABox slice (Theorem 4.1). Theorem 0.D.1 (ELK soundness and completeness on ℰℒ++EL^++) For every ℰℒ++EL^++ ontology O and concepts C,DC,D, if (,C,D) OWL2ELFragment(O,C,D) holds then (,C,D)⇔⊧C⊑D. Sat(O,C,D)\; \;O C D. (9) Proof Soundness (left to right) is unconditional in OWL2ELFragment and proved by structural induction on the ELK derivation, mechanized as ELKSDD.ELpp.sound_owl2el. Completeness (right to left) is by case-split on OWL2ELFragment to one of five canonical-model constructions (Kazakov 2014 §3, §6 for the merging case); mechanized as ELKSDD.ELpp.complete_owl2el. See [26] for the original arguments.∎ Theorem 0.D.2 (Polynomial Sat decision) For every ℰℒ++EL^++ ontology O there exists a list L of pairs of concepts with |L|≤|()|2|L|≤| Sub(O)|^2 such that for every C,D∈()C,D∈ Sub(O), (,C,D)⇔(C,D)∈L. Sat(O,C,D)\; \;(C,D)∈ L. Proof The witness L is the time-stamped Clark closure derivableClosure() derivableClosure(O): length bound by derivableClosure_length (counts concept pairs in the saturation closure); membership equivalence by sat_iff_in_derivableClosure (simultaneous induction over the Sat constructors). Mechanized as ELKSDD.ELpp.sat_decision_polynomial; an exact closure-size bound |L|≤5n3(r+1)|L|≤ 5n^3(r+1) that includes ranges, reflexive, and Self (n=|()|n=| Sub(O)|, r=|()|r=| Roles(O)|) is ELKSDD.ELpp.sat_closure_total_polynomial_bound, with per-shape exact lengths. See [26, Thm. 1, §5] for the original O(||4)O(|O|^4) saturation runtime. ∎ 0.D.2 Verified SDD encoding (Theorem 4.1) Proof (Proof of Theorem 4.1) The witness is t=(,C,D)t= cmp(O,C,D), mechanized in namespace ELKSDD.ELpp (with the SDD-side WMC theorems in namespace ELKSDD.SDD). Conjunct (1): the compiled Shannon tree’s models are exactly the worlds whose selected sub-ontology is Sat-derivable. Conjunct (2): a Shannon-recursive unfolding of WMC enumerating the 2||2^|O| leaves. Conjunct (3): by induction on |||O|, a Shannon node at depth k has 2||−k+1−12^|O|-k+1-1 descendants. Lean theorem identifiers are listed in Table 6. ∎ The standard probabilistic-DL “entailment-as-WMC-zero” phrasing [44] follows immediately: at uniform per-axiom prior w≡12w≡ 12, ℚ=0 WMC^Q=0 iff no world’s selected sub-ontology entails C⊑DC D (Theorem 4.2 combined with Theorem 0.D.1). The production four-extractor ground encoding (§3.2, Stages 6–7) is a separate ABox encoding whose soundness over the finite domain follows from Theorem 0.D.1 (Lean: ELKSDD.ELpp.sound_owl2el and ELKSDD.ELpp.complete_owl2el) under the partial-supervision role-pinning of §3.2. 0.D.3 Correctness of the closure-augmented circuit (Theorem 0.D.3) Theorem 0.D.3 (Correctness of the closure-augmented circuit) For every modeller-declared exhaustive family ℱ=D0,…,DK−1F=\D_0,…,D_K-1\, define π(a) match_π(a) as the conjunction of the positive and negated property literals specified by profile π. Then M⊧αclosM _clos iff M⊧αELM _EL and, at every a∈Δa∈ , both of the following hold: (i) the partition constraints ¬(Di(a)∧Dj(a)):i<j∪D0(a)∨⋯∨DK−1(a)\ (D_i(a) D_j(a)):i<j\∪\D_0(a) … D_K-1(a)\; and (i), for every distinct declared profile π, the reverse implication π(a)→⋁i:πi=πDi(a) match_π(a)→ _i:\, _i=πD_i(a). Proof (Proof of Theorem 0.D.3) αclos=SDDCompile(ΓEL∪Φclos) _clos= SDDCompile( _EL∪ _clos) by construction. For each marked family and individual, Φmutex _mutex contains the (K2) K2 clauses ¬Di(a)∨¬Dj(a) D_i(a) D_j(a), and Φcover _cover contains D0(a)∨⋯∨DK−1(a)D_0(a) … D_K-1(a). These are exactly the partition constraints in clausal form. For every distinct profile π, Φprofile _profile additionally contains the clausal form of π(a)→⋁i:πi=πDi(a) match_π(a)→ _i:\, _i=πD_i(a). Therefore, satisfaction of the full clause set is equivalent to conditions (i)–(i). Generic SDD compilation correctness then gives the stated model equivalence [17, 21]. The Lean theorem ELKSDD.SDD.compile_correct quantifies over the complete input clause list, so it applies to all three components of Φclos _ clos.∎ 0.D.4 Production-encoding size Theorem 0.D.2 bounds the saturation closure by |()|≤5n3(r+1)| Sat(O)|≤ 5n^3(r+1) atoms with n=|()|n=| Sub(O)| and r=|()|r=| Roles(O)| (Lean: ELKSDD.ELpp.sat_closure_total_polynomial_bound). Grounding the extractors of §3.2 over |Δ|=m| |=m named individuals adds an at-most m2m^2 multiplicative factor (AtomSub, Disj, Unsat contribute m clauses each; Links contributes up to m2m^2 for the NF3/NF4 clauses). Each declared exhaustive family of size K adds a further (K2)m+(K+1)m K2m+(K+1)m closure clauses ((K2)m K2m mutex, m covering, and up to KmKm profile-keyed reverse implications). SDD compilation of the resulting CNF is treated in Section 0.D.5. 0.D.5 SDD treewidth dependence and empirical scaling Bottom-up SDD compilation [17] of a CNF Γ produces an SDD whose worst-case size is exponential in |Γ|| | [21]. For CNFs whose primal graph has treewidth w, the resulting SDD admits a polynomial bound O(|Γ|⋅2w)O(| |· 2^w) because tractable WMC over bounded-treewidth instances is reducible to compact circuit compilation. Empirically on mnist the SDD node count fits ∝|Δ|2.9 | |^2.9 for |Δ|≤3| |≤ 3 (consistent with the bounded-treewidth regime), with a 40×40× compile-time jump between |Δ|=3| |=3 and |Δ|=4| |=4 as the primal-graph treewidth rises; at the |Δ|=2| |=2 configurations used in §5 compilation finishes well below one second on a CPU (1× RTX 4090, single CPU core; Section 0.F.1). 0.D.6 Inference complexity (Theorem 0.D.4) Theorem 0.D.4 (Inference complexity) Let |α||α| denote the node count of either αEL _EL or αclos _clos. The training loss Equation 11, conditional posterior Equation 12, entailment query Equation 13, and one training step (loss plus gradient) all run in O(|α|)O(|α|) time [21, 17], with the training step adding the cost of one forward and backward pass of fθf_θ. Proof (Proof of Theorem 0.D.4) The SDD α produced by Algorithm 1 is smooth, decomposable, and deterministic by PySDD construction [21, 17]; let |α||α| denote its node count. (a) WMC. The recursive traversal of §3.2 visits each node once (memoized by node id), contributing pC(a)p_C(a) or 1−pC(a)1-p_C(a) at literal nodes, 00 or 11 at constants, and ∑i(primei)⋅(subi) _i WMC( prime_i)· WMC( sub_i) at decision nodes. Determinism makes each sum disjoint and decomposability makes each product over disjoint variable scopes, so (α,p,) WMC(α;p,e) is exact and runs in O(|α|)O(|α|) time. Each per-node operation is differentiable in the literal weights, and PyTorch autograd composes the backward pass through the same traversal in O(|α|)O(|α|) additional time. (b) Conditional posterior. The ratio Pθ(C(a)∣,)=(α;pθ(),∪C(a):=)/(α;pθ(),)P_θ(C(a) ,e)= WMC(α;p_θ(x),e∪\C(a):= true\)/ WMC(α;p_θ(x),e) is two applications of (a), each O(|α|)O(|α|). The denominator is strictly positive whenever e is consistent with O. (c) Entailment query. Setting p≡12p≡ 12 gives the uniform prior; conditioning on ∪C(a):=e∪\C(a):= false\ clamps the corresponding literal. By Theorem 0.D.1 the SDD’s models are exactly the finite-domain interpretations satisfying the entailed clauses, so (α;12,∪C(a):=)=0 WMC(α; 12,e∪\C(a):= false\)=0 iff no model of α has C(a)=C(a)= false, iff ∪⊧C(a)O C(a). The check is one WMC call, O(|α|)O(|α|). (d) Training step. The loss L(θ,,)=−log(α,pθ(),)L(θ;x,e)=- WMC(α;p_θ(x),e) is one WMC call, O(|α|)O(|α|). Its gradient with respect to θ is computed by autograd through the WMC traversal (cost O(|α|)O(|α|)) followed by the perception backbone’s backward pass (cost equal to the forward pass of fθf_θ). Total: O(|α|)+O(cost of fθ())O(|α|)+O(cost of f_θ(x)). ∎ 0.D.7 Structural circuit properties We define three structural properties used to characterize the tractability of weighted model counting on a circuit [21]. A circuit over variables V is a rooted directed acyclic graph whose leaves are literals over V (or the constants ⊤ / ⊥ ), and whose internal nodes are either product nodes (⋀ , evaluating to the conjunction of their children) or sum nodes (⋁ , evaluating to the disjunction of their children). Let φ be such a circuit; the scope of a node is the set of variables appearing in the subcircuit rooted at it, and the support is the set of total assignments to V on which the node evaluates to a non-zero value. Definition 2 (Decomposability) A circuit is decomposable if at every product node the scopes of its children are pairwise disjoint. Definition 3 (Determinism) A circuit is deterministic if at every sum node the children have pairwise disjoint supports. Definition 4 (Smoothness) A circuit is smooth if at every sum node all children share the same scope. A Sentential Decision Diagram (SDD) is a circuit whose internal nodes are decision nodes of the form (p1,s1)∨⋯∨(pk,sk)(p_1,s_1) … (p_k,s_k), abbreviating ⋁i(pi∧si) _i(p_i s_i); each pip_i (the prime) and sis_i (the sub) are themselves SDDs over disjoint variable sets fixed by a v-tree, with the prime ranging over the variables of the left subtree and the sub over those of the right [20, 17]. This prime/sub decomposition realizes all three structural properties above by construction: every prime pip_i has scope disjoint from its corresponding sub sis_i (decomposability), the primes are pairwise inconsistent (determinism), and they cover the input space allotted to the node by its v-tree (smoothness) [20, 17]. Together, these properties make WMC linear in |α||α| and reduce conditioning, marginalization, and MAP inference to circuit traversals [21]. 0.D.8 Compositional SCC factorization lemmas (Theorems 4.3 and 4.4) The following lemmas establish the SCC factorization formalized in Lean: an arbitrary two-component partition of an ontology, =1∪2O=O_1 _2, with disjoint atom and role signatures, factors the closure exactly, modulo a single “global inconsistency” disjunct that captures the case where 2O_2 alone derives ⊤⊑⊥ (which then propagates to all of 1∪2O_1 _2 via the R⊥R_ rule, regardless of 1O_1). This is what allows the algorithm to compile per-SCC SDDs and combine them, rather than compiling one monolithic SDD over the union. Lemma 1 (Semantic SCC factorization) Let O1,O2O_1,O_2 be ℰℒ++EL^++ ontologies (finite sets of GCIs, role inclusions, and role chains). Let atoms(Oi)⊆Catoms(O_i) Sig_C and roles(Oi)⊆Rroles(O_i) Sig_R denote the sets of atomic concept names and role names appearing in axioms of OiO_i. Assume signature disjointness: atoms(O1)∩atoms(O2)=∅,roles(O1)∩roles(O2)=∅.atoms(O_1) (O_2)= , (O_1) (O_2)= . Then for every pair of ℰℒ++EL^++ concepts C,DC,D whose atom and role names lie entirely in O1O_1’s signature (atoms(C)∪atoms(D)⊆atoms(O1)(atoms(C) (D) (O_1) and roles(C)∪roles(D)⊆roles(O1)),roles(C) (D) (O_1)), the closure factors as (O1∪O2)C⊑D⇔(O1)C⊑D∨(O2)⊤⊑⊥. Sat(O_1∪ O_2)\;C D\;\; \;\; Sat(O_1)\;C D\; \; Sat(O_2)\; . (10) The statement holds for the nominal-free, range-chain-safe fragment of full OWL 2 EL (ℰℒ++EL^++ minus concrete domains): both O1O_1 and O2O_2 are nominal-free, both satisfy the range-chain safety condition ELKSDD.ELpp.RangeChainSafe (range axioms are forbidden on the rinc-ancestors of any role-chain target, so that range-guards transfer vacuously through chain composition; [26] §3.3), and C,DC,D are nominal-free. No restriction on ⊤ - or ⊥ -axioms is imposed on either side. OWL 2 EL nominals (ObjectOneOf singleton classes) are supported by the algorithm at the axiom level (normal forms NFnomR “A⊑aA \a\” and NFnomL “a⊑B\a\ B”) and at the concept level (Concept.nom, Interp.indiv, conceptIndividuals, ontologyIndividuals) in our Lean implementation. The proof of Lemma 1 below covers the nominal-free fragment. Shape 1 nominals (ABox-style ClassAssertion axioms a⊑D\a\ D with D nominal-free) are formalized by the relaxed ELKSDD.ELpp.Sat_factor_nomLHS theorem, under the OntologyNomLHS precondition (which permits LHS-nominal GCIs on the analyzed side O1O_1) and AllNomInhabited (every nominal index is consistent). The key observation is that an LHS-nominal a\a\ pins the prodInterp evaluation to the specific point ⟨ℐ1.indiv(a),b0⟩ _1. indiv(a),b_0 , so no general nominal-evaluation lemma is needed: the existing P2 (which is already general in the second coordinate) is applied at b=b0b=b_0. Shapes 2/4 (RHS nominal: A⊑aA \a\ or a⊑b\a\ \b\) and HasKey are handled by the merging canonical-model construction [26] (concept equivalence classes through nominals), fully mechanized in namespace ELKSDD.ELpp under the Shallow concept restriction of [26, §6]. The Sat-level SCC factorization theorem in this lemma is currently stated only for the nominal-free and LHS-nominal cases; lifting the WMC factorization to the merge fragment is a straightforward composition of ELKSDD.SCC.Sat_factor_refined with ELKSDD.ELpp.complete_via_mergedCanon_regular. Proof (Proof outline (full proof: ELKSDD.SCC.Sat_factor_refined)) The (⇐)( ) direction is monotonicity of Sat in the ontology, plus the R⊥R_ rule when the second disjunct holds. For (⇒)( ) we may assume ¬(O2)⊤⊑⊥ Sat(O_2)\; (else the second disjunct is immediate), so the canonical (term) model ℐcan(O2)I^can(O_2) of Theorem 0.D.1 is non-empty. Given an arbitrary ℐ1⊧O1I_1 O_1 on Δ1 _1, build the product interpretation ℐ′I on Δ1×ℐcan(O2) _1×I^can(O_2) that evaluates O1O_1-signature atoms and roles on the first coordinate and O2O_2-signature ones on the second. Signature disjointness (Disj) lets the evaluation of any OiO_i-signature concept factor cleanly through the corresponding component (Lean: eval_prodInterp_O1, eval_prodInterp_O2), which in turn gives ℐ′⊧O1∪O2I O_1∪ O_2 (prodInterp_satisfies). By ELK soundness on the union, ℐ′⊧C⊑DI C D; factoring back through the first coordinate at the basepoint ⟨a,x⊤⟩ a,x_ yields ℐ1⊧C⊑DI_1 C D. Since ℐ1I_1 was arbitrary, ELK completeness on O1O_1 closes the left-hand disjunct. ∎ Lemma 2 (Per-world Sat factorization) Let O=O1∪O2O=O_1∪ O_2 satisfy the signature-disjointness, nominal-free, and range-chain-safe preconditions of Lemma 1, and additionally assume O2O_2 consistent (¬(O2,⊤,⊥) \, Sat(O_2, , )). For every Boolean world M:O→M:O , write M1=M↾O1M_1=M O_1 and let sel(O,M):=α∈O:M(α)= sel(O,M):=\α∈ O:M(α)= true\ denote the sub-ontology selected by M. For nominal-free C,DC,D in O1O_1’s signature, (sel(O,M))C⊑D⇔(sel(O1,M1))C⊑D. Sat ( sel(O,M) )\;C D\;\; \;\; Sat ( sel(O_1,M_1) )\;C D. That is, Sat-derivability of C⊑DC D at world M factors through the O1O_1-restriction of M alone. Proof Two steps. (i) sel(O,M) sel(O,M) and sel(O1,M1)∪sel(O2,M2) sel(O_1,M_1)∪ sel(O_2,M_2) are equal as ontologies (each axiom α∈O=O1⊎O2α∈ O=O_1 O_2 lies in exactly one side and contributes to the corresponding selected sub-ontology by the same Boolean choice M(α)M(α)). Bidirectional sub-ontology inclusions yield Sat equivalence by monotonicity of Sat in the ontology (Sat_mono); the Lean witnesses are ELKSDD.ELpp.selectedAxioms_sub_decompose and decompose_sub_selectedAxioms. (i) Apply Lemma 1 in the generalized form ELKSDD.ELpp.Sat_factor_refined_general, which uses O1,O2O_1,O_2 as signature-defining outer ontologies while permitting the analyzed sides sel(O1,M1) sel(O_1,M_1) and sel(O2,M2) sel(O_2,M_2) to be sub-ontologies thereof. sel(O2,M2) sel(O_2,M_2) is consistent because it is a sub-ontology of the consistent O2O_2, so the right disjunct of Lemma 1 vanishes, leaving the clean factorization through O1O_1. See ELKSDD.ELpp.per_world_sat_factor_consistent. ∎ Lemma 3 (Closed-form WMC SCC factorization under uniform priors) Under the hypotheses of Lemma 2 (signature-disjoint, nominal-free, range-chain-safe O1,O2O_1,O_2 with O2O_2 consistent), for the rational DISPONTE marginal under the uniform per-axiom weight w≡1w≡ 1, wmcℚ(O1∪O2,C,D,w)=wmcℚ(O1,C,D,w)⋅2|O2|. wmc^Q(O_1∪ O_2,\,C,D,\,w)\;=\; wmc^Q(O_1,\,C,D,\,w)· 2^|O_2|. Proof By definition, wmcℚ(O,C,D,w):=∑M:O→[(sel(O,M))C⊑D]⋅worldWeight(M,w), wmc^Q(O,C,D,w)\;:=\; _M:O [ Sat( sel(O,M))\;C D ]· worldWeight(M,w), where the world weight is ∏α∈Ow(α,M(α)) _α∈ Ow(α,M(α)). Three steps. (a) Under w≡1w≡ 1, worldWeight(M,w)=1 worldWeight(M,w)=1 for every M (Lean: worldWeightRat_uniform). (b) By Lemma 2, the indicator depends on M only through M1=M↾O1M_1=M O_1. (c) The sum over M:O1⊎O2→M:O_1 O_2 of any function depending only on M↾O1M O_1 factorizes as ∑M1:O1→f(M1)⋅2|O2| _M_1:O_1 f(M_1)· 2^|O_2|. Step (c) is a combinatorial identity proved by induction on |O2||O_2| over the flatMap structure of the world enumeration (ELKSDD.ELpp.sum_enumerateWorlds_factor); combining (a)–(c) yields the displayed equation. The closed-form Lean theorem is ELKSDD.ELpp.disponteWMCRat_uniform_scc_factor, audit-clean with dependencies only on [propext, Classical.choice, Quot.sound]. ∎ Lemma 4 (Distribution-semantics correspondence (rational form)) For every ℰℒ++EL^++ ontology O, every concept pair (C,D)(C,D), and every per-axiom weight function w:DispAtom(O)×→ℚw: DispAtom(O)×B , wmcℚ(compile(O,C,D),w)=wmcℚ(O,C,D,w), wmc^Q ( compile(O,C,D);\,w )\;=\; wmc^Q(O,\,C,D,\,w), where the LHS is the SDD-level WMC of the verified compiled circuit compileSat and the RHS is the rational DISPONTE distribution-semantics marginal. No restriction on w is imposed (in particular, no probabilistic normalization of w). Proof By Shannon-decomposition correctness of SDD compilation, the LHS equals the sum over all axiom-extensions of [(sel(O,M))C⊑D]⋅weightAlong(M,w)[ Sat( sel(O,M))\;C D]· weightAlong(M,w). The RHS is the same sum indexed by worlds. The two index sets coincide as multisets (a routine permutation lemma), and permutation-invariance of ∑Σ over ℚQ closes the equality. This is the unconditional form: no distributional assumption is required; the entire Riguzzi 2015 distribution-semantics construction is internalized inside the SDD-WMC. Mechanized as ELKSDD.ELpp.wmc_compileSat_eq_disponteWMC_rat (Table 6). ∎ 0.D.9 DeepProbLog equivalence on the EL Horn theory We tighten the informal claim of §5.3 that Moose on ΓEL _ EL alone “yields the loss DeepProbLog [39] would minimize on the same Horn instance” into a formal proposition and a Lean 4 encoding in namespace Moose (the Lean identifiers retain the historical no_clos suffix as code artefacts). Setup. Let O be an ℰℒ++EL^++ ontology, Δ a finite ABox domain, and let ΓEL=AtomSub∪Disj∪Unsat∪Links _ EL= AtomSub∪ Disj∪ Unsat∪ Links be the ground clause set produced by the four Moose extractors after ELK saturation (Algorithm 1 of Appendix 0.C, before SDDCompile). Let αEL=SDDCompile(ΓEL) _ EL= SDDCompile( _ EL), let fθ:|Δ|→[0,1]|Δ|f_θ:X^| |→[0,1]^|V_O | be a perception model assigning probability pθ(ℓ)p_θ( ) to each positive ground literal (and weight 1−pθ(ℓ)1-p_θ( ) to its negation), and let e be an evidence set of literals. Translation (ΓEL)P( _ EL) to a ProbLog program. The translation maps Moose’s three Horn shapes plus the one non-Horn shape into the three native ProbLog constructs: 1. Each ground atom A(a)∈ΔA(a) _O becomes a probabilistic fact pθ(A(a))::A(a)p_θ(A(a))::A(a). 2. Each definite Horn clause ¬B1∨⋯∨¬Bk∨H∈ΓEL B_1 … B_k H∈ _ EL (AtomSub, Unsat, and Links shapes) becomes a Datalog rule H:-B1,…,BkH\, |:-|\,B_1,…,B_k. 3. Each non-Horn atomic-disjointness clause ¬A1∨⋯∨¬An A_1 … A_n (Disj shape) becomes a ProbLog integrity constraint :-A1,…,An |:-|\,A_1,…,A_n. Loss objects. LMoose/EL(θ,,):=−log(αEL,pθ(),)L_ Moose/ EL(θ;x,e):=- WMC( _ EL;p_θ(x),e) is the Semantic-loss WMC objective of §3.4 on the EL theory alone (no closure axioms); LDPL(θ,,):=−logPDPL(∣;θ)L_DPL(θ;x,e):=- P_DPL(e ;θ) is the DeepProbLog marginal loss [39] on (ΓEL)P( _ EL) under the ProbLog distribution semantics. Proposition 1 (DeepProbLog equivalence on the EL Horn theory) For every (,)(x,e) consistent with O, LMoose/EL(θ,,)=LDPL(θ,,),L_ Moose/ EL(θ;x,e)\;=\;L_DPL(θ;x,e), as values (in any commutative semiring carrying the literal weights) and as gradients in θ. The Lean mechanization instantiates the semiring at ℕN (the type of ELKSDD.SDD.wmc); the same induction is semiring-polymorphic and lifts to ℝ≥0R_≥ 0 used in the Manhaeve 2018 real-valued marginal (paragraph (B) below). Proof (Proof outline (full proof: Moose.moose_no_clos_dpl_equiv and ..._quantitative).) Both losses equal −log(ΓEL∪,wθ())- WMC( _ EL ;\,w_θ(x)), with wθw_θ assigning pθ(ℓ)p_θ( ) to positive literals and 1−pθ(ℓ)1-p_θ( ) to negative ones. SDD compilation preserves the model set, so (αEL,⋅)=(ΓEL,⋅) WMC( _ EL;·)= WMC( _ EL;·) [21, 17]. The translation (ΓEL)P( _ EL) defined above is shape-by-shape purely syntactic: a definite Horn rule, an atomic-disjointness integrity constraint, and a probabilistic fact each have the same satisfying assignments as the clause they came from, so M⊧ΓEL⇔M⊧(ΓEL)M _ EL M ( _ EL). The DeepProbLog distribution semantics then coincides with WMC by [39, Eq. 4]: each total assignment over the probabilistic facts is weighted by ∏apθ(a)M(a)(1−pθ(a))1−M(a) _ap_θ(a)^M(a)(1-p_θ(a))^1-M(a) exactly when it satisfies every rule and integrity constraint, which is the WMC weight of M. Equality of the losses as functions of θ implies equality of their gradients, and of any other operator respecting functional equality. ∎ Lean encoding. The argument is mechanized in namespace Moose at two levels. At the qualitative level (moose_no_clos_dpl_equiv), both losses unfold to the same model-existence predicate ∃M.M⊧ΓEL∧support(M)⊆support(w)∃ M.\,M _ EL (M) (w) and the equivalence closes by definitional unfolding (Iff.rfl) once the ProbLog translation is recognized as the identity on List Clause. At the quantitative level (moose_no_clos_dpl_equiv_quantitative), the equality is lifted from a proposition to a numeric identity wmcQOΔw=dplLossQOΔw wmcQ\,O\, \,w= dplLossQ\,O\, \,w via the key lemma wmc_compileWithCtx_eq_modelSum, which proves by structural induction on the variable list that the SDD weighted-model count equals the explicit Manhaeve-Eq. 4 sum-over-models computed by Shannon decomposition. The proof is semiring-polymorphic; the Lean library instantiates the weighted-model-count semiring at ℕN to keep the formalization free of a real-arithmetic dependency, while the same induction lifts verbatim to the ℝ≥0R_≥ 0 semiring of the original Manhaeve 2018 marginal. Gradient equality is a corollary (moose_no_clos_dpl_loss_function_eq, ..._operator_invariant): any operator respecting functional equality (differentiation, integration, point evaluation, PyTorch autograd) returns the same answer on both sides. Reading. Proposition 1 pins Moose’s contribution to the EL-to-Horn compilation algorithm (Theorems 4.1 and 0.D.2): given O in ℰℒ++EL^++, the algorithm produces in time polynomial in |||O| the ground Horn instance ΓEL _ EL on which Semantic-loss WMC and the DeepProbLog loss coincide, lifting DeepProbLog to OWL 2 EL with existentials, role hierarchy, and role chains. The closure-augmented variant adds the disjointness, covering, and reverse-implication clauses of Φclos _ clos on top of ΓEL _ EL. The content of these clauses is independent of ℰℒ++EL^++ entailment, and the DeepProbLog baseline correspondingly shows a higher RS-consistency rate (RScons_cons, the rate of confident wrong commitments) than closure-augmented Moose across Tables 2 and 3. 0.D.10 Lean mechanization: theorem index The Lean 4 library ELKSDD (introduced in Appendix 0.A) formalizes every Moose-cited theorem of the OWL 2 EL stack; the companion library Moose houses the DeepProbLog-equivalence layer. Table 6 cross-references each paper claim with its namespace-qualified Lean theorem. Every theorem listed depends only on the standard Lean foundation [propext, Classical.choice, Quot.sound] (audit-clean), and the formalization contains zero sorry or admit. An audit pass in each library runs #print axioms on every paper-cited theorem at build time and reports its dependency set. Table 6: Lean implementation index, namespace-qualified. Theorems are reported as <namespace>.<theorem>; the bulk live in ELKSDD.ELpp, with ELKSDD.SDD for the SDD calculus, ELKSDD.RangeNorm for the BBL 2008 path, and Moose for the DeepProbLog equivalence. Every listed theorem is audit-clean: #print axioms reports [propext, Classical.choice, Quot.sound] only, no Moose-specific axioms, no sorry, no admit. Each theorem stated in §4 corresponds to exactly one Lean theorem (top section); supporting lemmas, the closed-form WMC SCC factor under uniform priors (Theorem 4.4), and the LHS-nominal extension are listed in the per-topic sections that follow. Paper claim Lean theorem Section 4 (correctness and complexity): one Lean theorem per stated theorem Verified SDD encoding (Theorem 4.1) ELKSDD.ELpp.moose_inference_correct models iff Sat ELKSDD.ELpp.compileSat_models_iff_sat size =2||+1−1=2^|O|+1-1 ELKSDD.ELpp.compileSat_size_eq DISPONTE correspondence (Theorem 4.2) ELKSDD.ELpp.wmc_compileSat_eq_disponteWMC_rat SCC compositional, Sat (Theorem 4.3) ELKSDD.ELpp.scc_sat_factor SCC compositional, WMC uniform (Theorem 4.4) ELKSDD.ELpp.disponteWMCRat_uniform_scc_factor Reused ELK infrastructure (Section 0.D.1; mechanized from [26]) ELK soundness/completeness (Theorem 0.D.1) ELKSDD.ELpp.correct_owl2el soundness (unconditional) ELKSDD.ELpp.sound_owl2el completeness (with fragment witness) ELKSDD.ELpp.complete_owl2el Polynomial Sat decision (Theorem 0.D.2) ELKSDD.ELpp.sat_decision_polynomial exact closure-size bound ELKSDD.ELpp.sat_closure_total_polynomial_bound Closure-augmented circuit and inference complexity (appendix) Closure-augmented (Theorem 0.D.3) ELKSDD.SDD.compile_correct Inference complexity (Theorem 0.D.4) ELKSDD.SDD.wmc_linear, ELKSDD.ELpp.compileSat_wmcCost_eq Compositional and distributional results: supporting lemmas SCC Sat factor, sig-disjoint ELKSDD.SCC.Sat_factor_refined closed form (O2O_2 consistent) ELKSDD.ELpp.scc_sat_factor, ELKSDD.ELpp.scc_sat_factor_symm sub-ontology generalization ELKSDD.ELpp.Sat_factor_refined_general k-component generalization ELKSDD.ELpp.scc_sat_factor_k, ELKSDD.ELpp.joint_consistent_pair Per-world Sat factor (Lemma 2) ELKSDD.ELpp.per_world_sat_factor_consistent selectedAxioms decomposition ELKSDD.ELpp.selectedAxioms_sub_decompose World-summation factorization ELKSDD.ELpp.sum_enumerateWorlds_factor length-cast generalization ELKSDD.ELpp.sum_enumerateWorlds_factor_general WMC SCC factor (uniform, Lemma 3) ELKSDD.ELpp.disponteWMCRat_uniform_scc_factor DISPONTE corresp. (ℕN-valued) ELKSDD.ELpp.wmc_compileSat_eq_disponteWMC DISPONTE corresp. (ℚQ, Lemma 4) ELKSDD.ELpp.wmc_compileSat_eq_disponteWMC_rat existence form ELKSDD.ELpp.exists_disponte_correspondence_rat Nominal-aware SCC (LHS shape 1) ELKSDD.ELpp.Sat_factor_nomLHS, ELKSDD.ELpp.scc_sat_factor_nomLHS prodInterp on LHS-nominal axioms ELKSDD.ELpp.prodInterp_satisfies_nomLHS ELK calculus (Kazakov, Krötzsch, Simančík 2014) ELK soundness ELKSDD.EL.sound, ELKSDD.ELpp.sound ELK completeness (nom-free) ELKSDD.ELpp.complete_via_canon LHS-nominal extension ELKSDD.ELpp.complete_via_canon_nomLHS Canonical model ⊧ O (nom-free) ELKSDD.ELpp.canon_satisfies LHS-nominal extension ELKSDD.ELpp.canon_satisfies_nomLHS shallow-∃-nom-RHS extension ELKSDD.ELpp.canon_satisfies_nomLR Saturation termination ELKSDD.ELpp.saturation_terminates Sat ⇔ derivable closure ELKSDD.ELpp.sat_iff_in_derivableClosure Poly-time Sat decision ELKSDD.ELpp.sat_polynomial_decidable Bounded Sat closure size ELKSDD.ELpp.sat_closure_total_polynomial_bound SDD calculus (Darwiche 2002, Choi–Darwiche 2013) SDD compile-correctness ELKSDD.SDD.compile_correct, ELKSDD.SDD.compileWithCtx_correct SDD WMC linearity ELKSDD.SDD.wmc_linear, ELKSDD.SDD.wmcCost_eq_size MOOSE pipeline (paper-citation theorems) Inference correctness ELKSDD.ELpp.moose_inference_correct Pipeline completeness ELKSDD.ELpp.moose_pipeline_complete Polynomial Sat decision (algorithmic) ELKSDD.ELpp.sat_decision_polynomial SCC summary ELKSDD.ELpp.moose_scc_summary SCC, chain-free corollary ELKSDD.ELpp.scc_sat_factor_no_chain SCC, range-free corollary ELKSDD.ELpp.scc_sat_factor_no_range Syntactic range-elimination [6] §3.3 (Path B) Syntactic range-elimination ELKSDD.RangeNorm.eliminateRanges strict-output preservation ELKSDD.RangeNorm.eliminateRanges_strict NoRange degenerate baseline ELKSDD.RangeNorm.eliminateRanges_eq_under_no_range rinc closure (bounded fixed point) ELKSDD.RangeNorm.rincDescendants transitive reflexive-rinc propagation ELKSDD.RangeNorm.reflexiveTransitiveAxioms Forward Sat-conservativity (full) ELKSDD.RangeNorm.Sat_to_eliminated_full transitive marker membership ELKSDD.RangeNorm.reflexiveTransitive_axiom_… DeepProbLog equivalence (Manhaeve 2018, Riguzzi 2015) Qualitative (Proposition 1) Moose.moose_no_clos_dpl_equiv Quantitative (ℕN-valued) Moose.moose_no_clos_dpl_equiv_quantitative WMC == model sum (BoolAtom) Moose.wmc_compileWithCtx_eq_modelSum Appendix 0.E Inference, training, and RS-mitigation wrappers This appendix gives the explicit inference equations of §3.4 (Section 0.E.1), the gradient flow used at training time (Section 0.E.2), and the Moose+BEARS / Moose+NeSyDM wrapper losses used in the RS-aware experiments (Section 0.E.3). 0.E.1 Inference equations The differentiable WMC layer supports three inference operations on the same SDD α, varying only literal weights and evidence. Training loss. For (,)(x,e), L(θ,,)=−log(α,pθ(),).L(θ;x,e)\;=\;- WMC\! (α;\,p_θ(x),\,e ). (11) The literal-weight map (Table 1) sets w(ℓ):=pθ(ℓ)w( ):=p_θ( ) on positive ground literals ℓ∈Δ _O and w(¬ℓ):=1−pθ(ℓ)w( ):=1-p_θ( ) on negative ones; evidence literals ℓ∈ clamp the negation weight to zero (equivalent to conditioning the SDD on ℓ ). Conditional posterior at test time. For a query atom C(a)C(a), Pθ(C(a)∣,)=(α;pθ(),∪C(a):=)(α,pθ(),);P_θ(C(a) ,e)\;=\; WMC\! (α;\,p_θ(x),\,e∪\C(a):= true\ ) WMC\! (α;\,p_θ(x),\,e ); (12) the latent-class prediction on a closed family D is the argmax D^(a):=argmaxDi∈Pθ(Di(a)∣,) D(a):= _D_i P_θ(D_i(a) ,e). The denominator is strictly positive whenever e is consistent with O, so the ratio is well defined. Perception-free entailment query. ∪⊧C(a)⟺(α;w1/2,∪C(a):=)=0,O C(a)\; \; WMC\! (α;\,w_1/2,\,e∪\C(a):= false\ )=0, (13) where w1/2w_1/2 assigns 12 12 to every literal: asserting ¬C(a) C(a) leaves no O-consistent assignment iff the entailment holds. The same SDD acts as an off-line ELK reasoner over Δ , independent of any neural model. All three operations run in O(|α|)O(|α|) (Theorem 0.D.4). 0.E.2 Training step and gradient flow A single training step on minibatch (i,i)i\(x_i,e_i)\_i proceeds as follows. 1. Perception forward. The neural extractor fθ:|Δ|→[0,1]|Δ|f_θ:X^| |→[0,1]^|V_O | maps the input tuple to a per-atom probability vector pθ(i)p_θ(x_i), factorized as ∏ℓpθ(ℓ∣i) _ p_θ( _i) (the marginal-independence factorization targeted by the RS literature, §2.2). 2. Literal-weight assignment. The atom-weight map of Table 1 routes pθ(ℓ∣i)p_θ( _i) to literal ℓ and 1−pθ(ℓ∣i)1-p_θ( _i) to ¬ℓ . Evidence ie_i clamps observed literals. 3. SDD WMC traversal. The post-order traversal visits each node once (memoized by node id) and accumulates the WMC value (Equation 8) in O(|α|)O(|α|) time. Smoothness, decomposability, and determinism (Appendix 0.D) make each sum disjoint and each product over disjoint scopes, so the result is exact. 4. Loss aggregation. L(θ)=−1n∑ilog(α;pθ(i),i)L(θ)=- 1n _i WMC(α;p_θ(x_i),e_i). 5. Backward pass. PyTorch autograd composes the backward pass through the same WMC traversal at O(|α|)O(|α|) additional cost, plus the perception backbone’s own backward pass. Every intermediate WMC value is the product/sum of literal weights, hence differentiable in θ via the chain rule: ∇θL=−1n∑i(i)−1∇θi _θL=- 1n _i( WMC_i)^-1\, _θ WMC_i. No Monte-Carlo or sampling step is required; the gradient is computed exactly. This exact-gradient property is what makes the SDD a tractable surrogate for the ProbLog marginal that DeepProbLog approximates by proof-tree enumeration (Proposition 1). 0.E.3 RS-mitigation wrapper losses The compilation algorithm of §3.2 is independent of the perception’s output distribution: α depends only on (,Δ)(O, ), so RS-aware methods plug in by replacing the literal weights pθ()p_θ(x) in Equation 11 without modifying α or the WMC traversal. Moose+BEARS [40]. BEARS [40] trains a K-encoder ensemble θkk=1K\ _k\_k=1^K that shares α but diversifies over the RS equivalence class. Members are trained sequentially: at step k, the new encoder θk _k is fit by maximizing the BEARS objective [40, Eq. 7] LBears(θk;,)=L(θk;,)+γ1KL(pθk∥1k∑j=1kpθj)+γ2H(pθk),L_ Bears( _k;x,e)\;=\;L( _k;x,e)\,+\, _1\,KL\! (p_ _k\, \|\, 1k _j=1^kp_ _j )\,+\, _2\,H(p_ _k), (14) where the KL term against the running average over members 1,…,k1,…,k encourages θk _k to commit to a different shortcut than its predecessors, and the entropy term H(pθk)H(p_ _k) prevents collapse to a degenerate posterior. At test time, the ensemble averages the per-atom marginals: p(ℓ∣)=1K∑kpθk(ℓ∣)p( )= 1K _kp_ _k( ), spreading mass across multiple shortcut explanations. We use K=5K=5, entropy weight γ2=0.1 _2=0.1, and per-regime tuning of the KL weight γ1 _1 (Section 0.F.4). Moose+NeSyDM [30]. NeSyDM [30] replaces the marginal-independence factorization pθ(∣)=∏ipθ(ci∣)p_θ(c )= _ip_θ(c_i ) with a masked-discrete-diffusion variational distribution qθ(∣)q_θ(c ) that models cross-atom dependencies through a denoising trajectory over T timesteps. The continuous-time negative evidence lower bound (NELBO) objective is ℒNeSyDM(θ)=qθ[−log(α,qθ(),)]+γcℒc(θ)+γhℒh(θ),L_NeSyDM(θ)\;=\;E_q_θ\! [- WMC(α;q_θ(x),e) ]\;+\; _c\,L_c(θ)\;+\; _h\,L_h(θ), (15) where ℒcL_c is the masked-diffusion concept-unmasking loss LcL_c of [30, §3.2] and ℒhL_h the variational-entropy term LH[q]L_H[q] that maximizes the entropy of qθq_θ at the fully-masked step. The expectation under qθq_θ is intractable in closed form; we use two gradient estimators: (a) RLOO [28], a leave-one-out REINFORCE baseline that draws S samples from qθq_θ and uses the sample average over the other S−1S-1 as the control variate; (b) exact-WMC, which replaces sampling by direct WMC evaluation −log(α,q¯θ,)- WMC(α; q_θ,e) on the average per-atom marginal q¯θ q_θ when the diffusion-step posterior factorizes across atoms. We use the NeSyDM-repository defaults β=10β=10 and T=10T=10 continuous-time mask budget; (γc,γh)( _c, _h) are swept per regime (Section 0.F.4). Both wrappers share α across all encoders/timesteps and inherit the O(|α|)O(|α|) inference cost of Theorem 0.D.4, multiplied by K for BEARS or by the diffusion budget T⋅ST· S for NeSyDM. 0.E.4 Non-WMC baselines LTN and ELEmbeddings replace exact WMC over the compiled SDD with, respectively, a fuzzy-logic satisfaction objective and a geometric embedding loss. Both consume the same atom vocabulary and per-example domain as the WMC-based methods (the same circuit atoms drive the losses), so the only thing varying across baselines is the symbolic treatment. LTN [7]. Each ℰℒ++EL^++ axiom is grounded into a first-order formula over the per-example domain (a\a\ for Exp. 1 / Track A–C, a,b\a,b\ for Exps. 2–3) and scored under the product (Goguen) t-norm with Reichenbach implication (a∧b=aba b=ab, a∨b=a+b−aba b=a+b-ab, a→b=1−a+aba→ b=1-a+ab). The translations used are C⊑D↦∀x.C(x)→D(x)C D ∀ x.\,C(x)→ D(x), C⊓D⊑E↦∀x.C(x)∧D(x)→E(x)C D E ∀ x.\,C(x) D(x)→ E(x), C⊑∃R.D↦∀x.C(x)→∃y.R(x,y)∧D(y)C ∃ R.D ∀ x.\,C(x)→∃ y.\,R(x,y) D(y), and the symmetric variants for ∃R.C⊑D∃ R.C D, C⊓D⊑⊥C D , R⊑SR S, and R1∘R2⊑SR_1 R_2 S. Per-atom truth values come from the same perception output that the WMC baselines use; ∀ and ∃ are aggregated by the generalized mean p_mean(v1,…,vn)=(1n∑ivip)1/p p\_mean(v_1,…,v_n)=( 1n _iv_i^p)^1/p with sweepable exponent p∈2,4p∈\2,4\ (Section 0.F.4). The training loss is 1−SAT1-SAT where SATSAT is the satisfaction aggregator across all axiom-grounded formulas. LTN does not compute an exact joint distribution over ground atoms. ELEmbeddings [36, 54]. The same ℰℒ++EL^++ geometric encoding underlies DeepGO-SE [34], where ELEmbeddings approximate semantic entailment for protein-function prediction over the Gene Ontology; our use of ELEmbeddings here adopts the same NF1–NF4 losses but attaches them to the Moose perception backbone rather than a sequence encoder. Each named concept C is embedded as an n-ball with centre cC∈ℝdc_C ^d and radius rCr_C; each role R as a translation vector ρR∈ℝd _R ^d. A linear head projects the perception’s CNN latent ψ()∈ℝ128ψ(x) ^128 into the same ℝdR^d space, yielding a per-individual point zaz_a. The class-membership score is P(C(a))=σ(margin−(‖za−cC‖−rC))P(C(a))=σ( margin-(\|z_a-c_C\|-r_C)) (image inside the ball ⇒ atom true) and the role-atom score is P(R(a,b))=σ(margin−‖za+ρR−zb‖)P(R(a,b))=σ( margin-\|z_a+ _R-z_b\|). The TBox loss is the sum of mOWL’s NF1–NF4 losses [36, 54] (mean-aggregated per normal form), and the total objective is ℒ=ℒperception+λELℒTBoxL=L_perception+ _EL\,L_TBox with ℒperceptionL_perception a BCE over observed ABox literals. Vanilla ELEmbeddings has no normal form for role chains, and role chains are ignored for ELEmbeddings. Appendix 0.F Experimental details This part of the appendix collects the materials supporting experiments: the full MNIST ontology used by all three MNIST experiments (Section 0.F.2), per-method hyperparameter sweeps and the tuned configurations used in the result tables (Section 0.F.4), and the full per-regime breakdown across all six metrics (Section 0.F.6). 0.F.1 Compiled-circuit sizes and compilation cost All experiments were run on a single machine with one NVIDIA RTX 4090 GPU and a single CPU core allocated per job. SDD compilation is CPU-only and happens once at start-up; the resulting circuit is reused across every training step, seed, and method, so its size is a deterministic function of the ontology O and the ABox domain Δ alone, not of the learning method. Every Moose variant and every SDD-based baseline in a given regime therefore shares the circuit in the corresponding row of Table 7. Table 7: Compiled-circuit size and per-regime cost. SDD size (nodes, distinct atoms, CNF clauses) is method-independent; compile time is the range observed across all methods, learning rates, and seeds on one CPU core. Compilation finishes in ≤0.75≤ 0.75 s in every configuration, and in ≤0.35≤ 0.35 s in all but the two DeepProbLog cells (0.680.68 s on Exp. 2, 0.710.71 s on Exp. 3). ∗The Exp. 1 row was profiled separately on a CPU-only machine; its structural counts are machine-independent by the argument above, and its compile times are reported as measured there rather than merged into the RTX 4090 column. The last two columns report end-to-end training wall-clock and peak GPU memory during training for a single representative Moose-WMC run per regime (batch size 3232; the MNIST CNN encoder on Exps. 1–3, the larger Pizzaïolo encoder on Tracks A–C); unlike the circuit columns these depend on the backbone, batch size, and epoch budget rather than on the compiled circuit. Regime |Δ|| | SDD nodes atoms clauses compile (s) train (s) peak GPU (MB) MNIST Exp. 1 (atomic)∗ 1 155155 1414 117117 0.180.18–0.240.24 647647 35.335.3 MNIST Exp. 2 (relational) 2 10801080 3030 274274 0.290.29–0.680.68 38933893 56.456.4 MNIST Exp. 3 (role-chain) 2 11531153 3232 314314 0.230.23–0.710.71 44844484 56.456.4 Pizzaïolo Track A 2 245245 2626 103103 0.160.16–0.300.30 516516 903.4903.4 Pizzaïolo Track B 2 245245 2626 107107 0.140.14–0.230.23 507507 903.4903.4 Pizzaïolo Track C 2 1616 66 1010 0.150.15–0.230.23 2626 903.3903.3 Compile time grows with the ABox domain as analyzed in Section 0.D.5: the SDD node count fits ∝|Δ|2.9 | |^2.9 for |Δ|≤3| |≤ 3, with a 40×40× compile-time jump at |Δ|=4| |=4. The |Δ|=2| |=2 configurations used throughout §5 sit well inside the sub-second regime. Peak GPU memory at circuit-build time is 00 in every configuration: compilation is CPU-only and no tensor is allocated on the device before the encoder is moved there. Training cost is dominated by the perception backbone rather than the WMC layer. On the MNIST regimes end-to-end training takes roughly 1111 minutes at |Δ|=1| |=1 (Exp. 1) and 6565–7575 minutes at |Δ|=2| |=2 (Exps. 2–3), with peak GPU memory of 3535–5656 MB; the Pizzaïolo tracks train in under 99 minutes each (Track C, a single binary label, in well under a minute) but use ≈900≈ 900 MB, reflecting the larger image encoder rather than any growth in the circuit (Table 7). Peak memory therefore tracks the backbone and batch size, not the compiled SDD, whose own device footprint is negligible. 0.F.2 Full MNIST ontology The single OWL EL ontology MNISTO_ MNIST used by all three MNIST experiments (§5.1) consists of 7676 axioms over C=D0,…,D9,Even,Odd,Prime,Composite Sig_C=\D_0,…,D_9, Even, Odd, Prime, Composite\ and R=succ,plus_two Sig_R=\ succ, plus\_two\, listed below in EL DL syntax. Numerals 0–9 are read as the corresponding DiD_i. NF1: property subsumptions (1818). D0⊑EvenD_0 Even; D2⊑EvenD_2 Even; D4⊑EvenD_4 Even; D6⊑EvenD_6 Even; D8⊑EvenD_8 Even; D1⊑OddD_1 Odd; D3⊑OddD_3 Odd; D5⊑OddD_5 Odd; D7⊑OddD_7 Odd; D9⊑OddD_9 Odd; D2⊑PrimeD_2 Prime; D3⊑PrimeD_3 Prime; D5⊑PrimeD_5 Prime; D7⊑PrimeD_7 Prime; D4⊑CompositeD_4 Composite; D6⊑CompositeD_6 Composite; D8⊑CompositeD_8 Composite; D9⊑CompositeD_9 Composite. NF2: disjointness (4747). Even⊓Odd⊑⊥ Even Odd ; Prime⊓Composite⊑⊥ Prime Composite ; plus Di⊓Dj⊑⊥D_i D_j for every 0≤i<j≤90≤ i<j≤ 9 ((102)=45 102=45 pairs). NF3: successor existentials (1010). Di⊑∃succ.D(i+1)mod10D_i ∃ succ.\,D_(i+1) 10 for each i∈0,1,…,9i∈\0,1,…,9\. The chain is cyclic (D9⊑∃succ.D0D_9 ∃ succ.\,D_0); without the signature side condition (Appendix 0.C) saturation would diverge. NF7: role chain (11). succ∘succ⊑plus_two succ succ plus\_two. Saturation closure used by the experiments. ELK derives the chain consequence Di⊑∃plus_two.D(i+2)mod10D_i ∃ plus\_two.\,D_(i+2) 10 via the role-composition rule R∘R_ (given Di⊑∃succ.Di+1D_i ∃ succ.D_i+1, Di+1⊑∃succ.Di+2D_i+1 ∃ succ.D_i+2, and succ∘succ⊑plus_two succ succ plus\_two, infer Di⊑∃plus_two.Di+2D_i ∃ plus\_two.D_i+2 [26]) populating Λ with the plus_two links that the role-chain experiment relies on. The four Moose extractors then ground Σ and Λ into the clauses of ΓEL _ EL, and the closure axioms Φclos _ clos over the exhaustive family D0,…,D9\D_0,…,D_9\ supply (102)m+m 102m+m disjointness and covering clauses plus the six reverse clauses per individual (one per distinct parity-primality profile; §3.3). 0.F.3 Perception architecture Both MNIST and Pizzaïolo experiments train the perception encoder from scratch. The MNIST encoder (used in Experiments 1–3) takes a 28×2828×28 grayscale image through two Conv→ → (2×22×2) blocks of 3232 and 6464 channels (3×33×3 kernels, padding 11), flattens to 64⋅7⋅764·7·7 features, and applies a fully-connected layer to a 128128-dim latent followed by a linear head to per-concept logits. The Pizzaïolo encoder (Experiment 4) takes a 224×224224×224 RGB image through four Conv→ → blocks of 3232, 6464, 128128, 128128 channels (3×33×3 kernels, padding 11), then global average pooling to 128128 features and the same 128→128→n_concepts128→ 128 \_concepts head. Per-concept Bernoulli probabilities are obtained by a sigmoid; the same encoder is shared across all named individuals in a training instance. 0.F.4 Hyperparameter selection For every method in the headline tables we ran a single-seed sweep over a small per-method grid, picked the best configuration per regime by RScons_cons and AccdigitAcc_digit on the seed-0 cell, and then ran a 55-seed final at that configuration. All methods share Adam [27] with batch size 3232, 3030 epochs on MNIST and 6060 epochs on Pizzaïolo Tracks A/B (Track C uses 1515 epochs because the binary is_spicy supervision saturates faster), unless otherwise noted. The reported MNIST headline tables in Tables 2 and 3 use 55 seeds at the tuned HPs; the Pizzaïolo tables (Tables 2 and 3) use 55 seeds at the tuned HPs except where indicated. Moose / Semantic-loss WMC. Sweep over lr∈10−3,3⋅10−3lr∈\10^-3,3·10^-3\ per regime. Best: mnist1 / mnist3 / pizzaC use lr=3⋅10−3lr=3·10^-3; mnist2 / pizzaA / pizzaB use lr=10−3lr=10^-3. The SDD compilation is determined by O and Δ , so the only free knob is the perception backbone’s optimiser. A wider-range sensitivity analysis over this knob is in Section 0.F.5. DeepProbLog [39]. Sweep over lr∈10−3,3⋅10−3lr∈\10^-3,3·10^-3\. Both regimes (mnist2, mnist3) prefer lr=10−3lr=10^-3; the n(⋅) n(·) predicate’s softmax matches the latent signature Cℓ Sig _C exactly (one head per concept family); no additional HPs. Moose+BEARS [40]. Ensemble size K=5K=5, entropy weight γ2=0.1 _2=0.1 at the BEARS-paper default; sweep over the KL weight γ1∈0.5,1.0,2.0 _1∈\0.5,1.0,2.0\ on every regime. The MNIST sweep is uniform on γ1=1.0 _1=1.0 (the BEARS-paper default), so the final 5-seed run uses γ1=1.0 _1=1.0 on mnist1, mnist2, mnist3. On Pizzaïolo, γ1 _1 was tuned per track: pizzaA → γ1=1.0 _1=1.0, pizzaB → γ1=2.0 _1=2.0, pizzaC → γ1=1.0 _1=1.0. Moose+NeSyDM [30]. Sweep over (γc,γh)∈0.1,1.0×1.0,2.0( _c, _h)∈\0.1,1.0\×\1.0,2.0\ per regime (44 cells), at the RLOO gradient estimator. β=10β=10 and T=10T=10 (continuous-time mask budget) are the NeSyDM-repository defaults, adopted unchanged. Best per regime: mnist1 → (γc=1.0,γh=2.0)( _c=1.0,\, _h=2.0); mnist2 → (0.1,2.0)(0.1,2.0); mnist3 → (1.0,1.0)(1.0,1.0); pizzaA → (0.1,2.0)(0.1,2.0); pizzaB → (0.1,2.0)(0.1,2.0); pizzaC → (0.1,1.0)(0.1,1.0). LTN [7]. Product T-norm; sweep over the p-mean aggregator exponent forall_p=exists_p∈2,4 forall\_p= exists\_p∈\2,4\ on every regime, and additionally over exists_mode∈universe,skolem exists\_mode∈\ universe, skolem\ on MNIST relational/role-chain. Best: forall_p=4 forall\_p=4 uniformly across all six regimes; exists_mode=universe exists\_mode= universe on mnist2 and mnist3 (skolem produced equivalent or worse AccdigitAcc_digit at single seed). lr=10−3lr=10^-3. ELEmbeddings [36] / mOWL [54]. Sweep over (embed_dim,margin)∈50,128×0.1,0.5( embed\_dim, margin)∈\50,128\×\0.1,0.5\ per regime (44 cells). Best: mnist1 / mnist2 / mnist3 / pizzaB →(embed_dim=50,margin=0.1)→( embed\_dim=50,\, margin=0.1); pizzaA →(128,0.5)→(128,0.5) (best Brier among the four cells; all four reached AccC=1.0Acc_C=1.0 on the in-distribution split). For mnist3 the EL ball loss is augmented with an explicit plus_two role-chain penalty term (vanilla ELEmbeddings has no normal form for role chains; Section 0.E.4). Independent (BCE). Sweep over lr∈3⋅10−4,10−3,3⋅10−3lr∈\3·10^-4,10^-3,3·10^-3\ per MNIST regime. Best: mnist1 / mnist3 use lr=3⋅10−4lr=3·10^-4 (best AccatomAcc_atom + ECE); mnist2 uses lr=3⋅10−3lr=3·10^-3. Per-atom BCE on the observed evidence atoms only; no symbolic structure enters the loss. Summary. The final numbers in Tables 2 and 3 are 55-seed means at the per-regime-tuned hyperparameters above, after a per-method single-seed sweep. 0.F.5 Learning-rate sensitivity The per-method grids above are budget-matched: every method is tuned over a grid of the same size on the same seed-0 protocol, so no method is advantaged by a larger search. Because Moose exposes a single free hyperparameter, the perception backbone’s learning rate, while the SDD compilation has none, we additionally sweep it over a wider five-point grid to check that the headline numbers are not an artifact of a lucky rate. Table 8 reports Moose accuracy at each rate (33 seeds per cell); the metric is AccFAcc_F on MNIST and AccCAcc_C on Pizzaïolo (Section 5.3). Track C is not included in this sweep. Table 8: Moose learning-rate sensitivity (33 seeds per cell, mean ± s.d.). Metric: AccFAcc_F on MNIST Experiments 2–3, AccCAcc_C on Pizzaïolo Tracks A–B. The final row is the across-grid spread (max −- min over all per-seed runs in the grid). Learning rate Exp. 2 Exp. 3 Pizza A Pizza B 10−410^-4 0.729±0.0110.729± 0.011 0.941±0.0550.941± 0.055 0.861±0.0030.861± 0.003 0.810±0.0560.810± 0.056 3⋅10−43·10^-4 0.744±0.0200.744± 0.020 0.943±0.0680.943± 0.068 0.906±0.0000.906± 0.000 0.846±0.0100.846± 0.010 10−310^-3 0.786±0.0300.786± 0.030 0.943±0.0710.943± 0.071 0.948±0.0070.948± 0.007 0.827±0.0150.827± 0.015 3⋅10−33·10^-3 0.772±0.0220.772± 0.022 0.994±0.0010.994± 0.001 0.955±0.0000.955± 0.000 0.786±0.0380.786± 0.038 10−210^-2 0.743±0.0100.743± 0.010 0.880±0.0770.880± 0.077 0.925±0.0420.925± 0.042 0.821±0.0440.821± 0.044 spread (max−-min) 0.1000.100 0.1780.178 0.0960.096 0.1290.129 On MNIST and Pizza A the response is unimodal, with the optimum in the interior of the grid (10−310^-3 or 3⋅10−33·10^-3) and the extreme rates worst, as expected; Pizza B is flatter and less regular, its per-rate means varying little (all within 0.7860.786–0.8460.846) with no clear interior peak. Moose is robust on Exp. 2 and Pizza A (spread ≤0.10≤ 0.10) and more rate-sensitive on Exp. 3 and Pizza B (0.130.13–0.180.18), where the low-rate cells underfit and carry large seed variance. In every regime the tuned rate used for the headline tables sits at or adjacent to the best-performing rate in this grid, so the reported numbers are not a lucky-rate artifact. 0.F.6 Full per-regime results Table 9: Full per-regime results, six metrics. Means ± s.d. over 55 seeds. The third column is AccFAcc_F, family-argmax accuracy, on the MNIST blocks and AccCAcc_C, per-atom accuracy on the latent slice, on the Pizzaïolo blocks, which declare no exhaustive family on Track C (Section 0.F.7); the two are compared only within a block. Operative theory: ΓEL+Φclos _ EL+ _ clos for the Moose rows on MNIST, ΓEL _ EL for every other row (closure is opt-in and unused on Pizzaïolo), and none for Independent. RS=consConf⋅(1−Acc)_cons=Conf·(1-Acc) is the confidence-weighted error rate of that decode: lower is better, and a high value means confident commitment to a wrong latent explanation. F1macroF1_macro is the macro-averaged per-concept F1 on the latent signature. Bold marks the column-best within each block. On Track A the OOD harness records a single accuracy, so the AccatomAcc_atom and AccCAcc_C columns coincide there by construction rather than by coincidence. DeepProbLog‡ rows on Pizzaïolo Tracks A/B are not separate runs: no ProbLog program was written for Pizzaïolo, and the cells reproduce the Moose (Semantic-loss WMC) values, which Proposition 1 shows the translation (ΓEL)P( _ EL) would attain exactly. Note that this translation uses one independent probabilistic fact per ground atom, whereas the MNIST DeepProbLog programs use an n/4 n/4 annotated disjunction over the digit family, so the two halves of the row are different programs. RScons_cons and F1macroF1_macro on Track C (binary is_spicy supervision) collapse to 00 across all methods because the metric is defined over a multi-class concept family; we mark these cells N/A. Pizzaïolo Track A RScons_cons/F1macroF1_macro are computed on the in-distribution eval block (the OOD harness does not record per-atom logits for these metrics). Method Accatom↑Acc_atom\! AccF/C↑Acc_F/C\! NLL↓\! ECE↓\! RScons↓_cons\! F1macro↑F1_macro\! Experiment 1: atomic MNIST (RQ1). |Δ|=1| |=1, NF1/NF2 fragment. Independent (BCE) 58.0 ± 5.6 13.2 ± 7.9 2.9 ± 0.2 9.3 ± 4.5 15.7 ± 3.3 7.6 ± 5.7 DeepProbLog 89.0 ± 0.8 42.1 ± 1.3 1.2 ± 0.1 10.3 ± 0.9 31.3 ± 2.6 31.2 ± 6.9 LTN 92.2 ± 0.1 25.9 ± 6.5 1.1 ± 0.0 10.0 ± 0.0 47.1 ± 7.8 16.1 ± 6.7 ELEmbeddings/mOWL 90.0 ± 0.1 34.9 ± 4.2 0.3 ± 0.0 3.9 ± 0.4 14.9 ± 0.9 25.8 ± 2.8 Moose (Semantic-loss WMC) 89.3 ± 1.8 48.1 ± 10.1 1.6 ± 0.3 10.6 ± 1.8 29.0 ± 4.2 32.1 ± 10.0 Moose+BEARS 91.2 ± 0.9 50.1 ± 5.2 0.3 ± 0.1 3.9 ± 1.0 20.0 ± 1.4 28.0 ± 6.2 Moose+NeSyDM (RLOO) 90.6 ± 0.2 46.6 ± 2.1 0.3 ± 0.0 6.0 ± 0.6 23.2 ± 0.9 35.8 ± 1.9 Moose+NeSyDM (exact) 90.1 ± 1.6 49.4 ± 9.7 0.7 ± 0.2 5.1 ± 1.5 25.6 ± 2.1 35.9 ± 8.6 Experiment 2: relational MNIST (RQ2). |Δ|=2| |=2, NF3 cyclic-successor TBox. Independent (BCE) 61.8 ± 4.9 8.8 ± 4.5 2.8 ± 0.3 13.4 ± 3.6 17.6 ± 2.3 5.7 ± 3.3 DeepProbLog 85.3 ± 0.8 38.9 ± 3.2 1.4 ± 0.1 12.3 ± 0.9 57.9 ± 3.2 17.5 ± 4.1 LTN 91.9 ± 0.1 14.5 ± 4.9 1.2 ± 0.0 10.0 ± 0.0 40.1 ± 8.6 11.4 ± 5.8 ELEmbeddings/mOWL 90.1 ± 0.2 34.8 ± 3.6 0.4 ± 0.0 7.2 ± 0.1 6.9 ± 0.4 25.8 ± 3.7 Moose (Semantic-loss WMC) 93.8 ± 0.3 74.6 ± 0.3 0.5 ± 0.1 4.9 ± 0.3 24.9 ± 0.3 63.7 ± 1.1 Moose+BEARS 93.9 ± 1.1 76.5 ± 5.9 0.2 ± 0.0 4.0 ± 1.2 18.0 ± 4.5 67.8 ± 9.3 Moose+NeSyDM (RLOO) 90.9 ± 0.4 58.2 ± 1.4 0.3 ± 0.0 7.3 ± 0.7 30.3 ± 0.8 45.8 ± 4.3 Moose+NeSyDM (exact) 92.5 ± 1.2 62.6 ± 6.1 1.2 ± 0.2 7.4 ± 1.2 37.2 ± 6.1 59.1 ± 4.5 Experiment 3: role-chain MNIST (RQ3). |Δ|=2| |=2, plus_two=succ∘succ plus\_two= succ succ. Independent (BCE) 61.5 ± 3.3 12.2 ± 7.3 3.3 ± 0.4 9.0 ± 8.2 17.5 ± 3.5 7.9 ± 4.4 DeepProbLog 90.6 ± 3.1 59.6 ± 13.6 0.9 ± 0.3 8.0 ± 2.9 38.3 ± 12.7 48.4 ± 14.3 LTN 92.0 ± 0.1 11.0 ± 7.9 1.2 ± 0.0 10.0 ± 0.0 47.1 ± 6.9 8.2 ± 6.7 ELEmbeddings/mOWL 90.4 ± 0.1 27.4 ± 7.1 0.3 ± 0.0 6.3 ± 0.1 7.5 ± 0.7 18.7 ± 6.7 Moose (Semantic-loss WMC) 98.7 ± 1.8 96.1 ± 7.2 0.1 ± 0.2 1.1 ± 1.5 3.9 ± 7.1 93.8 ± 8.6 Moose+BEARS 94.8 ± 0.5 89.2 ± 7.2 0.1 ± 0.0 5.6 ± 1.1 8.3 ± 5.2 81.0 ± 12.2 Moose+NeSyDM (RLOO) 91.8 ± 0.5 62.7 ± 2.9 0.2 ± 0.0 4.6 ± 0.8 28.0 ± 2.1 57.6 ± 2.0 Moose+NeSyDM (exact) 92.0 ± 1.2 60.1 ± 5.7 1.3 ± 0.2 7.9 ± 1.1 36.1 ± 9.7 62.4 ± 10.1 Pizzaïolo Track A: pizza-type, OOD eval (RQ4). 55 held-out tie-breaker pizzas (Section 5.2). Independent (BCE) 46.6 ± 6.2 21.7 ± 9.7 6.4 ± 5.0 58.3 ± 15.4 62.2 ± 12.3 11.1 ± 6.4 DeepProbLog‡ 68.1 ± 0.3 68.1 ± 0.3 4.1 ± 0.2 30.8 ± 0.7 4.2 ± 7.6 14.1 ± 3.5 LTN 74.0 ± 3.4 22.1 ± 5.2 13.6 ± 5.4 52.7 ± 21.8 57.6 ± 17.3 10.9 ± 6.8 ELEmbeddings/mOWL 77.0 ± 0.9 25.7 ± 7.3 4.9 ± 1.0 49.7 ± 10.2 54.9 ± 6.6 11.2 ± 6.5 Moose (Semantic-loss WMC) 68.1 ± 0.3 68.1 ± 0.3 4.1 ± 0.2 30.8 ± 0.7 4.2 ± 7.6 14.1 ± 3.5 Moose+BEARS 68.6 ± 0.3 68.6 ± 0.3 3.3 ± 0.3 28.2 ± 1.5 0.6 ± 0.7 30.1 ± 10.2 Moose+NeSyDM (RLOO) 72.2 ± 1.3 72.2 ± 1.3 0.6 ± 0.0 7.5 ± 1.2 34.3 ± 4.2 44.8 ± 6.3 Moose+NeSyDM (exact) 67.4 ± 1.4 67.4 ± 1.4 4.6 ± 0.8 30.8 ± 3.2 3.8 ± 8.0 43.4 ± 3.0 Pizzaïolo Track B: property-class (RQ4, RQ5). 3-way RS over the property class. Independent (BCE) 57.2 ± 3.3 25.0 ± 0.0 2.7 ± 0.9 26.4 ± 17.1 37.0 ± 12.8 12.0 ± 1.1 DeepProbLog‡ 82.4 ± 1.9 84.5 ± 2.1 2.4 ± 0.3 15.5 ± 2.1 49.8 ± 4.6 37.8 ± 1.1 LTN 83.3 ± 1.6 32.5 ± 20.9 7.0 ± 6.0 39.3 ± 17.4 28.8 ± 12.5 23.4 ± 19.0 ELEmbeddings/mOWL 76.9 ± 0.0 25.0 ± 0.0 0.6 ± 0.0 16.1 ± 0.2 19.5 ± 0.1 10.0 ± 0.0 Moose (Semantic-loss WMC) 82.4 ± 1.9 84.5 ± 2.1 2.4 ± 0.3 15.5 ± 2.1 49.8 ± 4.6 37.8 ± 1.1 Moose+BEARS 85.4 ± 0.8 87.9 ± 0.9 0.3 ± 0.0 12.3 ± 1.0 30.3 ± 8.6 42.0 ± 9.0 Moose+NeSyDM (RLOO) 80.1 ± 0.8 78.5 ± 0.8 0.5 ± 0.0 2.6 ± 0.9 38.0 ± 4.7 22.6 ± 2.3 Moose+NeSyDM (exact) 86.3 ± 1.9 84.7 ± 2.2 2.5 ± 0.4 15.3 ± 2.2 50.3 ± 4.4 37.7 ± 1.0 Pizzaïolo Track C: is_spicy (RQ4, RQ5). Multi-witness disjunction; 1515 epochs. Independent (BCE) 55.2 ± 5.4 48.9 ± 5.6 1.0 ± 0.2 22.1 ± 9.2 N/A N/A DeepProbLog‡ 77.3 ± 2.8 81.0 ± 3.0 1.5 ± 0.3 15.3 ± 1.4 N/A N/A LTN 85.1 ± 0.9 84.8 ± 0.4 1.3 ± 0.3 14.1 ± 0.5 N/A N/A ELEmbeddings/mOWL 78.8 ± 6.5 75.4 ± 6.6 0.3 ± 0.1 11.8 ± 3.8 N/A N/A Moose (Semantic-loss WMC) 77.3 ± 2.8 81.0 ± 3.0 1.5 ± 0.3 15.3 ± 1.4 N/A N/A Moose+BEARS 79.9 ± 3.2 84.2 ± 3.6 0.4 ± 0.0 11.3 ± 3.4 N/A N/A Moose+NeSyDM (RLOO) 66.1 ± 3.7 63.9 ± 3.7 0.7 ± 0.0 8.9 ± 1.5 N/A N/A Moose+NeSyDM (exact) 75.9 ± 1.4 80.1 ± 1.5 0.8 ± 0.2 6.9 ± 2.2 N/A N/A Table 9 reports all six metrics (AccatomAcc_atom, the principal accuracy, NLL, ECE, RScons_cons, F1macroF1_macro) per regime, laid out as six row-blocks (MNIST Experiments 1–3, Pizzaïolo Tracks A–C). The compact main-paper tables Table 2 and Table 3 are summary views of the principal-accuracy and ECE columns of this table; per-regime AccatomAcc_atom, NLL, RScons_cons, and F1macroF1_macro appear only here. RScons_cons and F1macroF1_macro on Pizzaïolo Track A are computed from the in-distribution eval block (the OOD harness writes only per-pizza accuracies); on Track C (is_spicy binary supervision) both metrics are defined over a multi-class concept family and are not applicable. 0.F.7 Family-argmax on Pizzaïolo Family-argmax accuracy AccFAcc_F is defined per individual as the argmax of the WMC posterior over a declared exhaustive family, scored against ground truth. On MNIST the digit family D0,…,D9\D_0,…,D_9\ is declared exhaustive and AccFAcc_F is the reported metric. Pizzaïolo does not admit the same decode across its three tracks; we therefore report AccCAcc_C there and label it as such rather than folding two different quantities under one symbol. This appendix states the two metrics precisely and shows why the Pizzaïolo tracks carry AccCAcc_C. Track C is the clear case: is_spicy supervision is a multi-witness disjunction over four spicy toppings and declares no exhaustive family, so there is no set to take an argmax over and AccFAcc_F is undefined; the harness records 00 for these cells by absence, not as a score, and we report them as N/A throughout. Track A is reported on the out-of-distribution tie-breaker split, whose harness records per-pizza accuracies only and no family decode, so AccFAcc_F is unavailable there without a rerun. Track B does admit the decode, over the 33-way property class, and we report it in Table 10: every method lands between 48.048.0 and 50.250.2, a 2.22.2-point spread against per-method standard deviations of 3.63.6–5.35.3, so the metric separates no pair of methods. The AccCAcc_C column of the same runs spreads 78.578.5–87.987.9 and does separate them. Family-argmax on Pizzaïolo would therefore replace an informative metric with an uninformative one on the only track where it is even computable, which is why the headline tables keep AccCAcc_C and name it. Table 10: Pizzaïolo Track B under both accuracy metrics (55 seeds, mean ± s.d., %). AccFAcc_F is the family-argmax decode over the 33-way property class; AccCAcc_C is the per-atom accuracy on the latent slice reported in Table 2. Rows absent from the AccFAcc_F column did not record a family decode. Tracks A and C are omitted: the metric is unavailable and undefined there respectively (see text). Method AccFAcc_F AccCAcc_C LTN 49.5±3.649.5± 3.6 83.2±1.983.2± 1.9 Moose (Semantic-loss WMC) 50.2±4.650.2± 4.6 84.5±2.184.5± 2.1 Moose+BEARS 49.8±3.949.8± 3.9 87.9±0.987.9± 0.9 Moose+NeSyDM (RLOO) 48.0±5.348.0± 5.3 78.5±0.878.5± 0.8 Moose+NeSyDM (exact) 49.7±4.449.7± 4.4 84.7±2.284.7± 2.2 spread (max−-min) 2.22.2 9.49.4 0.F.8 Paired significance of the headline comparisons A mean ± s.d. over five runs is a stability summary rather than a significance test, and the shared evaluation instances call for a paired analysis. We therefore rerun the principal comparisons over 2020 seeds and test each Moose-vs-baseline difference with a paired Wilcoxon signed-rank test and an exact sign-flip permutation test on the mean difference, sharing seeds within every pair. Within each regime the p-values are Holm-corrected across the baselines, and we report significance at α=0.05α=0.05. The metric is the regime’s headline accuracy: family-argmax accuracy AccFAcc_F on MNIST Experiments 2–3, and latent-concept accuracy AccCAcc_C on Pizzaïolo Tracks A–C (Table 11); the Pizzaïolo significance statements therefore concern the latent-atom metric. Table 11: Paired significance of Moose (Semantic-loss WMC) against each baseline over 2020 shared seeds. “diff” is the mean per-seed difference (Moose −- baseline); “Holm p” is the Holm-corrected Wilcoxon p-value within the regime. The verdict is win (Moose significantly higher), loss (significantly lower), or ns (not significant) at α=0.05α=0.05. Metric: AccFAcc_F on MNIST, AccCAcc_C on Pizzaïolo. The 2020-seed reruns cover Moose, DeepProbLog, NeSyDM (RLOO), LTN, and BEARS on Experiments 2–3 and Pizzaïolo Tracks A–C; Experiment 1 and the remaining baselines (Independent, ELEmbeddings, NeSyDM-exact) are 55-seed only and are not part of the paired analysis. Regime Baseline Moose base diff Holm p verdict MNIST Exp. 2 DeepProbLog 0.7450.745 0.4230.423 +0.322+0.322 0.00020.0002 win NeSyDM 0.7450.745 0.5950.595 +0.150+0.150 0.00020.0002 win LTN 0.7450.745 0.1500.150 +0.595+0.595 0.00000.0000 win MNIST Exp. 3 DeepProbLog 0.9770.977 0.5980.598 +0.378+0.378 0.00000.0000 win NeSyDM 0.9770.977 0.6310.631 +0.346+0.346 0.00010.0001 win LTN 0.9770.977 0.1510.151 +0.825+0.825 0.00000.0000 win Pizza A (OOD) NeSyDM 0.6790.679 0.7090.709 −0.031-0.031 0.00040.0004 loss BEARS 0.6790.679 0.6830.683 −0.004-0.004 0.14540.1454 ns Pizza B NeSyDM 0.8410.841 0.7900.790 +0.052+0.052 0.00020.0002 win BEARS 0.8410.841 0.8800.880 −0.038-0.038 0.00020.0002 loss Pizza C NeSyDM 0.8090.809 0.6170.617 +0.192+0.192 0.00020.0002 win BEARS 0.8090.809 0.8560.856 −0.047-0.047 0.00030.0003 loss The relational and role-chain regimes are unambiguous: Moose beats every propositional baseline on Experiments 2–3 by margins that are large and significant (Holm p≤0.0002p≤ 0.0002). On Pizzaïolo the picture is mixed, and we report it as such. Moose is significantly stronger than NeSyDM on Tracks B and C, but BEARS is significantly stronger than Moose on both; on the Track A OOD split NeSyDM significantly overtakes Moose, while the Moose-vs-BEARS gap there is not significant. Moose is therefore competitive but not dominant under symbolic ambiguity, and its clear advantage is in the relational regime where EL-aware grounding propagates evidence that propositional encodings cannot. The cell means here differ marginally from the 55-seed headline tables (Table 2) because this analysis uses the 2020-seed reruns; e.g. Moose on Exp. 2 is 0.7450.745 here versus 0.7460.746 in the 55-seed table. These paired tests compare Moose against each baseline; the headline tables mark the raw column-best rather than a significance verdict, since the 2020-seed reruns do not cover every method or regime (Table 11). The test covers accuracy only, so Table 3 still marks the raw column-best. 0.F.9 Inductive generalization A further question is whether the learned models generalize to new query individuals rather than only to held-out images. We test this with an inductive held-out-edge split of the relational (Exp. 2) and role-chain (Exp. 3) regimes. On Exp. 2 we supervise only the successor edges whose source digit lies in 0,2,4,6,8\0,2,4,6,8\ (→1,→3,…,→90\!→\!1,2\!→\!3,…,8\!→\!9) and query individuals on the held-out edges 1,3,5,7,9\1,3,5,7,9\ (→2,→4,…,→01\!→\!2,3\!→\!4,…,9\!→\!0); on Exp. 3 the plus_two relation forms two 55-cycles, and we supervise sources 0,1,2,3,6,7\0,1,2,3,6,7\ and query the held-out sources 4,5,8,9\4,5,8,9\. In both splits the training and query edge sets jointly cover all ten digit nodes, so the shared perception network sees every digit during training; only the relational configuration of a query pair is novel, not its images; this is a test of relational generalization, not zero-shot perception. As a control we also evaluate on the supervised edge types with fresh images (the transductive column of Table 12). Table 12: Inductive generalization over 2020 seeds (AccFAcc_F, family-argmax accuracy). Inductive evaluates on relational configurations never supervised; transductive is the same-edge-type control on new images; drop is transductive −- inductive (positive means degradation on unseen configurations). Regime Method Inductive Transductive Drop Exp. 2 (relational) Moose (WMC) 0.717±0.0710.717± 0.071 0.6850.685 −0.032-0.032 Independent 0.582±0.0360.582± 0.036 0.6050.605 +0.023+0.023 NeSyDM 0.135±0.0240.135± 0.024 0.5940.594 +0.459+0.459 Exp. 3 (role-chain) Moose (WMC) 0.595±0.1380.595± 0.138 0.5740.574 −0.021-0.021 Independent 0.551±0.0930.551± 0.093 0.7100.710 +0.159+0.159 NeSyDM 0.254±0.0420.254± 0.042 0.7120.712 +0.458+0.458 Moose shows no inductive degradation on either regime: its held-out-configuration accuracy matches its transductive control to within noise (−0.032-0.032 and −0.021-0.021, i.e. marginally higher inductive). NeSyDM, by contrast, collapses from 0.5940.594/0.7120.712 transductive to 0.1350.135/0.2540.254 on held-out configurations, and the Independent baseline degrades moderately. The WMC layer scores whole declared families rather than memorized edge identities, so a query pair in an unseen configuration is handled by the same exact-inference path as a supervised one, which is what preserves accuracy. The paired Moose-vs-Independent advantage on the inductive split is significant on Exp. 2 (Wilcoxon p<10−4p<10^-4, n=20n=20) but not on Exp. 3 (p=0.52p=0.52), where the role-chain circuit leaves both methods with high seed-to-seed variance. 0.F.10 Closure ablation: separating ΓEL _ EL from Φclos _ clos The compiled theory combines the EL-aware extractors ΓEL _ EL with the optional closure clauses Φclos _ clos, whose covering axiom ⊤⊑⨆iDi _iD_i lies outside the EL profile. To isolate their contributions we disable Φclos _ clos on all three MNIST regimes (--no-closed-world, 55 seeds) and pair against the with-closure baseline (Table 13). Table 13: Closure ablation on MNIST. AccFAcc_F (mean ± s.d. over 55 seeds) with and without the exhaustive-family closure clauses Φclos _ clos. The --no-closed-world arm removes mutual exclusion and covering in all three regimes and profile-keyed reverse implications in Experiment 1. Δ is the change in the mean when Φclos _ clos is removed. Regime Method with Φclos _ clos without Φclos _ clos Δ Exp. 1 (atomic) Moose 48.1±10.148.1± 10.1 21.7±0.021.7± 0.0 −26.4-26.4 +BEARS 50.1±5.250.1± 5.2 21.7±0.021.7± 0.0 −28.4-28.4 +NeSyDM (RLOO) 46.6±2.146.6± 2.1 21.7±0.021.7± 0.0 −24.9-24.9 +NeSyDM (exact) 49.4±9.749.4± 9.7 21.7±0.021.7± 0.0 −27.7-27.7 Exp. 2 (relational) Moose 74.6±0.374.6± 0.3 17.4±1.817.4± 1.8 −57.2-57.2 +BEARS 76.5±5.976.5± 5.9 30.9±4.530.9± 4.5 −45.6-45.6 +NeSyDM (RLOO) 58.2±1.458.2± 1.4 39.4±3.039.4± 3.0 −18.8-18.8 +NeSyDM (exact) 62.6±6.162.6± 6.1 17.3±5.117.3± 5.1 −45.3-45.3 Exp. 3 (role-chain) Moose 96.1±7.296.1± 7.2 9.4±0.9 09.4± 0.9 −86.7-86.7 +BEARS 89.2±7.289.2± 7.2 37.1±6.537.1± 6.5 −52.1-52.1 +NeSyDM (RLOO) 62.7±2.962.7± 2.9 46.5±3.046.5± 3.0 −16.2-16.2 +NeSyDM (exact) 60.1±5.760.1± 5.7 54.3±3.054.3± 3.0 −5.8 0-5.8 Without Φclos _ clos the base WMC objective collapses toward chance in every regime, and the collapse deepens with relational complexity: AccFAcc_F falls by 26.426.4, 57.257.2, and 86.786.7 points on Experiments 1–3, reaching 9.49.4 (chance is 10.010.0) on the role-chain regime. Experiment 1 is degenerate: all four methods land on the same seed-independent 21.7±0.021.7± 0.0, because without the complete closure package the digit family receives no disambiguating gradient. The EL-aware extractors provide the structural scaffold, but the complete Φclos _ clos package supplies the learning signal that makes the latent digit identifiable; the MNIST gains cannot be attributed to ΓEL _ EL alone. The reasoning-shortcut mitigations can partially substitute for closure on the relational regimes, but which objective helps, and by how much, is regime-dependent rather than systematic. NeSyDM (RLOO) is the most robust, retaining 39.439.4 (Exp. 2) and 46.546.5 (Exp. 3) against plain Moose’s 17.417.4 and 9.49.4; BEARS buffers partially in both (30.930.9 and 37.137.1); and NeSyDM (exact) splits the two regimes, collapsing with the base objective on Experiment 2 (17.317.3, Δ=−45.3 =-45.3) yet proving the most closure-robust of any method on Experiment 3 (54.354.3, Δ=−5.8 =-5.8). The wrappers that resist collapse also hold RSconsRS_cons down (to 0.280.28–0.430.43, against plain Moose’s 0.430.43–0.500.50 where it does not collapse outright), reshaping the posterior enough to recover a substantial fraction of the signal, though never to the with-closure level. No single mitigation is a general substitute for Φclos _ clos: closure is necessary for the exact base objective and only partially, inconsistently replaceable by a reasoning-shortcut objective, which connects the mitigation behaviour of §5.3 to the ΓEL _ EL-versus-Φclos _ clos separation. Appendix 0.G Related work: compilation, refinement, and embedding approaches Rewriting-based approaches. ℰℒ++EL^++ is Datalog-rewritable, and a substantial line of work recasts description logic reasoning as rule evaluation: consequence-based calculi for EL can be expressed as Datalog programs [33], and data-independent transformations carry richer Horn DLs into Datalog while preserving assertion entailment [11]. Moose shares this view: Stage 2 of the pipeline (§3.2) treats the ELK saturation as a monotone Datalog program, but the two lines answer different questions. A rewriting produces a reasoning procedure whose output is an entailment set; it supplies no gradient and no per-individual marginal, so it cannot act as a supervision channel. The probabilistic description logics [12, 13, 24] attach a distribution to the axioms and answer probabilistic queries, but that distribution is specified by the modeller rather than learned from perception; the fuzzy line [53, 8] gains differentiability by replacing model-theoretic entailment with a t-norm relaxation. Moose compiles the classical semantics into a circuit that is at once exact and differentiable, which is what allows neural outputs to serve as atom-level evidence. Compilation-based approaches. Two recent works compile a description logic ontology into a differentiable representation for use with neural networks. Lazzari et al. [37] compile an ℒℐALCI TBox to a smooth, decomposable, deterministic circuit using a domino-style reduction, then plug the circuit into a multi-label classifier as either a Semantic-Loss regulariser or the head of a Semantic Probabilistic Layer; their experiments report on synthetically generated inputs and target the link- and classification-prediction setting in which every output label of the multi-label classifier is observed during training. Their treatment leaves three regimes open: the EL profile with role chains and role hierarchies, partial supervision in which a subset of the ground atoms is latent, and an RS analysis of the resulting predictor. DF-EL++ [53] approximates ℰℒ++EL^++ with a product-based fuzzy semantics that preserves PTIME-tractability and reports knowledge-base completion results on SNOMED CT (377K concepts); its loss replaces the classical model-theoretic entailment with a continuous relaxation, and it does not address exact WMC, partial-supervision concept learning, or RS metrics. Refinement, clustering, and embeddings. Iterative Local Refinement (ILR) [19] corrects neural predictions at inference time so they satisfy a fuzzy-logic relaxation of a propositional formula; Embed2Sym [4] trains a perception network end-to-end on the downstream label, clusters the resulting embedding, and labels the clusters via a symbolic solver over a logic program. ELEmbeddings [36] maps concepts to n-balls and roles to translation vectors with NF1–NF4 margin losses that geometrise the ℰℒ++EL^++ axioms. DeepGOZero [35] trains a protein-sequence encoder jointly with these geometric class embeddings, supervising on observed protein–GO-class annotations via binary cross-entropy while the NF1–NF4 losses constrain the class n-balls through the GO axioms; predictions for a GO class with no training proteins are read off the same trained n-ball, giving zero-shot annotations that ride on the ontology axioms alone. DeepGO-SE [34] reframes the same encoding as approximate semantic entailment. Our ELEmbeddings baseline (Section 0.E.4) adopts the identical NF1–NF4 losses and ball-distance per-atom scoring but differs in the supervision regime, per-class function annotations there versus latent ABox atoms here. OWL2Vec∗ [15] embeds an ontology by training a word model on random walks over its axioms; a recent survey [16] covers the ontology-embedding landscape more broadly. ILR and Embed2Sym have not been instantiated for OWL EL with role chains; the embedding methods target subsumption inference and knowledge-base completion rather than partial-supervision concept learning. All four trade the model-theoretic semantics for a continuous representation, whereas Moose compiles the same ELK semantics into a differentiable circuit.