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

# Latent concept learning with reasoning-shortcut awareness in ⁢ E L + ⁣ +
Source: [https://arxiv.org/html/2608.12961](https://arxiv.org/html/2608.12961)
Olga MashkovaOrcID:[0000\-0002\-4916\-1660](https://orcid.org/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 ArabiaAsaad MohammedsalehOrcID:[0009\-0007\-3160\-8819](https://orcid.org/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 ArabiaAffiliation:E\-mail[\{first\_name\.last\_name\}@kaust\.edu\.sa](mailto:{first_name.last_name}@kaust.edu.sa)Fernando Zhapa\-Camacho and Robert HoehndorfOrcID:[0000\-0002\-0710\-2259](https://orcid.org/0000-0002-0710-2259)OrcID:[0000\-0001\-8149\-5890](https://orcid.org/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 ArabiaAffiliation: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 presentMoose, 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 evaluateMooseon MNIST\-with\-ontology and Pizzaïolo\.Mooseimproves 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\.

## 1Introduction

The OWL 2 EL profile underpins some of the largest and most widely\-used ontologies, such as the Gene Ontology with∼\\sim50K classes and∼\\sim8M annotations\[[3](https://arxiv.org/html/2608.12961#bib.bib3),[49](https://arxiv.org/html/2608.12961#bib.bib49)\], SNOMED CT\[[22](https://arxiv.org/html/2608.12961#bib.bib22)\], and most of the OBO Foundry ontologies\[[45](https://arxiv.org/html/2608.12961#bib.bib45),[25](https://arxiv.org/html/2608.12961#bib.bib25)\], because EL trades expressivity for polynomial\-time reasoning on subsumption, instance checking, and consistency\[[5](https://arxiv.org/html/2608.12961#bib.bib5),[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\. 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](https://arxiv.org/html/2608.12961#bib.bib7)\]; embedding methods score entities and relations in a continuous geometry\[[36](https://arxiv.org/html/2608.12961#bib.bib36),[15](https://arxiv.org/html/2608.12961#bib.bib15),[16](https://arxiv.org/html/2608.12961#bib.bib16)\];*knowledge\-compilation*methods compile the constraint to an arithmetic circuit whose weighted model count \(WMC\) is differentiable in the inputs\[[39](https://arxiv.org/html/2608.12961#bib.bib39),[51](https://arxiv.org/html/2608.12961#bib.bib51),[43](https://arxiv.org/html/2608.12961#bib.bib43),[1](https://arxiv.org/html/2608.12961#bib.bib1)\]\. 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](https://arxiv.org/html/2608.12961#bib.bib39),[41](https://arxiv.org/html/2608.12961#bib.bib41),[29](https://arxiv.org/html/2608.12961#bib.bib29)\]\.

Existing knowledge\-compilation NeSy frameworks accept propositional formulas, Datalog programs, or finite\-domain rules\[[39](https://arxiv.org/html/2608.12961#bib.bib39),[51](https://arxiv.org/html/2608.12961#bib.bib51),[43](https://arxiv.org/html/2608.12961#bib.bib43),[1](https://arxiv.org/html/2608.12961#bib.bib1)\], but not OWL ontologies directly\. Two recent works target description logics: a domino\-style reduction of𝒜​ℒ​𝒞​ℐ\\mathcal\{ALCI\}to a probabilistic circuit\[[37](https://arxiv.org/html/2608.12961#bib.bib37)\]that treats the circuit as a regulariser under full label supervision, and a fuzzy approximation ofℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}via Goguen\-implication semantics\[[53](https://arxiv.org/html/2608.12961#bib.bib53)\]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](https://arxiv.org/html/2608.12961#bib.bib36),[15](https://arxiv.org/html/2608.12961#bib.bib15)\]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](https://arxiv.org/html/2608.12961#bib.bib41),[40](https://arxiv.org/html/2608.12961#bib.bib40),[29](https://arxiv.org/html/2608.12961#bib.bib29),[31](https://arxiv.org/html/2608.12961#bib.bib31),[30](https://arxiv.org/html/2608.12961#bib.bib30),[9](https://arxiv.org/html/2608.12961#bib.bib9)\]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](https://arxiv.org/html/2608.12961#bib.bib33),[11](https://arxiv.org/html/2608.12961#bib.bib11)\], and probabilistic\[[12](https://arxiv.org/html/2608.12961#bib.bib12),[13](https://arxiv.org/html/2608.12961#bib.bib13)\]and fuzzy\[[53](https://arxiv.org/html/2608.12961#bib.bib53),[8](https://arxiv.org/html/2608.12961#bib.bib8)\]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 presentMoose, a method that compiles anℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology and a finite ABox domain into a Sentential Decision Diagram\[[20](https://arxiv.org/html/2608.12961#bib.bib20),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]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. 1\.End\-to\-end OWL 2 EL compilation with full proofs\.We compile the EL profile, including role chainsR1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq Sand role hierarchies \(the constructs that distinguish SNOMED CT and the Gene Ontology from a propositional or𝒜​ℒ​𝒞​ℐ\\mathcal\{ALCI\}setting\), via ELK\-style saturation\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]to an SDD supporting WMC\. The four formal contributions are a verified SDD encoding \([Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\), the rational DISPONTE\[[44](https://arxiv.org/html/2608.12961#bib.bib44)\]distribution\-semantics correspondence \([Theorem4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2)\), and SCC\-compositional factorizations at the Sat and WMC levels \([Theorems4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3)and[4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)\)\. All four are mechanized in Lean 4 \(noMoose\-specific axioms;[Appendices0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)and[0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)\), along with the supporting Lean libraries for ELK saturation, soundness/completeness onℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\], and SDD knowledge compilation, which to our knowledge are the first such formalizations \([Section0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.SS1)\)\. The closure\-augmented variant is correct \([Theorem0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3)\) and inference is linear in the SDD \([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)\.
2. 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𝗍𝗋𝗎𝖾\\mathsf\{true\}and𝖿𝖺𝗅𝗌𝖾\\mathsf\{false\}, so that they are not confused with theℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}concepts⊤\\topand⊥\\bot\), 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](https://arxiv.org/html/2608.12961#bib.bib39)\]and Semantic Loss\[[51](https://arxiv.org/html/2608.12961#bib.bib51)\]to description logic constraints with role chains and role hierarchies\.
3. 3\.Reasoning\-shortcut analysis transposed to OWL EL\.We compute family\-argmax accuracy, expected calibration error \(ECE\), and the RS\-consistency rate underMooseand two plug\-in mitigations \(Moose\+BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]andMoose\+NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]\), 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. 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](https://arxiv.org/html/2608.12961#bib.bib10)\]that transfers the method to a real expert\-authored OWL EL ontology\.

## 2Background and related work

### 2\.1Preliminaries: OWL EL, knowledge compilation, partial\-supervision NeSy

#### The OWL 2 EL profile\.

ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}\[[5](https://arxiv.org/html/2608.12961#bib.bib5)\]is the description logic basis of OWL 2 EL \(syntax and semantics in[Table4](https://arxiv.org/html/2608.12961#Pt0.A1.T4)\)\. Concepts are built from atomic names,⊤\\top,⊥\\bot, conjunctionC⊓DC\\sqcap D, and existential restriction∃R\.C\\exists R\.C; an ontology𝒪\\mathcal\{O\}contains GCIsC⊑DC\\sqsubseteq D, role inclusionsR⊑SR\\sqsubseteq S, and role chainsR1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq S, with subsumption, instance checking, and consistency decidable in time polynomial in\|𝒪\|\|\\mathcal\{O\}\|\. ELK\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]realizes this bound through a consequence\-based saturation closure under ten completion rules\[[48](https://arxiv.org/html/2608.12961#bib.bib48)\]\.ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}is moreover Datalog\-rewritable: consequence\-based reasoning can be recast as the evaluation of a Datalog program\[[33](https://arxiv.org/html/2608.12961#bib.bib33),[11](https://arxiv.org/html/2608.12961#bib.bib11)\], and Stage 2 of our pipeline \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\) 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ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}\[[12](https://arxiv.org/html/2608.12961#bib.bib12),[13](https://arxiv.org/html/2608.12961#bib.bib13),[24](https://arxiv.org/html/2608.12961#bib.bib24)\]attaches weights via Bayesian\-network encodings; fuzzyℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}\[[53](https://arxiv.org/html/2608.12961#bib.bib53),[8](https://arxiv.org/html/2608.12961#bib.bib8)\]replaces model\-theoretic semantics with a t\-norm\-based approximation\.

#### Knowledge compilation, WMC, and SDDs\.

For a propositional formulaφ\\varphiand literal weightsw⁡\(ℓ\)≥0w\(\\ell\)\\geq 0, the weighted model count is𝖶𝖬𝖢⁡\(φ,w\)=∑M⊧φ∏ℓ∈Mw⁡\(ℓ\)\\mathsf\{WMC\}\(\\varphi;w\)=\\sum\_\{M\\models\\varphi\}\\prod\_\{\\ell\\in M\}w\(\\ell\)\[[14](https://arxiv.org/html/2608.12961#bib.bib14)\]\. With arbitrary non\-negative weights𝖶𝖬𝖢\\mathsf\{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\(\\neg X\)=1for every variableXX\. Under that condition the weights specify a product distribution over truth assignments, and𝖶𝖬𝖢⁡\(φ,w\)\\mathsf\{WMC\}\(\\varphi;w\)is exactly the probability that a sample from this distribution satisfiesφ\\varphi: it lies in\[0,1\]\[0,1\]and𝖶𝖬𝖢⁡\(φ,w\)\+𝖶𝖬𝖢⁡\(¬φ,w\)=1\\mathsf\{WMC\}\(\\varphi;w\)\+\\mathsf\{WMC\}\(\\neg\\varphi;w\)=1\[[14](https://arxiv.org/html/2608.12961#bib.bib14)\]\.Mooseenforces this normalization by construction \(§[3\.1](https://arxiv.org/html/2608.12961#S3.SS1),[Table1](https://arxiv.org/html/2608.12961#S3.T1)\), and[Theorem4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2)establishes the resulting WMC/distribution\-semantics identity for the compiled circuit\. When the per\-variable weights are produced by a neural network,𝖶𝖬𝖢\\mathsf\{WMC\}is differentiable in the network’s outputs\. Knowledge compilation translatesφ\\varphito a circuit whose structural properties \(smoothness, decomposability, determinism\) make𝖶𝖬𝖢\\mathsf\{WMC\}linear in circuit size and reduce probabilistic queries to circuit traversals\[[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\. A Sentential Decision Diagram \(SDD\)\[[20](https://arxiv.org/html/2608.12961#bib.bib20),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]is one such circuit and supports polynomial\-time conjunction, disjunction, conditioning, and weighted model counting; exact definitions are in[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4), and[Section0\.C\.3](https://arxiv.org/html/2608.12961#Pt0.A3.SS3)shows a small example\.

#### Knowledge\-compilation NeSy and partial supervision\.

A predictor composes a neural concept extractorpθ​\(𝐜∣𝐱\)p\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)with a symbolic constraintφ\\varphiand trains by maximizing the marginal

pθ\(𝐲∣𝐱\)=∑𝐜pθ\(𝐜∣𝐱\)1\[φ\(𝐜\)=𝐲\],p\_\{\\theta\}\(\\mathbf\{y\}\\mid\\mathbf\{x\}\)=\\sum\_\{\\mathbf\{c\}\}p\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)\\,\\mathbf\{1\}\[\\varphi\(\\mathbf\{c\}\)=\\mathbf\{y\}\],\(1\)the standard objective across this family\[[39](https://arxiv.org/html/2608.12961#bib.bib39),[51](https://arxiv.org/html/2608.12961#bib.bib51),[1](https://arxiv.org/html/2608.12961#bib.bib1),[43](https://arxiv.org/html/2608.12961#bib.bib43),[30](https://arxiv.org/html/2608.12961#bib.bib30)\]\. DeepProbLog\[[39](https://arxiv.org/html/2608.12961#bib.bib39)\]groundsφ\\varphias probabilistic Datalog with neural\-network annotated facts; Semantic Loss\[[51](https://arxiv.org/html/2608.12961#bib.bib51)\]adds−log⁡𝖶𝖬𝖢⁡\(φ\)\-\\log\\mathsf\{WMC\}\(\\varphi\)on propositional constraints; Semantic Probabilistic Layers\[[1](https://arxiv.org/html/2608.12961#bib.bib1)\]combine exact probabilistic inference with logical constraints in a single tractable circuit; Scallop\[[38](https://arxiv.org/html/2608.12961#bib.bib38)\]compiles differentiable Datalog with provenance semirings; NeurASP\[[52](https://arxiv.org/html/2608.12961#bib.bib52)\]embeds neural perception inside answer\-set programs; and A\-NeSI\[[32](https://arxiv.org/html/2608.12961#bib.bib32)\]amortizes the intractable WMC marginal with a neural surrogate\. A*partial\-supervision*instance reveals labels for a subset of𝐲\\mathbf\{y\}\-atoms only; the latent concept vector𝐜\\mathbf\{c\}is recovered through the WMC gradient \([Definition1](https://arxiv.org/html/2608.12961#Thmdefinition1)\)\. 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](https://arxiv.org/html/2608.12961#bib.bib26)\]in the process\.

### 2\.2The independence assumption and reasoning shortcuts

Knowledge\-compilation NeSy predictors almost universally factorizepθ​\(𝐜∣𝐱\)=∏ipθ​\(ci∣𝐱\)p\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)=\\prod\_\{i\}p\_\{\\theta\}\(c\_\{i\}\\mid\\mathbf\{x\}\)\. Marconato et al\.\[[41](https://arxiv.org/html/2608.12961#bib.bib41)\]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](https://arxiv.org/html/2608.12961#bib.bib9)\]quantifies RS rates across NeSy architectures\.\[[29](https://arxiv.org/html/2608.12961#bib.bib29),[31](https://arxiv.org/html/2608.12961#bib.bib31)\]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](https://arxiv.org/html/2608.12961#bib.bib40)\]keeps the independent extractor and trains aKK\-encoder ensemble whose members commit to distinct shortcut explanations; NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]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](https://arxiv.org/html/2608.12961#bib.bib37),[53](https://arxiv.org/html/2608.12961#bib.bib53)\], refinement\[[19](https://arxiv.org/html/2608.12961#bib.bib19),[4](https://arxiv.org/html/2608.12961#bib.bib4)\], and ontology embeddings\[[36](https://arxiv.org/html/2608.12961#bib.bib36),[15](https://arxiv.org/html/2608.12961#bib.bib15),[16](https://arxiv.org/html/2608.12961#bib.bib16)\]is reviewed in[Appendix0\.G](https://arxiv.org/html/2608.12961#Pt0.A7)\.

## 3Methods

![Refer to caption](https://arxiv.org/html/2608.12961v1/workflow.png)Figure 1:End\-to\-endMooseworkflow on𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}atΔ=\{a,b\}\\Delta\{=\}\\\{a,b\\\}\. The TBox is compiled once via ELK saturation→\\toshape\-aware extractors→ΓEL\\to\\Gamma\_\{\\mathrm\{EL\}\}\(\+Φclos\+\\Phi\_\{\\mathrm\{clos\}\}when supplied\)→\\toSDDα\\alpha\. The differentiable WMC layer evaluates𝖶𝖬𝖢⁡\(α,pθ​\(𝐱\),𝐞\)\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)for the training loss, the conditional posterior, and the entailment query\.### 3\.1Task and ground vocabulary

Given anℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology𝒪\\mathcal\{O\}and a finite ABox domainΔ=\{a1,…,am\}\\Delta=\\\{a\_\{1\},\\dots,a\_\{m\}\\\}, the*ground vocabulary*is𝒱𝒪Δ:=\{C\(a\):C∈𝖲𝗂𝗀C,a∈Δ\}∪\{R\(a,b\):R∈𝖲𝗂𝗀R,a,b∈Δ\}\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}:=\\\{C\(a\):C\\in\\mathsf\{Sig\}\_\{C\},a\\in\\Delta\\\}\\cup\\\{R\(a,b\):R\\in\\mathsf\{Sig\}\_\{R\},a,b\\in\\Delta\\\}\. The modeller partitions each signature into*observable*and*latent*names,𝖲𝗂𝗀C=𝖲𝗂𝗀Co⊎𝖲𝗂𝗀Cℓ\\mathsf\{Sig\}\_\{C\}=\\mathsf\{Sig\}^\{o\}\_\{C\}\\uplus\\mathsf\{Sig\}^\{\\ell\}\_\{C\}and𝖲𝗂𝗀R=𝖲𝗂𝗀Ro⊎𝖲𝗂𝗀Rℓ\\mathsf\{Sig\}\_\{R\}=\\mathsf\{Sig\}^\{o\}\_\{R\}\\uplus\\mathsf\{Sig\}^\{\\ell\}\_\{R\}\. A training instance\(Δ,𝐱,𝐞\)\(\\Delta,\\mathbf\{x\},\\mathbf\{e\}\)comprises a per\-individual input tuple𝐱=\(xa\)a∈Δ\\mathbf\{x\}=\(x\_\{a\}\)\_\{a\\in\\Delta\}with eachxa∈𝒳x\_\{a\}\\in\\mathcal\{X\}and a partial set of ABox literals𝐞\\mathbf\{e\}over the observable ground vocabulary \(Definition[1](https://arxiv.org/html/2608.12961#Thmdefinition1),[Appendix0\.B](https://arxiv.org/html/2608.12961#Pt0.A2)\)\. We learn a weight\-shared per\-individual classifierfθ:𝒳→\[0,1\]\|𝖲𝗂𝗀Cℓ\|f\_\{\\theta\}:\\mathcal\{X\}\\to\[0,1\]^\{\|\\mathsf\{Sig\}^\{\\ell\}\_\{C\}\|\}that approximates the marginal of each latent atom under𝒪∪𝐞\\mathcal\{O\}\\cup\\mathbf\{e\}\. The differentiable WMC layer evaluates𝖶𝖬𝖢⁡\(α,w,𝐞\)\\mathsf\{WMC\}\(\\alpha;w,\\mathbf\{e\}\)under the literal\-weight mapwwthat assignsfθ​\(xa\)f\_\{\\theta\}\(x\_\{a\}\)to each latent concept atomC⁡\(a\)C\(a\), its observed truth value to each observed atom,12\\tfrac\{1\}\{2\}to each unobserved observable and to each latent role atom, and1−w⁡\(X\)1\-w\(X\)to each negative literal¬X\\neg X, whereXXranges over the ground atoms of𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\([Table1](https://arxiv.org/html/2608.12961#S3.T1)\)\. Becausew⁡\(X\)\+w⁡\(¬X\)=1w\(X\)\+w\(\\neg X\)=1for everyXXby construction, the map is per\-variable normalized: it defines a product distribution over the ground atoms whose per\-atom marginal isww, and𝖶𝖬𝖢⁡\(α,w,𝐞\)\\mathsf\{WMC\}\(\\alpha;w,\\mathbf\{e\}\)is the probability under this distribution that a sample satisfiesα\\alphaand the evidence𝐞\\mathbf\{e\}\(§[2\.1](https://arxiv.org/html/2608.12961#S2.SS1);[Theorem4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2)\)\. This product form encodes the per\-atom*independence*factorizationpθ​\(𝐜∣𝐱\)=∏ipθ​\(ci∣𝐱\)p\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)=\\prod\_\{i\}p\_\{\\theta\}\(c\_\{i\}\\mid\\mathbf\{x\}\)shared by knowledge\-compilation NeSy predictors \(§[2\.2](https://arxiv.org/html/2608.12961#S2.SS2)\)\. 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 viaRScons\\mathrm\{RS\}\_\{\\text\{cons\}\}and which the BEARS and NeSyDM variants \(§[3\.4](https://arxiv.org/html/2608.12961#S3.SS4)\) are designed to mitigate\.

Table 1:Literal\-weight mapww; the two weights of each variable sum to11\.
### 3\.2Compilation algorithm

The algorithm \(full pseudocode in[Algorithm1](https://arxiv.org/html/2608.12961#alg1),[Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3)\) compiles anℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology and a finite ABox domain to an SDD over𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}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 asxC⊑Dx\_\{C\\sqsubseteq D\}andxE→𝑅Cx\_\{E\\xrightarrow\{R\}C\}, including derived complex concepts \(e\.g\.C⊑∃R\.∃S\.DC\\sqsubseteq\\exists R\.\\exists S\.D\); the input axiom variablesαi\\alpha\_\{i\}in this theory are free, so the theory supports*probabilistic ontology reasoning*: assigning a weightpip\_\{i\}to eachαi\\alpha\_\{i\}and computing the WMC givesP⁡\(query entailed\)P\(\\text\{query entailed\}\)\. Stages 6–7 operate on the ground vocabulary𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}whose variables are ABox atomsC⁡\(a\)C\(a\)andR⁡\(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 \([Table1](https://arxiv.org/html/2608.12961#S3.T1)\), 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\\exists R\.Cor∃R\.∃S\.D\\exists R\.\\exists S\.D\) do not lie in the named signature𝖲𝗂𝗀C​\(𝒪\)\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{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\)\(\\mathcal\{O\},E\)runs the ten ELK completion rules\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]and returns the saturation pair\(Σ,Λ\)\(\\Sigma,\\Lambda\), whereΣ\\Sigmais the set of derived subsumptionsC⊑DC\\sqsubseteq DandΛ\\Lambdathe set of derived role linksE→𝑅CE\\xrightarrow\{R\}C, sound and complete with respect to𝒪\\mathcal\{O\}\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\. We writeSat​\(𝒪\):=Σ∪Λ\\textsf\{Sat\}\(\\mathcal\{O\}\):=\\Sigma\\cup\\Lambdafor 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\\exists R\.C,∃R\.∃S\.D\\exists R\.\\exists 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[Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3), and[Section0\.C\.3](https://arxiv.org/html/2608.12961#Pt0.A3.SS3)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](https://arxiv.org/html/2608.12961#bib.bib18)\]\. Stages 2–5 turn it into a propositional TBox theory: Clark completion\[[18](https://arxiv.org/html/2608.12961#bib.bib18)\]replaces each derived atom’s justifications with a biconditional, Tarjan’s algorithm\[[47](https://arxiv.org/html/2608.12961#bib.bib47)\]isolates cyclic strongly\-connected components, these are broken by SCC\-local time\-stamped unrolling, and the Tseitin transformation\[[50](https://arxiv.org/html/2608.12961#bib.bib50)\]yields an equisatisfiable CNF\. With all input\-axiom variables true this theory hasSat​\(𝒪\)\\textsf\{Sat\}\(\\mathcal\{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[Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3)\.

#### Stage 6: shape\-aware extractors and ABox grounding\.

Stage 6 extractors return to the Stage 1 saturation output\(Σ,Λ\)\(\\Sigma,\\Lambda\)and select the subset that maps to ground ABox atoms over𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\.AtomSubemits¬A⁡\(a\)∨B⁡\(a\)\\neg A\(a\)\\vee B\(a\)for every subsumptionA⊑BA\\sqsubseteq BinΣ\\Sigmawhere bothAAandBBare named concepts in𝖲𝗂𝗀C​\(𝒪\)\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\);Disjemits⋁i¬Ai​\(a\)\\bigvee\_\{i\}\\neg A\_\{i\}\(a\)fornn\-ary atomic disjointnessA1⊓⋯⊓An⊑⊥A\_\{1\}\\sqcap\\dots\\sqcap A\_\{n\}\\sqsubseteq\\bot\(flattened from any parenthesization\);Unsatemits¬A⁡\(a\)\\neg A\(a\)for atomicA⊑⊥A\\sqsubseteq\\bot;Linksemits the NF3\-forward clause¬E⁡\(a\)∨¬R⁡\(a,b\)∨C⁡\(b\)\\neg E\(a\)\\vee\\neg R\(a,b\)\\vee C\(b\)per saturation\-derived atomic link\(E,R,C\)∈Λ\(E,R,C\)\\in\\Lambda\(i\.e\.E⊑∃R\.CE\\sqsubseteq\\exists R\.CwithE,C∈𝖲𝗂𝗀C​\(𝒪\)E,C\\in\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\)\), plus an NF4\-reverse clause¬R⁡\(a,b\)∨¬C⁡\(b\)∨E⁡\(a\)\\neg R\(a,b\)\\vee\\neg C\(b\)\\vee E\(a\)whenL⁡\(E,R\):=\{C:\(E,R,C\)∈Λ\}L\(E,R\):=\\\{C:\(E,R,C\)\\in\\Lambda\\\}is a singleton \(so the NF4 direction is deterministic\)\. The union of the clauses produced by these extractors is the propositional Horn programΓ\\Gammaover𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}; the saturation closure is polynomial by[Theorem0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2)and grounding multiplies it by at most\|Δ\|2\|\\Delta\|^\{2\}\([Section0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.SS4)\)\.

#### Stage 7: SDD compilation\.

Γ\\Gammais compiled bottom\-up into an SDDα\\alphathat is smooth, decomposable, and deterministic\[[17](https://arxiv.org/html/2608.12961#bib.bib17),[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\. The role\-pinning caveat applies to theLinksclause: ELK derivesE⊑∃R\.CE\\sqsubseteq\\exists R\.C\(existential, “some witness”\);Mooseencodes the propositional clauseE⁡\(a\)∧R⁡\(a,b\)→C⁡\(b\)E\(a\)\\wedge R\(a,b\)\\to C\(b\), which is universal on the named pair\. Soundness depends onΔ\\Deltabeing closed and on role atoms over𝖲𝗂𝗀Ro\\mathsf\{Sig\}^\{o\}\_\{R\}being pinned by evidence \(aMoose\-specific encoding choice for the finite\-named\-domain regime, not an ELK theorem\)\. The differentiable WMC layer traversesα\\alphaand evaluates𝖶𝖬𝖢⁡\(α,w\)\\mathsf\{WMC\}\(\\alpha;w\)by the standard smooth/decomposable/deterministic recursion \([Equation8](https://arxiv.org/html/2608.12961#Pt0.A3.E8)in[Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3)\), with literal weightswwread from[Table1](https://arxiv.org/html/2608.12961#S3.T1)\. 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𝐞\\mathbf\{e\}clamps the literal weight of every observed atom to00or11\.

### 3\.3Closure axioms outside the EL profile

OWL EL is open\-world and lacks both right\-hand\-side disjunction and cardinality constructors\[[5](https://arxiv.org/html/2608.12961#bib.bib5)\], so the covering axiom⊤⊑D0⊔⋯⊔DK−1\\top\\sqsubseteq D\_\{0\}\\sqcup\\dots\\sqcup 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, observingEven​\(a\)\\textsf\{Even\}\(a\)without closure leaves the digit posterior uninformative\)\. We therefore optionally append a finite set of*closure axioms*Φclos\\Phi\_\{\\textsf\{clos\}\}toΓEL\\Gamma\_\{\\textsf\{EL\}\}on each modeller\-declared exhaustive familyℱ\\mathcal\{F\}: pairwise disjointness, the covering clause⋁iDi​\(a\)\\bigvee\_\{i\}D\_\{i\}\(a\), and \(when eachDiD\_\{i\}carries a distinguishing property profileπi\\pi\_\{i\}\) profile\-keyed reverse implications\. We write these three jointly manipulated components asΦclos=Φmutex∪Φcover∪Φprofile\\Phi\_\{\\textsf\{clos\}\}=\\Phi\_\{\\textsf\{mutex\}\}\\cup\\Phi\_\{\\textsf\{cover\}\}\\cup\\Phi\_\{\\textsf\{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\\Phi\_\{\\textsf\{clos\}\}at the propositional level, so the same compilation yieldsαEL\\alpha\_\{\\textsf\{EL\}\}orαclos\\alpha\_\{\\textsf\{clos\}\}with no method change\. This absorption is free at the CNF level \(Φclos\\Phi\_\{\\textsf\{clos\}\}adds at most\(K2\)​m\+\(K\+1\)​m\\binom\{K\}\{2\}m\+\(K\{\+\}1\)mclauses per declared family:\(K2\)​m\\binom\{K\}\{2\}mmutex,mmcovering, and up toK​mKmprofile\-keyed reverse implications\), but the polynomial saturation\-closure bound of[Theorem0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2)applies to the EL Horn fragment only and does not transfer toΓEL∪Φclos\\Gamma\_\{\\textsf\{EL\}\}\\cup\\Phi\_\{\\textsf\{clos\}\}: covering disjunctions can raise the primal\-graph treewidth, and SDD compilation is worst\-case exponential in\|Γ\|\|\\Gamma\|with aO⁡\(\|Γ\|⋅2w\)O\(\|\\Gamma\|\\cdot 2^\{w\}\)bound under treewidthww\([Section0\.D\.5](https://arxiv.org/html/2608.12961#Pt0.A4.SS5)\); inference remainsO⁡\(\|α\|\)O\(\|\\alpha\|\)in the SDD node count regardless \([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)\. 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 viann​\(⋅\)\\textsf\{nn\}\(\\cdot\), 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](https://arxiv.org/html/2608.12961#bib.bib41),[29](https://arxiv.org/html/2608.12961#bib.bib29)\]and is implemented by the BEARS / NeSyDM wrappers of §[3\.4](https://arxiv.org/html/2608.12961#S3.SS4)\.[Section0\.B\.1](https://arxiv.org/html/2608.12961#Pt0.A2.SS1)summarizes the assumptions introduced by each pipeline component and what each concedes against open\-world semantics\.

### 3\.4Inference 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 isL⁡\(θ,𝐱,𝐞\)=−log⁡𝖶𝖬𝖢⁡\(α,pθ​\(𝐱\),𝐞\)L\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\)=\-\\log\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)\[[51](https://arxiv.org/html/2608.12961#bib.bib51)\], which coincides with the DeepProbLog marginal loss on this Horn theory by[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)\. The conditional posteriorPθ​\(C​\(a\)∣𝐱,𝐞\)P\_\{\\theta\}\(C\(a\)\\mid\\mathbf\{x\},\\mathbf\{e\}\)is the ratio of two WMCs withC⁡\(a\)C\(a\)clamped vs\. left free; the perception\-free entailment query𝒪∪𝐞⊧C⁡\(a\)\\mathcal\{O\}\\cup\\mathbf\{e\}\\models C\(a\)holds iff𝖶𝖬𝖢\(α;w1/2,𝐞∪\{C\(a\):=𝖿𝖺𝗅𝗌𝖾\}\)=0\\mathsf\{WMC\}\(\\alpha;w\_\{1/2\},\\mathbf\{e\}\\cup\\\{C\(a\)\{:=\}\\mathsf\{false\}\\\}\)=0\(the12\\tfrac\{1\}\{2\}\-weighted SDD acts as a satisfiability oracle\)\. All three run inO⁡\(\|α\|\)O\(\|\\alpha\|\)\([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4),[Equations11](https://arxiv.org/html/2608.12961#Pt0.A5.E11),[12](https://arxiv.org/html/2608.12961#Pt0.A5.E12)and[13](https://arxiv.org/html/2608.12961#Pt0.A5.E13)in[Section0\.E\.1](https://arxiv.org/html/2608.12961#Pt0.A5.SS1)\)\. The compilation algorithm is independent of the perception’s output distribution, so RS\-aware methods \(§[2\.2](https://arxiv.org/html/2608.12961#S2.SS2)\) plug in by replacingpθ​\(𝐱\)p\_\{\\theta\}\(\\mathbf\{x\}\)inwwwithout modifyingα\\alpha\.Moose\+BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]trains aKK\-encoder ensemble diversified by Kullback–Leibler \(KL\) divergence against the running ensemble average;Moose\+NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]replaces∏ipθ​\(ci∣𝐱\)\\prod\_\{i\}p\_\{\\theta\}\(c\_\{i\}\\mid\\mathbf\{x\}\)with a masked discrete\-diffusionqθq\_\{\\theta\}, evaluated with both the REINFORCE leave\-one\-out \(RLOO\) estimator\[[28](https://arxiv.org/html/2608.12961#bib.bib28)\]and an exact\-WMC gradient estimator\. Wrapper losses with hyperparameters are in[Section0\.E\.3](https://arxiv.org/html/2608.12961#Pt0.A5.SS3)\.

## 4Correctness and complexity

This section states the four theorems that constitute the formal contribution ofMoose: 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ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}and polynomial\-time Sat decidability\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\) is reused unchanged from the ELK literature and re\-mechanized in our Lean library \([Section0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.SS1)\)\. Proofs, Lean theorem names, and audit\-surface details are deferred to[Appendices0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)and[0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)\.

#### Notation\.

𝒪\\mathcal\{O\}ranges overℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontologies \(OWL 2 EL minus datatype properties and concrete domains\)\.𝖲𝖺𝗍⁡\(𝒪,C,D\)\\mathsf\{Sat\}\(\\mathcal\{O\},C,D\)holds iff ELK derivesC⊑DC\\sqsubseteq Dfrom𝒪\\mathcal\{O\}\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\. A*world*M:𝒪→\{0,1\}M:\\mathcal\{O\}\\to\\\{0,1\\\}selects the sub\-ontology𝗌𝖾𝗅⁡\(𝒪,M\):=\{α∈𝒪:M⁡\(α\)=1\}\\mathsf\{sel\}\(\\mathcal\{O\},M\):=\\\{\\alpha\\in\\mathcal\{O\}:M\(\\alpha\)=1\\\}\(*sel*short for*selectedAxioms*in the Lean library\)\. For a weightw:𝒪×\{0,1\}→ℚw:\\mathcal\{O\}\\times\\\{0,1\\\}\\to\\mathbb\{Q\}, the rational DISPONTE marginal\[[44](https://arxiv.org/html/2608.12961#bib.bib44)\]is

𝖯ℚ\(𝒪,C,D,w\):=∑M:𝒪→\{0,1\}𝟏\[𝖲𝖺𝗍\(𝗌𝖾𝗅\(𝒪,M\),C,D\)\]⋅∏α∈𝒪w\(α,M\(α\)\);\\mathsf\{P\}^\{\\mathbb\{Q\}\}\(\\mathcal\{O\},C,D,w\)\\;:=\\;\\sum\_\{M:\\mathcal\{O\}\\to\\\{0,1\\\}\}\\mathbf\{1\}\[\\,\\mathsf\{Sat\}\(\\mathsf\{sel\}\(\\mathcal\{O\},M\),C,D\)\\,\]\\cdot\\prod\_\{\\alpha\\in\\mathcal\{O\}\}w\(\\alpha,M\(\\alpha\)\);𝖯⁡\(𝒪,C,D,w\)\\mathsf\{P\}\(\\mathcal\{O\},C,D,w\)denotes the natural\-valued analogue whenwwtakes values inℕ\\mathbb\{N\}\.𝖼𝗆𝗉⁡\(𝒪,C,D\)\\mathsf\{cmp\}\(\\mathcal\{O\},C,D\)\(*cmp*short for*compileSat*\) is the verified Shannon\-tree SDD produced by the algorithm of §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2), and𝖶𝖬𝖢ℚ​\(t,w\)\\mathsf\{WMC\}^\{\\mathbb\{Q\}\}\(t,w\)is its rational weighted model count\.

###### Theorem 4\.1\(Verified SDD encoding\)

For everyℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology𝒪\\mathcal\{O\}and conceptsC,DC,D, there exists an SDD treettsuch that

1. 1\.model⁡\(t,M\)⇔𝖲𝖺𝗍⁡\(𝗌𝖾𝗅⁡\(𝒪,M\),C,D\)\\mathrm\{model\}\(t,M\)\\iff\\mathsf\{Sat\}\(\\mathsf\{sel\}\(\\mathcal\{O\},M\),C,D\)for every worldM:𝒪→\{0,1\}M:\\mathcal\{O\}\\to\\\{0,1\\\};
2. 2\.for every weightww,𝖶𝖬𝖢⁡\(t,w\)=𝖯⁡\(𝒪,C,D,w\)\\mathsf\{WMC\}\(t,w\)=\\mathsf\{P\}\(\\mathcal\{O\},C,D,w\);
3. 3\.\|t\|=2\|𝒪\|\+1−1\|t\|\\,=\\,2^\{\|\\mathcal\{O\}\|\+1\}\-1\.

[Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)is the formal contract ofMoose’s compilation step: the SDD’s models are exactly the worlds whose selected sub\-ontology ELK\-entailsC⊑DC\\sqsubseteq D, the SDD’s WMC is the DISPONTE marginal under arbitrary weights, and the worst\-case size is the explicit2\|𝒪\|\+1−12^\{\|\\mathcal\{O\}\|\+1\}\-1bound of the Shannon expansion \([Section0\.D\.5](https://arxiv.org/html/2608.12961#Pt0.A4.SS5)\)\. Lean proof: see[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)\.

###### Theorem 4\.2\(Rational DISPONTE correspondence\)

For everyℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology𝒪\\mathcal\{O\}, every conceptsC,DC,D, and every rational weightww,

𝖶𝖬𝖢ℚ​\(𝖼𝗆𝗉⁡\(𝒪,C,D\),w\)=𝖯ℚ​\(𝒪,C,D,w\)\.\\mathsf\{WMC\}^\{\\mathbb\{Q\}\}\\\!\\bigl\(\\mathsf\{cmp\}\(\\mathcal\{O\},C,D\),\\,w\\bigr\)\\;=\\;\\mathsf\{P\}^\{\\mathbb\{Q\}\}\(\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib44)\]\(at the uniform priorw≡12w\\equiv\\tfrac\{1\}\{2\},𝖶𝖬𝖢ℚ=0\\mathsf\{WMC\}^\{\\mathbb\{Q\}\}=0iff no world’s sub\-ontology entailsC⊑DC\\sqsubseteq D\), and lifts that phrasing from the propositional encoding to the verified compiled circuit\. Lean proof: see[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)\.

###### Theorem 4\.3\(SCC compositional theorem, Sat level\)

Let𝒪=𝒪1⊎𝒪2\\mathcal\{O\}=\\mathcal\{O\}\_\{1\}\\uplus\\mathcal\{O\}\_\{2\}with disjoint signatures, both components nominal\-free and range\-chain\-safe,𝒪2\\mathcal\{O\}\_\{2\}consistent \(¬𝖲𝖺𝗍⁡\(𝒪2,⊤,⊥\)\\neg\\,\\mathsf\{Sat\}\(\\mathcal\{O\}\_\{2\},\\top,\\bot\)\), andC,DC,Dnominal\-free withC,DC,Din the signature of𝒪1\\mathcal\{O\}\_\{1\}\. Then

𝖲𝖺𝗍⁡\(𝒪1⊎𝒪2,C,D\)⇔𝖲𝖺𝗍⁡\(𝒪1,C,D\)\.\\mathsf\{Sat\}\(\\mathcal\{O\}\_\{1\}\\uplus\\mathcal\{O\}\_\{2\},C,D\)\\;\\iff\\;\\mathsf\{Sat\}\(\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib6)\]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:[Appendices0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)and[0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)\.

###### Theorem 4\.4\(Per\-SCC posterior equivalence\)

Under the hypotheses of[Theorem4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3), for any uniform per\-axiom priorw≡cw\\equiv cwithc\>0c\>0, the per\-SCC and joint DISPONTE posteriors coincide\. In the unnormalized counting casew≡1w\\equiv 1,

𝖯ℚ​\(𝒪1⊎𝒪2,C,D,w\)=𝖯ℚ​\(𝒪1,C,D,w\)⋅2\|𝒪2\|\.\\mathsf\{P\}^\{\\mathbb\{Q\}\}\(\\mathcal\{O\}\_\{1\}\\uplus\\mathcal\{O\}\_\{2\},C,D,w\)\\;=\\;\\mathsf\{P\}^\{\\mathbb\{Q\}\}\(\\mathcal\{O\}\_\{1\},C,D,w\)\\cdot 2^\{\|\\mathcal\{O\}\_\{2\}\|\}\.\(3\)

The multiplicative2\|𝒪2\|2^\{\|\\mathcal\{O\}\_\{2\}\|\}from the irrelevant SCC cancels under posterior normalization, and the same cancellation extends the identity to anyc\>0c\>0after factoring outc\|𝒪1\|\+\|𝒪2\|c^\{\|\\mathcal\{O\}\_\{1\}\|\+\|\\mathcal\{O\}\_\{2\}\|\}\. This is the WMC\-level analogue of[Theorem4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3): per\-SCC compilation is posterior\-faithful\. Lean proof:[Appendices0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)and[0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)\.

The closure\-augmented variant of the SDD \(which materializes the per\-individual partition constraints on declared exhaustive families\) satisfies an analogous correctness theorem \([Theorem0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3), appendix\)\. Inference is linear in\|𝖼𝗆𝗉⁡\(𝒪,C,D\)\|\|\\mathsf\{cmp\}\(\\mathcal\{O\},C,D\)\|\[[17](https://arxiv.org/html/2608.12961#bib.bib17),[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4), appendix\)\. All proofs and the DeepProbLog equivalence[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)are in[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4); the implementation index in[Section0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)cross\-references every paper claim with its formalized counterpart\.

## 5Research questions and experiments

We evaluateMooseon two benchmarks: the MNIST\-with\-ontology benchmark we developed for this work \([Example1](https://arxiv.org/html/2608.12961#Thmexample1)\), instantiated under three supervision regimes \(atomic property literals, relational∃R\.C\\exists R\.Cevidence, and role\-chain evidence\); and the Pizzaïolo dataset\[[10](https://arxiv.org/html/2608.12961#bib.bib10)\]of4,8004\{,\}800synthetic pizza images generated to conform to the published OWL pizza ontology\[[46](https://arxiv.org/html/2608.12961#bib.bib46)\], 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\|Δ\|\|\\Delta\|, and the supplied evidence\.

We address five research questions\.RQ1–RQ3test latent digit recovery on𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}as the supervision signal grows from a single individual with unary property literals \(RQ1\), to a pair of individuals connected by an observedr⁡\(a,b\)r\(a,b\)role literal under an∃R\.C\\exists R\.Caxiom \(RQ2\), to a pair connected by observed role literals only through an ELK\-derived role\-chain consequence \(RQ3\)\.RQ4tests transfer to the pre\-existing third\-party OWL pizza ontology, restricted to its EL fragment \(Pizzaïolo, §[5\.2](https://arxiv.org/html/2608.12961#S5.SS2)\)\.RQ5asks 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\),Mooseon the EL theory alone \(the DPL surface,[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)\),Moosewith closureΦclos\\Phi\_\{\\textsf\{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](https://arxiv.org/html/2608.12961#bib.bib41),[29](https://arxiv.org/html/2608.12961#bib.bib29)\]\.

### 5\.1The MNIST ontology and supervision regimes

A single OWL EL ontology𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}\(1414concepts,22roles,7676axioms; full listing in[Section0\.F\.2](https://arxiv.org/html/2608.12961#Pt0.A6.SS2)\) is used in all three MNIST experiments; the experiments differ only in\|Δ\|\|\\Delta\|and the evidence regime, never in the TBox\. ELK saturation derives the chain consequenceDi⊑∃plus\_two\.D\(i\+2\)mod10D\_\{i\}\\sqsubseteq\\exists\\textsf\{plus\\\_two\}\.\\,D\_\{\(i\+2\)\\bmod 10\}from the axiomsucc∘succ⊑plus\_two\\textsf\{succ\}\\circ\\textsf\{succ\}\\sqsubseteq\\textsf\{plus\\\_two\}at compile time\. The compiled SDD has14​m\+2​m214m\+2m^\{2\}ground atoms\. A small convolutional neural network \(CNN\)fθf\_\{\\theta\}\(22conv blocks \+22fully\-connected layers, weight\-shared across individuals;[Section0\.F\.3](https://arxiv.org/html/2608.12961#Pt0.A6.SS3)\) maps each image to per\-atom probabilities; training minimizesℒ⁡\(θ\)=−log⁡𝖶𝖬𝖢⁡\(αclos,pθ​\(𝐱\),𝐞\)\\mathcal\{L\}\(\\theta\)=\-\\log\\mathsf\{WMC\}\(\\alpha\_\{\\text\{clos\}\};p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)with Adam, batch3232,55seeds; per\-regime learning rates and epoch counts are in[Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\. EL\-only ablations omitΦclos\\Phi\_\{\\textsf\{clos\}\}and train againstαEL\\alpha\_\{\\text\{EL\}\}, recovering the DPL loss \([Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)\)\.Exp\. 1 \(atomic, RQ1\)usesΔ=\{a\}\\Delta=\\\{a\\\}withnobs∈\{1,2,3\}n\_\{\\text\{obs\}\}\\in\\\{1,2,3\\\}unary literals over𝖲𝗂𝗀Co=\{Even,Odd,Prime,Composite\}\\mathsf\{Sig\}^\{o\}\_\{C\}=\\\{\\textsf\{Even\},\\textsf\{Odd\},\\textsf\{Prime\},\\textsf\{Composite\}\\\}\.Exp\. 2 \(relational, RQ2\)usesΔ=\{a,b\}\\Delta=\\\{a,b\\\}with the role atomsucc​\(a,b\)\\textsf\{succ\}\(a,b\)asserted \(digits satisfydigit​\(b\)=\(digit​\(a\)\+1\)mod10\\textsf\{digit\}\(b\)=\(\\textsf\{digit\}\(a\)\{\+\}1\)\\bmod 10\) plusnobs∈\{1,2,3\}n\_\{\\text\{obs\}\}\\in\\\{1,2,3\\\}primality literals\.Exp\. 3 \(role chain, RQ3\)flips the asserted role toplus\_two​\(a,c\)\\textsf\{plus\\\_two\}\(a,c\)and widens the unary pool to parity and primality; the only chain fromaatoccis the NF7\-derived consequence above\. The digit family is declared exhaustive at every individual;Φclos\\Phi\_\{\\textsf\{clos\}\}supplies pairwise disjointness, covering, and reverse\-implication clauses\. Some property profiles uniquely identify the latent digit \(e\.g\.Even​\(a\)∧Prime​\(a\)\\textsf\{Even\}\(a\)\\wedge\\textsf\{Prime\}\(a\)pinsD2D\_\{2\}\), while others leave it ambiguous \(e\.g\.Even​\(a\)\\textsf\{Even\}\(a\)alone admits\{D0,D2,D4,D6,D8\}\\\{D\_\{0\},D\_\{2\},D\_\{4\},D\_\{6\},D\_\{8\}\\\}\); RScons\{\}\_\{\\text\{cons\}\}on the ambiguous cases measures confident commitment to a wrong digit\.

### 5\.2Experiment 4: Pizzaïolo \(RQ4\)

Pizzaïolo\[[10](https://arxiv.org/html/2608.12961#bib.bib10)\]provides4,8004\{,\}800synthetic pizza images\. The canonical pizza ontology contains non\-EL constructs \(universal restrictions onhasTopping, complement\-based definitions such asVegetarianPizza≡Pizza⊓¬∃⁡hasTopping\.MeatTopping⊓¬∃⁡hasTopping\.FishTopping\\textsf\{VegetarianPizza\}\\equiv\\textsf\{Pizza\}\\sqcap\\neg\\exists\\textsf\{hasTopping\}\.\\textsf\{MeatTopping\}\\sqcap\\neg\\exists\\textsf\{hasTopping\}\.\\textsf\{FishTopping\}, and cardinality onNumberedPizza\); 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\}\\\{\\textsf\{Mushroom\},\\textsf\{Cajun\},\\textsf\{Capricciosa\},\\textsf\{FourSeasons\}\\\}over1616topping concepts, with conjunctive per\-pizza axioms \(e\.g\.Capricciosa⊑Ham⊓Anchovy⊓Olive⊓Peperonata\\textsf\{Capricciosa\}\\sqsubseteq\\textsf\{Ham\}\\sqcap\\textsf\{Anchovy\}\\sqcap\\textsf\{Olive\}\\sqcap\\textsf\{Peperonata\}\), pairwise pizza disjointness, and disjointness axiomsP⊓T⊑⊥P\\sqcap T\\sqsubseteq\\botfor every toppingTToutsidePP’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 Areveals pizza identity; toppings are latent\. We test distribution shift via an OOD split: the four training pizzas all carryAnchovyandOlivetogether, 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 Breveals one of four property\-class atoms \(NonVegetarianPizza,SpicyPizza,RealFrenchPizza,VegetarianPizza\); revealingNonVegetarianPizzaleaves\{Cajun,Capricciosa,FourSeasons\}\\\{\\textsf\{Cajun\},\\textsf\{Capricciosa\},\\textsf\{FourSeasons\}\\\}indistinguishable \(a 3\-way RS over pizza identity\)\.Track C\(theis\_spicytask in the codebase\) adds four axiomsTi⊑SpicyToppingT\_\{i\}\\sqsubseteq\\textsf\{SpicyTopping\}forTi∈\{Jalapeno,Peperonata,PeperoniSausage,Prawn\}T\_\{i\}\\in\\\{\\textsf\{Jalapeno\},\\textsf\{Peperonata\},\\textsf\{PeperoniSausage\},\\textsf\{Prawn\}\\\}together withSpicyTopping≡SpicyPizza\\textsf\{SpicyTopping\}\\equiv\\textsf\{SpicyPizza\}\(two GCIs; hereSpicyToppingacts as a label\-class denoting “pizza with a spicy topping”\)\. Symbolic supervisionSpicyPizza​\(a\)\\textsf\{SpicyPizza\}\(a\)forcesSpicyTopping​\(a\)\\textsf\{SpicyTopping\}\(a\)but the EL theory leaves the witness ambiguous over24=162^\{4\}\{=\}16topping subsets \(the multi\-witness regime BEARS/NeSyDM target\)\. We train the perception CNN from scratch with batch size3232,55seeds, and6060epochs on Tracks A and B \(Track C uses1515epochs\); per\-method hyperparameters and the NeSyDM\(γc,γh\)\(\\gamma\_\{c\},\\gamma\_\{h\}\)sweep results are in[Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\.

### 5\.3Baselines, metrics, and results

We compareMooseagainst seven baselines\.Independent\(BCE on observed atoms\) is the NeSy\-free lower bound\.Semantic Loss\[[51](https://arxiv.org/html/2608.12961#bib.bib51)\]shares the−log⁡𝖶𝖬𝖢\-\\log\\mathsf\{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](https://arxiv.org/html/2608.12961#S3.SS2)\.DeepProbLog\[[39](https://arxiv.org/html/2608.12961#bib.bib39)\]hand\-codes each MNIST regime as a ProbLog program with onenn​\(⋅\)\\textsf\{nn\}\(\\cdot\)digit directive; by[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)DPL andMoosecompute the same loss on the same Horn theory, though that directive is an annotated disjunction, so DPL is not closure\-free\.Moose\+BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]keeps the factorized perception andαclos\\alpha\_\{\\text\{clos\}\}but replaces the single encoder withK=5K\{=\}5diversified encoders\.Moose\+NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]replaces the factorized extractor with a masked\-diffusion concept distribution; we evaluate both RLOO and exact\-WMC gradient estimators\.LTN\[[7](https://arxiv.org/html/2608.12961#bib.bib7)\]substitutes a fuzzy product T\-norm;ELEmbeddings\[[36](https://arxiv.org/html/2608.12961#bib.bib36),[54](https://arxiv.org/html/2608.12961#bib.bib54)\]embeds the EL ontology into ball geometries with a classifier head; both are detailed in[Section0\.E\.4](https://arxiv.org/html/2608.12961#Pt0.A5.SS4)\.

Metrics\.The headline tables[Tables2](https://arxiv.org/html/2608.12961#S5.T2)and[3](https://arxiv.org/html/2608.12961#S5.T3)report the regime’s principal accuracy and ECE, the expected calibration error binned by predicted confidence\[[23](https://arxiv.org/html/2608.12961#bib.bib23)\]\. The two ontologies do not admit the same accuracy metric\. On MNIST the digit family is declared exhaustive and we reportAccF\\text\{Acc\}\_\{F\},*family\-argmax*accuracy: per individual, the argmax of the WMC posterior over that family\. On Pizzaïolo we reportAccC\\text\{Acc\}\_\{C\}, per\-atom accuracy on the latent slice, since Track C declares no exhaustive family and the decode degenerates on the other two \([Section0\.F\.7](https://arxiv.org/html/2608.12961#Pt0.A6.SS7)\)\. The full per\-regime breakdown \([Table9](https://arxiv.org/html/2608.12961#Pt0.A6.T9),[Section0\.F\.6](https://arxiv.org/html/2608.12961#Pt0.A6.SS6)\) 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\)\{\}\_\{\\text\{cons\}\}=\\mathrm\{Conf\}\\cdot\(1\{\-\}\\mathrm\{Acc\}\_\{F\}\)on the latent family\-argmax \(higher = more confident commitment to a wrong shortcut; on Pizzaïolo the complement usesAccC\\text\{Acc\}\_\{C\}, and on Track C it is not applicable\); per\-atom accuracyAccatom\\text\{Acc\}\_\{\\text\{atom\}\}on the latent signature; and the macro\-averaged per\-concept F1,F1macro\\text\{F1\}\_\{\\text\{macro\}\}\. A paired significance analysis of the headline comparisons over2020seeds is given in[Section0\.F\.8](https://arxiv.org/html/2608.12961#Pt0.A6.SS8), and a learning\-rate sensitivity analysis in[Section0\.F\.5](https://arxiv.org/html/2608.12961#Pt0.A6.SS5)\.

Table 2:Principal accuracy \(%, mean±\\pms\.d\. over55seeds\. MNIST Experiments 1–3 \([Section5\.1](https://arxiv.org/html/2608.12961#S5.SS1)\), Pizzaïolo Tracks A–C \([Section5\.2](https://arxiv.org/html/2608.12961#S5.SS2)\); Track A is the out\-of\-distribution split\. Metric:AccF\\text\{Acc\}\_\{F\}\(family\-argmax\) on MNIST,AccC\\text\{Acc\}\_\{C\}\(per\-atom, latent slice\) on Pizzaïolo; compare only within a column \([Section0\.F\.7](https://arxiv.org/html/2608.12961#Pt0.A6.SS7)\)\. Operative theory:ΓEL\+Φclos\\Gamma\_\{\\textsf\{EL\}\}\{\+\}\\Phi\_\{\\textsf\{clos\}\}for theMooserows on MNIST,ΓEL\\Gamma\_\{\\textsf\{EL\}\}elsewhere, none for Independent \(§[3\.3](https://arxiv.org/html/2608.12961#S3.SS3)\)\. Bold = column\-best;†= highest but not significant \([Section0\.F\.8](https://arxiv.org/html/2608.12961#Pt0.A6.SS8)\); DeepProbLog on Pizzaïolo is not a separate run \([Section0\.F\.6](https://arxiv.org/html/2608.12961#Pt0.A6.SS6)\)\. FullAccatom\\text\{Acc\}\_\{\\text\{atom\}\}, NLL, RScons\{\}\_\{\\text\{cons\}\}, andF1macro\\text\{F1\}\_\{\\text\{macro\}\}in[Table9](https://arxiv.org/html/2608.12961#Pt0.A6.T9)\.Table 3:Expected calibration error ECE \(%, mean±\\pms\.d\.\)\. Lower is better\. Same baselines, seed counts, operative theories, and metric conventions as[Table2](https://arxiv.org/html/2608.12961#S5.T2); bold = column\-best per regime, not significance\-tested\. Per\-regimeAccatom\\text\{Acc\}\_\{\\text\{atom\}\}, NLL, RScons\{\}\_\{\\text\{cons\}\}, andF1macro\\text\{F1\}\_\{\\text\{macro\}\}alongside ECE are in[Table9](https://arxiv.org/html/2608.12961#Pt0.A6.T9)\([Section0\.F\.6](https://arxiv.org/html/2608.12961#Pt0.A6.SS6)\)\.#### Findings on Experiments 1–3 \(RQ1–3, RQ5\)\.

At\|Δ\|=1\|\\Delta\|\{=\}1\(Exp\. 1\)Mooseleads DeepProbLog onAccF\\text\{Acc\}\_\{F\}\(48\.148\.1vs\.42\.142\.1\)\. Independent stays near random \(AccF=13\.2\\text\{Acc\}\_\{F\}=13\.2\)\. BEARS cuts ECE from10\.610\.6to3\.93\.9at no cost to accuracy; at\|Δ\|=1\|\\Delta\|\{=\}1there is little diversifiable structure left for the ensemble to exploit\. NeSyDM matchesMooseonAccF\\text\{Acc\}\_\{F\}\(46\.646\.6and49\.449\.4for the RLOO and exact estimators vs\.48\.148\.1\)\. On the relational and role\-chain regimes \(Exps\. 2–3\)Moosedominates DeepProbLog by tens of points onAccF\\text\{Acc\}\_\{F\}\(74\.674\.6vs\.38\.938\.9on Exp\. 2;96\.196\.1vs\.59\.659\.6on Exp\. 3\): the EL\-aware Links extractor propagates evidence across the\|Δ\|=2\|\\Delta\|\{=\}2ground individuals, but the closure clausesΦclos\\Phi\_\{\\textsf\{clos\}\}are what make this signal learnable\. The ablation in[Section0\.F\.10](https://arxiv.org/html/2608.12961#Pt0.A6.SS10)shows the base WMC objective falling to17\.417\.4and9\.49\.4\(near chance\) onceΦclos\\Phi\_\{\\textsf\{clos\}\}is removed, so the EL compilation supplies the structure andΦclos\\Phi\_\{\\textsf\{clos\}\}the identifying constraint, with reasoning\-shortcut mitigations partially substituting for the latter \([Table13](https://arxiv.org/html/2608.12961#Pt0.A6.T13)\)\. BEARS reduces RScons\{\}\_\{\\text\{cons\}\}\([Table9](https://arxiv.org/html/2608.12961#Pt0.A6.T9),[Section0\.F\.6](https://arxiv.org/html/2608.12961#Pt0.A6.SS6)\) but gives up a few points of accuracy on Exp\. 3 \(89\.289\.2vs\.96\.196\.1\); NeSyDM lags even at tuned\(γc,γh\)\(\\gamma\_\{c\},\\gamma\_\{h\}\)\. LTN and ELEmbeddings under\-perform onAccF\\text\{Acc\}\_\{F\}\(14\.514\.5and34\.834\.8on 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, leavesMoose’s accuracy essentially unchanged while NeSyDM collapses to near\-chance \([Section0\.F\.9](https://arxiv.org/html/2608.12961#Pt0.A6.SS9)\)\.

#### 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\}\\\{\\textsf\{Anchovy\},\\textsf\{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 theMoosefamily clusters around6767–7272% onAccC\\text\{Acc\}\_\{C\}\([Table2](https://arxiv.org/html/2608.12961#S5.T2)\)\. Track B is the canonical RS test \(3\-way symbolic ambiguity: a property\-class observation leaves three pizzas indistinguishable\)\. PlainMoose\-WMC commits to a single constraint\-consistent latent \(“Mechanism A” of\[[41](https://arxiv.org/html/2608.12961#bib.bib41)\]\); BEARS liftsAccC\\text\{Acc\}\_\{C\}from84\.584\.5to87\.987\.9via 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\_spicydisjunction\) is the multi\-witness regime NeSyDM was designed for: among theMoosevariants BEARS leads onAccC\\text\{Acc\}\_\{C\}\(84\.284\.2vs\.81\.081\.0for plainMoose\-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,[Section0\.F\.8](https://arxiv.org/html/2608.12961#Pt0.A6.SS8)\) at higher ECE \(14\.114\.1\)\. On both Track B and Track C theMoose\-family results separate along an argmax\-vs\-calibration axis \(BEARS leads accuracy, NeSyDM leads ECE\)\. These mitigation effects are sizeable rather than marginal: paired over2020seeds, BEARS significantly exceeds plainMoose\-WMC on both Track B and Track C, and NeSyDM significantly exceeds it on the Track A OOD split \([Section0\.F\.8](https://arxiv.org/html/2608.12961#Pt0.A6.SS8)\)\. 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 plainMooseis 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\.

## 6Conclusion and outlook

Moosecompiles 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 \([Section0\.F\.10](https://arxiv.org/html/2608.12961#Pt0.A6.SS10)\); 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\|\\Delta\|=2; the compiled SDD grows empirically as≈\|Δ\|2\.9\\approx\|\\Delta\|^\{2\.9\}with a40×40\\timescompile\-time jump at\|Δ\|=4\|\\Delta\|=4\([Section0\.D\.5](https://arxiv.org/html/2608.12961#Pt0.A4.SS5)\)\. 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\.*\(ii\) Finite named domain\.*Mooselearns over a given finite ABox of named individuals \([Definition1](https://arxiv.org/html/2608.12961#Thmdefinition1)\); this defines the ABox\-supervised task rather than weakening it, but it does not by itself perform open\-domain inference over unnamed individuals\.*\(iii\) Role\-pinning\.*Soundness of theLinksencoding treats an existential as universal on the named pair, assuming role atoms over𝖲𝗂𝗀Ro\\mathsf\{Sig\}^\{o\}\_\{R\}are pinned by evidence \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2), Stage 7\), aMoose\-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](https://arxiv.org/html/2608.12961#bib.bib37)\]for larger ABox domains,𝒜​ℒ​𝒞\\mathcal\{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 atomsR⁡\(a,b\)R\(a,b\)that the weight map \([Table1](https://arxiv.org/html/2608.12961#S3.T1)\) currently fixes at12\\tfrac\{1\}\{2\}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:

#### Declaration of use of Generative AI\.

A large language model assisted with copy\-editing and with Lean 4 transcription of the proofs in[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)\. 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\)\. pp\. 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](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 Genetics25\(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\)\. pp\. 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\)\. pp\. 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 Intelligence303, 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 Reasoning52\(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](https://hal.science/hal-04401953)\(2024\), dataset DOI:[https://doi\.org/10\.5281/zenodo\.10165941](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 Intelligence33\(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, pp\. 447–458 \(2014\)
- \[13\]Ceylan, İ\.İ\., Peñaloza, R\.: The bayesian ontology languageℬ​ℰ​ℒ\\mathcal\{BEL\}\. Journal of Automated Reasoning58\(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 Intelligence172\(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 Learning110\(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 Engineering37\(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, pp\. 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 Learning112\(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\)\. pp\. 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 Research17, 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 Informatics121, 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\)\. pp\. 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\)\. pp\. 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\. Database2021, 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ℰ​ℒ\\mathcal\{EL\}ontologies\. Journal of Automated Reasoning53\(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, pp\. 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, pp\. 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 Intelligence6, 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\. Bioinformatics38\(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\)\. pp\. 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\. CoRRabs/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\)\. pp\. 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\. CoRRabs/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\)\. pp\. 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 preprintabs/2412\.08739\(2024\),[https://arxiv\.org/abs/2412\.08739](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\)\. pp\. 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 Web6\(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 Biotechnology25\(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](https://github.com/owlcs/pizza-ontology), manchester University tutorial OWL ontology
- \[47\]Tarjan, R\.: Depth\-first search and linear graph algorithms\. SIAM Journal on Computing1\(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, pp\. 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\. Genetics224\(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, pp\. 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, pp\. 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\. Bioinformatics39\(1\), btac811 \(2023\)\. https://doi\.org/10\.1093/bioinformatics/btac811

## Appendix 0\.Aℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}syntax, semantics, and ELK calculus

This appendix collects the formal foundations on whichMooseis built: the syntax and semantics of theℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}profile of OWL 2 EL, the Baader–Brandt–Lutz \(BBL\) normal\-form rules NF1–NF7\[[5](https://arxiv.org/html/2608.12961#bib.bib5)\], and the ELK saturation calculus\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]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;[Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)contains the full proofs of §[4](https://arxiv.org/html/2608.12961#S4)\.

#### The Lean library\.

All formalized statements cited in this paper live in the Lean 4 libraryELKSDD, distributed with the supplementary release at[https://github\.com/bio\-ontology\-research\-group/moose\-iswc/](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](https://arxiv.org/html/2608.12961#bib.bib6)\]\), and theELKSDD\.ELandELKSDD\.MiniELfragments for testing purposes\. The DeepProbLog equivalence layer lives in a companion library under namespaceMoose\. Inline references of the form<namespace\>\.<theorem\>point to a specific theorem; the index in[Section0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)cross\-references every paper claim with its mechanized counterpart\. Every theorem listed in[Section0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)is*audit\-clean*: its proof depends only on the standard Lean foundation\{propext,Classical\.choice,Quot\.sound\}\\\{\\texttt\{propext\},\\,\\texttt\{Classical\.choice\},\\,\\texttt\{Quot\.sound\}\\\}and the formalization contains zerosorryoradmit\. An audit pass in each library runs\#print axiomson every paper\-cited theorem at build time and reports its dependency set\.

#### Syntax\.

Fix countably infinite, pairwise\-disjoint vocabularies of*atomic concept names*𝖭𝖢\\mathsf\{N\_\{C\}\},*role names*𝖭𝖱\\mathsf\{N\_\{R\}\}, and*individual names*𝖭𝖨\\mathsf\{N\_\{I\}\}\.ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}*concepts*are built by the grammar

C,D::=⊤∣⊥∣A∣​\{a\}∣​C⊓D\|∃R\.C,C,D\\;::=\\;\\top\\mid\\bot\\mid A\\mid\\\{a\\\}\\mid C\\sqcap D\\mid\\exists R\.C,whereA∈𝖭𝖢A\\in\\mathsf\{N\_\{C\}\},a∈𝖭𝖨a\\in\\mathsf\{N\_\{I\}\}, andR∈𝖭𝖱R\\in\\mathsf\{N\_\{R\}\}\. An*ontology*𝒪\\mathcal\{O\}is a finite set of axioms of one of the following shapes \([Table4](https://arxiv.org/html/2608.12961#Pt0.A1.T4)\): general concept inclusionsC⊑DC\\sqsubseteq D, role inclusionsR⊑SR\\sqsubseteq S, role chainsR1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq S, range restrictionsrange⁡\(R\)⊑C\\mathrm\{range\}\(R\)\\sqsubseteq C, reflexive\-role declarationsRef⁡\(R\)\\mathrm\{Ref\}\(R\), local\-reflexivity∃R\.𝖲𝖾𝗅𝖿\\exists R\.\\mathsf\{Self\}, and key axiomsHasKey⁡\(C,R1,…,Rn\)\\mathrm\{HasKey\}\(C,R\_\{1\},\\dots,R\_\{n\}\)\. The*ground vocabulary*of𝒪\\mathcal\{O\}over a finite individual setΔ\\Deltais𝒱𝒪Δ:=\{A\(a\):A∈𝖲𝗂𝗀C\(𝒪\),a∈Δ\}∪\{R\(a,b\):R∈𝖲𝗂𝗀R\(𝒪\),a,b∈Δ\}\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}:=\\\{A\(a\):A\\in\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\),\\,a\\in\\Delta\\\}\\cup\\\{R\(a,b\):R\\in\\mathsf\{Sig\}\_\{R\}\(\\mathcal\{O\}\),\\,a,b\\in\\Delta\\\}\.

#### Semantics\.

An*interpretation*ℐ=\(Δℐ,⋅ℐ\)\\mathcal\{I\}=\(\\Delta^\{\\mathcal\{I\}\},\\cdot^\{\\mathcal\{I\}\}\)comprises a non\-empty domainΔℐ\\Delta^\{\\mathcal\{I\}\}and a mapping⋅ℐ\\cdot^\{\\mathcal\{I\}\}that sends eachA∈𝖭𝖢A\\in\\mathsf\{N\_\{C\}\}toAℐ⊆ΔℐA^\{\\mathcal\{I\}\}\\subseteq\\Delta^\{\\mathcal\{I\}\}, eachR∈𝖭𝖱R\\in\\mathsf\{N\_\{R\}\}toRℐ⊆Δℐ×ΔℐR^\{\\mathcal\{I\}\}\\subseteq\\Delta^\{\\mathcal\{I\}\}\\times\\Delta^\{\\mathcal\{I\}\}, and eacha∈𝖭𝖨a\\in\\mathsf\{N\_\{I\}\}toaℐ∈Δℐa^\{\\mathcal\{I\}\}\\in\\Delta^\{\\mathcal\{I\}\}\. Concept and axiom semantics extend⋅ℐ\\cdot^\{\\mathcal\{I\}\}to compound concepts and constraints as in[Table4](https://arxiv.org/html/2608.12961#Pt0.A1.T4)\.ℐ\\mathcal\{I\}is a*model*of𝒪\\mathcal\{O\}, writtenℐ⊧𝒪\\mathcal\{I\}\\models\\mathcal\{O\}, if it satisfies every axiom in𝒪\\mathcal\{O\};𝒪⊧C⊑D\\mathcal\{O\}\\models C\\sqsubseteq DmeansCℐ⊆DℐC^\{\\mathcal\{I\}\}\\subseteq D^\{\\mathcal\{I\}\}in every modelℐ\\mathcal\{I\}of𝒪\\mathcal\{O\}\.

Table 4:ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}syntax and semantics\. Together with role inclusion, role chain, and range axioms, plus the ABox\-style constructs \(nominals,𝖲𝖾𝗅𝖿\\mathsf\{Self\},HasKey\\mathrm\{HasKey\}\), this is the OWL 2 EL profile minus datatype properties\.
#### BBL normal forms NF1–NF7\.

Baader, Brandt, and Lutz\[[5](https://arxiv.org/html/2608.12961#bib.bib5)\]show everyℰ​ℒ\+⁣\+\\mathcal\{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\}\\sqcap\\dots\\sqcap A\_\{n\}\\sqsubseteq B\(atomic conjunctive LHS\); NF2,∃R\.A⊑B\\exists R\.A\\sqsubseteq B\(atomic existential LHS\); NF3,A⊑∃R\.BA\\sqsubseteq\\exists R\.B\(atomic existential RHS\); NF4,A⊑⊥A\\sqsubseteq\\bot\(atomic unsat\); NF5,A⊑BA\\sqsubseteq B\(atomic\-atomic\); NF6,⊤⊑A\\top\\sqsubseteq A\(top\-LHS\); NF7,⊥⊑A\\bot\\sqsubseteq A\(vacuous\)\. Our Lean formalization \(namespaceELKSDD\.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](https://arxiv.org/html/2608.12961#bib.bib26)\]give a saturation procedure that decides Sat\-derivability𝖲𝖺𝗍⁡\(𝒪,C,D\)\\mathsf\{Sat\}\(\\mathcal\{O\},C,D\)for the full OWL 2 EL profile \(minus datatypes\) in timeO⁡\(\|𝒪\|4\)O\(\|\\mathcal\{O\}\|^\{4\}\)\. The calculus operates on a finite collection of*atomic*subsumptions and*links*E→𝑅DE\\xrightarrow\{R\}D, closed under a fixed rule set:R0\\mathrm\{R\_\{0\}\}\(A⊑AA\\sqsubseteq A\),R⊤\\mathrm\{R\_\{\\top\}\}\(A⊑⊤A\\sqsubseteq\\top\),R⊑\\mathrm\{R\_\{\\sqsubseteq\}\}\(transitivity along axioms\),R⊓−\\mathrm\{R^\{\-\}\_\{\\sqcap\}\}andR⊓\+\\mathrm\{R^\{\+\}\_\{\\sqcap\}\}\(conjunction\),R⊥\\mathrm\{R\_\{\\bot\}\}\(unsatisfiability propagation\),R∃\+\\mathrm\{R^\{\+\}\_\{\\exists\}\}andR⊥\-∃\\mathrm\{R\_\{\\bot\\text\{\-\}\\exists\}\}\(existential constructors\), role\-side rulesRrinc\\mathrm\{R\_\{rinc\}\},Rrchain\\mathrm\{R\_\{rchain\}\}for role inclusions and chains, plus specialized rules for ranges, reflexive roles,𝖲𝖾𝗅𝖿\\mathsf\{Self\}, the nominal\-handling rules of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §3\], and the merging canonical\-model construction of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §6\]for shapes 1–4 of nominals together withHasKey\\mathrm\{HasKey\}\. Saturation terminates because all derivable atoms are over the finite vocabulary of𝖲𝗎𝖻⁡\(𝒪\)∪𝖱𝗈𝗅𝖾𝗌⁡\(𝒪\)\\mathsf\{Sub\}\(\\mathcal\{O\}\)\\cup\\mathsf\{Roles\}\(\\mathcal\{O\}\); the resulting closure has sizeO⁡\(n2​r\)O\(n^\{2\}r\)forn=\|𝖲𝗎𝖻⁡\(𝒪\)\|n=\|\\mathsf\{Sub\}\(\\mathcal\{O\}\)\|andr=\|𝖱𝗈𝗅𝖾𝗌⁡\(𝒪\)\|r=\|\\mathsf\{Roles\}\(\\mathcal\{O\}\)\|\[[26](https://arxiv.org/html/2608.12961#bib.bib26), Thm\. 1\]\. Our formalization \(namespaceELKSDD\.ELpp\) mechanizes the same calculus, sound and complete on the nominal\-free fragment \(with ranges, reflexive roles,𝖲𝖾𝗅𝖿\\mathsf\{Self\}, role inclusions, and role chains\) and on the LHS\-nominal and shallow\-exist\-RHS\-nominal extensions; shapes 2/4 \(RHS\-nominal GCIsC⊑\{a\}C\\sqsubseteq\\\{a\\\},\{a\}⊑\{b\}\\\{a\\\}\\sqsubseteq\\\{b\\\}\) andHasKey\\mathrm\{HasKey\}are handled by the merging canonical\-model construction of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §6\], fully mechanized asELKSDD\.ELpp\.complete\_via\_mergedCanon\_regularandELKSDD\.ELpp\.complete\_via\_mergedCanon\_nom\(both audit\-clean\), under the shallow concept restriction of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §6\]: concepts may not contain deep existentials with non\-nominal targets\. The unified completeness theoremELKSDD\.ELpp\.complete\_owl2elcases on a fragment witness to invoke the appropriate canonical\-model construction; together withELKSDD\.ELpp\.sound\_owl2el, it gives Sat⇔\\iffEntails on every ontology meeting at least one of its five branch preconditions\. Every individualℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}construct \(nominals, ranges, role chains, reflexive,𝖲𝖾𝗅𝖿\\mathsf\{Self\},HasKey\\mathrm\{HasKey\}\) is supported in some branch, but the branches are not jointly compatible: shapes 2/4 \(RHS\-nominal GCIsC⊑\{a\}C\\sqsubseteq\\\{a\\\},\{a\}⊑\{b\}\\\{a\\\}\\sqsubseteq\\\{b\\\}\) combined with deep non\-nominal existentials, and the merging fragment combined with role chains or ranges, hit the case\-disabling preconditions of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §6\]\(an ontology may have a model whereCCis empty and another whereCCis forced into the\{a\}\\\{a\\\}\-class; a single canonical construction must pick one\); the supported shapes follow the consequence\-based reasoning literature\[[48](https://arxiv.org/html/2608.12961#bib.bib48),[2](https://arxiv.org/html/2608.12961#bib.bib2)\]\. The concurrent verified\-reasoner effort VEL\[[42](https://arxiv.org/html/2608.12961#bib.bib42)\]mechanizes BBL 2005ℰ​ℒ\+⁣\+\\mathcal\{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\|≤5​n3​\(r\+1\)\|L\|\\leq 5n^\{3\}\(r\+1\)that includes ranges, reflexive, and𝖲𝖾𝗅𝖿\\mathsf\{Self\}isELKSDD\.ELpp\.sat\_closure\_total\_polynomial\_bound\.

## Appendix 0\.BTask formalism and MNIST instantiation

###### Definition 1\(ABox\-supervised latent concept learning\)

A training instance is a triple\(Δ,𝐱,𝐞\)\(\\Delta,\\mathbf\{x\},\\mathbf\{e\}\)where𝐱=\(xa\)a∈Δ\\mathbf\{x\}=\(x\_\{a\}\)\_\{a\\in\\Delta\}with eachxa∈𝒳x\_\{a\}\\in\\mathcal\{X\}and𝐞\\mathbf\{e\}is a set of literals \(truth\-tagged ground atoms\) over the observable ground vocabulary; ground atoms not in𝐞\\mathbf\{e\}are unobserved\. The task is to learn a weight\-shared per\-individual classifierfθ:𝒳→\[0,1\]\|𝖲𝗂𝗀Cℓ\|f\_\{\\theta\}:\\mathcal\{X\}\\to\[0,1\]^\{\|\\mathsf\{Sig\}^\{\\ell\}\_\{C\}\|\}such thatfθ​\(xa\)​\[C\]f\_\{\\theta\}\(x\_\{a\}\)\[C\]approximates the marginal probability ofC⁡\(a\)C\(a\)given𝒪\\mathcal\{O\}and𝐞\\mathbf\{e\}, for everyC∈𝖲𝗂𝗀CℓC\\in\\mathsf\{Sig\}^\{\\ell\}\_\{C\}anda∈Δa\\in\\Delta\. A negative literal¬C⁡\(a\)∈𝐞\\neg C\(a\)\\in\\mathbf\{e\}encodes the polarity of a ground variable in𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\(ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}itself has no concept negation\); role atoms are not classified byfθf\_\{\\theta\}, and latent role atoms are marginalized at the uniform prior\.

A boolean assignmentM:𝒱𝒪Δ→\{0,1\}M:\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\\to\\\{0,1\\\}induces an ABox interpretationℐM=\(Δ,⋅M\)\\mathcal\{I\}\_\{M\}=\(\\Delta,\\cdot^\{M\}\)viaCM:=\{a:M⁡\(C⁡\(a\)\)=1\}C^\{M\}:=\\\{a:M\(C\(a\)\)=1\\\}andRM:=\{\(a,b\):M⁡\(R⁡\(a,b\)\)=1\}R^\{M\}:=\\\{\(a,b\):M\(R\(a,b\)\)=1\\\}\. The differentiable WMC layer evaluates𝖶𝖬𝖢⁡\(α,w,𝐞\)\\mathsf\{WMC\}\(\\alpha;w,\\mathbf\{e\}\)where the literal\-weight mapwwis the unique extension offθ​\(𝐱\)f\_\{\\theta\}\(\\mathbf\{x\}\)and𝐞\\mathbf\{e\}that makes the training\-loss, posterior, and entailment\-query operations of §[3\.4](https://arxiv.org/html/2608.12961#S3.SS4)three settings of the same SDD traversal:

The literal\-weight map itself is now inlined in §[3\.1](https://arxiv.org/html/2608.12961#S3.SS1)as[Table1](https://arxiv.org/html/2608.12961#S3.T1)\.

###### Example 1\(MNIST instantiation\)

[Definition1](https://arxiv.org/html/2608.12961#Thmdefinition1)instantiates on MNIST as follows\. The TBox is𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}over𝖲𝗂𝗀C=\{D0,…,D9,Even,Odd,Prime,Composite\}\\mathsf\{Sig\}\_\{C\}=\\\{D\_\{0\},\\dots,D\_\{9\},\\,\\textsf\{Even\},\\textsf\{Odd\},\\textsf\{Prime\},\\textsf\{Composite\}\\\}and𝖲𝗂𝗀R=\{succ,plus\_two\}\\mathsf\{Sig\}\_\{R\}=\\\{\\textsf\{succ\},\\textsf\{plus\\\_two\}\\\}\(full listing in[Section0\.F\.2](https://arxiv.org/html/2608.12961#Pt0.A6.SS2)\)\. The observable signature is𝖲𝗂𝗀Co=\{Even,Odd,Prime,Composite\}\\mathsf\{Sig\}^\{o\}\_\{C\}=\\\{\\textsf\{Even\},\\textsf\{Odd\},\\textsf\{Prime\},\\textsf\{Composite\}\\\}; the latent signature is𝖲𝗂𝗀Cℓ=\{D0,…,D9\}\\mathsf\{Sig\}^\{\\ell\}\_\{C\}=\\\{D\_\{0\},\\dots,D\_\{9\}\\\}\(the digit class is never revealed\)\. A training instance places one MNIST imagexax\_\{a\}at each named individual and supplies one or two property literals as evidence, e\.g\.𝐞=\{Even​\(a\),¬Prime​\(a\)\}\\mathbf\{e\}=\\\{\\textsf\{Even\}\(a\),\\,\\neg\\textsf\{Prime\}\(a\)\\\}for an image of digit44\. 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 allOdd⊓Prime\\textsf\{Odd\}\\sqcap\\textsf\{Prime\}\)\[[39](https://arxiv.org/html/2608.12961#bib.bib39),[41](https://arxiv.org/html/2608.12961#bib.bib41),[29](https://arxiv.org/html/2608.12961#bib.bib29)\]\.

### 0\.B\.1Summary of pipeline assumptions

[Table5](https://arxiv.org/html/2608.12961#Pt0.A2.T5)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 \([Definition1](https://arxiv.org/html/2608.12961#Thmdefinition1)\); the right\-hand column makes explicit what a user gives up by adopting them\.

Table 5:Assumptions introduced by each component of theMoosepipeline and their departure from open\-world semantics\.

## Appendix 0\.CCompilation algorithm and worked example

This appendix gives the seven\-stage compilation pseudocode \([Algorithm1](https://arxiv.org/html/2608.12961#alg1)\) and works a concrete two\-axiom ontology through it \([Section0\.C\.3](https://arxiv.org/html/2608.12961#Pt0.A3.SS3)\)\.

### 0\.C\.1Pseudocode

[Algorithm1](https://arxiv.org/html/2608.12961#alg1)gives the full pseudocode of the seven\-stage compilation algorithm summarized in §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\. 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 ruleR∃\+R^\{\+\}\_\{\\exists\}: the rule fires only on existentials already in𝖲𝗎𝖻⁡\(𝒪\)\\mathsf\{Sub\}\(\\mathcal\{O\}\)\(line 1 of the algorithm\)\. This is the standard ELK rule\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §5\]and is what keeps saturation finite on ontologies with cyclic role inclusions\. The second is*uniform super\-role materialization*under the role\-composition ruleR∘R\_\{\\circ\}: 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 withR1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq SandS⊑TS\\sqsubseteq Tproduces theSS\-link from the chain rule but silently loses theTT\-link, breaking ELK completeness \([Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)\) on chain heads with a super\-role\.

Algorithm 1Moose:ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology to SDD over ground atoms1:Ontology

𝒪\\mathcal\{O\}as a set of GCIs

C⊑DC\\sqsubseteq D, role inclusions

R⊑SR\\sqsubseteq S, role chains

R1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq S\. Finite ABox domain

Δ\\Delta\.

2:SDD

α\\alphaover

𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\([Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\)\.

3:

4:\[Stage 1: ELK saturation\]

5:

ℰ∃←\{∃R\.D∣∃R\.D∈𝖲𝗎𝖻\(𝒪\)\}\\mathcal\{E\}\_\{\\exists\}\\leftarrow\\\{\\exists R\.D\\mid\\exists R\.D\\in\\mathsf\{Sub\}\(\\mathcal\{O\}\)\\\}⊳\\trianglerightsignature side condition onR∃\+R^\{\+\}\_\{\\exists\}

6:

\(Σ,Λ\)←Saturate​\(𝒪,ℰ∃\)\(\\Sigma,\\Lambda\)\\leftarrow\\textsf\{Saturate\}\(\\mathcal\{O\},\\mathcal\{E\}\_\{\\exists\}\)⊳\\trianglerightΣ\\Sigma: subsumptionsC⊑DC\\sqsubseteq D;Λ\\Lambda: linksE→𝑅CE\\xrightarrow\{R\}C

7:

8:\[Stages 2–5: Clark completion, SCC, unrolling, CNF\]

9:foreach derived atom

h∈Σ∪Λh\\in\\Sigma\\cup\\Lambdado

10:

Clark​\(h\)←h↔⋁j\(⋀b∈𝑏𝑜𝑑𝑦j​\(h\)b\)\\textsf\{Clark\}\(h\)\\leftarrow h\\leftrightarrow\\bigvee\_\{j\}\(\\bigwedge\_\{b\\in\\mathit\{body\}\_\{j\}\(h\)\}b\)⊳\\trianglerightStage 2: Clark completion

11:endfor

12:

SCCs←Tarjan​\(DepGraph​\(Clark\)\)\\textsf\{SCCs\}\\leftarrow\\textsf\{Tarjan\}\(\\textsf\{DepGraph\}\(\\textsf\{Clark\}\)\)⊳\\trianglerightStage 3: SCC detection

13:foreach non\-trivial SCC

SSof size

T=\|S\|T\{=\}\|S\|\(

\|S\|\>1\|S\|\>1or self\-loop\)do⊳\\trianglerightStage 4: time\-stamped unrolling

14:foreach

h∈Sh\\in Sdo

15:emit

xh\(0\)↔⊥x\_\{h\}^\{\(0\)\}\\leftrightarrow\\bot;

xh↔xh\(T\)x\_\{h\}\\leftrightarrow x\_\{h\}^\{\(T\)\}
16:endfor

17:foreach

h∈Sh\\in S,

t=0,…,T−1t=0,\\dots,T\{\-\}1do

18:emit

xh\(t\+1\)↔xh\(t\)∨⋁j\(⋀bxb\(t\)\)x\_\{h\}^\{\(t\+1\)\}\\leftrightarrow x\_\{h\}^\{\(t\)\}\\lor\\bigvee\_\{j\}\(\\bigwedge\_\{b\}x\_\{b\}^\{\(t\)\}\)
19:endfor

20:endfor

21:

CNF←Tseitin​\(all formulas\)\\textsf\{CNF\}\\leftarrow\\textsf\{Tseitin\}\(\\text\{all formulas\}\)⊳\\trianglerightStage 5: CNF conversion

22:

23:\[Stages 6–7: ABox grounding and SDD compilation\]

24:

AtomSub←\{\(X,Y\)∈Σ:X,Y∈𝖲𝗂𝗀C\(𝒪\),X≠Y\}\\textsf\{AtomSub\}\\leftarrow\\\{\(X,Y\)\\in\\Sigma:X,Y\\in\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\),\\ X\\neq Y\\\}
25:

Disj←\{flatten\(C\):\(C⊑⊥\)∈Σ,Catomic conjunction\}\\textsf\{Disj\}\\leftarrow\\\{\\textsf\{flatten\}\(C\):\(C\\sqsubseteq\\bot\)\\in\\Sigma,\\ C\\text\{ atomic conjunction\}\\\}
26:

Unsat←\{X∈Σ:X⊑⊥,X∈𝖲𝗂𝗀C\(𝒪\)\}\\textsf\{Unsat\}\\leftarrow\\\{X\\in\\Sigma:X\\sqsubseteq\\bot,\\ X\\in\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\)\\\}
27:

Links←\{\(X,R,Y\)∈Λ:X,Y∈𝖲𝗂𝗀C\(𝒪\)\}\\textsf\{Links\}\\leftarrow\\\{\(X,R,Y\)\\in\\Lambda:X,Y\\in\\mathsf\{Sig\}\_\{C\}\(\\mathcal\{O\}\)\\\}
28:

Γ←∅\\Gamma\\leftarrow\\emptyset
29:for

\(X,Y\)∈AtomSub,a∈Δ\(X,Y\)\\in\\textsf\{AtomSub\},\\ a\\in\\Deltado

Γ∪=\{¬X⁡\(a\)∨Y⁡\(a\)\}\\Gamma\{\\;\\cup\\\!=\\;\}\\\{\\neg X\(a\)\\vee Y\(a\)\\\}
30:endfor

31:for

\(X1,…,Xn\)∈Disj,a∈Δ\(X\_\{1\},\\dots,X\_\{n\}\)\\in\\textsf\{Disj\},\\ a\\in\\Deltado

Γ∪=\{⋁i¬Xi​\(a\)\}\\Gamma\{\\;\\cup\\\!=\\;\}\\\{\\bigvee\_\{i\}\\neg X\_\{i\}\(a\)\\\}
32:endfor

33:for

X∈Unsat,a∈ΔX\\in\\textsf\{Unsat\},\\ a\\in\\Deltado

Γ∪=\{¬X⁡\(a\)\}\\Gamma\{\\;\\cup\\\!=\\;\}\\\{\\neg X\(a\)\\\}
34:endfor

35:for

\(X,R,Y\)∈Links,\(a,b\)∈Δ2,a≠b\(X,R,Y\)\\in\\textsf\{Links\},\\ \(a,b\)\\in\\Delta^\{2\},\\ a\\neq bdo

36:

Γ∪=\{¬X⁡\(a\)∨¬R⁡\(a,b\)∨Y⁡\(b\)\}\\Gamma\{\\;\\cup\\\!=\\;\}\\\{\\neg X\(a\)\\vee\\neg R\(a,b\)\\vee Y\(b\)\\\}⊳\\trianglerightNF3 forward

37:if

\|\{Y′:\(X,R,Y′\)∈Links\}\|=1\|\\\{Y^\{\\prime\}:\(X,R,Y^\{\\prime\}\)\\in\\textsf\{Links\}\\\}\|=1then

38:

Γ∪=\{¬R⁡\(a,b\)∨¬Y⁡\(b\)∨X⁡\(a\)\}\\Gamma\{\\;\\cup\\\!=\\;\}\\\{\\neg R\(a,b\)\\vee\\neg Y\(b\)\\vee X\(a\)\\\}⊳\\trianglerightNF4 reverse

39:endif

40:endfor

41:return

SDDCompile​\(Γ\)\\textsf\{SDDCompile\}\(\\Gamma\)⊳\\trianglerightPySDD bottom\-up

### 0\.C\.2Stages 2–5: the TBox\-level encoding

This subsection expands the Stage 2–5 block of[Algorithm1](https://arxiv.org/html/2608.12961#alg1), which turns the Stage\-1 saturation into a propositional TBox theory\. For NeSy learning these stages are diagnostic \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\); 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](https://arxiv.org/html/2608.12961#bib.bib18)\]: each derived atomhhhas one or more grounded rule body𝑏𝑜𝑑𝑦1,…,𝑏𝑜𝑑𝑦k\\mathit\{body\}\_\{1\},\\dots,\\mathit\{body\}\_\{k\}that can derive it\. The*Clark completion*replaces these defining clauses with a biconditional

h⟷𝑏𝑜𝑑𝑦1∨𝑏𝑜𝑑𝑦2∨⋯∨𝑏𝑜𝑑𝑦k,h\\;\\longleftrightarrow\\;\\mathit\{body\}\_\{1\}\\;\\lor\\;\\mathit\{body\}\_\{2\}\\;\\lor\\;\\cdots\\;\\lor\\;\\mathit\{body\}\_\{k\},\(4\)asserting thathhholds if and only if at least one of its justifications holds\. Each𝑏𝑜𝑑𝑦j\\mathit\{body\}\_\{j\}is a conjunction of previously derived atoms and*input axiom variables*αi\\alpha\_\{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\\alpha\_\{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](https://arxiv.org/html/2608.12961#bib.bib18)\]\. 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\\alpha\_\{i\}true, that model is exactly the set of atoms ELK derives from𝒪\\mathcal\{O\}, i\.e\. the saturation closureSat​\(𝒪\)\\textsf\{Sat\}\(\\mathcal\{O\}\)\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\.

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\}\\sqsubseteq\\exists R\.\\exists R\.D\_\{k\}\}\. For NeSy training, the Clark completion is restricted to atoms whose head is an atomic concept, a conjunction of atomic concepts,⊤\\top, or⊥\\bot\(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𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\.

#### Stage 3: SCC detection\.

The dependency graph among derived atoms may contain cycles\. For example, a cyclic successor chainD0⊑∃succ\.D1⊑∃succ\.∃succ\.D2⊑⋯⊑D0D\_\{0\}\\sqsubseteq\\exists\\textsf\{succ\}\.D\_\{1\}\\sqsubseteq\\exists\\textsf\{succ\}\.\\exists\\textsf\{succ\}\.D\_\{2\}\\sqsubseteq\\cdots\\sqsubseteq 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](https://arxiv.org/html/2608.12961#bib.bib47)\]to find strongly connected components \(SCCs\) of the dependency graph\. Acyclic atoms \(trivial SCCs\) can use the plain biconditional of[Equation4](https://arxiv.org/html/2608.12961#Pt0.A3.E4)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[Equation4](https://arxiv.org/html/2608.12961#Pt0.A3.E4)is directly expressible in propositional logic\. For cyclic SCCs we break the circularity by introducing time\-stamped copiesxh\(0\),xh\(1\),…,xh\(T\)x\_\{h\}^\{\(0\)\},x\_\{h\}^\{\(1\)\},\\dots,x\_\{h\}^\{\(T\)\}of each atomhhwithin the SCC and defining:

xh\(0\)\\displaystyle x\_\{h\}^\{\(0\)\}⟷⁣⊥,\\displaystyle\\;\\longleftrightarrow\\;\\bot,\(5\)xh\(t\+1\)\\displaystyle x\_\{h\}^\{\(t\+1\)\}⟷xh\(t\)∨⋁j\(⋀b∈𝑏𝑜𝑑𝑦j​\(h\)xb\(t\)\),\\displaystyle\\;\\longleftrightarrow\\;x\_\{h\}^\{\(t\)\}\\;\\lor\\;\\bigvee\_\{j\}\\Bigl\(\\bigwedge\_\{b\\in\\mathit\{body\}\_\{j\}\(h\)\}x\_\{b\}^\{\(t\)\}\\Bigr\),\(6\)xh\\displaystyle x\_\{h\}⟷xh\(T\),\\displaystyle\\;\\longleftrightarrow\\;x\_\{h\}^\{\(T\)\},\(7\)where the local boundT=\|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\\sum\_\{S\}\|S\|^\{2\}instead of\|𝒱\|2\|\\mathcal\{V\}\|^\{2\}for global unrolling\.

#### Stage 5: CNF conversion\.

The Tseitin transformation\[[50](https://arxiv.org/html/2608.12961#bib.bib50)\]converts the nested propositional formulas from Stage 4 into equisatisfiable conjunctive normal form \(CNF\) by introducing an auxiliary variable for each sub\-formulaφ\\varphiand adding clauses that enforce the auxiliary to equalφ\\varphi\. 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𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\.

#### WMC recursion\.

The differentiable WMC layer of Stage 7 traverses the compiled SDDα\\alphaand evaluates

𝖶𝖬𝖢⁡\(α,w\)=\{w⁡\(ℓ\)if​α=ℓ​is a literal node,0ifα=⊥,1ifα=⊤,∑\(pi,si\)∈α𝖶𝖬𝖢⁡\(pi,w\)⋅𝖶𝖬𝖢⁡\(si,w\)if​α​is a decision node,\\mathsf\{WMC\}\(\\alpha;w\)\\;=\\;\\begin\{cases\}w\(\\ell\)&\\text\{if \}\\alpha=\\ell\\text\{ is a literal node,\}\\\\ 0&\\text\{if \}\\alpha=\\bot,\\\\ 1&\\text\{if \}\\alpha=\\top,\\\\ \\displaystyle\\sum\_\{\(p\_\{i\},s\_\{i\}\)\\in\\alpha\}\\mathsf\{WMC\}\(p\_\{i\};w\)\\cdot\\mathsf\{WMC\}\(s\_\{i\};w\)&\\text\{if \}\\alpha\\text\{ is a decision node,\}\\end\{cases\}\(8\)with literal weightswwread from[Table1](https://arxiv.org/html/2608.12961#S3.T1)\.

### 0\.C\.3Worked example

Consider the two\-axiom fragment𝒪5:=\{D5⊑Odd,D5⊑Prime\}\\mathcal\{O\}\_\{5\}:=\\\{D\_\{5\}\\sqsubseteq\\textsf\{Odd\},\\,D\_\{5\}\\sqsubseteq\\textsf\{Prime\}\\\}onΔ=\{a\}\\Delta=\\\{a\\\}, drawn from𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}\(§[5\.1](https://arxiv.org/html/2608.12961#S5.SS1)\)\.Stage 1runs the ELK ruleR⊑R\_\{\\sqsubseteq\}over𝒪5\\mathcal\{O\}\_\{5\}and adds the two input axioms toΣ\\Sigmaas atomic subsumptions; no role axioms, soΛ=∅\\Lambda=\\emptyset\. 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 6applies the four extractors to\(Σ,Λ\)\(\\Sigma,\\Lambda\): both subsumptions match theAtomSubshape \(atomic\-atomic,X≠YX\\neq Y\), soAtomSub=\{\(D5,Odd\),\(D5,Prime\)\}\\textsf\{AtomSub\}=\\\{\(D\_\{5\},\\textsf\{Odd\}\),\\,\(D\_\{5\},\\textsf\{Prime\}\)\\\}; the other extractors produce nothing\. The extractors ground each\(X,Y\)∈AtomSub\(X,Y\)\\in\\textsf\{AtomSub\}on everya∈Δa\\in\\Delta, emittingΓ=\{¬D5​\(a\)∨Odd​\(a\),¬D5​\(a\)∨Prime​\(a\)\}\\Gamma=\\\{\\,\\neg D\_\{5\}\(a\)\\vee\\textsf\{Odd\}\(a\),\\;\\neg D\_\{5\}\(a\)\\vee\\textsf\{Prime\}\(a\)\\,\\\}over𝒱𝒪5\{a\}\\mathcal\{V\}\_\{\\mathcal\{O\}\_\{5\}\}^\{\\\{a\\\}\}\.Stage 7compilesΓ\\Gammainto an SDD whose models are exactly the assignments in whichD5​\(a\)=1D\_\{5\}\(a\)=1impliesOdd​\(a\)=1\\textsf\{Odd\}\(a\)=1andPrime​\(a\)=1\\textsf\{Prime\}\(a\)=1\. The full𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}extends𝒪5\\mathcal\{O\}\_\{5\}with the analogous property axioms for the remaining digits, the4545pairwise digit disjointness axioms \(handled byDisj\), the1010NF3 successor existentials, and the NF7 role chain \([Section0\.F\.2](https://arxiv.org/html/2608.12961#Pt0.A6.SS2)\); the SDD is155155nodes over1414atoms and compiles in under a quarter of a second \([Section0\.F\.1](https://arxiv.org/html/2608.12961#Pt0.A6.SS1)\)\.

## Appendix 0\.DFull proofs

This part of the appendix contains the full proofs of the §[4](https://arxiv.org/html/2608.12961#S4)theorems \([Theorems4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1),[4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2),[4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3)and[4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)\), the ELK mechanization of the reused infrastructure \([Theorems0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)and[0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2),[Section0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.SS1)\), and the closure\-augmented and inference\-time variants \([Theorems0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3)and[0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)\. The final subsection \([Section0\.D\.10](https://arxiv.org/html/2608.12961#Pt0.A4.SS10)\) cross\-references each paper claim with its Lean module and theorem identifier\. We use the notation introduced in §[4](https://arxiv.org/html/2608.12961#S4)\.

#### Mechanized statements\.

The Lean libraryELKSDD\([Appendix0\.A](https://arxiv.org/html/2608.12961#Pt0.A1)\) proves every prior\-work result it relies on rather than admitting it as an axiom: ELK soundness/completeness\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]is proved end\-to\-end in namespacesELKSDD\.ELandELKSDD\.ELpp; SDD compilation correctness\[[21](https://arxiv.org/html/2608.12961#bib.bib21),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]and the WMC\-correctness theorem underlying[Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\(c\) are proved structurally in namespaceELKSDD\.SDD; the four ELK extractors are concretenoncomputable 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](https://arxiv.org/html/2608.12961#bib.bib21)\]SDD\-WMC correctness, by structural induction\)\. Running\#print axiomson every paper\-cited theorem at build time confirms that the dependency set is exactly\{propext,Classical\.choice,Quot\.sound\}\\\{\\texttt\{propext\},\\texttt\{Classical\.choice\},\\texttt\{Quot\.sound\}\\\}\.

### 0\.D\.1Reused 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](https://arxiv.org/html/2608.12961#bib.bib26)\]\. They are reused unchanged in §[4](https://arxiv.org/html/2608.12961#S4)but re\-mechanized in our Lean library so that[Theorems4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1),[4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2),[4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3)and[4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)can be proved within the same audit\-clean foundation\.𝖮𝖶𝖫𝟤𝖤𝖫𝖥𝗋𝖺𝗀𝗆𝖾𝗇𝗍\\mathsf\{OWL2ELFragment\}abbreviates the syntactic fragment witness selecting the canonical\-model construction used for completeness on\(𝒪,C,D\)\(\\mathcal\{O\},C,D\): \(a\) nominal\-free withC,DC,Din the signature of𝒪\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib26), §6\]for shapes 1–4 of nominals andHasKey\\mathrm\{HasKey\}, restricted to Shallow concepts \(no deep existentials with non\-nominal targets\)\. The disjunction is the inductive predicateELKSDD\.ELpp\.OWL2ELFragment; together with𝖮𝖶𝖫𝟤𝖤𝖫𝖥𝗋𝖺𝗀𝗆𝖾𝗇𝗍\\mathsf\{OWL2ELFragment\}the unified completeness theoremELKSDD\.ELpp\.complete\_owl2elcovers any ontology meeting at least one branch precondition \(a\)–\(e\)\. Every individualℰ​ℒ\+⁣\+\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib26), §6\]and constitute open work in the ELK literature itself rather than gaps in the Lean formalization \(see[Appendix0\.A](https://arxiv.org/html/2608.12961#Pt0.A1)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𝒱𝒪Δ\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}used by the SDD encoding \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\) 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 \([Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\)\.

###### Theorem 0\.D\.1\(ELK soundness and completeness onℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}\)

For everyℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology𝒪\\mathcal\{O\}and conceptsC,DC,D, if𝖮𝖶𝖫𝟤𝖤𝖫𝖥𝗋𝖺𝗀𝗆𝖾𝗇𝗍⁡\(𝒪,C,D\)\\mathsf\{OWL2ELFragment\}\(\\mathcal\{O\},C,D\)holds then

𝖲𝖺𝗍⁡\(𝒪,C,D\)⇔𝒪⊧C⊑D\.\\mathsf\{Sat\}\(\\mathcal\{O\},C,D\)\\;\\iff\\;\\mathcal\{O\}\\models C\\sqsubseteq D\.\(9\)

###### Proof

Soundness \(left to right\) is unconditional in𝖮𝖶𝖫𝟤𝖤𝖫𝖥𝗋𝖺𝗀𝗆𝖾𝗇𝗍\\mathsf\{OWL2ELFragment\}and proved by structural induction on the ELK derivation, mechanized asELKSDD\.ELpp\.sound\_owl2el\. Completeness \(right to left\) is by case\-split on𝖮𝖶𝖫𝟤𝖤𝖫𝖥𝗋𝖺𝗀𝗆𝖾𝗇𝗍\\mathsf\{OWL2ELFragment\}to one of five canonical\-model constructions \(Kazakov 2014 §3, §6 for the merging case\); mechanized asELKSDD\.ELpp\.complete\_owl2el\. See\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]for the original arguments\.∎

###### Theorem 0\.D\.2\(Polynomial Sat decision\)

For everyℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology𝒪\\mathcal\{O\}there exists a listLLof pairs of concepts with\|L\|≤\|𝖲𝗎𝖻⁡\(𝒪\)\|2\|L\|\\leq\|\\mathsf\{Sub\}\(\\mathcal\{O\}\)\|^\{2\}such that for everyC,D∈𝖲𝗎𝖻⁡\(𝒪\)C,D\\in\\mathsf\{Sub\}\(\\mathcal\{O\}\),

𝖲𝖺𝗍⁡\(𝒪,C,D\)⇔\(C,D\)∈L\.\\mathsf\{Sat\}\(\\mathcal\{O\},C,D\)\\;\\iff\\;\(C,D\)\\in L\.

###### Proof

The witnessLLis the time\-stamped Clark closurederivableClosure​\(𝒪\)\\texttt\{derivableClosure\}\(\\mathcal\{O\}\): length bound byderivableClosure\_length\(counts concept pairs in the saturation closure\); membership equivalence bysat\_iff\_in\_derivableClosure\(simultaneous induction over the Sat constructors\)\. Mechanized asELKSDD\.ELpp\.sat\_decision\_polynomial; an exact closure\-size bound\|L\|≤5​n3​\(r\+1\)\|L\|\\leq 5n^\{3\}\(r\+1\)that includes ranges, reflexive, and Self \(n=\|𝖲𝗎𝖻⁡\(𝒪\)\|n=\|\\mathsf\{Sub\}\(\\mathcal\{O\}\)\|,r=\|𝖱𝗈𝗅𝖾𝗌⁡\(𝒪\)\|r=\|\\mathsf\{Roles\}\(\\mathcal\{O\}\)\|\) isELKSDD\.ELpp\.sat\_closure\_total\_polynomial\_bound, with per\-shape exact lengths\. See\[[26](https://arxiv.org/html/2608.12961#bib.bib26), Thm\. 1, §5\]for the originalO⁡\(\|𝒪\|4\)O\(\|\\mathcal\{O\}\|^\{4\}\)saturation runtime\. ∎

### 0\.D\.2Verified SDD encoding \([Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\)

###### Proof\(Proof of[Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\)

The witness ist=𝖼𝗆𝗉⁡\(𝒪,C,D\)t=\\mathsf\{cmp\}\(\\mathcal\{O\},C,D\), mechanized in namespaceELKSDD\.ELpp\(with the SDD\-side WMC theorems in namespaceELKSDD\.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𝖶𝖬𝖢\\mathsf\{WMC\}enumerating the2\|𝒪\|2^\{\|\\mathcal\{O\}\|\}leaves\. Conjunct \(3\): by induction on\|𝒪\|\|\\mathcal\{O\}\|, a Shannon node at depthkkhas2\|𝒪\|−k\+1−12^\{\|\\mathcal\{O\}\|\-k\+1\}\-1descendants\. Lean theorem identifiers are listed in[Table6](https://arxiv.org/html/2608.12961#Pt0.A4.T6)\. ∎

The standard probabilistic\-DL “entailment\-as\-WMC\-zero” phrasing\[[44](https://arxiv.org/html/2608.12961#bib.bib44)\]follows immediately: at uniform per\-axiom priorw≡12w\\equiv\\tfrac\{1\}\{2\},𝖶𝖬𝖢ℚ=0\\mathsf\{WMC\}^\{\\mathbb\{Q\}\}=0iff no world’s selected sub\-ontology entailsC⊑DC\\sqsubseteq D\([Theorem4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2)combined with[Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)\)\. The production four\-extractor ground encoding \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2), Stages 6–7\) is a separate ABox encoding whose soundness over the finite domain follows from[Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)\(Lean:ELKSDD\.ELpp\.sound\_owl2elandELKSDD\.ELpp\.complete\_owl2el\) under the partial\-supervision role\-pinning of §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\.

### 0\.D\.3Correctness of the closure\-augmented circuit \([Theorem0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3)\)

###### Theorem 0\.D\.3\(Correctness of the closure\-augmented circuit\)

For every modeller\-declared exhaustive familyℱ=\{D0,…,DK−1\}\\mathcal\{F\}=\\\{D\_\{0\},\\dots,D\_\{K\-1\}\\\}, define𝗆𝖺𝗍𝖼𝗁π​\(a\)\\mathsf\{match\}\_\{\\pi\}\(a\)as the conjunction of the positive and negated property literals specified by profileπ\\pi\. ThenM⊧αclosM\\models\\alpha\_\{\\text\{clos\}\}iffM⊧αELM\\models\\alpha\_\{\\text\{EL\}\}and, at everya∈Δa\\in\\Delta, both of the following hold: \(i\) the partition constraints\{¬\(Di​\(a\)∧Dj​\(a\)\):i<j\}∪\{D0​\(a\)∨⋯∨DK−1​\(a\)\}\\\{\\neg\(D\_\{i\}\(a\)\\wedge D\_\{j\}\(a\)\):i<j\\\}\\cup\\\{D\_\{0\}\(a\)\\vee\\dots\\vee D\_\{K\-1\}\(a\)\\\}; and \(ii\), for every distinct declared profileπ\\pi, the reverse implication𝗆𝖺𝗍𝖼𝗁π\(a\)→⋁i:πi=πDi\(a\)\\mathsf\{match\}\_\{\\pi\}\(a\)\\rightarrow\\bigvee\_\{i:\\,\\pi\_\{i\}=\\pi\}D\_\{i\}\(a\)\.

###### Proof\(Proof of[Theorem0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3)\)

αclos=SDDCompile​\(ΓEL∪Φclos\)\\alpha\_\{\\text\{clos\}\}=\\textsf\{SDDCompile\}\(\\Gamma\_\{\\text\{EL\}\}\\cup\\Phi\_\{\\text\{clos\}\}\)by construction\. For each marked family and individual,Φmutex\\Phi\_\{\\text\{mutex\}\}contains the\(K2\)\\binom\{K\}\{2\}clauses¬Di​\(a\)∨¬Dj​\(a\)\\neg D\_\{i\}\(a\)\\vee\\neg D\_\{j\}\(a\), andΦcover\\Phi\_\{\\text\{cover\}\}containsD0​\(a\)∨⋯∨DK−1​\(a\)D\_\{0\}\(a\)\\vee\\dots\\vee D\_\{K\-1\}\(a\)\. These are exactly the partition constraints in clausal form\. For every distinct profileπ\\pi,Φprofile\\Phi\_\{\\text\{profile\}\}additionally contains the clausal form of𝗆𝖺𝗍𝖼𝗁π\(a\)→⋁i:πi=πDi\(a\)\\mathsf\{match\}\_\{\\pi\}\(a\)\\rightarrow\\bigvee\_\{i:\\,\\pi\_\{i\}=\\pi\}D\_\{i\}\(a\)\. Therefore, satisfaction of the full clause set is equivalent to conditions \(i\)–\(ii\)\. Generic SDD compilation correctness then gives the stated model equivalence\[[17](https://arxiv.org/html/2608.12961#bib.bib17),[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\. The Lean theoremELKSDD\.SDD\.compile\_correctquantifies over the complete input clause list, so it applies to all three components ofΦclos\\Phi\_\{\\textsf\{clos\}\}\.∎

### 0\.D\.4Production\-encoding size

[Theorem0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2)bounds the saturation closure by\|𝖲𝖺𝗍⁡\(𝒪\)\|≤5​n3​\(r\+1\)\|\\mathsf\{Sat\}\(\\mathcal\{O\}\)\|\\leq 5n^\{3\}\(r\{\+\}1\)atoms withn=\|𝖲𝗎𝖻⁡\(𝒪\)\|n=\|\\mathsf\{Sub\}\(\\mathcal\{O\}\)\|andr=\|𝖱𝗈𝗅𝖾𝗌⁡\(𝒪\)\|r=\|\\mathsf\{Roles\}\(\\mathcal\{O\}\)\|\(Lean:ELKSDD\.ELpp\.sat\_closure\_total\_polynomial\_bound\)\. Grounding the extractors of §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)over\|Δ\|=m\|\\Delta\|=mnamed individuals adds an at\-mostm2m^\{2\}multiplicative factor \(AtomSub,Disj,Unsatcontributemmclauses each;Linkscontributes up tom2m^\{2\}for the NF3/NF4 clauses\)\. Each declared exhaustive family of sizeKKadds a further\(K2\)​m\+\(K\+1\)​m\\binom\{K\}\{2\}m\+\(K\{\+\}1\)mclosure clauses \(\(K2\)​m\\binom\{K\}\{2\}mmutex,mmcovering, and up toK​mKmprofile\-keyed reverse implications\)\. SDD compilation of the resulting CNF is treated in[Section0\.D\.5](https://arxiv.org/html/2608.12961#Pt0.A4.SS5)\.

### 0\.D\.5SDD treewidth dependence and empirical scaling

Bottom\-up SDD compilation\[[17](https://arxiv.org/html/2608.12961#bib.bib17)\]of a CNFΓ\\Gammaproduces an SDD whose worst\-case size is exponential in\|Γ\|\|\\Gamma\|\[[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\. For CNFs whose primal graph has treewidthww, the resulting SDD admits a polynomial boundO⁡\(\|Γ\|⋅2w\)O\(\|\\Gamma\|\\cdot 2^\{w\}\)because tractable WMC over bounded\-treewidth instances is reducible to compact circuit compilation\. Empirically onmnistthe SDD node count fits∝\|Δ\|2\.9\\propto\|\\Delta\|^\{2\.9\}for\|Δ\|≤3\|\\Delta\|\\leq 3\(consistent with the bounded\-treewidth regime\), with a40×40\\timescompile\-time jump between\|Δ\|=3\|\\Delta\|=3and\|Δ\|=4\|\\Delta\|=4as the primal\-graph treewidth rises; at the\|Δ\|=2\|\\Delta\|=2configurations used in §[5](https://arxiv.org/html/2608.12961#S5)compilation finishes well below one second on a CPU \(1×\\timesRTX 4090, single CPU core;[Section0\.F\.1](https://arxiv.org/html/2608.12961#Pt0.A6.SS1)\)\.

### 0\.D\.6Inference complexity \([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)

###### Theorem 0\.D\.4\(Inference complexity\)

Let\|α\|\|\\alpha\|denote the node count of eitherαEL\\alpha\_\{\\text\{EL\}\}orαclos\\alpha\_\{\\text\{clos\}\}\. The training loss[Equation11](https://arxiv.org/html/2608.12961#Pt0.A5.E11), conditional posterior[Equation12](https://arxiv.org/html/2608.12961#Pt0.A5.E12), entailment query[Equation13](https://arxiv.org/html/2608.12961#Pt0.A5.E13), and one training step \(loss plus gradient\) all run inO⁡\(\|α\|\)O\(\|\\alpha\|\)time\[[21](https://arxiv.org/html/2608.12961#bib.bib21),[17](https://arxiv.org/html/2608.12961#bib.bib17)\], with the training step adding the cost of one forward and backward pass offθf\_\{\\theta\}\.

###### Proof\(Proof of[Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)

The SDDα\\alphaproduced by[Algorithm1](https://arxiv.org/html/2608.12961#alg1)is smooth, decomposable, and deterministic by PySDD construction\[[21](https://arxiv.org/html/2608.12961#bib.bib21),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]; let\|α\|\|\\alpha\|denote its node count\.

\(a\) WMC\.The recursive traversal of §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)visits each node once \(memoized by node id\), contributingpC⁡\(a\)p\_\{C\(a\)\}or1−pC⁡\(a\)1\-p\_\{C\(a\)\}at literal nodes,00or11at constants, and∑i𝖶𝖬𝖢⁡\(primei\)⋅𝖶𝖬𝖢⁡\(subi\)\\sum\_\{i\}\\mathsf\{WMC\}\(\\textsf\{prime\}\_\{i\}\)\\cdot\\mathsf\{WMC\}\(\\textsf\{sub\}\_\{i\}\)at decision nodes\. Determinism makes each sum disjoint and decomposability makes each product over disjoint variable scopes, so𝖶𝖬𝖢⁡\(α,p,𝐞\)\\mathsf\{WMC\}\(\\alpha;p,\\mathbf\{e\}\)is exact and runs inO⁡\(\|α\|\)O\(\|\\alpha\|\)time\. Each per\-node operation is differentiable in the literal weights, and PyTorch autograd composes the backward pass through the same traversal inO⁡\(\|α\|\)O\(\|\\alpha\|\)additional time\.

\(b\) Conditional posterior\.The ratioPθ\(C\(a\)∣𝐱,𝐞\)=𝖶𝖬𝖢\(α;pθ\(𝐱\),𝐞∪\{C\(a\):=𝗍𝗋𝗎𝖾\}\)/𝖶𝖬𝖢\(α;pθ\(𝐱\),𝐞\)P\_\{\\theta\}\(C\(a\)\\mid\\mathbf\{x\},\\mathbf\{e\}\)=\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\\cup\\\{C\(a\):=\\mathsf\{true\}\\\}\)/\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)is two applications of \(a\), eachO⁡\(\|α\|\)O\(\|\\alpha\|\)\. The denominator is strictly positive whenever𝐞\\mathbf\{e\}is consistent with𝒪\\mathcal\{O\}\.

\(c\) Entailment query\.Settingp≡12p\\equiv\\tfrac\{1\}\{2\}gives the uniform prior; conditioning on𝐞∪\{C\(a\):=𝖿𝖺𝗅𝗌𝖾\}\\mathbf\{e\}\\cup\\\{C\(a\):=\\mathsf\{false\}\\\}clamps the corresponding literal\. By[Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)the SDD’s models are exactly the finite\-domain interpretations satisfying the entailed clauses, so𝖶𝖬𝖢\(α;12,𝐞∪\{C\(a\):=𝖿𝖺𝗅𝗌𝖾\}\)=0\\mathsf\{WMC\}\(\\alpha;\\tfrac\{1\}\{2\},\\mathbf\{e\}\\cup\\\{C\(a\):=\\mathsf\{false\}\\\}\)=0iff no model ofα\\alphahasC⁡\(a\)=𝖿𝖺𝗅𝗌𝖾C\(a\)=\\mathsf\{false\}, iff𝒪∪𝐞⊧C⁡\(a\)\\mathcal\{O\}\\cup\\mathbf\{e\}\\models C\(a\)\. The check is one WMC call,O⁡\(\|α\|\)O\(\|\\alpha\|\)\.

\(d\) Training step\.The lossL⁡\(θ,𝐱,𝐞\)=−log⁡𝖶𝖬𝖢⁡\(α,pθ​\(𝐱\),𝐞\)L\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\)=\-\\log\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)is one WMC call,O⁡\(\|α\|\)O\(\|\\alpha\|\)\. Its gradient with respect toθ\\thetais computed by autograd through the WMC traversal \(costO⁡\(\|α\|\)O\(\|\\alpha\|\)\) followed by the perception backbone’s backward pass \(cost equal to the forward pass offθf\_\{\\theta\}\)\. Total:O⁡\(\|α\|\)\+O⁡\(cost of​fθ​\(𝐱\)\)O\(\|\\alpha\|\)\+O\(\\text\{cost of \}f\_\{\\theta\}\(\\mathbf\{x\}\)\)\. ∎

### 0\.D\.7Structural circuit properties

We define three structural properties used to characterize the tractability of weighted model counting on a circuit\[[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\. A*circuit*over variables𝐕\\mathbf\{V\}is a rooted directed acyclic graph whose leaves are literals over𝐕\\mathbf\{V\}\(or the constants⊤\\top/⊥\\bot\), and whose internal nodes are either*product nodes*\(⋀\\bigwedge, evaluating to the conjunction of their children\) or*sum nodes*\(⋁\\bigvee, evaluating to the disjunction of their children\)\. Letφ\\varphibe 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𝐕\\mathbf\{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\}\)\\vee\\dots\\vee\(p\_\{k\},s\_\{k\}\), abbreviating⋁i\(pi∧si\)\\bigvee\_\{i\}\(p\_\{i\}\\wedge s\_\{i\}\); eachpip\_\{i\}\(the*prime*\) andsis\_\{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](https://arxiv.org/html/2608.12961#bib.bib20),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]\. This prime/sub decomposition realizes all three structural properties above by construction: every primepip\_\{i\}has scope disjoint from its corresponding subsis\_\{i\}\(decomposability\), the primes are pairwise inconsistent \(determinism\), and they cover the input space allotted to the node by its v\-tree \(smoothness\)\[[20](https://arxiv.org/html/2608.12961#bib.bib20),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]\. Together, these properties make𝖶𝖬𝖢\\mathsf\{WMC\}linear in\|α\|\|\\alpha\|and reduce conditioning, marginalization, and MAP inference to circuit traversals\[[21](https://arxiv.org/html/2608.12961#bib.bib21)\]\.

### 0\.D\.8Compositional SCC factorization lemmas \([Theorems4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3)and[4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)\)

The following lemmas establish the SCC factorization formalized in Lean: an arbitrary two\-component partition of an ontology,𝒪=𝒪1∪𝒪2\\mathcal\{O\}=\\mathcal\{O\}\_\{1\}\\cup\\mathcal\{O\}\_\{2\}, with disjoint atom and role signatures, factors the closure exactly, modulo a single “global inconsistency” disjunct that captures the case where𝒪2\\mathcal\{O\}\_\{2\}alone derives⊤⊑⊥\\top\\sqsubseteq\\bot\(which then propagates to all of𝒪1∪𝒪2\\mathcal\{O\}\_\{1\}\\cup\\mathcal\{O\}\_\{2\}via theR⊥R\_\{\\bot\}rule, regardless of𝒪1\\mathcal\{O\}\_\{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\)

LetO1,O2O\_\{1\},O\_\{2\}beℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontologies \(finite sets of GCIs, role inclusions, and role chains\)\. Letatoms⁡\(Oi\)⊆𝖲𝗂𝗀C\\mathrm\{atoms\}\(O\_\{i\}\)\\subseteq\\mathsf\{Sig\}\_\{C\}androles⁡\(Oi\)⊆𝖲𝗂𝗀R\\mathrm\{roles\}\(O\_\{i\}\)\\subseteq\\mathsf\{Sig\}\_\{R\}denote the sets of atomic concept names and role names appearing in axioms ofOiO\_\{i\}\. Assume signature disjointness:

atoms⁡\(O1\)∩atoms⁡\(O2\)=∅,roles⁡\(O1\)∩roles⁡\(O2\)=∅\.\\mathrm\{atoms\}\(O\_\{1\}\)\\cap\\mathrm\{atoms\}\(O\_\{2\}\)=\\emptyset,\\qquad\\mathrm\{roles\}\(O\_\{1\}\)\\cap\\mathrm\{roles\}\(O\_\{2\}\)=\\emptyset\.Then for every pair ofℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}conceptsC,DC,Dwhose atom and role names lie entirely inO1O\_\{1\}’s signature\(atoms⁡\(C\)∪atoms⁡\(D\)⊆atoms⁡\(O1\)𝐶𝐿𝑂𝑆𝐸\(\\mathrm\{atoms\}\(C\)\\cup\\mathrm\{atoms\}\(D\)\\subseteq\\mathrm\{atoms\}\(O\_\{1\}\)and𝑂𝑃𝐸𝑁roles⁡\(C\)∪roles⁡\(D\)⊆roles⁡\(O1\)\),\\mathrm\{roles\}\(C\)\\cup\\mathrm\{roles\}\(D\)\\subseteq\\mathrm\{roles\}\(O\_\{1\}\)\),the closure factors as

𝖲𝖺𝗍\(O1∪O2\)C⊑D⇔𝖲𝖺𝗍\(O1\)C⊑D∨𝖲𝖺𝗍\(O2\)⊤⊑⊥\.\\mathsf\{Sat\}\(O\_\{1\}\\cup O\_\{2\}\)\\;C\\sqsubseteq D\\;\\;\\iff\\;\\;\\mathsf\{Sat\}\(O\_\{1\}\)\\;C\\sqsubseteq D\\;\\lor\\;\\mathsf\{Sat\}\(O\_\{2\}\)\\;\\top\\sqsubseteq\\bot\.\(10\)The statement holds for the nominal\-free, range\-chain\-safe fragment of full OWL 2 EL \(ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}minus concrete domains\): bothO1O\_\{1\}andO2O\_\{2\}are nominal\-free, both satisfy the range\-chain safety conditionELKSDD\.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](https://arxiv.org/html/2608.12961#bib.bib26)\]§3\.3\), andC,DC,Dare nominal\-free\. No restriction on⊤\\top\- or⊥\\bot\-axioms is imposed on either side\.

OWL 2 EL nominals \(ObjectOneOfsingleton classes\) are supported by the algorithm at the axiom level \(normal formsNFnomR“A⊑\{a\}A\\sqsubseteq\\\{a\\\}” andNFnomL“\{a\}⊑B\\\{a\\\}\\sqsubseteq B”\) and at the concept level \(Concept\.nom,Interp\.indiv,conceptIndividuals,ontologyIndividuals\) in our Lean implementation\. The proof of[Lemma1](https://arxiv.org/html/2608.12961#Thmlemma1)below covers the nominal\-free fragment\. Shape 1 nominals \(ABox\-styleClassAssertionaxioms\{a\}⊑D\\\{a\\\}\\sqsubseteq DwithDDnominal\-free\) are formalized by the relaxedELKSDD\.ELpp\.Sat\_factor\_nomLHStheorem, under theOntologyNomLHSprecondition \(which permits LHS\-nominal GCIs on the analyzed sideO1O\_\{1\}\) andAllNomInhabited\(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⟩\\langle\\mathcal\{I\}\_\{1\}\.\\textsf\{indiv\}\(a\),b\_\{0\}\\rangle, so no general nominal\-evaluation lemma is needed: the existing P2 \(which is already general in the second coordinate\) is applied atb=b0b=b\_\{0\}\. Shapes 2/4 \(RHS nominal:A⊑\{a\}A\\sqsubseteq\\\{a\\\}or\{a\}⊑\{b\}\\\{a\\\}\\sqsubseteq\\\{b\\\}\) andHasKeyare handled by the merging canonical\-model construction\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\(concept equivalence classes through nominals\), fully mechanized in namespaceELKSDD\.ELppunder the Shallow concept restriction of\[[26](https://arxiv.org/html/2608.12961#bib.bib26), §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 ofELKSDD\.SCC\.Sat\_factor\_refinedwithELKSDD\.ELpp\.complete\_via\_mergedCanon\_regular\.

###### Proof\(Proof outline \(full proof:ELKSDD\.SCC\.Sat\_factor\_refined\)\)

The\(⇐\)\(\\Leftarrow\)direction is monotonicity of𝖲𝖺𝗍\\mathsf\{Sat\}in the ontology, plus theR⊥R\_\{\\bot\}rule when the second disjunct holds\. For\(⇒\)\(\\Rightarrow\)we may assume¬𝖲𝖺𝗍\(O2\)⊤⊑⊥\\neg\\mathsf\{Sat\}\(O\_\{2\}\)\\;\\top\\sqsubseteq\\bot\(else the second disjunct is immediate\), so the canonical \(term\) modelℐcan​\(O2\)\\mathcal\{I\}^\{\\mathrm\{can\}\}\(O\_\{2\}\)of[Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)is non\-empty\. Given an arbitraryℐ1⊧O1\\mathcal\{I\}\_\{1\}\\models O\_\{1\}onΔ1\\Delta\_\{1\}, build the*product interpretation*ℐ′\\mathcal\{I\}^\{\\prime\}onΔ1×ℐcan​\(O2\)\\Delta\_\{1\}\\times\\mathcal\{I\}^\{\\mathrm\{can\}\}\(O\_\{2\}\)that evaluatesO1O\_\{1\}\-signature atoms and roles on the first coordinate andO2O\_\{2\}\-signature ones on the second\. Signature disjointness \(Disj\) lets the evaluation of anyOiO\_\{i\}\-signature concept factor cleanly through the corresponding component \(Lean:eval\_prodInterp\_O1,eval\_prodInterp\_O2\), which in turn givesℐ′⊧O1∪O2\\mathcal\{I\}^\{\\prime\}\\models O\_\{1\}\\cup O\_\{2\}\(prodInterp\_satisfies\)\. By ELK soundness on the union,ℐ′⊧C⊑D\\mathcal\{I\}^\{\\prime\}\\models C\\sqsubseteq D; factoring back through the first coordinate at the basepoint⟨a,x⊤⟩\\langle a,x\_\{\\top\}\\rangleyieldsℐ1⊧C⊑D\\mathcal\{I\}\_\{1\}\\models C\\sqsubseteq D\. Sinceℐ1\\mathcal\{I\}\_\{1\}was arbitrary, ELK completeness onO1O\_\{1\}closes the left\-hand disjunct\. ∎

###### Lemma 2\(Per\-world Sat factorization\)

LetO=O1∪O2O=O\_\{1\}\\cup O\_\{2\}satisfy the signature\-disjointness, nominal\-free, and range\-chain\-safe preconditions of[Lemma1](https://arxiv.org/html/2608.12961#Thmlemma1), and additionally assumeO2O\_\{2\}consistent \(¬𝖲𝖺𝗍⁡\(O2,⊤,⊥\)\\neg\\,\\mathsf\{Sat\}\(O\_\{2\},\\top,\\bot\)\)\. For every Boolean worldM:O→𝔹M:O\\to\\mathbb\{B\}, writeM1=M↾O1M\_\{1\}=M\{\\restriction\}O\_\{1\}and letsel​\(O,M\):=\{α∈O:M⁡\(α\)=𝗍𝗋𝗎𝖾\}\\textsf\{sel\}\(O,M\):=\\\{\\alpha\\in O:M\(\\alpha\)=\\mathsf\{true\}\\\}denote the sub\-ontology selected byMM\. For nominal\-freeC,DC,DinO1O\_\{1\}’s signature,

𝖲𝖺𝗍⁡\(sel​\(O,M\)\)​C⊑D⇔𝖲𝖺𝗍⁡\(sel​\(O1,M1\)\)​C⊑D\.\\mathsf\{Sat\}\\bigl\(\\textsf\{sel\}\(O,M\)\\bigr\)\\;C\\sqsubseteq D\\;\\;\\iff\\;\\;\\mathsf\{Sat\}\\bigl\(\\textsf\{sel\}\(O\_\{1\},M\_\{1\}\)\\bigr\)\\;C\\sqsubseteq D\.That is,𝖲𝖺𝗍\\mathsf\{Sat\}\-derivability ofC⊑DC\\sqsubseteq Dat worldMMfactors through theO1O\_\{1\}\-restriction ofMMalone\.

###### Proof

Two steps\. \(i\)sel​\(O,M\)\\textsf\{sel\}\(O,M\)andsel​\(O1,M1\)∪sel​\(O2,M2\)\\textsf\{sel\}\(O\_\{1\},M\_\{1\}\)\\cup\\textsf\{sel\}\(O\_\{2\},M\_\{2\}\)are equal as ontologies \(each axiomα∈O=O1⊎O2\\alpha\\in O=O\_\{1\}\\uplus O\_\{2\}lies in exactly one side and contributes to the corresponding selected sub\-ontology by the same Boolean choiceM⁡\(α\)M\(\\alpha\)\)\. Bidirectional sub\-ontology inclusions yield Sat equivalence by monotonicity of𝖲𝖺𝗍\\mathsf\{Sat\}in the ontology \(Sat\_mono\); the Lean witnesses areELKSDD\.ELpp\.selectedAxioms\_sub\_decomposeanddecompose\_sub\_selectedAxioms\. \(ii\) Apply[Lemma1](https://arxiv.org/html/2608.12961#Thmlemma1)in the generalized formELKSDD\.ELpp\.Sat\_factor\_refined\_general, which usesO1,O2O\_\{1\},O\_\{2\}as*signature\-defining*outer ontologies while permitting the analyzed sidessel​\(O1,M1\)\\textsf\{sel\}\(O\_\{1\},M\_\{1\}\)andsel​\(O2,M2\)\\textsf\{sel\}\(O\_\{2\},M\_\{2\}\)to be sub\-ontologies thereof\.sel​\(O2,M2\)\\textsf\{sel\}\(O\_\{2\},M\_\{2\}\)is consistent because it is a sub\-ontology of the consistentO2O\_\{2\}, so the right disjunct of[Lemma1](https://arxiv.org/html/2608.12961#Thmlemma1)vanishes, leaving the clean factorization throughO1O\_\{1\}\. SeeELKSDD\.ELpp\.per\_world\_sat\_factor\_consistent\. ∎

###### Lemma 3\(Closed\-form WMC SCC factorization under uniform priors\)

Under the hypotheses of[Lemma2](https://arxiv.org/html/2608.12961#Thmlemma2)\(signature\-disjoint, nominal\-free, range\-chain\-safeO1,O2O\_\{1\},O\_\{2\}withO2O\_\{2\}consistent\), for the rational DISPONTE marginal under the uniform per\-axiom weightw≡1w\\equiv 1,

wmcℚ​\(O1∪O2,C,D,w\)=wmcℚ​\(O1,C,D,w\)⋅2\|O2\|\.\\textsf\{wmc\}^\{\\mathbb\{Q\}\}\(O\_\{1\}\\cup O\_\{2\},\\,C,D,\\,w\)\\;=\\;\\textsf\{wmc\}^\{\\mathbb\{Q\}\}\(O\_\{1\},\\,C,D,\\,w\)\\cdot 2^\{\|O\_\{2\}\|\}\.

###### Proof

By definition,

wmcℚ\(O,C,D,w\):=∑M:O→𝔹\[𝖲𝖺𝗍\(sel\(O,M\)\)C⊑D\]⋅worldWeight\(M,w\),\\textsf\{wmc\}^\{\\mathbb\{Q\}\}\(O,C,D,w\)\\;:=\\;\\sum\_\{M:O\\to\\mathbb\{B\}\}\\bigl\[\\mathsf\{Sat\}\(\\textsf\{sel\}\(O,M\)\)\\;C\\sqsubseteq D\\bigr\]\\cdot\\textsf\{worldWeight\}\(M,w\),where the world weight is∏α∈Ow⁡\(α,M⁡\(α\)\)\\prod\_\{\\alpha\\in O\}w\(\\alpha,M\(\\alpha\)\)\. Three steps\. \(a\) Underw≡1w\\equiv 1,worldWeight​\(M,w\)=1\\textsf\{worldWeight\}\(M,w\)=1for everyMM\(Lean:worldWeightRat\_uniform\)\. \(b\) By[Lemma2](https://arxiv.org/html/2608.12961#Thmlemma2), the indicator depends onMMonly throughM1=M↾O1M\_\{1\}=M\{\\restriction\}O\_\{1\}\. \(c\) The sum overM:O1⊎O2→𝔹M:O\_\{1\}\\uplus O\_\{2\}\\to\\mathbb\{B\}of any function depending only onM↾O1M\{\\restriction\}O\_\{1\}factorizes as∑M1:O1→𝔹f\(M1\)⋅2\|O2\|\\sum\_\{M\_\{1\}:O\_\{1\}\\to\\mathbb\{B\}\}f\(M\_\{1\}\)\\cdot 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 isELKSDD\.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ℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontologyOO, every concept pair\(C,D\)\(C,D\), and every per\-axiom weight functionw:DispAtom​\(O\)×𝔹→ℚw:\\textsf\{DispAtom\}\(O\)\\times\\mathbb\{B\}\\to\\mathbb\{Q\},

wmcℚ​\(compile​\(O,C,D\),w\)=wmcℚ​\(O,C,D,w\),\\textsf\{wmc\}^\{\\mathbb\{Q\}\}\\bigl\(\\textsf\{compile\}\(O,C,D\);\\,w\\bigr\)\\;=\\;\\textsf\{wmc\}^\{\\mathbb\{Q\}\}\(O,\\,C,D,\\,w\),where the LHS is the SDD\-level WMC of the verified compiled circuitcompileSatand the RHS is the rational DISPONTE distribution\-semantics marginal\. No restriction onwwis imposed \(in particular, no probabilistic normalization ofww\)\.

###### 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\)\[\\mathsf\{Sat\}\(\\textsf\{sel\}\(O,M\)\)\\;C\\sqsubseteq D\]\\cdot\\textsf\{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∑\\sumoverℚ\\mathbb\{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 asELKSDD\.ELpp\.wmc\_compileSat\_eq\_disponteWMC\_rat\([Table6](https://arxiv.org/html/2608.12961#Pt0.A4.T6)\)\. ∎

### 0\.D\.9DeepProbLog equivalence on the EL Horn theory

We tighten the informal claim of §[5\.3](https://arxiv.org/html/2608.12961#S5.SS3)thatMooseonΓEL\\Gamma\_\{\\textsf\{EL\}\}alone “yields the loss DeepProbLog\[[39](https://arxiv.org/html/2608.12961#bib.bib39)\]would minimize on the same Horn instance” into a formal proposition and a Lean 4 encoding in namespaceMoose\(the Lean identifiers retain the historicalno\_clossuffix as code artefacts\)\.

#### Setup\.

Let𝒪\\mathcal\{O\}be anℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}ontology,Δ\\Deltaa finite ABox domain, and letΓEL=AtomSub∪Disj∪Unsat∪Links\\Gamma\_\{\\textsf\{EL\}\}=\\textsf\{AtomSub\}\\cup\\textsf\{Disj\}\\cup\\textsf\{Unsat\}\\cup\\textsf\{Links\}be the ground clause set produced by the fourMooseextractors after ELK saturation \([Algorithm1](https://arxiv.org/html/2608.12961#alg1)of[Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3), beforeSDDCompile\)\. LetαEL=SDDCompile​\(ΓEL\)\\alpha\_\{\\textsf\{EL\}\}=\\textsf\{SDDCompile\}\(\\Gamma\_\{\\textsf\{EL\}\}\), letfθ:𝒳\|Δ\|→\[0,1\]\|𝒱𝒪Δ\|f\_\{\\theta\}:\\mathcal\{X\}^\{\|\\Delta\|\}\\to\[0,1\]^\{\|\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\|\}be a perception model assigning probabilitypθ​\(ℓ\)p\_\{\\theta\}\(\\ell\)to each positive ground literal \(and weight1−pθ​\(ℓ\)1\-p\_\{\\theta\}\(\\ell\)to its negation\), and let𝐞\\mathbf\{e\}be an evidence set of literals\.

#### Translation𝒫⁡\(ΓEL\)\\mathcal\{P\}\(\\Gamma\_\{\\textsf\{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. 1\.Each ground atomA⁡\(a\)∈𝒱𝒪ΔA\(a\)\\in\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}becomes a*probabilistic fact*pθ​\(A⁡\(a\)\)::A⁡\(a\)p\_\{\\theta\}\(A\(a\)\)::A\(a\)\.
2. 2\.Each definite Horn clause¬B1∨⋯∨¬Bk∨H∈ΓEL\\neg B\_\{1\}\\vee\\dots\\vee\\neg B\_\{k\}\\vee H\\in\\Gamma\_\{\\textsf\{EL\}\}\(AtomSub,Unsat, andLinksshapes\) becomes a Datalog*rule*H:\-B1,…,BkH\\,\\verb\|:\-\|\\,B\_\{1\},\\dots,B\_\{k\}\.
3. 3\.Each non\-Horn atomic\-disjointness clause¬A1∨⋯∨¬An\\neg A\_\{1\}\\vee\\dots\\vee\\neg A\_\{n\}\(Disjshape\) becomes a ProbLog*integrity constraint*:\-A1,…,An\\verb\|:\-\|\\,A\_\{1\},\\dots,A\_\{n\}\.

#### Loss objects\.

LMoose/EL​\(θ,𝐱,𝐞\):=−log⁡𝖶𝖬𝖢⁡\(αEL,pθ​\(𝐱\),𝐞\)L\_\{\\textsc\{Moose\}/\\textsf\{EL\}\}\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\):=\-\\log\\mathsf\{WMC\}\(\\alpha\_\{\\textsf\{EL\}\};p\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)is the Semantic\-loss WMC objective of §[3\.4](https://arxiv.org/html/2608.12961#S3.SS4)on the EL theory alone \(no closure axioms\);LDPL​\(θ,𝐱,𝐞\):=−log⁡PDPL​\(𝐞∣𝐱;θ\)L\_\{\\mathrm\{DPL\}\}\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\):=\-\\log P\_\{\\mathrm\{DPL\}\}\(\\mathbf\{e\}\\mid\\mathbf\{x\};\\theta\)is the DeepProbLog marginal loss\[[39](https://arxiv.org/html/2608.12961#bib.bib39)\]on𝒫⁡\(ΓEL\)\\mathcal\{P\}\(\\Gamma\_\{\\textsf\{EL\}\}\)under the ProbLog distribution semantics\.

###### Proposition 1\(DeepProbLog equivalence on the EL Horn theory\)

For every\(𝐱,𝐞\)\(\\mathbf\{x\},\\mathbf\{e\}\)consistent with𝒪\\mathcal\{O\},

LMoose/EL​\(θ,𝐱,𝐞\)=LDPL​\(θ,𝐱,𝐞\),L\_\{\\textsc\{Moose\}/\\textsf\{EL\}\}\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\)\\;=\\;L\_\{\\mathrm\{DPL\}\}\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\),as values \(in any commutative semiring carrying the literal weights\) and as gradients inθ\\theta\. The Lean mechanization instantiates the semiring atℕ\\mathbb\{N\}\(the type ofELKSDD\.SDD\.wmc\); the same induction is semiring\-polymorphic and lifts toℝ≥0\\mathbb\{R\}\_\{\\geq 0\}used in the Manhaeve 2018 real\-valued marginal \(paragraph \(B\) below\)\.

###### Proof\(Proof outline \(full proof:Moose\.moose\_no\_clos\_dpl\_equivand\.\.\.\_quantitative\)\.\)

Both losses equal−log⁡𝖶𝖬𝖢⁡\(ΓEL∪𝐞,wθ​\(𝐱\)\)\-\\log\\mathsf\{WMC\}\(\\Gamma\_\{\\textsf\{EL\}\}\\cup\\mathbf\{e\};\\,w\_\{\\theta\}\(\\mathbf\{x\}\)\), withwθw\_\{\\theta\}assigningpθ​\(ℓ\)p\_\{\\theta\}\(\\ell\)to positive literals and1−pθ​\(ℓ\)1\-p\_\{\\theta\}\(\\ell\)to negative ones\. SDD compilation preserves the model set, so𝖶𝖬𝖢⁡\(αEL,⋅\)=𝖶𝖬𝖢⁡\(ΓEL,⋅\)\\mathsf\{WMC\}\(\\alpha\_\{\\textsf\{EL\}\};\\cdot\)=\\mathsf\{WMC\}\(\\Gamma\_\{\\textsf\{EL\}\};\\cdot\)\[[21](https://arxiv.org/html/2608.12961#bib.bib21),[17](https://arxiv.org/html/2608.12961#bib.bib17)\]\. The translation𝒫⁡\(ΓEL\)\\mathcal\{P\}\(\\Gamma\_\{\\textsf\{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, soM⊧ΓEL⇔M⊧𝒫⁡\(ΓEL\)M\\models\\Gamma\_\{\\textsf\{EL\}\}\\Leftrightarrow M\\models\\mathcal\{P\}\(\\Gamma\_\{\\textsf\{EL\}\}\)\. The DeepProbLog distribution semantics then coincides with WMC by\[[39](https://arxiv.org/html/2608.12961#bib.bib39), Eq\. 4\]: each total assignment over the probabilistic facts is weighted by∏apθ​\(a\)M⁡\(a\)​\(1−pθ​\(a\)\)1−M⁡\(a\)\\prod\_\{a\}p\_\{\\theta\}\(a\)^\{M\(a\)\}\(1\-p\_\{\\theta\}\(a\)\)^\{1\-M\(a\)\}exactly when it satisfies every rule and integrity constraint, which is the WMC weight ofMM\. Equality of the losses as functions ofθ\\thetaimplies equality of their gradients, and of any other operator respecting functional equality\. ∎

#### Lean encoding\.

The argument is mechanized in namespaceMooseat 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\)\\exists M\.\\,M\\models\\Gamma\_\{\\textsf\{EL\}\}\\wedge\\mathrm\{support\}\(M\)\\subseteq\\mathrm\{support\}\(w\)and the equivalence closes by definitional unfolding \(Iff\.rfl\) once the ProbLog translation is recognized as the identity onList Clause\. At the quantitative level \(moose\_no\_clos\_dpl\_equiv\_quantitative\), the equality is lifted from a proposition to a numeric identitywmcQ​O​Δ​w=dplLossQ​O​Δ​w\\textsf\{wmcQ\}\\,O\\,\\Delta\\,w=\\textsf\{dplLossQ\}\\,O\\,\\Delta\\,wvia the key lemmawmc\_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ℕ\\mathbb\{N\}to keep the formalization free of a real\-arithmetic dependency, while the same induction lifts verbatim to theℝ≥0\\mathbb\{R\}\_\{\\geq 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\.

[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)pinsMoose’s contribution to the EL\-to\-Horn compilation algorithm \([Theorems4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)and[0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2)\): given𝒪\\mathcal\{O\}inℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}, the algorithm produces in time polynomial in\|𝒪\|\|\\mathcal\{O\}\|the ground Horn instanceΓEL\\Gamma\_\{\\textsf\{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\\Phi\_\{\\textsf\{clos\}\}on top ofΓEL\\Gamma\_\{\\textsf\{EL\}\}\. The content of these clauses is independent ofℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}entailment, and the DeepProbLog baseline correspondingly shows a higher RS\-consistency rate \(RScons\{\}\_\{\\text\{cons\}\}, the rate of confident wrong commitments\) than closure\-augmentedMooseacross[Tables2](https://arxiv.org/html/2608.12961#S5.T2)and[3](https://arxiv.org/html/2608.12961#S5.T3)\.

### 0\.D\.10Lean mechanization: theorem index

The Lean 4 libraryELKSDD\(introduced in[Appendix0\.A](https://arxiv.org/html/2608.12961#Pt0.A1)\) formalizes everyMoose\-cited theorem of the OWL 2 EL stack; the companion libraryMoosehouses the DeepProbLog\-equivalence layer\.[Table6](https://arxiv.org/html/2608.12961#Pt0.A4.T6)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 zerosorryoradmit\. An audit pass in each library runs\#print axiomson 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 inELKSDD\.ELpp, withELKSDD\.SDDfor the SDD calculus,ELKSDD\.RangeNormfor the BBL 2008 path, andMoosefor the DeepProbLog equivalence\. Every listed theorem is audit\-clean:\#print axiomsreports\[propext, Classical\.choice, Quot\.sound\]only, noMoose\-specific axioms, nosorry, noadmit\. Each theorem stated in §[4](https://arxiv.org/html/2608.12961#S4)corresponds to exactly one Lean theorem \(top section\); supporting lemmas, the closed\-form WMC SCC factor under uniform priors \([Theorem4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)\), and the LHS\-nominal extension are listed in the per\-topic sections that follow\.Paper claimLean theoremSection 4 \(correctness and complexity\): one Lean theorem per stated theoremVerified SDD encoding \([Theorem4\.1](https://arxiv.org/html/2608.12961#S4.Thmtheorem1)\)ELKSDD\.ELpp\.moose\_inference\_correctmodels iff SatELKSDD\.ELpp\.compileSat\_models\_iff\_satsize=2\|𝒪\|\+1−1=2^\{\|\\mathcal\{O\}\|\+1\}\-1ELKSDD\.ELpp\.compileSat\_size\_eqDISPONTE correspondence \([Theorem4\.2](https://arxiv.org/html/2608.12961#S4.Thmtheorem2)\)ELKSDD\.ELpp\.wmc\_compileSat\_eq\_disponteWMC\_ratSCC compositional, Sat \([Theorem4\.3](https://arxiv.org/html/2608.12961#S4.Thmtheorem3)\)ELKSDD\.ELpp\.scc\_sat\_factorSCC compositional, WMC uniform \([Theorem4\.4](https://arxiv.org/html/2608.12961#S4.Thmtheorem4)\)ELKSDD\.ELpp\.disponteWMCRat\_uniform\_scc\_factorReused ELK infrastructure \([Section0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.SS1); mechanized from\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\)ELK soundness/completeness \([Theorem0\.D\.1](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem1)\)ELKSDD\.ELpp\.correct\_owl2elsoundness \(unconditional\)ELKSDD\.ELpp\.sound\_owl2elcompleteness \(with fragment witness\)ELKSDD\.ELpp\.complete\_owl2elPolynomial Sat decision \([Theorem0\.D\.2](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem2)\)ELKSDD\.ELpp\.sat\_decision\_polynomialexact closure\-size boundELKSDD\.ELpp\.sat\_closure\_total\_polynomial\_boundClosure\-augmented circuit and inference complexity \(appendix\)Closure\-augmented \([Theorem0\.D\.3](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem3)\)ELKSDD\.SDD\.compile\_correctInference complexity \([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)ELKSDD\.SDD\.wmc\_linear,ELKSDD\.ELpp\.compileSat\_wmcCost\_eqCompositional and distributional results: supporting lemmasSCC Sat factor, sig\-disjointELKSDD\.SCC\.Sat\_factor\_refinedclosed form \(O2O\_\{2\}consistent\)ELKSDD\.ELpp\.scc\_sat\_factor,ELKSDD\.ELpp\.scc\_sat\_factor\_symmsub\-ontology generalizationELKSDD\.ELpp\.Sat\_factor\_refined\_generalkk\-component generalizationELKSDD\.ELpp\.scc\_sat\_factor\_k,
ELKSDD\.ELpp\.joint\_consistent\_pairPer\-world Sat factor \([Lemma2](https://arxiv.org/html/2608.12961#Thmlemma2)\)ELKSDD\.ELpp\.per\_world\_sat\_factor\_consistentselectedAxioms decompositionELKSDD\.ELpp\.selectedAxioms\_sub\_decomposeWorld\-summation factorizationELKSDD\.ELpp\.sum\_enumerateWorlds\_factorlength\-cast generalizationELKSDD\.ELpp\.sum\_enumerateWorlds\_factor\_generalWMC SCC factor \(uniform,[Lemma3](https://arxiv.org/html/2608.12961#Thmlemma3)\)ELKSDD\.ELpp\.disponteWMCRat\_uniform\_scc\_factorDISPONTE corresp\. \(ℕ\\mathbb\{N\}\-valued\)ELKSDD\.ELpp\.wmc\_compileSat\_eq\_disponteWMCDISPONTE corresp\. \(ℚ\\mathbb\{Q\},[Lemma4](https://arxiv.org/html/2608.12961#Thmlemma4)\)ELKSDD\.ELpp\.wmc\_compileSat\_eq\_disponteWMC\_ratexistence formELKSDD\.ELpp\.exists\_disponte\_correspondence\_ratNominal\-aware SCC \(LHS shape 1\)ELKSDD\.ELpp\.Sat\_factor\_nomLHS,
ELKSDD\.ELpp\.scc\_sat\_factor\_nomLHSprodInterp on LHS\-nominal axiomsELKSDD\.ELpp\.prodInterp\_satisfies\_nomLHSELK calculus \(Kazakov, Krötzsch, Simančík 2014\)ELK soundnessELKSDD\.EL\.sound,ELKSDD\.ELpp\.soundELK completeness \(nom\-free\)ELKSDD\.ELpp\.complete\_via\_canonLHS\-nominal extensionELKSDD\.ELpp\.complete\_via\_canon\_nomLHSCanonical model⊧\\modelsOO\(nom\-free\)ELKSDD\.ELpp\.canon\_satisfiesLHS\-nominal extensionELKSDD\.ELpp\.canon\_satisfies\_nomLHSshallow\-∃\\exists\-nom\-RHS extensionELKSDD\.ELpp\.canon\_satisfies\_nomLRSaturation terminationELKSDD\.ELpp\.saturation\_terminatesSat⇔\\Leftrightarrowderivable closureELKSDD\.ELpp\.sat\_iff\_in\_derivableClosurePoly\-time Sat decisionELKSDD\.ELpp\.sat\_polynomial\_decidableBounded Sat closure sizeELKSDD\.ELpp\.sat\_closure\_total\_polynomial\_boundSDD calculus \(Darwiche 2002, Choi–Darwiche 2013\)SDD compile\-correctnessELKSDD\.SDD\.compile\_correct,
ELKSDD\.SDD\.compileWithCtx\_correctSDD WMC linearityELKSDD\.SDD\.wmc\_linear,ELKSDD\.SDD\.wmcCost\_eq\_sizeMOOSE pipeline \(paper\-citation theorems\)Inference correctnessELKSDD\.ELpp\.moose\_inference\_correctPipeline completenessELKSDD\.ELpp\.moose\_pipeline\_completePolynomial Sat decision \(algorithmic\)ELKSDD\.ELpp\.sat\_decision\_polynomialSCC summaryELKSDD\.ELpp\.moose\_scc\_summarySCC, chain\-free corollaryELKSDD\.ELpp\.scc\_sat\_factor\_no\_chainSCC, range\-free corollaryELKSDD\.ELpp\.scc\_sat\_factor\_no\_rangeSyntactic range\-elimination\[[6](https://arxiv.org/html/2608.12961#bib.bib6)\]§3\.3 \(Path B\)Syntactic range\-eliminationELKSDD\.RangeNorm\.eliminateRangesstrict\-output preservationELKSDD\.RangeNorm\.eliminateRanges\_strictNoRange degenerate baselineELKSDD\.RangeNorm\.eliminateRanges\_eq\_under\_no\_rangerinc closure \(bounded fixed point\)ELKSDD\.RangeNorm\.rincDescendantstransitive reflexive\-rinc propagationELKSDD\.RangeNorm\.reflexiveTransitiveAxiomsForward Sat\-conservativity \(full\)ELKSDD\.RangeNorm\.Sat\_to\_eliminated\_fulltransitive marker membershipELKSDD\.RangeNorm\.reflexiveTransitive\_axiom\_…DeepProbLog equivalence \(Manhaeve 2018, Riguzzi 2015\)Qualitative \([Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)\)Moose\.moose\_no\_clos\_dpl\_equivQuantitative \(ℕ\\mathbb\{N\}\-valued\)Moose\.moose\_no\_clos\_dpl\_equiv\_quantitativeWMC==model sum \(BoolAtom\)Moose\.wmc\_compileWithCtx\_eq\_modelSum

## Appendix 0\.EInference, training, and RS\-mitigation wrappers

This appendix gives the explicit inference equations of §[3\.4](https://arxiv.org/html/2608.12961#S3.SS4)\([Section0\.E\.1](https://arxiv.org/html/2608.12961#Pt0.A5.SS1)\), the gradient flow used at training time \([Section0\.E\.2](https://arxiv.org/html/2608.12961#Pt0.A5.SS2)\), and theMoose\+BEARS /Moose\+NeSyDM wrapper losses used in the RS\-aware experiments \([Section0\.E\.3](https://arxiv.org/html/2608.12961#Pt0.A5.SS3)\)\.

### 0\.E\.1Inference equations

The differentiable WMC layer supports three inference operations on the same SDDα\\alpha, varying only literal weights and evidence\.

#### Training loss\.

For\(𝐱,𝐞\)\(\\mathbf\{x\},\\mathbf\{e\}\),

L⁡\(θ,𝐱,𝐞\)=−log⁡𝖶𝖬𝖢⁡\(α,pθ​\(𝐱\),𝐞\)\.L\(\\theta;\\mathbf\{x\},\\mathbf\{e\}\)\\;=\\;\-\\log\\mathsf\{WMC\}\\\!\\bigl\(\\alpha;\\,p\_\{\\theta\}\(\\mathbf\{x\}\),\\,\\mathbf\{e\}\\bigr\)\.\(11\)The literal\-weight map \([Table1](https://arxiv.org/html/2608.12961#S3.T1)\) setsw​\(ℓ\):=pθ​\(ℓ\)w\(\\ell\):=p\_\{\\theta\}\(\\ell\)on positive ground literalsℓ∈𝒱𝒪Δ\\ell\\in\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}andw⁡\(¬ℓ\):=1−pθ​\(ℓ\)w\(\\neg\\ell\):=1\-p\_\{\\theta\}\(\\ell\)on negative ones; evidence literalsℓ∈𝐞\\ell\\in\\mathbf\{e\}clamp the negation weight to zero \(equivalent to conditioning the SDD onℓ\\ell\)\.

#### Conditional posterior at test time\.

For a query atomC⁡\(a\)C\(a\),

Pθ\(C\(a\)∣𝐱,𝐞\)=𝖶𝖬𝖢\(α;pθ\(𝐱\),𝐞∪\{C\(a\):=𝗍𝗋𝗎𝖾\}\)𝖶𝖬𝖢⁡\(α,pθ​\(𝐱\),𝐞\);P\_\{\\theta\}\(C\(a\)\\mid\\mathbf\{x\},\\mathbf\{e\}\)\\;=\\;\\frac\{\\mathsf\{WMC\}\\\!\\bigl\(\\alpha;\\,p\_\{\\theta\}\(\\mathbf\{x\}\),\\,\\mathbf\{e\}\\cup\\\{C\(a\):=\\mathsf\{true\}\\\}\\bigr\)\}\{\\mathsf\{WMC\}\\\!\\bigl\(\\alpha;\\,p\_\{\\theta\}\(\\mathbf\{x\}\),\\,\\mathbf\{e\}\\bigr\)\};\(12\)the latent\-class prediction on a closed family𝒟\\mathcal\{D\}is the argmaxD^​\(a\):=arg⁡maxDi∈𝒟​Pθ​\(Di​\(a\)∣𝐱,𝐞\)\\hat\{D\}\(a\):=\\arg\\max\_\{D\_\{i\}\\in\\mathcal\{D\}\}P\_\{\\theta\}\(D\_\{i\}\(a\)\\mid\\mathbf\{x\},\\mathbf\{e\}\)\. The denominator is strictly positive whenever𝐞\\mathbf\{e\}is consistent with𝒪\\mathcal\{O\}, so the ratio is well defined\.

#### Perception\-free entailment query\.

𝒪∪𝐞⊧C\(a\)⟺𝖶𝖬𝖢\(α;w1/2,𝐞∪\{C\(a\):=𝖿𝖺𝗅𝗌𝖾\}\)=0,\\mathcal\{O\}\\cup\\mathbf\{e\}\\models C\(a\)\\;\\Longleftrightarrow\\;\\mathsf\{WMC\}\\\!\\bigl\(\\alpha;\\,w\_\{1/2\},\\,\\mathbf\{e\}\\cup\\\{C\(a\):=\\mathsf\{false\}\\\}\\bigr\)=0,\(13\)wherew1/2w\_\{1/2\}assigns12\\tfrac\{1\}\{2\}to every literal: asserting¬C⁡\(a\)\\neg C\(a\)leaves no𝒪\\mathcal\{O\}\-consistent assignment iff the entailment holds\. The same SDD acts as an off\-line ELK reasoner overΔ\\Delta, independent of any neural model\. All three operations run inO⁡\(\|α\|\)O\(\|\\alpha\|\)\([Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4)\)\.

### 0\.E\.2Training step and gradient flow

A single training step on minibatch\{\(𝐱i,𝐞i\)\}i\\\{\(\\mathbf\{x\}\_\{i\},\\mathbf\{e\}\_\{i\}\)\\\}\_\{i\}proceeds as follows\.

1. 1\.*Perception forward\.*The neural extractorfθ:𝒳\|Δ\|→\[0,1\]\|𝒱𝒪Δ\|f\_\{\\theta\}:\\mathcal\{X\}^\{\|\\Delta\|\}\\to\[0,1\]^\{\|\\mathcal\{V\}\_\{\\mathcal\{O\}\}^\{\\Delta\}\|\}maps the input tuple to a per\-atom probability vectorpθ​\(𝐱i\)p\_\{\\theta\}\(\\mathbf\{x\}\_\{i\}\), factorized as∏ℓpθ​\(ℓ∣𝐱i\)\\prod\_\{\\ell\}p\_\{\\theta\}\(\\ell\\mid\\mathbf\{x\}\_\{i\}\)\(the marginal\-independence factorization targeted by the RS literature, §[2\.2](https://arxiv.org/html/2608.12961#S2.SS2)\)\.
2. 2\.*Literal\-weight assignment\.*The atom\-weight map of[Table1](https://arxiv.org/html/2608.12961#S3.T1)routespθ​\(ℓ∣𝐱i\)p\_\{\\theta\}\(\\ell\\mid\\mathbf\{x\}\_\{i\}\)to literalℓ\\elland1−pθ​\(ℓ∣𝐱i\)1\-p\_\{\\theta\}\(\\ell\\mid\\mathbf\{x\}\_\{i\}\)to¬ℓ\\neg\\ell\. Evidence𝐞i\\mathbf\{e\}\_\{i\}clamps observed literals\.
3. 3\.*SDD WMC traversal\.*The post\-order traversal visits each node once \(memoized by node id\) and accumulates the WMC value \([Equation8](https://arxiv.org/html/2608.12961#Pt0.A3.E8)\) inO⁡\(\|α\|\)O\(\|\\alpha\|\)time\. Smoothness, decomposability, and determinism \([Appendix0\.D](https://arxiv.org/html/2608.12961#Pt0.A4)\) make each sum disjoint and each product over disjoint scopes, so the result is exact\.
4. 4\.*Loss aggregation\.*L\(θ\)=−1n∑ilog𝖶𝖬𝖢\(α;pθ\(𝐱i\),𝐞i\)L\(\\theta\)=\-\\frac\{1\}\{n\}\\sum\_\{i\}\\log\\mathsf\{WMC\}\(\\alpha;p\_\{\\theta\}\(\\mathbf\{x\}\_\{i\}\),\\mathbf\{e\}\_\{i\}\)\.
5. 5\.*Backward pass\.*PyTorch autograd composes the backward pass through the same WMC traversal atO⁡\(\|α\|\)O\(\|\\alpha\|\)additional cost, plus the perception backbone’s own backward pass\. Every intermediate WMC value is the product/sum of literal weights, hence differentiable inθ\\thetavia the chain rule:∇θL=−1n∑i\(𝖶𝖬𝖢i\)−1∇θ𝖶𝖬𝖢i\\nabla\_\{\\theta\}L=\-\\frac\{1\}\{n\}\\sum\_\{i\}\(\\mathsf\{WMC\}\_\{i\}\)^\{\-1\}\\,\\nabla\_\{\\theta\}\\mathsf\{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 \([Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)\)\.

### 0\.E\.3RS\-mitigation wrapper losses

The compilation algorithm of §[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)is independent of the perception’s output distribution:α\\alphadepends only on\(𝒪,Δ\)\(\\mathcal\{O\},\\Delta\), so RS\-aware methods plug in by replacing the literal weightspθ​\(𝐱\)p\_\{\\theta\}\(\\mathbf\{x\}\)in[Equation11](https://arxiv.org/html/2608.12961#Pt0.A5.E11)without modifyingα\\alphaor the WMC traversal\.

#### Moose\+BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]\.

BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]trains aKK\-encoder ensemble\{θk\}k=1K\\\{\\theta\_\{k\}\\\}\_\{k=1\}^\{K\}that sharesα\\alphabut diversifies over the RS equivalence class\. Members are trained sequentially: at stepkk, the new encoderθk\\theta\_\{k\}is fit by maximizing the BEARS objective\[[40](https://arxiv.org/html/2608.12961#bib.bib40), Eq\. 7\]

LBears\(θk;𝐱,𝐞\)=L\(θk;𝐱,𝐞\)\+γ1KL\(pθk∥1k∑j=1kpθj\)\+γ2H\(pθk\),L\_\{\\textsc\{Bears\}\}\(\\theta\_\{k\};\\mathbf\{x\},\\mathbf\{e\}\)\\;=\\;L\(\\theta\_\{k\};\\mathbf\{x\},\\mathbf\{e\}\)\\,\+\\,\\gamma\_\{1\}\\,\\mathrm\{KL\}\\\!\\left\(p\_\{\\theta\_\{k\}\}\\,\\Big\\\|\\,\\tfrac\{1\}\{k\}\\sum\_\{j=1\}^\{k\}p\_\{\\theta\_\{j\}\}\\right\)\\,\+\\,\\gamma\_\{2\}\\,H\(p\_\{\\theta\_\{k\}\}\),\(14\)where the KL term against the running average over members1,…,k1,\\dots,kencouragesθk\\theta\_\{k\}to commit to a different shortcut than its predecessors, and the entropy termH⁡\(pθk\)H\(p\_\{\\theta\_\{k\}\}\)prevents collapse to a degenerate posterior\. At test time, the ensemble averages the per\-atom marginals:p⁡\(ℓ∣𝐱\)=1K​∑kpθk​\(ℓ∣𝐱\)p\(\\ell\\mid\\mathbf\{x\}\)=\\tfrac\{1\}\{K\}\\sum\_\{k\}p\_\{\\theta\_\{k\}\}\(\\ell\\mid\\mathbf\{x\}\), spreading mass across multiple shortcut explanations\. We useK=5K\{=\}5, entropy weightγ2=0\.1\\gamma\_\{2\}\{=\}0\.1, and per\-regime tuning of the KL weightγ1\\gamma\_\{1\}\([Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\)\.

#### Moose\+NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]\.

NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]replaces the marginal\-independence factorizationpθ​\(𝐜∣𝐱\)=∏ipθ​\(ci∣𝐱\)p\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)=\\prod\_\{i\}p\_\{\\theta\}\(c\_\{i\}\\mid\\mathbf\{x\}\)with a masked\-discrete\-diffusion variational distributionqθ​\(𝐜∣𝐱\)q\_\{\\theta\}\(\\mathbf\{c\}\\mid\\mathbf\{x\}\)that models cross\-atom dependencies through a denoising trajectory overTTtimesteps\. The continuous\-time negative evidence lower bound \(NELBO\) objective is

ℒNeSyDM​\(θ\)=𝔼qθ​\[−log⁡𝖶𝖬𝖢⁡\(α,qθ​\(𝐱\),𝐞\)\]\+γc​ℒc​\(θ\)\+γh​ℒh​\(θ\),\\mathcal\{L\}\_\{\\text\{NeSyDM\}\}\(\\theta\)\\;=\\;\\mathbb\{E\}\_\{q\_\{\\theta\}\}\\\!\\bigl\[\-\\log\\mathsf\{WMC\}\(\\alpha;q\_\{\\theta\}\(\\mathbf\{x\}\),\\mathbf\{e\}\)\\bigr\]\\;\+\\;\\gamma\_\{c\}\\,\\mathcal\{L\}\_\{c\}\(\\theta\)\\;\+\\;\\gamma\_\{h\}\\,\\mathcal\{L\}\_\{h\}\(\\theta\),\(15\)whereℒc\\mathcal\{L\}\_\{c\}is the masked\-diffusion concept\-unmasking lossLcL\_\{c\}of\[[30](https://arxiv.org/html/2608.12961#bib.bib30), §3\.2\]andℒh\\mathcal\{L\}\_\{h\}the variational\-entropy termLH⁡\[q\]L\_\{H\[q\]\}that maximizes the entropy ofqθq\_\{\\theta\}at the fully\-masked step\. The expectation underqθq\_\{\\theta\}is intractable in closed form; we use two gradient estimators:*\(a\) RLOO*\[[28](https://arxiv.org/html/2608.12961#bib.bib28)\], a leave\-one\-out REINFORCE baseline that drawsSSsamples fromqθq\_\{\\theta\}and uses the sample average over the otherS−1S\{\-\}1as the control variate;*\(b\) exact\-WMC*, which replaces sampling by direct WMC evaluation−log⁡𝖶𝖬𝖢⁡\(α,q¯θ,𝐞\)\-\\log\\mathsf\{WMC\}\(\\alpha;\\bar\{q\}\_\{\\theta\},\\mathbf\{e\}\)on the average per\-atom marginalq¯θ\\bar\{q\}\_\{\\theta\}when the diffusion\-step posterior factorizes across atoms\. We use the NeSyDM\-repository defaultsβ=10\\beta\{=\}10andT=10T\{=\}10continuous\-time mask budget;\(γc,γh\)\(\\gamma\_\{c\},\\gamma\_\{h\}\)are swept per regime \([Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\)\.

Both wrappers shareα\\alphaacross all encoders/timesteps and inherit theO⁡\(\|α\|\)O\(\|\\alpha\|\)inference cost of[Theorem0\.D\.4](https://arxiv.org/html/2608.12961#Pt0.A4.Thmtheorem4), multiplied byKKfor BEARS or by the diffusion budgetT⋅ST\\cdot Sfor NeSyDM\.

### 0\.E\.4Non\-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](https://arxiv.org/html/2608.12961#bib.bib7)\]\.

Eachℰ​ℒ\+⁣\+\\mathcal\{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=a​ba\\wedge b=ab,a∨b=a\+b−a​ba\\vee b=a\+b\-ab,a→b=1−a\+a​ba\\to b=1\-a\+ab\)\. The translations used areC⊑D↦∀x\.C⁡\(x\)→D⁡\(x\)C\\sqsubseteq D\\mapsto\\forall x\.\\,C\(x\)\\to D\(x\),C⊓D⊑E↦∀x\.C⁡\(x\)∧D⁡\(x\)→E⁡\(x\)C\\sqcap D\\sqsubseteq E\\mapsto\\forall x\.\\,C\(x\)\\wedge D\(x\)\\to E\(x\),C⊑∃R\.D↦∀x\.C⁡\(x\)→∃y\.R⁡\(x,y\)∧D⁡\(y\)C\\sqsubseteq\\exists R\.D\\mapsto\\forall x\.\\,C\(x\)\\to\\exists y\.\\,R\(x,y\)\\wedge D\(y\), and the symmetric variants for∃R\.C⊑D\\exists R\.C\\sqsubseteq D,C⊓D⊑⊥C\\sqcap D\\sqsubseteq\\bot,R⊑SR\\sqsubseteq S, andR1∘R2⊑SR\_\{1\}\\circ R\_\{2\}\\sqsubseteq S\. Per\-atom truth values come from the same perception output that the WMC baselines use;∀\\foralland∃\\existsare aggregated by the generalized meanp\_mean​\(v1,…,vn\)=\(1n​∑ivip\)1/p\\textsf\{p\\\_mean\}\(v\_\{1\},\\dots,v\_\{n\}\)=\(\\tfrac\{1\}\{n\}\\sum\_\{i\}v\_\{i\}^\{p\}\)^\{1/p\}with sweepable exponentp∈\{2,4\}p\\in\\\{2,4\\\}\([Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\)\. The training loss is1−SAT1\-\\mathrm\{SAT\}whereSAT\\mathrm\{SAT\}is the satisfaction aggregator across all axiom\-grounded formulas\. LTN does not compute an exact joint distribution over ground atoms\.

#### ELEmbeddings\[[36](https://arxiv.org/html/2608.12961#bib.bib36),[54](https://arxiv.org/html/2608.12961#bib.bib54)\]\.

The sameℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}geometric encoding underlies DeepGO\-SE\[[34](https://arxiv.org/html/2608.12961#bib.bib34)\], 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 theMooseperception backbone rather than a sequence encoder\. Each named conceptCCis embedded as annn\-ball with centrecC∈ℝdc\_\{C\}\\in\\mathbb\{R\}^\{d\}and radiusrCr\_\{C\}; each roleRRas a translation vectorρR∈ℝd\\rho\_\{R\}\\in\\mathbb\{R\}^\{d\}\. A linear head projects the perception’s CNN latentψ⁡\(𝐱\)∈ℝ128\\psi\(\\mathbf\{x\}\)\\in\\mathbb\{R\}^\{128\}into the sameℝd\\mathbb\{R\}^\{d\}space, yielding a per\-individual pointzaz\_\{a\}\. The class\-membership score isP⁡\(C⁡\(a\)\)=σ⁡\(margin−\(‖za−cC‖−rC\)\)P\(C\(a\)\)=\\sigma\(\\textsf\{margin\}\-\(\\\|z\_\{a\}\-c\_\{C\}\\\|\-r\_\{C\}\)\)\(image inside the ball⇒\\Rightarrowatom true\) and the role\-atom score isP⁡\(R⁡\(a,b\)\)=σ⁡\(margin−‖za\+ρR−zb‖\)P\(R\(a,b\)\)=\\sigma\(\\textsf\{margin\}\-\\\|z\_\{a\}\+\\rho\_\{R\}\-z\_\{b\}\\\|\)\. The TBox loss is the sum of mOWL’s NF1–NF4 losses\[[36](https://arxiv.org/html/2608.12961#bib.bib36),[54](https://arxiv.org/html/2608.12961#bib.bib54)\]\(mean\-aggregated per normal form\), and the total objective isℒ=ℒperception\+λEL​ℒTBox\\mathcal\{L\}=\\mathcal\{L\}\_\{\\text\{perception\}\}\+\\lambda\_\{\\text\{EL\}\}\\,\\mathcal\{L\}\_\{\\text\{TBox\}\}withℒperception\\mathcal\{L\}\_\{\\text\{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\.FExperimental details

This part of the appendix collects the materials supporting experiments: the full MNIST ontology used by all three MNIST experiments \([Section0\.F\.2](https://arxiv.org/html/2608.12961#Pt0.A6.SS2)\), per\-method hyperparameter sweeps and the tuned configurations used in the result tables \([Section0\.F\.4](https://arxiv.org/html/2608.12961#Pt0.A6.SS4)\), and the full per\-regime breakdown across all six metrics \([Section0\.F\.6](https://arxiv.org/html/2608.12961#Pt0.A6.SS6)\)\.

### 0\.F\.1Compiled\-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𝒪\\mathcal\{O\}and the ABox domainΔ\\Deltaalone, not of the learning method\. EveryMoosevariant and every SDD\-based baseline in a given regime therefore shares the circuit in the corresponding row of[Table7](https://arxiv.org/html/2608.12961#Pt0.A6.T7)\.

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\\leq 0\.75s in every configuration, and in≤0\.35\\leq 0\.35s in all but the two DeepProbLog cells \(0\.680\.68s on Exp\. 2,0\.710\.71s 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 representativeMoose\-WMC run per regime \(batch size3232; 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\.Compile time grows with the ABox domain as analyzed in[Section0\.D\.5](https://arxiv.org/html/2608.12961#Pt0.A4.SS5): the SDD node count fits∝\|Δ\|2\.9\\propto\|\\Delta\|^\{2\.9\}for\|Δ\|≤3\|\\Delta\|\\leq 3, with a40×40\\timescompile\-time jump at\|Δ\|=4\|\\Delta\|=4\. The\|Δ\|=2\|\\Delta\|=2configurations used throughout §[5](https://arxiv.org/html/2608.12961#S5)sit well inside the sub\-second regime\.

Peak GPU memory at circuit\-build time is00in 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 roughly1111minutes at\|Δ\|=1\|\\Delta\|\{=\}1\(Exp\. 1\) and6565–7575minutes at\|Δ\|=2\|\\Delta\|\{=\}2\(Exps\. 2–3\), with peak GPU memory of3535–5656MB; the Pizzaïolo tracks train in under99minutes each \(Track C, a single binary label, in well under a minute\) but use≈900\\approx 900MB, reflecting the larger image encoder rather than any growth in the circuit \([Table7](https://arxiv.org/html/2608.12961#Pt0.A6.T7)\)\. Peak memory therefore tracks the backbone and batch size, not the compiled SDD, whose own device footprint is negligible\.

### 0\.F\.2Full MNIST ontology

The single OWL EL ontology𝒪MNIST\\mathcal\{O\}\_\{\\textsf\{MNIST\}\}used by all three MNIST experiments \(§[5\.1](https://arxiv.org/html/2608.12961#S5.SS1)\) consists of7676axioms over𝖲𝗂𝗀C=\{D0,…,D9,Even,Odd,Prime,Composite\}\\mathsf\{Sig\}\_\{C\}=\\\{D\_\{0\},\\dots,D\_\{9\},\\textsf\{Even\},\\textsf\{Odd\},\\textsf\{Prime\},\\textsf\{Composite\}\\\}and𝖲𝗂𝗀R=\{succ,plus\_two\}\\mathsf\{Sig\}\_\{R\}=\\\{\\textsf\{succ\},\\textsf\{plus\\\_two\}\\\}, listed below in EL DL syntax\. Numerals 0–9 are read as the correspondingDiD\_\{i\}\.

#### NF1: property subsumptions \(1818\)\.

D0⊑EvenD\_\{0\}\\sqsubseteq\\textsf\{Even\};D2⊑EvenD\_\{2\}\\sqsubseteq\\textsf\{Even\};D4⊑EvenD\_\{4\}\\sqsubseteq\\textsf\{Even\};D6⊑EvenD\_\{6\}\\sqsubseteq\\textsf\{Even\};D8⊑EvenD\_\{8\}\\sqsubseteq\\textsf\{Even\};D1⊑OddD\_\{1\}\\sqsubseteq\\textsf\{Odd\};D3⊑OddD\_\{3\}\\sqsubseteq\\textsf\{Odd\};D5⊑OddD\_\{5\}\\sqsubseteq\\textsf\{Odd\};D7⊑OddD\_\{7\}\\sqsubseteq\\textsf\{Odd\};D9⊑OddD\_\{9\}\\sqsubseteq\\textsf\{Odd\};D2⊑PrimeD\_\{2\}\\sqsubseteq\\textsf\{Prime\};D3⊑PrimeD\_\{3\}\\sqsubseteq\\textsf\{Prime\};D5⊑PrimeD\_\{5\}\\sqsubseteq\\textsf\{Prime\};D7⊑PrimeD\_\{7\}\\sqsubseteq\\textsf\{Prime\};D4⊑CompositeD\_\{4\}\\sqsubseteq\\textsf\{Composite\};D6⊑CompositeD\_\{6\}\\sqsubseteq\\textsf\{Composite\};D8⊑CompositeD\_\{8\}\\sqsubseteq\\textsf\{Composite\};D9⊑CompositeD\_\{9\}\\sqsubseteq\\textsf\{Composite\}\.

#### NF2: disjointness \(4747\)\.

Even⊓Odd⊑⊥\\textsf\{Even\}\\sqcap\\textsf\{Odd\}\\sqsubseteq\\bot;Prime⊓Composite⊑⊥\\textsf\{Prime\}\\sqcap\\textsf\{Composite\}\\sqsubseteq\\bot; plusDi⊓Dj⊑⊥D\_\{i\}\\sqcap D\_\{j\}\\sqsubseteq\\botfor every0≤i<j≤90\\leq i<j\\leq 9\(\(102\)=45\\binom\{10\}\{2\}=45pairs\)\.

#### NF3: successor existentials \(1010\)\.

Di⊑∃succ\.D\(i\+1\)mod10D\_\{i\}\\sqsubseteq\\exists\\textsf\{succ\}\.\\,D\_\{\(i\+1\)\\bmod 10\}for eachi∈\{0,1,…,9\}i\\in\\\{0,1,\\dots,9\\\}\. The chain is cyclic \(D9⊑∃succ\.D0D\_\{9\}\\sqsubseteq\\exists\\textsf\{succ\}\.\\,D\_\{0\}\); without the signature side condition \([Appendix0\.C](https://arxiv.org/html/2608.12961#Pt0.A3)\) saturation would diverge\.

#### NF7: role chain \(11\)\.

succ∘succ⊑plus\_two\\textsf\{succ\}\\circ\\textsf\{succ\}\\sqsubseteq\\textsf\{plus\\\_two\}\.

#### Saturation closure used by the experiments\.

ELK derives the chain consequenceDi⊑∃plus\_two\.D\(i\+2\)mod10D\_\{i\}\\sqsubseteq\\exists\\textsf\{plus\\\_two\}\.\\,D\_\{\(i\+2\)\\bmod 10\}via the role\-composition ruleR∘R\_\{\\circ\}\(givenDi⊑∃succ\.Di\+1D\_\{i\}\\sqsubseteq\\exists\\textsf\{succ\}\.D\_\{i\+1\},Di\+1⊑∃succ\.Di\+2D\_\{i\+1\}\\sqsubseteq\\exists\\textsf\{succ\}\.D\_\{i\+2\}, andsucc∘succ⊑plus\_two\\textsf\{succ\}\\circ\\textsf\{succ\}\\sqsubseteq\\textsf\{plus\\\_two\}, inferDi⊑∃plus\_two\.Di\+2D\_\{i\}\\sqsubseteq\\exists\\textsf\{plus\\\_two\}\.D\_\{i\+2\}\[[26](https://arxiv.org/html/2608.12961#bib.bib26)\]\) populatingΛ\\Lambdawith theplus\_twolinks that the role\-chain experiment relies on\. The fourMooseextractors then groundΣ\\SigmaandΛ\\Lambdainto the clauses ofΓEL\\Gamma\_\{\\textsf\{EL\}\}, and the closure axiomsΦclos\\Phi\_\{\\textsf\{clos\}\}over the exhaustive family\{D0,…,D9\}\\\{D\_\{0\},\\dots,D\_\{9\}\\\}supply\(102\)​m\+m\\binom\{10\}\{2\}m\+mdisjointness and covering clauses plus the six reverse clauses per individual \(one per distinct parity\-primality profile; §[3\.3](https://arxiv.org/html/2608.12961#S3.SS3)\)\.

### 0\.F\.3Perception architecture

Both MNIST and Pizzaïolo experiments train the perception encoder from scratch\. The MNIST encoder \(used in Experiments 1–3\) takes a28×2828\{\\times\}28grayscale image through two Conv→\\toReLU→\\toMaxPool\(2×22\{\\times\}2\) blocks of3232and6464channels \(3×33\{\\times\}3kernels, padding11\), flattens to64⋅7⋅764\{\\cdot\}7\{\\cdot\}7features, and applies a fully\-connected layer to a128128\-dim latent followed by a linear head to per\-concept logits\. The Pizzaïolo encoder \(Experiment 4\) takes a224×224224\{\\times\}224RGB image through four Conv→\\toReLU→\\toMaxPool blocks of3232,6464,128128,128128channels \(3×33\{\\times\}3kernels, padding11\), then global average pooling to128128features and the same128→128→n\_concepts128\\to 128\\to\\text\{n\\\_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\.4Hyperparameter 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\{\}\_\{\\text\{cons\}\}andAccdigit\\text\{Acc\}\_\{\\text\{digit\}\}on the seed\-0 cell, and then ran a55\-seed final at that configuration\. All methods share Adam\[[27](https://arxiv.org/html/2608.12961#bib.bib27)\]with batch size3232,3030epochs on MNIST and6060epochs on Pizzaïolo Tracks A/B \(Track C uses1515epochs because the binaryis\_spicysupervision saturates faster\), unless otherwise noted\. The reported MNIST headline tables in[Tables2](https://arxiv.org/html/2608.12961#S5.T2)and[3](https://arxiv.org/html/2608.12961#S5.T3)use55seeds at the tuned HPs; the Pizzaïolo tables \([Tables2](https://arxiv.org/html/2608.12961#S5.T2)and[3](https://arxiv.org/html/2608.12961#S5.T3)\) use55seeds at the tuned HPs except where indicated\.

#### Moose/ Semantic\-loss WMC\.

Sweep overlr∈\{10−3,3⋅10−3\}\\textit\{lr\}\\in\\\{10^\{\-3\},3\{\\cdot\}10^\{\-3\}\\\}per regime\. Best: mnist1 / mnist3 / pizzaC uselr=3⋅10−3\\textit\{lr\}\{=\}3\{\\cdot\}10^\{\-3\}; mnist2 / pizzaA / pizzaB uselr=10−3\\textit\{lr\}\{=\}10^\{\-3\}\. The SDD compilation is determined by𝒪\\mathcal\{O\}andΔ\\Delta, so the only free knob is the perception backbone’s optimiser\. A wider\-range sensitivity analysis over this knob is in[Section0\.F\.5](https://arxiv.org/html/2608.12961#Pt0.A6.SS5)\.

#### DeepProbLog\[[39](https://arxiv.org/html/2608.12961#bib.bib39)\]\.

Sweep overlr∈\{10−3,3⋅10−3\}\\textit\{lr\}\\in\\\{10^\{\-3\},3\{\\cdot\}10^\{\-3\}\\\}\. Both regimes \(mnist2, mnist3\) preferlr=10−3\\textit\{lr\}\{=\}10^\{\-3\}; thenn​\(⋅\)\\textsf\{nn\}\(\\cdot\)predicate’s softmax matches the latent signature𝖲𝗂𝗀Cℓ\\mathsf\{Sig\}^\{\\ell\}\_\{C\}exactly \(one head per concept family\); no additional HPs\.

#### Moose\+BEARS\[[40](https://arxiv.org/html/2608.12961#bib.bib40)\]\.

Ensemble sizeK=5K\{=\}5, entropy weightγ2=0\.1\\gamma\_\{2\}\{=\}0\.1at the BEARS\-paper default; sweep over the KL weightγ1∈\{0\.5,1\.0,2\.0\}\\gamma\_\{1\}\\in\\\{0\.5,1\.0,2\.0\\\}on every regime\. The MNIST sweep is uniform onγ1=1\.0\\gamma\_\{1\}\{=\}1\.0\(the BEARS\-paper default\), so the final 5\-seed run usesγ1=1\.0\\gamma\_\{1\}\{=\}1\.0on mnist1, mnist2, mnist3\. On Pizzaïolo,γ1\\gamma\_\{1\}was tuned per track: pizzaA →γ1=1\.0\\gamma\_\{1\}\{=\}1\.0, pizzaB →γ1=2\.0\\gamma\_\{1\}\{=\}2\.0, pizzaC →γ1=1\.0\\gamma\_\{1\}\{=\}1\.0\.

#### Moose\+NeSyDM\[[30](https://arxiv.org/html/2608.12961#bib.bib30)\]\.

Sweep over\(γc,γh\)∈\{0\.1,1\.0\}×\{1\.0,2\.0\}\(\\gamma\_\{c\},\\gamma\_\{h\}\)\\in\\\{0\.1,1\.0\\\}\\times\\\{1\.0,2\.0\\\}per regime \(44cells\), at the RLOO gradient estimator\.β=10\\beta\{=\}10andT=10T\{=\}10\(continuous\-time mask budget\) are the NeSyDM\-repository defaults, adopted unchanged\. Best per regime: mnist1 →\(γc=1\.0,γh=2\.0\)\(\\gamma\_\{c\}\{=\}1\.0,\\,\\gamma\_\{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](https://arxiv.org/html/2608.12961#bib.bib7)\]\.

Product T\-norm; sweep over the p\-mean aggregator exponentforall\_p=exists\_p∈\{2,4\}\\textsf\{forall\\\_p\}\{=\}\\textsf\{exists\\\_p\}\\in\\\{2,4\\\}on every regime, and additionally overexists\_mode∈\{universe,skolem\}\\textsf\{exists\\\_mode\}\\in\\\{\\textsf\{universe\},\\textsf\{skolem\}\\\}on MNIST relational/role\-chain\. Best:forall\_p=4\\textsf\{forall\\\_p\}\{=\}4uniformly across all six regimes;exists\_mode=universe\\textsf\{exists\\\_mode\}\{=\}\\textsf\{universe\}on mnist2 and mnist3 \(skolem produced equivalent or worseAccdigit\\text\{Acc\}\_\{\\text\{digit\}\}at single seed\)\.lr=10−3\\textit\{lr\}\{=\}10^\{\-3\}\.

#### ELEmbeddings\[[36](https://arxiv.org/html/2608.12961#bib.bib36)\]/ mOWL\[[54](https://arxiv.org/html/2608.12961#bib.bib54)\]\.

Sweep over\(embed\_dim,margin\)∈\{50,128\}×\{0\.1,0\.5\}\(\\textsf\{embed\\\_dim\},\\textsf\{margin\}\)\\in\\\{50,128\\\}\\times\\\{0\.1,0\.5\\\}per regime \(44cells\)\. Best: mnist1 / mnist2 / mnist3 / pizzaB→\(embed\_dim=50,margin=0\.1\)\\to\(\\textsf\{embed\\\_dim\}\{=\}50,\\,\\textsf\{margin\}\{=\}0\.1\); pizzaA→\(128,0\.5\)\\to\(128,0\.5\)\(best Brier among the four cells; all four reachedAccC=1\.0\\text\{Acc\}\_\{C\}\{=\}1\.0on the in\-distribution split\)\. For mnist3 the EL ball loss is augmented with an explicitplus\_tworole\-chain penalty term \(vanilla ELEmbeddings has no normal form for role chains;[Section0\.E\.4](https://arxiv.org/html/2608.12961#Pt0.A5.SS4)\)\.

#### Independent \(BCE\)\.

Sweep overlr∈\{3⋅10−4,10−3,3⋅10−3\}\\textit\{lr\}\\in\\\{3\{\\cdot\}10^\{\-4\},10^\{\-3\},3\{\\cdot\}10^\{\-3\}\\\}per MNIST regime\. Best: mnist1 / mnist3 uselr=3⋅10−4\\textit\{lr\}\{=\}3\{\\cdot\}10^\{\-4\}\(bestAccatom\\text\{Acc\}\_\{\\text\{atom\}\}\+ ECE\); mnist2 useslr=3⋅10−3\\textit\{lr\}\{=\}3\{\\cdot\}10^\{\-3\}\. Per\-atom BCE on the observed evidence atoms only; no symbolic structure enters the loss\.

#### Summary\.

The final numbers in[Tables2](https://arxiv.org/html/2608.12961#S5.T2)and[3](https://arxiv.org/html/2608.12961#S5.T3)are55\-seed means at the per\-regime\-tuned hyperparameters above, after a per\-method single\-seed sweep\.

### 0\.F\.5Learning\-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\. BecauseMooseexposes 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\.[Table8](https://arxiv.org/html/2608.12961#Pt0.A6.T8)reportsMooseaccuracy at each rate \(33seeds per cell\); the metric isAccF\\text\{Acc\}\_\{F\}on MNIST andAccC\\text\{Acc\}\_\{C\}on Pizzaïolo \([Section5\.3](https://arxiv.org/html/2608.12961#S5.SS3)\)\. Track C is not included in this sweep\.

Table 8:Mooselearning\-rate sensitivity \(33seeds per cell, mean±\\pms\.d\.\)\. Metric:AccF\\text\{Acc\}\_\{F\}on MNIST Experiments 2–3,AccC\\text\{Acc\}\_\{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\)\.On MNIST and Pizza A the response is unimodal, with the optimum in the interior of the grid \(10−310^\{\-3\}or3⋅10−33\{\\cdot\}10^\{\-3\}\) and the extreme rates worst, as expected; Pizza B is flatter and less regular, its per\-rate means varying little \(all within0\.7860\.786–0\.8460\.846\) with no clear interior peak\.Mooseis robust on Exp\. 2 and Pizza A \(spread≤0\.10\\leq 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\.6Full per\-regime results

Table 9:Full per\-regime results, six metrics\. Means±\\pms\.d\. over55seeds\. The third column isAccF\\text\{Acc\}\_\{F\}, family\-argmax accuracy, on the MNIST blocks andAccC\\text\{Acc\}\_\{C\}, per\-atom accuracy on the latent slice, on the Pizzaïolo blocks, which declare no exhaustive family on Track C \([Section0\.F\.7](https://arxiv.org/html/2608.12961#Pt0.A6.SS7)\); the two are compared only within a block\. Operative theory:ΓEL\+Φclos\\Gamma\_\{\\textsf\{EL\}\}\{\+\}\\Phi\_\{\\textsf\{clos\}\}for theMooserows on MNIST,ΓEL\\Gamma\_\{\\textsf\{EL\}\}for every other row \(closure is opt\-in and unused on Pizzaïolo\), and none for Independent\. RS=consConf⋅\(1−Acc\)\{\}\_\{\\text\{cons\}\}=\\mathrm\{Conf\}\\cdot\(1\-\\mathrm\{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\.F1macro\\text\{F1\}\_\{\\text\{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 theAccatom\\text\{Acc\}\_\{\\text\{atom\}\}andAccC\\text\{Acc\}\_\{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 theMoose\(Semantic\-loss WMC\) values, which[Proposition1](https://arxiv.org/html/2608.12961#Thmproposition1)shows the translation𝒫⁡\(ΓEL\)\\mathcal\{P\}\(\\Gamma\_\{\\textsf\{EL\}\}\)would attain exactly\. Note that this translation uses one independent probabilistic fact per ground atom, whereas the MNIST DeepProbLog programs use annn/4\\textsf\{nn\}/4annotated disjunction over the digit family, so the two halves of the row are different programs\. RScons\{\}\_\{\\text\{cons\}\}andF1macro\\text\{F1\}\_\{\\text\{macro\}\}on Track C \(binaryis\_spicysupervision\) collapse to00across all methods because the metric is defined over a multi\-class concept family; we mark these cells N/A\. Pizzaïolo Track A RScons\{\}\_\{\\text\{cons\}\}/F1macro\\text\{F1\}\_\{\\text\{macro\}\}are computed on the in\-distribution eval block \(the OOD harness does not record per\-atom logits for these metrics\)\.MethodAccatom↑\\text\{Acc\}\_\{\\text\{atom\}\}\\\!\\uparrowAccF/C↑\\text\{Acc\}\_\{F/C\}\\\!\\uparrowNLL↓\\\!\\downarrowECE↓\\\!\\downarrowRScons↓\{\}\_\{\\text\{cons\}\}\\\!\\downarrowF1macro↑\\text\{F1\}\_\{\\text\{macro\}\}\\\!\\uparrow*Experiment 1: atomic MNIST \(RQ1\)\.*\|Δ\|=1\|\\Delta\|\{=\}1, NF1/NF2 fragment\.Independent \(BCE\)58\.0±\\pm5\.613\.2±\\pm7\.92\.9±\\pm0\.29\.3±\\pm4\.515\.7±\\pm3\.37\.6±\\pm5\.7DeepProbLog89\.0±\\pm0\.842\.1±\\pm1\.31\.2±\\pm0\.110\.3±\\pm0\.931\.3±\\pm2\.631\.2±\\pm6\.9LTN92\.2±\\pm0\.125\.9±\\pm6\.51\.1±\\pm0\.010\.0±\\pm0\.047\.1±\\pm7\.816\.1±\\pm6\.7ELEmbeddings/mOWL90\.0±\\pm0\.134\.9±\\pm4\.20\.3±\\pm0\.03\.9±\\pm0\.414\.9±\\pm0\.925\.8±\\pm2\.8Moose\(Semantic\-loss WMC\)89\.3±\\pm1\.848\.1±\\pm10\.11\.6±\\pm0\.310\.6±\\pm1\.829\.0±\\pm4\.232\.1±\\pm10\.0Moose\+BEARS91\.2±\\pm0\.950\.1±\\pm5\.20\.3±\\pm0\.13\.9±\\pm1\.020\.0±\\pm1\.428\.0±\\pm6\.2Moose\+NeSyDM \(RLOO\)90\.6±\\pm0\.246\.6±\\pm2\.10\.3±\\pm0\.06\.0±\\pm0\.623\.2±\\pm0\.935\.8±\\pm1\.9Moose\+NeSyDM \(exact\)90\.1±\\pm1\.649\.4±\\pm9\.70\.7±\\pm0\.25\.1±\\pm1\.525\.6±\\pm2\.135\.9±\\pm8\.6*Experiment 2: relational MNIST \(RQ2\)\.*\|Δ\|=2\|\\Delta\|\{=\}2, NF3 cyclic\-successor TBox\.Independent \(BCE\)61\.8±\\pm4\.98\.8±\\pm4\.52\.8±\\pm0\.313\.4±\\pm3\.617\.6±\\pm2\.35\.7±\\pm3\.3DeepProbLog85\.3±\\pm0\.838\.9±\\pm3\.21\.4±\\pm0\.112\.3±\\pm0\.957\.9±\\pm3\.217\.5±\\pm4\.1LTN91\.9±\\pm0\.114\.5±\\pm4\.91\.2±\\pm0\.010\.0±\\pm0\.040\.1±\\pm8\.611\.4±\\pm5\.8ELEmbeddings/mOWL90\.1±\\pm0\.234\.8±\\pm3\.60\.4±\\pm0\.07\.2±\\pm0\.16\.9±\\pm0\.425\.8±\\pm3\.7Moose\(Semantic\-loss WMC\)93\.8±\\pm0\.374\.6±\\pm0\.30\.5±\\pm0\.14\.9±\\pm0\.324\.9±\\pm0\.363\.7±\\pm1\.1Moose\+BEARS93\.9±\\pm1\.176\.5±\\pm5\.90\.2±\\pm0\.04\.0±\\pm1\.218\.0±\\pm4\.567\.8±\\pm9\.3Moose\+NeSyDM \(RLOO\)90\.9±\\pm0\.458\.2±\\pm1\.40\.3±\\pm0\.07\.3±\\pm0\.730\.3±\\pm0\.845\.8±\\pm4\.3Moose\+NeSyDM \(exact\)92\.5±\\pm1\.262\.6±\\pm6\.11\.2±\\pm0\.27\.4±\\pm1\.237\.2±\\pm6\.159\.1±\\pm4\.5*Experiment 3: role\-chain MNIST \(RQ3\)\.*\|Δ\|=2\|\\Delta\|\{=\}2,plus\_two=succ∘succ\\textsf\{plus\\\_two\}\{=\}\\textsf\{succ\}\\circ\\textsf\{succ\}\.Independent \(BCE\)61\.5±\\pm3\.312\.2±\\pm7\.33\.3±\\pm0\.49\.0±\\pm8\.217\.5±\\pm3\.57\.9±\\pm4\.4DeepProbLog90\.6±\\pm3\.159\.6±\\pm13\.60\.9±\\pm0\.38\.0±\\pm2\.938\.3±\\pm12\.748\.4±\\pm14\.3LTN92\.0±\\pm0\.111\.0±\\pm7\.91\.2±\\pm0\.010\.0±\\pm0\.047\.1±\\pm6\.98\.2±\\pm6\.7ELEmbeddings/mOWL90\.4±\\pm0\.127\.4±\\pm7\.10\.3±\\pm0\.06\.3±\\pm0\.17\.5±\\pm0\.718\.7±\\pm6\.7Moose\(Semantic\-loss WMC\)98\.7±\\pm1\.896\.1±\\pm7\.20\.1±\\pm0\.21\.1±\\pm1\.53\.9±\\pm7\.193\.8±\\pm8\.6Moose\+BEARS94\.8±\\pm0\.589\.2±\\pm7\.20\.1±\\pm0\.05\.6±\\pm1\.18\.3±\\pm5\.281\.0±\\pm12\.2Moose\+NeSyDM \(RLOO\)91\.8±\\pm0\.562\.7±\\pm2\.90\.2±\\pm0\.04\.6±\\pm0\.828\.0±\\pm2\.157\.6±\\pm2\.0Moose\+NeSyDM \(exact\)92\.0±\\pm1\.260\.1±\\pm5\.71\.3±\\pm0\.27\.9±\\pm1\.136\.1±\\pm9\.762\.4±\\pm10\.1*Pizzaïolo Track A: pizza\-type, OOD eval \(RQ4\)\.*55held\-out tie\-breaker pizzas \([Section5\.2](https://arxiv.org/html/2608.12961#S5.SS2)\)\.Independent \(BCE\)46\.6±\\pm6\.221\.7±\\pm9\.76\.4±\\pm5\.058\.3±\\pm15\.462\.2±\\pm12\.311\.1±\\pm6\.4DeepProbLog‡68\.1±\\pm0\.368\.1±\\pm0\.34\.1±\\pm0\.230\.8±\\pm0\.74\.2±\\pm7\.614\.1±\\pm3\.5LTN74\.0±\\pm3\.422\.1±\\pm5\.213\.6±\\pm5\.452\.7±\\pm21\.857\.6±\\pm17\.310\.9±\\pm6\.8ELEmbeddings/mOWL77\.0±\\pm0\.925\.7±\\pm7\.34\.9±\\pm1\.049\.7±\\pm10\.254\.9±\\pm6\.611\.2±\\pm6\.5Moose\(Semantic\-loss WMC\)68\.1±\\pm0\.368\.1±\\pm0\.34\.1±\\pm0\.230\.8±\\pm0\.74\.2±\\pm7\.614\.1±\\pm3\.5Moose\+BEARS68\.6±\\pm0\.368\.6±\\pm0\.33\.3±\\pm0\.328\.2±\\pm1\.50\.6±\\pm0\.730\.1±\\pm10\.2Moose\+NeSyDM \(RLOO\)72\.2±\\pm1\.372\.2±\\pm1\.30\.6±\\pm0\.07\.5±\\pm1\.234\.3±\\pm4\.244\.8±\\pm6\.3Moose\+NeSyDM \(exact\)67\.4±\\pm1\.467\.4±\\pm1\.44\.6±\\pm0\.830\.8±\\pm3\.23\.8±\\pm8\.043\.4±\\pm3\.0*Pizzaïolo Track B: property\-class \(RQ4, RQ5\)\.*3\-way RS over the property class\.Independent \(BCE\)57\.2±\\pm3\.325\.0±\\pm0\.02\.7±\\pm0\.926\.4±\\pm17\.137\.0±\\pm12\.812\.0±\\pm1\.1DeepProbLog‡82\.4±\\pm1\.984\.5±\\pm2\.12\.4±\\pm0\.315\.5±\\pm2\.149\.8±\\pm4\.637\.8±\\pm1\.1LTN83\.3±\\pm1\.632\.5±\\pm20\.97\.0±\\pm6\.039\.3±\\pm17\.428\.8±\\pm12\.523\.4±\\pm19\.0ELEmbeddings/mOWL76\.9±\\pm0\.025\.0±\\pm0\.00\.6±\\pm0\.016\.1±\\pm0\.219\.5±\\pm0\.110\.0±\\pm0\.0Moose\(Semantic\-loss WMC\)82\.4±\\pm1\.984\.5±\\pm2\.12\.4±\\pm0\.315\.5±\\pm2\.149\.8±\\pm4\.637\.8±\\pm1\.1Moose\+BEARS85\.4±\\pm0\.887\.9±\\pm0\.90\.3±\\pm0\.012\.3±\\pm1\.030\.3±\\pm8\.642\.0±\\pm9\.0Moose\+NeSyDM \(RLOO\)80\.1±\\pm0\.878\.5±\\pm0\.80\.5±\\pm0\.02\.6±\\pm0\.938\.0±\\pm4\.722\.6±\\pm2\.3Moose\+NeSyDM \(exact\)86\.3±\\pm1\.984\.7±\\pm2\.22\.5±\\pm0\.415\.3±\\pm2\.250\.3±\\pm4\.437\.7±\\pm1\.0*Pizzaïolo Track C: is\_spicy \(RQ4, RQ5\)\.*Multi\-witness disjunction;1515epochs\.Independent \(BCE\)55\.2±\\pm5\.448\.9±\\pm5\.61\.0±\\pm0\.222\.1±\\pm9\.2N/AN/ADeepProbLog‡77\.3±\\pm2\.881\.0±\\pm3\.01\.5±\\pm0\.315\.3±\\pm1\.4N/AN/ALTN85\.1±\\pm0\.984\.8±\\pm0\.41\.3±\\pm0\.314\.1±\\pm0\.5N/AN/AELEmbeddings/mOWL78\.8±\\pm6\.575\.4±\\pm6\.60\.3±\\pm0\.111\.8±\\pm3\.8N/AN/AMoose\(Semantic\-loss WMC\)77\.3±\\pm2\.881\.0±\\pm3\.01\.5±\\pm0\.315\.3±\\pm1\.4N/AN/AMoose\+BEARS79\.9±\\pm3\.284\.2±\\pm3\.60\.4±\\pm0\.011\.3±\\pm3\.4N/AN/AMoose\+NeSyDM \(RLOO\)66\.1±\\pm3\.763\.9±\\pm3\.70\.7±\\pm0\.08\.9±\\pm1\.5N/AN/AMoose\+NeSyDM \(exact\)75\.9±\\pm1\.480\.1±\\pm1\.50\.8±\\pm0\.26\.9±\\pm2\.2N/AN/A[Table9](https://arxiv.org/html/2608.12961#Pt0.A6.T9)reports all six metrics \(Accatom\\text\{Acc\}\_\{\\text\{atom\}\}, the principal accuracy, NLL, ECE, RScons\{\}\_\{\\text\{cons\}\},F1macro\\text\{F1\}\_\{\\text\{macro\}\}\) per regime, laid out as six row\-blocks \(MNIST Experiments 1–3, Pizzaïolo Tracks A–C\)\. The compact main\-paper tables[Table2](https://arxiv.org/html/2608.12961#S5.T2)and[Table3](https://arxiv.org/html/2608.12961#S5.T3)are summary views of the principal\-accuracy and ECE columns of this table; per\-regimeAccatom\\text\{Acc\}\_\{\\text\{atom\}\}, NLL, RScons\{\}\_\{\\text\{cons\}\}, andF1macro\\text\{F1\}\_\{\\text\{macro\}\}appear only here\. RScons\{\}\_\{\\text\{cons\}\}andF1macro\\text\{F1\}\_\{\\text\{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\_spicybinary supervision\) both metrics are defined over a multi\-class concept family and are not applicable\.

### 0\.F\.7Family\-argmax on Pizzaïolo

Family\-argmax accuracyAccF\\text\{Acc\}\_\{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\},\\dots,D\_\{9\}\\\}is declared exhaustive andAccF\\text\{Acc\}\_\{F\}is the reported metric\. Pizzaïolo does not admit the same decode across its three tracks; we therefore reportAccC\\text\{Acc\}\_\{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 carryAccC\\text\{Acc\}\_\{C\}\.

Track C is the clear case:is\_spicysupervision is a multi\-witness disjunction over four spicy toppings and declares no exhaustive family, so there is no set to take an argmax over andAccF\\text\{Acc\}\_\{F\}is undefined; the harness records00for 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, soAccF\\text\{Acc\}\_\{F\}is unavailable there without a rerun\. Track B does admit the decode, over the33\-way property class, and we report it in[Table10](https://arxiv.org/html/2608.12961#Pt0.A6.T10): every method lands between48\.048\.0and50\.250\.2, a2\.22\.2\-point spread against per\-method standard deviations of3\.63\.6–5\.35\.3, so the metric separates no pair of methods\. TheAccC\\text\{Acc\}\_\{C\}column of the same runs spreads78\.578\.5–87\.987\.9and 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 keepAccC\\text\{Acc\}\_\{C\}and name it\.

Table 10:Pizzaïolo Track B under both accuracy metrics \(55seeds, mean±\\pms\.d\., %\)\.AccF\\text\{Acc\}\_\{F\}is the family\-argmax decode over the33\-way property class;AccC\\text\{Acc\}\_\{C\}is the per\-atom accuracy on the latent slice reported in[Table2](https://arxiv.org/html/2608.12961#S5.T2)\. Rows absent from theAccF\\text\{Acc\}\_\{F\}column did not record a family decode\. Tracks A and C are omitted: the metric is unavailable and undefined there respectively \(see text\)\.
### 0\.F\.8Paired significance of the headline comparisons

A mean±\\pms\.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 over2020seeds and test eachMoose\-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 thepp\-values are Holm\-corrected across the baselines, and we report significance atα=0\.05\\alpha=0\.05\. The metric is the regime’s headline accuracy: family\-argmax accuracyAccF\\text\{Acc\}\_\{F\}on MNIST Experiments 2–3, and latent\-concept accuracyAccC\\text\{Acc\}\_\{C\}on Pizzaïolo Tracks A–C \([Table11](https://arxiv.org/html/2608.12961#Pt0.A6.T11)\); the Pizzaïolo significance statements therefore concern the latent\-atom metric\.

Table 11:Paired significance ofMoose\(Semantic\-loss WMC\) against each baseline over2020shared seeds\. “diff” is the mean per\-seed difference \(Moose−\-baseline\); “Holmpp” is the Holm\-corrected Wilcoxonpp\-value within the regime\. The verdict is*win*\(Moosesignificantly higher\),*loss*\(significantly lower\), or*ns*\(not significant\) atα=0\.05\\alpha=0\.05\. Metric:AccF\\text\{Acc\}\_\{F\}on MNIST,AccC\\text\{Acc\}\_\{C\}on Pizzaïolo\. The2020\-seed reruns coverMoose, 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\) are55\-seed only and are not part of the paired analysis\.The relational and role\-chain regimes are unambiguous:Moosebeats every propositional baseline on Experiments 2–3 by margins that are large and significant \(Holmp≤0\.0002p\\leq 0\.0002\)\. On Pizzaïolo the picture is mixed, and we report it as such\.Mooseis significantly stronger than NeSyDM on Tracks B and C, but BEARS is significantly stronger thanMooseon both; on the Track A OOD split NeSyDM significantly overtakesMoose, while theMoose\-vs\-BEARS gap there is not significant\.Mooseis 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 the55\-seed headline tables \([Table2](https://arxiv.org/html/2608.12961#S5.T2)\) because this analysis uses the2020\-seed reruns; e\.g\.Mooseon Exp\. 2 is0\.7450\.745here versus0\.7460\.746in the55\-seed table\. These paired tests compareMooseagainst each baseline; the headline tables mark the raw column\-best rather than a significance verdict, since the2020\-seed reruns do not cover every method or regime \([Table11](https://arxiv.org/html/2608.12961#Pt0.A6.T11)\)\. The test covers accuracy only, so[Table3](https://arxiv.org/html/2608.12961#S5.T3)still marks the raw column\-best\.

### 0\.F\.9Inductive 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\\\!\\to\\\!1,2\\\!\\to\\\!3,\\dots,8\\\!\\to\\\!9\) and query individuals on the held\-out edges\{1,3,5,7,9\}\\\{1,3,5,7,9\\\}\(→2,→4,…,→01\\\!\\to\\\!2,3\\\!\\to\\\!4,\\dots,9\\\!\\to\\\!0\); on Exp\. 3 theplus\_tworelation forms two55\-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[Table12](https://arxiv.org/html/2608.12961#Pt0.A6.T12)\)\.

Table 12:Inductive generalization over2020seeds \(AccF\\text\{Acc\}\_\{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\)\.Mooseshows no inductive degradation on either regime: its held\-out\-configuration accuracy matches its transductive control to within noise \(−0\.032\-0\.032and−0\.021\-0\.021, i\.e\. marginally higher inductive\)\. NeSyDM, by contrast, collapses from0\.5940\.594/0\.7120\.712transductive to0\.1350\.135/0\.2540\.254on 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 pairedMoose\-vs\-Independent advantage on the inductive split is significant on Exp\. 2 \(Wilcoxonp<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\.10Closure ablation: separatingΓEL\\Gamma\_\{\\textsf\{EL\}\}fromΦclos\\Phi\_\{\\textsf\{clos\}\}

The compiled theory combines the EL\-aware extractorsΓEL\\Gamma\_\{\\textsf\{EL\}\}with the optional closure clausesΦclos\\Phi\_\{\\textsf\{clos\}\}, whose covering axiom⊤⊑⨆iDi\\top\\sqsubseteq\\bigsqcup\_\{i\}D\_\{i\}lies outside the EL profile\. To isolate their contributions we disableΦclos\\Phi\_\{\\textsf\{clos\}\}on all three MNIST regimes \(\-\-no\-closed\-world,55seeds\) and pair against the with\-closure baseline \([Table13](https://arxiv.org/html/2608.12961#Pt0.A6.T13)\)\.

Table 13:Closure ablation on MNIST\.AccF\\text\{Acc\}\_\{F\}\(mean±\\pms\.d\. over55seeds\) with and without the exhaustive\-family closure clausesΦclos\\Phi\_\{\\textsf\{clos\}\}\. The\-\-no\-closed\-worldarm removes mutual exclusion and covering in all three regimes and profile\-keyed reverse implications in Experiment 1\.Δ\\Deltais the change in the mean whenΦclos\\Phi\_\{\\textsf\{clos\}\}is removed\.WithoutΦclos\\Phi\_\{\\textsf\{clos\}\}the base WMC objective collapses toward chance in every regime, and the collapse deepens with relational complexity:AccF\\text\{Acc\}\_\{F\}falls by26\.426\.4,57\.257\.2, and86\.786\.7points on Experiments 1–3, reaching9\.49\.4\(chance is10\.010\.0\) on the role\-chain regime\. Experiment 1 is degenerate: all four methods land on the same seed\-independent21\.7±0\.021\.7\\pm 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\\Phi\_\{\\textsf\{clos\}\}package supplies the learning signal that makes the latent digit identifiable; the MNIST gains cannot be attributed toΓEL\\Gamma\_\{\\textsf\{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, retaining39\.439\.4\(Exp\. 2\) and46\.546\.5\(Exp\. 3\) against plainMoose’s17\.417\.4and9\.49\.4; BEARS buffers partially in both \(30\.930\.9and37\.137\.1\); and NeSyDM \(exact\) splits the two regimes, collapsing with the base objective on Experiment 2 \(17\.317\.3,Δ=−45\.3\\Delta\{=\}\{\-\}45\.3\) yet proving the most closure\-robust of any method on Experiment 3 \(54\.354\.3,Δ=−5\.8\\Delta\{=\}\{\-\}5\.8\)\. The wrappers that resist collapse also holdRScons\\text\{RS\}\_\{\\text\{cons\}\}down \(to0\.280\.28–0\.430\.43, against plainMoose’s0\.430\.43–0\.500\.50where 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\\Phi\_\{\\textsf\{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](https://arxiv.org/html/2608.12961#S5.SS3)to theΓEL\\Gamma\_\{\\textsf\{EL\}\}\-versus\-Φclos\\Phi\_\{\\textsf\{clos\}\}separation\.

## Appendix 0\.GRelated work: compilation, refinement, and embedding approaches

#### Rewriting\-based approaches\.

ℰ​ℒ\+⁣\+\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib33)\], and data\-independent transformations carry richer Horn DLs into Datalog while preserving assertion entailment\[[11](https://arxiv.org/html/2608.12961#bib.bib11)\]\.Mooseshares this view: Stage 2 of the pipeline \(§[3\.2](https://arxiv.org/html/2608.12961#S3.SS2)\) 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](https://arxiv.org/html/2608.12961#bib.bib12),[13](https://arxiv.org/html/2608.12961#bib.bib13),[24](https://arxiv.org/html/2608.12961#bib.bib24)\]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](https://arxiv.org/html/2608.12961#bib.bib53),[8](https://arxiv.org/html/2608.12961#bib.bib8)\]gains differentiability by replacing model\-theoretic entailment with a t\-norm relaxation\.Moosecompiles 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](https://arxiv.org/html/2608.12961#bib.bib37)\]compile an𝒜​ℒ​𝒞​ℐ\\mathcal\{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](https://arxiv.org/html/2608.12961#bib.bib53)\]approximatesℰ​ℒ\+⁣\+\\mathcal\{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𝖶𝖬𝖢\\mathsf\{WMC\}, partial\-supervision concept learning, or RS metrics\.

#### Refinement, clustering, and embeddings\.

Iterative Local Refinement \(ILR\)\[[19](https://arxiv.org/html/2608.12961#bib.bib19)\]corrects neural predictions at inference time so they satisfy a fuzzy\-logic relaxation of a propositional formula; Embed2Sym\[[4](https://arxiv.org/html/2608.12961#bib.bib4)\]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](https://arxiv.org/html/2608.12961#bib.bib36)\]maps concepts tonn\-balls and roles to translation vectors with NF1–NF4 margin losses that geometrise theℰ​ℒ\+⁣\+\\mathcal\{EL\}^\{\+\+\}axioms\. DeepGOZero\[[35](https://arxiv.org/html/2608.12961#bib.bib35)\]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 classnn\-balls through the GO axioms; predictions for a GO class with no training proteins are read off the same trainednn\-ball, giving zero\-shot annotations that ride on the ontology axioms alone\. DeepGO\-SE\[[34](https://arxiv.org/html/2608.12961#bib.bib34)\]reframes the same encoding as approximate semantic entailment\. Our ELEmbeddings baseline \([Section0\.E\.4](https://arxiv.org/html/2608.12961#Pt0.A5.SS4)\) 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](https://arxiv.org/html/2608.12961#bib.bib15)\]embeds an ontology by training a word model on random walks over its axioms; a recent survey\[[16](https://arxiv.org/html/2608.12961#bib.bib16)\]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, whereasMoosecompiles the same ELK semantics into a differentiable circuit\.