Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Olga Mashkova; Asaad Mohammedsaleh; Fernando Zhapa-Camacho; Robert Hoehndorf

Source-linked AI summary

Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho, Robert Hoehndorf

arXiv:2608.17741v1Aug 18, 2026cs.AI

TL;DR

Neuro-symbolic learners for description logics either abandon classical entailment or restrict expressivity, while independent perception can collapse ambiguous ontology-consistent interpretations. Baobab compiles SROIQ ontologies into SDDs for weighted-model-count training and circuit-anchored mixtures, recovering latent concepts and attaining Bayes-optimal calibrated posteriors where single-WMC and learned mixtures do not.

Problem
When supervision admits multiple ontology-consistent completions, independent atomwise perception commits to a single mode instead of representing the calibrated posterior.
Method
Baobab compiles SROIQ ontologies into SDDs whose evidence-conditioned weighted model counts train perception, while enumerated justifications anchor posterior mixtures.
Results
Anchoring mixtures to circuit-enumerated completions attains the Bayes-optimal calibrated posterior on real-image MNIST where single-WMC and learned mixtures do not.
Takeaways & Limitations
The paper demonstrates neuro-symbolic learning over non-Horn SROIQ while retaining classical entailment and mitigating reasoning shortcuts under ambiguous supervision.
Takeaways & Limitations
The compiler is sound but bounded and incomplete beyond grounding-covered or function-free existentials, and larger ABoxes incur polynomial ground-theory growth.

Abstract

from arXiv · show

OWL 2 DL ontologies, grounded in the description logic $\mathcal{SROIQ}$, express large knowledge bases in biomedicine and the Semantic Web. Neuro-symbolic (NeSy) learners over description logics either embed the ontology in a continuous space, abandoning classical entailment, or restrict to the Horn fragment $\mathcal{EL}^{++}$, which has a single canonical model. We present Baobab, which compiles a $\mathcal{SROIQ}$ ontology with a finite ABox into a Sentential Decision Diagram (SDD): it saturates a propositional core under a consequence-based calculus and instantiates the remaining $\mathcal{SROIQ}$ features (nominals, number restrictions, and the role axioms) over the active domain. The SDD's evidence-conditioned weighted model count then trains a perception network to recognize real images under partial ABox supervision: on an ontology that exercises every distinctive $\mathcal{SROIQ}$ feature, a CNN learns to read MNIST digits coupled by a successor relation and recovers latent ontology concepts that an independent perception leaves at chance. When the supervision admits several ontology-consistent completions, an independent perception collapses onto one, a reasoning shortcut: we show that a mixture indexed by the query's justifications can represent the calibrated posterior no independent perception can, and that seeding it from the circuit's enumerated completions attains the Bayes-optimal posterior on a real-image MNIST task where single-WMC and learned mixtures (the BEARS-ensemble hypothesis class) do not: to our knowledge the first to characterize and mitigate reasoning shortcuts in a non-Horn description logic. Soundness of the compiler and the representation result are machine-checked in Lean 4. Code is available at https://github.com/bio-ontology-research-group/baobab.

1 Introduction

Baobab closes a structural gap in neuro-symbolic learning by compiling OWL 2 DL/SROIQ ontologies into differentiable circuits that preserve classical entailment. Its evidence-conditioned weighted model count enables perception to recover unobserved concepts and, with justification-indexed mixtures, represent calibrated posteriors under multiple ontology-consistent completions.

Motivation: Embedding-based OWL-aware learners scale to OWL-shaped knowledge graphs but do not compute classical entailment during training.Knowledge-compilation methods preserve classical semantics but existing description-logic approaches target ALC, Horn profiles, propositional formulas, or Datalog-shaped programs.
Compilation: Baobab compiles any OWL 2 DL ontology into a sound SDD by saturating an ALCHOQ propositional core and finitely grounding SROIQ-specific extensions.The extensions include nominals, qualified cardinalities, and role axioms over the finite ABox grounding.
Perception learning: An evidence-conditioned WMC trains perception from partial ABox supervision, allowing a CNN to learn latent ontology concepts absent from direct labels.On MNIST, digit identity rises from 0.25→0.99 while ontology violations approach zero; independent perception remains at chance.
Reasoning shortcuts: A justification-indexed mixture can represent calibrated posterior mass across several ontology-consistent completions when independent perception cannot.The mixture is realized as one network, JustWMC, and can be seeded from completions enumerated by the circuit.
Results: JustWMC attains the Bayes-optimal calibrated posterior on a real-image MNIST task where single-WMC and learned BEARS-ensemble mixtures do not.A per-axiom comparison also finds that 23% of SROIQ axioms lie outside DeepProbLog’s Horn fragment.

