Crate owl_dl_core 

Core IR, normalization, and shared utilities for the rustdl OWL DL reasoner.

Phase 0 (in progress) lands the interned concept IR with structural sharing. Phase 1 will add NNF, structural transformation, absorption, told-subsumers, and told-disjoints.

See owl-dl-reasoner-rust-strategy-v2.md at the workspace root for the full plan.

Re-exports

pub use absorb::AbsorbedTBox;

pub use absorb::ConceptRule;

pub use absorb::NominalRule;

pub use absorb::RoleRule;

pub use absorb::absorb;

pub use absorb::absorb_roles;

pub use convert::ConversionError;

pub use convert::convert_class_expression;

pub use convert::convert_component;

pub use convert::convert_individual;

pub use convert::convert_object_property;

pub use convert::convert_ontology;

pub use convert_back::axiom_to_component;

pub use convert_back::concept_to_class_expression;

pub use convert_back::convert_back;

pub use definitions::Definitions;

pub use definitions::extract_definitions;

pub use ir::ClassId;

pub use ir::ConceptExpr;

pub use ir::ConceptId;

pub use ir::ConceptPool;

pub use ir::IndividualId;

pub use ir::Role;

pub use ir::RoleId;

pub use normalize::is_nnf;

pub use normalize::nnf_axioms;

pub use normalize::nnf_complement;

pub use normalize::to_nnf;

pub use ontology::Axiom;

pub use ontology::InternalOntology;

pub use ontology::SubRolePath;

pub use role_hierarchy::RoleHierarchy;

pub use role_hierarchy::RoleHierarchyBuilder;

pub use told::ToldTables;

pub use told::build_told_tables;

pub use transform::transform;

pub use vocab::Vocabulary;

Modules

absorb

Absorption: turn TBox axioms into focused triggers the tableau can apply lazily.

clause

DL-clause representation and clausifier — hypertableau Phase H0.

convert

Conversion from horned-owl’s model into our InternalOntology.

convert_back

Reverse conversion: InternalOntology back to a horned-owl SetOntology. Pairs with crate::convert to close the bijection for the axiom shapes our IR can faithfully represent.

data_axioms

Phase D4 (2026-06-03): preprocessing pass that recognizes specific OWL 2 data-axiom patterns and emits derived class-level axioms, sidestepping the need for full ConceptExpr extensions or tableau- side data-cardinality reasoning.

definitions

Definition extraction for lazy unfolding.

ir

IR for OWL DL concepts, roles, and identifiers.

locality

Signature-based locality analysis — Phase 1 scaffolding.

normalize

Normalization passes that prepare an ontology for reasoning.

ontology

InternalOntology — the workspace’s in-memory representation of an OWL ontology after conversion from horned-owl.

residual_trigger

Residual-GCI trigger analysis — Phase 1 scaffolding.

role_hierarchy

Named role hierarchy with reflexive-transitive closure.

told

Told-subsumer and told-disjoint tables.

transform

Structural transformation (Tseitin-style fresh-name introduction).

vocab

Vocabulary: bidirectional interning between OWL IRIs and our compact ids.