ontologos_explain/
lib.rs

1//! Explanation engine with proof graphs and export formats.
2
3mod build;
4mod format;
5mod query;
6
7use ontologos_core::{
8    EntityId, Error as CoreError, InferenceTrace, Ontology, Profile, Reasoner, ReasonerConfig,
9};
10use ontologos_el::ElClassifier;
11use ontologos_profile::{detect_profile, OwlProfile};
12use ontologos_rl::RlEngine;
13use serde::{Deserialize, Serialize};
14use thiserror::Error;
15
16pub use build::build_proof_graph;
17pub use format::render_text;
18pub use query::{
19    explain_subsumption, explain_unsatisfiable, find_bottom_subsumption, find_subsumption_step,
20    subsumption_from_axioms,
21};
22
23pub type Result<T> = std::result::Result<T, Error>;
24
25#[derive(Debug, Error)]
26pub enum Error {
27    #[error("explanation generation not yet implemented")]
28    NotImplemented,
29    #[error("profile detection failed: {0}")]
30    Profile(String),
31    #[error("classification not supported for profile {0:?}")]
32    UnsupportedProfile(OwlProfile),
33    #[error(transparent)]
34    Core(#[from] CoreError),
35    #[error(transparent)]
36    Rdfs(#[from] ontologos_rdfs::Error),
37    #[error(transparent)]
38    Rl(#[from] ontologos_rl::Error),
39    #[error(transparent)]
40    El(#[from] ontologos_el::Error),
41}
42
43/// Node identifier within a proof graph.
44#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
45pub struct NodeId(pub u32);
46
47/// Single step in a reasoning proof.
48#[derive(Debug, Clone, Serialize, Deserialize)]
49pub struct ProofNode {
50    /// Rule that produced this step.
51    pub rule: String,
52    /// Premise nodes in the proof graph.
53    pub premises: Vec<NodeId>,
54    /// Concluded axiom, when applicable.
55    #[serde(skip_serializing_if = "Option::is_none")]
56    pub conclusion_axiom: Option<ontologos_core::AxiomId>,
57    /// EL subsumption conclusion `sub ⊑ sup`.
58    #[serde(skip_serializing_if = "Option::is_none")]
59    pub conclusion_sub: Option<(EntityId, EntityId)>,
60    /// EL existential conclusion.
61    #[serde(skip_serializing_if = "Option::is_none")]
62    pub conclusion_existential: Option<(EntityId, EntityId, EntityId)>,
63    /// EL subproperty conclusion.
64    #[serde(skip_serializing_if = "Option::is_none")]
65    pub conclusion_subproperty: Option<(EntityId, EntityId)>,
66}
67
68/// Proof graph backing explanation traces.
69#[derive(Debug, Default, Serialize, Deserialize)]
70pub struct ProofGraph {
71    /// Nodes in topological construction order.
72    pub nodes: Vec<ProofNode>,
73}
74
75impl ProofGraph {
76    /// Export the proof graph as JSON.
77    pub fn to_json(&self) -> Result<String> {
78        serde_json::to_string_pretty(self)
79            .map_err(|e| Error::Core(CoreError::Message(e.to_string())))
80    }
81
82    /// Number of proof nodes.
83    #[must_use]
84    pub fn node_count(&self) -> usize {
85        self.nodes.len()
86    }
87
88    /// Whether premise links form a directed acyclic graph.
89    #[must_use]
90    pub fn is_acyclic(&self) -> bool {
91        build::validate_proof_acyclic(&self.nodes).is_ok()
92    }
93}
94
95/// Collect inference trace with explanations enabled on `reasoner`'s ontology.
96pub fn collect_trace(reasoner: &mut Reasoner) -> Result<InferenceTrace> {
97    match reasoner.profile() {
98        Profile::Rdfs => Ok(ontologos_rdfs::RdfsEngine::new()
99            .with_traces(true)
100            .materialize(reasoner.ontology_mut())?
101            .trace),
102        Profile::Rl => Ok(RlEngine::try_new(reasoner.config().parallelism)?
103            .with_traces(true)
104            .saturate(reasoner.ontology_mut())?
105            .trace),
106        Profile::El => Ok(ElClassifier::new()
107            .classify_with_options(reasoner.ontology(), true)?
108            .trace),
109        Profile::Auto => collect_trace_auto(reasoner),
110    }
111}
112
113fn collect_trace_auto(reasoner: &mut Reasoner) -> Result<InferenceTrace> {
114    let report = detect_profile(reasoner.ontology()).map_err(|e| Error::Profile(e.to_string()))?;
115    let detected = report
116        .detected
117        .ok_or_else(|| Error::Profile("no profile detected".into()))?;
118
119    match detected {
120        OwlProfile::El | OwlProfile::Ql => Ok(ElClassifier::new()
121            .classify_with_options(reasoner.ontology(), true)?
122            .trace),
123        OwlProfile::Rl => Ok(RlEngine::try_new(reasoner.config().parallelism)?
124            .with_traces(true)
125            .saturate(reasoner.ontology_mut())?
126            .trace),
127        OwlProfile::Dl => Err(Error::UnsupportedProfile(detected)),
128    }
129}
130
131/// Generate a full proof graph using automatic profile detection.
132pub fn explain(ontology: &Ontology) -> Result<ProofGraph> {
133    let mut reasoner = Reasoner::builder()
134        .profile(Profile::Auto)
135        .config(ReasonerConfig {
136            explanations: true,
137            ..ReasonerConfig::default()
138        })
139        .build(ontology.clone())?;
140    explain_with_profile(&mut reasoner)
141}
142
143/// Generate proof graph for RDFS materialization traces.
144pub fn explain_rdfs(ontology: &mut Ontology) -> Result<ProofGraph> {
145    let trace = ontologos_rdfs::RdfsEngine::new()
146        .with_traces(true)
147        .materialize(ontology)?
148        .trace;
149    build_proof_graph(ontology, &trace)
150}
151
152/// Generate proof graph for OWL RL saturation traces.
153pub fn explain_rl(ontology: &mut Ontology) -> Result<ProofGraph> {
154    let trace = RlEngine::try_new(1)?
155        .with_traces(true)
156        .saturate(ontology)?
157        .trace;
158    build_proof_graph(ontology, &trace)
159}
160
161/// Generate proof graph for OWL EL classification traces.
162pub fn explain_el(ontology: &Ontology) -> Result<ProofGraph> {
163    let trace = ElClassifier::new()
164        .classify_with_options(ontology, true)?
165        .trace;
166    build_proof_graph(ontology, &trace)
167}
168
169/// Route explanation collection by reasoner profile (like classify).
170pub fn explain_with_profile(reasoner: &mut Reasoner) -> Result<ProofGraph> {
171    let trace = collect_trace(reasoner)?;
172    build_proof_graph(reasoner.ontology(), &trace)
173}
174
175#[cfg(test)]
176mod tests {
177    use ontologos_core::{Axiom, EntityKind, Ontology};
178
179    use super::*;
180
181    fn class(ontology: &mut Ontology, iri: &str) -> EntityId {
182        ontology.entity_id(iri, EntityKind::Class).expect("class")
183    }
184
185    #[test]
186    fn explain_rdfs_builds_graph() {
187        let mut ontology = Ontology::new();
188        let a = class(&mut ontology, "http://ex.org/A");
189        let b = class(&mut ontology, "http://ex.org/B");
190        let c = class(&mut ontology, "http://ex.org/C");
191        ontology
192            .add_axiom(Axiom::SubClassOf {
193                subclass: a,
194                superclass: b,
195            })
196            .unwrap();
197        ontology
198            .add_axiom(Axiom::SubClassOf {
199                subclass: b,
200                superclass: c,
201            })
202            .unwrap();
203
204        let graph = explain_rdfs(&mut ontology).expect("graph");
205        assert!(graph.node_count() > 2);
206        graph.to_json().expect("json");
207    }
208
209    #[test]
210    fn explain_el_builds_graph() {
211        let mut ontology = Ontology::new();
212        let a = class(&mut ontology, "http://ex.org/A");
213        let b = class(&mut ontology, "http://ex.org/B");
214        let c = class(&mut ontology, "http://ex.org/C");
215        ontology
216            .add_axiom(Axiom::SubClassOf {
217                subclass: a,
218                superclass: b,
219            })
220            .unwrap();
221        ontology
222            .add_axiom(Axiom::SubClassOf {
223                subclass: b,
224                superclass: c,
225            })
226            .unwrap();
227
228        let graph = explain_el(&ontology).expect("graph");
229        assert!(graph.node_count() > 2);
230    }
231}
ontologos_explain/lib.rs

ontologos_explain/
lib.rs