2 Background

SROIQ knowledge bases combine TBox, ABox, and RBox axioms, while consequence-based reasoning derives entailments through saturation. Knowledge compilation converts propositional theories into SDD circuits supporting efficient weighted model counting and differentiable distribution semantics.

SROIQ knowledge bases: A SROIQ knowledge base contains TBox inclusions, ABox assertions with (in)equalities, and RBox role hierarchies, chains, and characteristics.Its syntax includes Boolean concepts, nominals, qualified number restrictions, and ∃R.Self.
Consequence-based reasoning: Consequence-based reasoning saturates clauses with fixed resolution-like rules and reads entailed concept subsumptions from the closure instead of searching for a model.Contexts group clauses anchored at concepts and propagate consequences between them.
Knowledge compilation: An SDD is a decomposable, deterministic circuit over a fixed vtree whose size can be worst-case exponential in theory treewidth but supports linear-time weighted model counting once built.Weighted model counting evaluates the total weight of a theory’s models in one bottom-up circuit pass.
Distribution semantics: Under distribution semantics, independent Bernoulli atom weights make weighted model counting equal the probability that a sampled world satisfies the theory.This correspondence turns per-atom probabilities into a differentiable training signal for knowledge-compilation neuro-symbolic methods.

3 Methods

Baobab compiles finite-ABox SROIQ knowledge bases into SDDs through consequence-based saturation, active-domain grounding, and propositional compilation, providing differentiable weighted-model-count training signals. The method also formalizes partial-supervision learning, characterizes independent-perception reasoning shortcuts, and introduces justification-indexed mixtures with circuit-seeded anchoring.

Compilation workflow: Baobab transforms a finite-ABox SROIQ knowledge base into an SDD through normalization, DL-clause transformation, consequence-based saturation, active-domain grounding, and CNF compilation.The SDD is built once per ontology, while a shared CNN supplies per-atom posteriors that weight its leaves during training.
Compilation workflow: Saturation eliminates existential witness function terms symbolically, while grounding expands deferred SROIQ features over the finite active domain into a sound propositional CNF.The resulting models exactly capture SROIQ interpretations over the active domain when existential consequences are grounding-covered or function-free.
ABox-supervised learning: Partial ABox supervision trains latent concept and role predictions through an evidence-conditioned WMC over complete ontology-consistent assignments, distributing gradients when supervision leaves multiple completions.The loss combines observed-label BCE with the negative log WMC of the ontology conjoined with supervisory evidence.
Reasoning shortcuts: When valid completions span multiple query justifications, independent perceptions cannot distribute mass across them and instead collapse onto an arbitrary reasoning shortcut.Theorem 5 establishes this characterization for SROIQ.
Reasoning shortcuts: A justification-indexed mixture of independent distributions represents these reasoning-shortcut mixtures, and JustWMC implements it with multiple atom heads, a selector, and diversity regularization.Anchored JustWMC seeds heads from circuit-enumerated ontology-consistent completions and learns only the mixture selector.
Formal guarantees: Lean 4 formalizes the compiler’s metatheory, including saturation soundness, SDD-WMC probabilistic semantics, SROIQ reasoning-shortcut characterization, and polynomial grounding bounds.The development also proves the ALC core sound and complete.

4 Experiments

Across MNIST-SROIQ and Pizzaiolo experiments, Baobab recovers latent ontology concepts from image evidence while enforcing ontology consistency, including under partial supervision and role-based structure. In an underdetermined gender task, justification-anchored mixtures achieve calibrated multimodal posteriors that factorized methods fail to learn, while full SDD compilation encounters a circuit-size wall on the real ontology.

