Crate ontologos_alc 

OWL ALC/DL tableau classification.

Modules

blocking_concepts

Known at-least concepts used in blocking tests.

graph_merge

Description graph tuple merging (HermiT GraphTest.testGraphMerging).

test_helpers

Test helpers matching HermiT AbstractReasonerInternalsTest.

Structs

AlcClassifier

ALC tableau classifier entry point.

AlcEngine

OWL ALC profile engine adapter.

AnnotatedEquality

Annotated equality @atMost(n <R> <C>)(X) (HermiT AnnotatedEquality).

BlockingStrategy

HermiT AnywhereValidatedBlocking direct blocking computation.

BlockingValidator

HermiT BlockingValidator.

BranchingPoint

Branching point marker (HermiT BranchingPoint).

ClauseSet

Clause set produced by clausification.

DependencySetFactory

Factory for interned PermanentDependencySet values (HermiT DependencySetFactory).

DescriptionGraph

HermiT DescriptionGraph — vertices carry atomic concept names.

DescriptionGraphEdge

Directed edge labelled by an atomic role name.

DescriptionGraphId

Stable graph identity for extension-table tuples.

DlClauseEvaluator

HermiT DLClauseEvaluator for simple chain rules.

DlOntology

OWL 2 DL internal ontology (core entities + CE store + clauses).

ExtensionManagerRef

Mutable access to extension manager operations bound to a tableau.

ExtensionTable

Binary or ternary extension table with tuple indexes.

HyperClauseSet

Clause set with positive facts.

Node

Tableau node handle (reference equality like HermiT Node).

NominalIntroductionManager

HermiT NominalIntroductionManager.

PermanentDependencySet

Persistent dependency set: a sorted linked list of branching points (head = largest).

Tableau

Minimal HermiT Tableau for internal unit tests.

TableauSeed

Facts from DL saturation to seed the initial tableau state.

TupleIndex

Index tuples by a permuted key sequence (HermiT TupleIndex).

TupleIndexRetrieval

Prefix iteration over stored tuples (HermiT TupleIndexRetrieval).

TupleTable

Paged tuple storage (HermiT TupleTable).

TupleTableFullIndex

Hash-index over the first indexed_arity components of tuples in a TupleTable.

UnionDependencySet

Temporary union of dependency sets.

UnsatCache

Memoizes label sets known to be inconsistent.

Enums

Clause

A clause in DL normal form after clausification.

DependencySetRef

Reference to a permanent or union dependency set.

DlObject

Stored tuple component.

DlPredicate

DL predicate in extension tables.

Error

ALC engine errors.

ExtensionView

Extension view (HermiT ExtensionTable.View).

RoleRef

Role reference with optional inverse.

Functions

blocking_test_annotated_equalities_clauses

Clauses for BlockingValidatorTest.testInvalidBlockWithAnnotatedEqualities.

blocking_test_one_invalid_block_clauses

Clauses for BlockingValidatorTest.testOneInvalidBlock.

classify

Classify an ontology under ALC tableau semantics.

classify_object_property_expressions

Classify object-property expressions into equivalence classes (HermiT m_objectRoleHierarchy nodes).

classify_reasoner

Classify via ontologos_core::Reasoner when profile is ALC-compatible.

classify_with_dl_and_seed

Classify using a pre-clausified ontology (avoids duplicate clausification).

classify_with_seed

Classify with saturation-derived seed facts.

classify_with_seed_for_entailment

Classify with saturation seed, skipping expensive pairwise subsumption inference.

clausify

Convert ontology axioms + DL store into clausal form.

clausify_hyper

Clausify an ontology into HermiT DL clause strings (normalization + hyperresolution).

derive_at_most_equalities

Derive annotated equalities from at-most constraints.

dl_clause_evaluation_test_clause

Test ontology clause from HermiT DLClauseEvaluationTest.

do_iteration

Single tableau iteration: clause derivation + NI processing + clash backtrack.

equivalent_object_property_expressions

OWL API getEquivalentObjectProperties via surrogate classification.

format_hyper_clauses

Format a clause set for an ontology (stable HermiT abbreviations).

inverse_object_property_expressions

OWL API getInverseObjectProperties (HermiT: getEquivalentObjectProperties(inverse(pe))).

is_ce_intersection_satisfiable_with_seed

Test whether C ⊓ D is satisfiable in the TBox.

is_ce_satisfiable_with_seed

Test whether a class expression is satisfiable in the TBox (empty ABox).

is_consistent

Tableau consistency check.

is_named_class_satisfiable_with_cache

Like is_named_class_satisfiable_with_seed but reuses an unsat label cache across calls.

is_named_class_satisfiable_with_seed

Test whether a named class is satisfiable, expanding EquivalentClasses definitions.

role_expression_subsumes

Whether sub_role ⊑ super_role in the role hierarchy (atomic and inverse expressions).

run_calculus

Run registered evaluators (HermiT runCalculus fragment).

structural_unsat_classes

Propagate obvious atomic class unsatisfiability without tableau expansion.

sub_object_property_expressions

OWL API getSubObjectProperties via surrogate classification (HermiT m_objectRoleHierarchy).

tableau_classify

Classify via tableau on clausified ontology.

tableau_classify_with_dl_and_seed

Classify using a pre-built clausified ontology (avoids duplicate clausification).

tableau_classify_with_seed

Classify with optional saturation seed.

tableau_classify_with_seed_options

Classify with optional saturation seed and control over pairwise subsumption inference.

tableau_is_consistent

Tableau consistency test (ABox + TBox when individuals are present).

tableau_is_consistent_with_seed

Tableau KB consistency with saturation seed facts.

Type Aliases

Result

Result type for ALC operations.