Crate ontologos_dl 

OWL 2 DL reasoner: coupled saturation + tableau (Konclude-style hybrid).

Structs

ConsistencyResult

Result of an ontology consistency check.

DependencyIndex

Tracks which axioms mention each entity (forward index).

DlClassifier

OWL 2 DL classifier facade.

DlEngine

OWL 2 DL profile engine adapter.

DlPerfTimings

Per-phase wall times for one DlClassifier::classify invocation (seconds).

DlReport

DL classification report.

LiteralIndex

Index of data literals and facet constraints.

LiteralValue

Literal with lexical form and datatype.

RoleHierarchy

Saturate role hierarchy with complex chain inclusions.

RolePropertyQueryContext

Reusable prepared state for object-property queries (avoids repeated augmentation).

SaturatedFacts

Facts produced by saturation pass.

Enums

Error

DL engine errors.

Functions

check_consistency

Check ontology consistency under DL with optional wall-clock budget.

classify

Classify an ontology under OWL 2 DL semantics.

classify_for_entailment

Classify for OWL entailment checks (skips pairwise named subsumption inference).

classify_object_property_expressions

Classify object-property expressions into equivalence classes.

classify_reasoner

Classify via Reasoner when profile is DL.

dl_max_workers

Max parallel unsat workers (ONTOLOGOS_DL_MAX_WORKERS, default 4).

entails_class_assertion

Check whether ontology ⊨ ClassAssertion(class, individual).

equivalent_object_property_expressions

OWL API getEquivalentObjectProperties.

inverse_object_property_expressions

OWL API getInverseObjectProperties.

is_class_assertion_probe_satisfiable

Returns whether the ontology’s class-assertion probe CE is satisfiable.

is_class_expression_satisfiable

Returns whether a class expression is satisfiable under the ontology TBox.

is_consistent

Check ontology consistency under DL (errors when the answer is incomplete).

is_data_range_satisfiable

Returns true when a data range has at least one satisfying literal witness.

is_datatype_consistent

Returns false when datatype constraints are unsatisfiable.

is_named_class_unsatisfiable

Check whether a named class is unsatisfiable in the ontology TBox.

is_property_hierarchy_regular

Returns whether the object-property axioms form a regular hierarchy.

is_property_hierarchy_simple

Returns whether every object property used in cardinality restrictions is simple.

is_subsumed

Check named class subsumption after DL classification.

named_class_datatype_satisfiable

Returns false when a named class’s data restrictions (including property ranges) are unsatisfiable.

named_classes_unsatisfiable

Returns true when every listed named class is unsatisfiable in the ontology TBox.

perf_enabled

Whether DL perf tracing is enabled (ONTOLOGOS_DL_PERF=1).

run_bounded

Run work on a worker thread with an optional wall-clock budget.

saturate

Run lightweight saturation on existential/subsumption clauses.

sub_object_property_expressions

OWL API getSubObjectProperties.

Type Aliases

Result

Result type for DL operations.