MNIST-SROIQ: Grounded MNIST supervision raises never-supervised digit recovery from 0.25 →0.99, with violation 0.02 and concept ECE 0.002, while independent perception remains at chance.The grounded regime has #RS = 1 and uses role and concept evidence to pin the digits through the ontology.
MNIST-SROIQ: Under-determined MNIST evidence leaves #RS = 5 cyclic relabelings, causing WMC digit accuracy 0.18, violation 0.78, and concept ECE 0.15.A single parity atom reduces #RS to 3, while full parity grounding reduces it to 1 and restores violation to 0.02.
Pizzaiolo: Ablating closed qualified-existential grounding lowers latent property recovery from 0.92 to 0.78, isolating a 14-point gain beyond forward EL-style grounding.Supervised topping accuracy changes from 0.93→0.95, while the reported violation becomes 0.00 because the removed clause was the counted constraint.
Multimodal supervision: On four uninformed gender modes, independent perception has NLL 6.93 and TV 1.00, while single-WMC and JustWMC reach NLL 6.13 / 6.69 and TV 0.99.The four modes are equally plausible, with Bayes-optimal latent NLL 6 log 2 ≈4.16; gradient descent collapses learned mixtures onto a seed-dependent mode.
Multimodal supervision: Seeding four mixture heads from enumerated circuit completions achieves NLL 4.17, zero concept ECE, and TV 0.02 without seed variance.Only the selector is learned, converging to the uniform posterior and realizing the theorem’s positive direction in practice.

5 Related work

Baobab extends circuit-based neuro-symbolic learning from description-logic fragments to SROIQ, adding consequence-based compilation, mechanized metatheory, real perception, and mitigation of reasoning shortcuts. It differs from embedding, probabilistic-DL, and prior reduction approaches by preserving exact differentiable weighted model counting.

Circuit-based neuro-symbolic learning: Baobab extends the closest concurrent SDD-based DL compiler to SROIQ, using consequence-based compilation and adding mechanized metatheory, real perception, and reasoning-shortcut mitigation.The concurrent work uses hand-built feature vectors and addresses neither the characterized shortcuts nor real perception.
Embedding and knowledge-compilation approaches: DL embeddings and fuzzy-DL variants scale through continuous relaxations of OWL semantics but do not compute classical WMC; Embed2Sym clusters embeddings to recover symbols.Related knowledge-compilation systems instead use circuits or propositional WMC, including DeepProbLog, Semantic Loss, Semantic Probabilistic Layers, and A-NeSI.
Expressive-DL reductions: Unlike reductions such as KAON2’s SHIQ-to-disjunctive-Datalog translation, Baobab adds a path from expressive-DL compilation to an exact, differentiable WMC learner.The passage states that a reduction alone yields no learner.
Reasoning shortcuts and probabilistic-DL systems: Baobab attacks the independence assumption with an SROIQ instance of the BEARS recipe and an RS-awareness characterization, while probabilistic-DL systems differ in their world-sum, explanation enumeration, or user-set rule weights.DISPONTE fixes the world-sum; BUNDLE and TRILL enumerate tableau explanations; LNNs use user-set rule weights.

6 Limitations and future work

Baobab’s compilation is sound but bounded, with scope limited by grounding, active-domain, and datatype assumptions. Its evaluations are controlled ablations rather than end-to-end comparisons with external NeSy systems, while fuller disjunctive reasoning remains future work.

Compilation limits: Guarded saturation is sound but incomplete for deep ungrounded existential chains; the full disjunctive context calculus is future work because large-ontology convergence is unresolved.It is sound and complete under trivial expansion, but not yet convergent on large ontologies.
Scope assumptions: 0.92 to 0.78: latent recovery degrades without the refinement, which becomes over-permissive and trades open-world faithfulness for identifiability under partial supervision.Datatypes are out of scope, and the refinement is used in benchmarks to support latent recovery.
Evaluation limits: The DeepProbLog comparison reports 23% of axioms outside ProbLog’s Horn fragment, not accuracy, and no external NeSy system receives an end-to-end non-Horn head-to-head run.Independent, single-WMC, and learned-mixture results are controlled ablations of one pipeline.

7 Conclusion · A SROIQ syntax and semantics · B Normalization and clausification

Baobab compiles SROIQ knowledge bases into differentiable circuits that support neuro-symbolic learning under partial supervision, including Bayes-optimal inference when supervision leaves multiple ontology-consistent completions. The paper formalizes SROIQ syntax and Tarskian semantics, then normalizes and clausifies its axioms using proxies, Skolem terms, and grounding hooks.

