ontologos_alc/
lib.rs

1//! OWL ALC/DL tableau classification.
2
3#![warn(missing_docs)]
4
5mod clause;
6mod dl_ontology;
7mod engine;
8mod hyper_abox;
9mod hyper_cardinality;
10mod hyper_clausify;
11mod hyper_nominals;
12mod hyper_object;
13mod hyperclause;
14mod normalize;
15mod object_property_classify;
16mod tableau;
17
18use ontologos_core::{Ontology, Taxonomy};
19use ontologos_profile::{OwlProfile, detect_profile};
20use thiserror::Error;
21
22pub use clause::{Clause, ClauseSet};
23pub use dl_ontology::DlOntology;
24pub use engine::AlcEngine;
25pub use hyper_clausify::clausify_hyper;
26pub use hyperclause::{HyperClauseSet, format_hyper_clauses};
27pub use normalize::clausify;
28#[doc(hidden)]
29pub use object_property_classify::{
30    PreparedRoleSurrogateContext, augment_for_role_classification,
31    classify_object_property_on_augmented, equivalent_object_property_on_augmented,
32    sub_object_property_on_augmented,
33};
34pub use object_property_classify::{
35    classify_object_property_expressions, equivalent_object_property_expressions,
36    inverse_object_property_expressions, sub_object_property_expressions,
37};
38pub use tableau::AlcClassifier;
39pub use tableau::blocking_validator::{
40    BlockingStrategy, BlockingValidator, RoleRef, blocking_concepts,
41    blocking_test_annotated_equalities_clauses, blocking_test_one_invalid_block_clauses,
42};
43pub use tableau::cache::UnsatCache;
44pub use tableau::dependency_set::{
45    DependencySetFactory, DependencySetRef, PermanentDependencySet, UnionDependencySet,
46};
47pub use tableau::description_graph::{DescriptionGraph, DescriptionGraphEdge, DescriptionGraphId};
48pub use tableau::dl_clause_eval::{
49    DlClauseEvaluator, derive_at_most_equalities, dl_clause_evaluation_test_clause, do_iteration,
50    run_calculus,
51};
52pub use tableau::extension_manager::{
53    BranchingPoint, DlObject, DlPredicate, ExtensionManagerRef, ExtensionTable, ExtensionView,
54    Node, Tableau, test_helpers,
55};
56pub use tableau::graph_merge;
57pub use tableau::ni_rules::{AnnotatedEquality, NominalIntroductionManager};
58pub use tableau::tuple_index::{TupleIndex, TupleIndexRetrieval};
59pub use tableau::tuple_table::{TupleTable, TupleTableFullIndex};
60pub use tableau::{
61    TableauSeed, classify as tableau_classify,
62    classify_with_dl_and_seed as tableau_classify_with_dl_and_seed,
63    classify_with_seed as tableau_classify_with_seed,
64    classify_with_seed_options as tableau_classify_with_seed_options,
65    is_ce_intersection_satisfiable_with_seed, is_ce_satisfiable_with_seed,
66    is_consistent as tableau_is_consistent,
67    is_consistent_with_seed as tableau_is_consistent_with_seed,
68    is_named_class_satisfiable_with_cache, is_named_class_satisfiable_with_seed,
69    role_expression_subsumes, structural_unsat_classes,
70};
71
72/// Result type for ALC operations.
73pub type Result<T> = std::result::Result<T, Error>;
74
75/// ALC engine errors.
76#[derive(Debug, Error)]
77pub enum Error {
78    /// Profile mismatch.
79    #[error("ontology exceeds ALC fragment ({0:?})")]
80    NonAlcProfile(OwlProfile),
81    /// Core error.
82    #[error(transparent)]
83    Core(#[from] ontologos_core::Error),
84    /// Parser error.
85    #[error(transparent)]
86    Parser(#[from] ontologos_parser::Error),
87    /// Profile detection error.
88    #[error(transparent)]
89    Profile(#[from] ontologos_profile::Error),
90    /// General message.
91    #[error("{0}")]
92    Message(String),
93    /// Tableau expansion budget exhausted (incomplete reasoning).
94    #[error("tableau expansion budget exhausted ({0} expansions)")]
95    ResourceLimit(u32),
96    /// Tuple index trie node space exhausted.
97    #[error("tuple index node space exhausted")]
98    TupleIndexExhausted,
99}
100
101/// Classify an ontology under ALC tableau semantics.
102pub fn classify(ontology: &Ontology) -> Result<Taxonomy> {
103    let report = detect_profile(ontology)?;
104    if !matches!(
105        report.detected,
106        Some(OwlProfile::El | OwlProfile::Ql | OwlProfile::Dl)
107    ) && let Some(p) = report.detected
108        && p == OwlProfile::Rl
109    {
110        return Err(Error::NonAlcProfile(p));
111    }
112    tableau::classify(ontology)
113}
114
115/// Classify with saturation-derived seed facts.
116pub fn classify_with_seed(ontology: &Ontology, seed: &TableauSeed) -> Result<Taxonomy> {
117    tableau::classify_with_seed_options(ontology, seed, true)
118}
119
120/// Classify using a pre-clausified ontology (avoids duplicate clausification).
121pub fn classify_with_dl_and_seed(
122    dl: &DlOntology,
123    seed: &TableauSeed,
124    infer_pairwise_subsumptions: bool,
125) -> Result<Taxonomy> {
126    tableau::classify_with_dl_and_seed(dl, seed, infer_pairwise_subsumptions)
127}
128
129/// Classify with saturation seed, skipping expensive pairwise subsumption inference.
130pub fn classify_with_seed_for_entailment(
131    ontology: &Ontology,
132    seed: &TableauSeed,
133) -> Result<Taxonomy> {
134    tableau::classify_with_seed_options(ontology, seed, false)
135}
136
137/// Tableau consistency check.
138pub fn is_consistent(ontology: &Ontology) -> Result<bool> {
139    tableau::is_consistent(ontology)
140}
141
142/// Classify via [`ontologos_core::Reasoner`] when profile is ALC-compatible.
143pub fn classify_reasoner(reasoner: &ontologos_core::Reasoner) -> Result<Taxonomy> {
144    classify(reasoner.ontology())
145}
ontologos_alc/lib.rs

ontologos_alc/
lib.rs