7 Conclusion: Baobab uses consequence-based saturation over ALCHOQ plus ABox grounding of SROIQ features to produce an SDD whose evidence-conditioned WMC trains perception under partial supervision.When supervision underdetermines latents, mixtures anchored to enumerated circuit justifications recover the Bayes-optimal posterior that learned mixtures miss.
7 Conclusion: Anchoring a mixture to the circuit’s enumerated justifications recovers the Bayes-optimal posterior where supervision admits multiple ontology-consistent latent completions.The conclusion contrasts this with learned mixtures, which miss that calibrated posterior.
A SROIQ syntax and semantics: An SROIQ knowledge base is a triple (T, R, A) over atomic concept names, atomic role names, and individual names.The TBox contains concept inclusions, the ABox contains assertions and equalities, and the RBox contains role inclusions, chains, and role characteristics.
A SROIQ syntax and semantics: SROIQ concepts include nominals, Boolean connectives, existential and universal restrictions, qualified number restrictions, and self restrictions over atomic, inverse, and universal roles.The implementation represents these constructs with dedicated syntax dataclasses and flattened, deduplicated operand sets for conjunctions and disjunctions.
A SROIQ syntax and semantics: SROIQ uses Tarskian semantics, interpreting concepts as domain subsets, roles as binary relations, and individuals as domain elements, with standard readings for role axioms.The Lean development takes this semantics as its definition of truth.
B Normalization and clausification: Grounding hooks handle nominals, qualified number restrictions, inverse and universal roles, and route RBox characteristics to native clauses or corresponding proxies.Nominals map to stable proxies linked to individuals; the universal role emits →U(x, y).
B Normalization and clausification: Normalization first converts axioms to negation-normal form by pushing negation through Boolean, quantifier, and cardinality constructs while preserving atomic negations and self restrictions.Cardinality dualities include ¬(≥n R.C) ⇝ ≤(n−1) R.C and ¬(≤n R.C) ⇝ ≥(n+1) R.C.
B Normalization and clausification: Each non-atomic subconcept receives a fresh concept name, and inclusions become clauses defining conjunction, disjunction, quantifier, negation, self, and number-restriction behavior.Existential restrictions use unary Skolem functions, while qualified number restrictions add distinct successors and closure clauses.

C Consequence-based saturation

Baobab uses guarded propositional hyperresolution to saturate DL clauses to a terminating, sound fixpoint. Although the bounded calculus is incomplete, grounding makes the relevant consequences faithful without changing the model set or circuit.

C Consequence-based saturation: Baobab saturates DL clauses by propositional hyperresolution with most-general-unifier matching, repeatedly re-resolving clause pairs until a fixpoint adds nothing.Unification uses Robinson’s algorithm with occurs-check over four term kinds.
C Consequence-based saturation: Four guards bound context generation: tautology elimination, variable count, role-atom count, and function-term depth at most one.The variable and role-atom bounds scale with the input and constructs such as chains and ≤n restrictions.
C Consequence-based saturation: The guarded saturation terminates and every derived clause is a logical consequence of its input.Termination follows from a finite reachable atom-and-clause universe and subsumption-minimal pooling; soundness is mechanized for the underlying ALCHOQ saturation.
C Consequence-based saturation: The bounded calculus is incomplete, but faithful ground-time CNF for relevant features means added saturation clauses change neither the model set nor the circuit.The affected features include nominals, number restrictions, local reflexivity, and role characteristics; circuit invariance assumes a fixed vtree.

D Grounding the SROIQ features · E SDD compilation, WMC, and the distribution semantics

The compiler grounds SROIQ features over the active domain with sound propositional clauses, while optional refinements can reduce circuits or add closed-world constraints under explicit assumptions. The resulting CNF is compiled into an SDD whose differentiable, evidence-conditioned WMC exactly sums the weights of satisfying assignments and supplies training gradients.

D Grounding the SROIQ features: Grounding materializes GroundHooks over the active domain, emitting a bounded number of propositional clauses per rule justified by Tarskian-semantics soundness lemmas.Table 2 records each rule’s clause schema and ground-clause count.
D Grounding the SROIQ features: The grounder allocates concept atoms per individual and role atoms per ordered pair, adding an equality theory when nominals, qualified number restrictions, or functional roles are present.The dominant terms include cubic transitivity and equality-transitivity clauses, with d^(k+1) and O(d^(n+1)) entries for chains and number restrictions.
D Grounding the SROIQ features: Role-typing, equality-skip, and closed-existential refinements are opt-in and off by default, leaving other circuits byte-identical to the unrefined grounding.The first two refinements preserve WMC through factorization over independent atom blocks and unique satisfying assignments.
D Grounding the SROIQ features: Removing closed-existential closure lowers latent property recovery from 0.92 to 0.78 while the reported violation falls to 0.00.The open variant retains only the forward direction, whereas the closed variant restores the biconditional over named fillers.
D Grounding the SROIQ features: Closed-existential grounding is sound only under named-filler closure, which holds for the fully observed Pizzaiolo topping lists but is not an open-world consequence.Accordingly, this refinement lies outside the mechanized guarantees.
E SDD compilation, WMC, and the distribution semantics: Compilation runs once per ontology, after which the differentiable WMC pass runs once per training step on the CNF compiled to an SDD with PySDD.The WmcLayer evaluates the circuit bottom-up and memoizes node computations so each node is visited once.
E SDD compilation, WMC, and the distribution semantics: Evidence conditioning fixes atom probabilities to 1 or 0 for observed truth values, while clamping probabilities to [ε, 1−ε] provides log-stability and preserves differentiable gradient flow into pθ.The pass is exact in floating point and evaluates decision nodes by multiplying prime and sub WMCs.
E SDD compilation, WMC, and the distribution semantics: Under the distribution semantics, the circuit computes the total probability mass of interpretations satisfying Θ∧e, and the resulting world-sum is the quantity optimized by the losses.The correspondence between bottom-up evaluation and this sum is mechanized in Lean.

F Saturation and circuit size · G Learning objectives

Baobab’s saturation is size-neutral under a fixed vtree but essential for completeness when grounding misses existential consequences; dynamic vtree minimization can change size non-monotonically. Its learning objectives compare independent, WMC, learned-mixture, and justification-anchored approaches, with mixtures representing reasoning-shortcut posteriors.

F Saturation and circuit size: Under a fixed vtree, adding soundly saturated, entailed clauses leaves the compressed, trimmed SDD identical, including node count and weighted model count.Saturation introduces no new ground atoms, so equivalent clause sets compile to the same canonical diagram.
F Saturation and circuit size: Dynamic vtree minimization makes saturation’s size effect real but non-monotone: disjunction shrinks from 17 to 12, whereas bird-penguin grows from 139 to 143.These changes occur because minimized SDD size is not canonical across logically equivalent inputs.
F Saturation and circuit size: The benchmarks use only function-free or grounding-covered constructs, so their grounded circuits are faithful and saturation is unnecessary for reported results.Accordingly, the experiments report results without relying on saturation or imposing a wall-clock cutoff.
F Saturation and circuit size: Saturation is load-bearing for ungrounded existentials: without it, the model set can enlarge and an ontology entailment can disappear from universal validity.For A ⊑∃R.B, B ⊑C, ∃R.C ⊑D with A(a), saturation yields 6 models and forces D(a); skipping it yields 14 models, with D(a) in 0.71 of them.
F Saturation and circuit size: The full Pizza¨ıolo compilation wall is driven by treewidth from disjointness, right-hand-side disjunctions, and complement coupling, not grounding size alone.A hand-pruned role-based sub-signature compiles where the full ontology cannot, because SDD size is worst-case exponential in treewidth.
G Learning objectives: The baselines isolate two mechanisms: WMC over the compiled constraint versus Independent, and compiled support in anchored mixtures versus learned support in JustWMC.The learning objectives include observed-atom BCE, a circuit semantic-loss term, and mixture-specific diversity machinery for distinct constraint-consistent modes.
G Learning objectives: Every reasoning-shortcut mixture over an SROIQ query is representable by a categorical mixture of UCIs indexed by the query’s justifications.This result is verified in Lean and motivates learned mixtures whose heads occupy distinct Θ-consistent modes.

H Experimental details

Experiments evaluate Baobab on unseen individuals across synthetic and real-image tasks, including ontologies that exercise distinctive SROIQ features and settings with ambiguous ontology-consistent completions. The results show successful latent-concept recovery and calibrated posterior estimation when completion-aware mixtures are seeded from circuit-enumerated explanations.

Evaluation protocol: All methods compile the SDD once and train with Adam on held-out unseen individuals, using shared optimizer and training settings within each comparison.MNIST uses a CNN on real 28×28 images; Pizzaiolo uses a frozen ResNet-18 with a linear head; synthetic Pizza uses a noisy 12-bit vector and MLP.
Pizza-SROIQ: The synthetic Pizza-SROIQ control exposes 50% of topping atoms while never supervising 11 latent class atoms, testing recovery of named pizzas and derived ontology classes.Each example is a noisy 12-bit topping vector, with 128 training and 64 evaluation examples.
MNIST-SROIQ: MNIST-SROIQ compiles a 52-axiom ontology over digits 0−4 into a 114-atom SDD with 5.3·10^9 models and instantiates every distinctive SROIQ feature.The ontology includes disjunction, complements, successor closures, qualified number restrictions, role hierarchies and chains, transitivity, symmetry, asymmetry, irreflexivity, reflexivity, and functionality.
Experimental scale: The MNIST-SROIQ circuit compiles in <1 s, while its 114-atom SDD contains 5.3·10^9 models and training uses 3000/1000 train/evaluation examples for 12 epochs.The two experimental regimes differ only in the evidence revealed.
MNIST-Disjunction: 0.99 digit recovery is achieved across MNIST-Disjunction methods, but anchored JustWMC reaches Bayes-optimal NLL 4.17, mode-coverage TV 0.02, and no seed variance.JustWMC is seeded from the four completions enumerated by the gender circuit; single-WMC and learned-mixture methods remain at TV ≈0.99.

I Mechanized guarantees

The paper gives Lean-checked guarantees for saturation, grounding, weighted model counting, and reasoning-shortcut expressivity in SROIQ. Its grounding is exact on a grounding-covered, function-free fragment and otherwise over-approximates models only through unnamed head-existential witnesses.

Saturation and grounding: Saturation is sound, preserves models, and leaves the weighted model count unchanged relative to Θ∆.Every derived clause is entailed by its input, so adding saturated clauses changes neither interpretations nor their weights.
Saturation and grounding: Grounding is sound for all SROIQ interpretations and exact when every existential consequence is grounded or function-free.Otherwise, Θ∆ over-approximates SROIQ models precisely because finite grounding cannot name witnesses for head-existential consequences.
Weighted model counting: WMC(Θ | pθ) equals the ontology’s model probability under distribution semantics, matching the quantity optimized by the training losses.The equality follows from bottom-up SDD evaluation computing the distribution-semantics world-sum.
Reasoning-shortcut awareness: A single independent perception represents a reasoning-shortcut mixture only when valid completions form one justification’s subcube, whereas justification-indexed UCI mixtures represent every such mixture.Both necessity and sufficiency are mechanized for SROIQ by instantiating the relevant implicants as query justifications.
Mechanization: The development is foundation-only, with no sorrys or added axioms; audited theorems report only propext, Classical.choice, and Quot.sound.ALCHOQ saturation soundness is additionally reported as axiom-free.

J Lean module inventory

The Lean 4 development formalizes the description-logic syntax, semantics, consequence rules, context-structure calculus, complexity bounds, and weighted-model-count refinements. It fully proves core soundness and selected completeness or preservation results, while full SROIQ completeness remains conjectural; all modules pass the foundation-only axiom audit.

Core and feature modules: ALC.lean and ALCHOQ.lean formalize syntax, Tarskian semantics, sound consequence rules, nominals, qualified number restrictions, and their cardinality and monotonicity lemmas.ALCHOQ extends ALC with Concept.nom, atLeast, atMost, atLeastCard, atMostCard, monoAtLeast, and monoAtMost.
Role axioms: SROIQ.lean defines role-axiom shapes and proves soundness lemmas for inclusions, chains, transitivity, symmetry, asymmetry, reflexivity, irreflexivity, inverses, and disjointness.Role identities justify transitivity-as-chain and symmetric-asinverse shortcuts, while has self supports local-reflexivity proxy grounding.
Completeness: ALC completeness is fully mechanized through a Lindenbaum canonical model, and SROIQCompleteness adds sound role-axis consequence rules but leaves full SROIQ completeness as a conjecture.The added rules cover role inclusion, binary and k-ary chains, transitivity, reflexivity, irreflexivity, and role disjointness.
Tena Cucala calculus: The Tena Cucala calculus is encoded with its context structures, twelve inference rules, concrete refinements, per-rule soundness, unified meta-soundness, and an unconditional empty-ontology completeness sliver.The sliver applies to a propositionally-refutable fragment of queries; the full completeness statement is exposed as a typed Prop with separate semantic ingredients.
Complexity and refinements: Grounding bounds are formalized as polynomial in ontology signature size, with explicit per-feature bounds for number restrictions, chains, transitivity, hierarchies, and inverses.The saturation pair bound gives |Sat(O)| ≤ |Σ|^2, while feature contributions include 4n · d^(n+1) literals, d^(k+1) chain tuples, and d^2 or d^3 terms.
Complexity and refinements: Weighted-model-count refinements preserve model counts through independent-atom factorization and unique satisfying assignments, and every theorem passes the foundation-only axiom audit without sorry or user axioms.The audit reports only {propext, Classical.choice, Quot.sound}.