ontologos_explain/
lib.rs

1//! Explanation engine with proof graphs and export formats.
2
3mod build;
4mod format;
5
6use ontologos_core::{EngineKind, InferenceTrace, Ontology, Reasoner};
7use ontologos_el::ElClassifier;
8use ontologos_profile::resolve_route;
9use serde::{Deserialize, Serialize};
10use thiserror::Error;
11
12pub use build::build_proof_graph;
13pub use format::render_text;
14
15pub type Result<T> = std::result::Result<T, Error>;
16
17#[derive(Debug, Error)]
18pub enum Error {
19    #[error("explanation generation not yet implemented")]
20    NotImplemented,
21    #[error(transparent)]
22    Profile(#[from] ontologos_profile::Error),
23    #[error("explanation is only supported for OWL EL classification (got {0:?})")]
24    UnsupportedEngine(EngineKind),
25    #[error(transparent)]
26    Core(#[from] ontologos_core::Error),
27    #[error(transparent)]
28    El(#[from] ontologos_el::Error),
29}
30
31/// Node identifier within a proof graph.
32#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
33pub struct NodeId(pub u32);
34
35/// Single step in a reasoning proof.
36#[derive(Debug, Clone, Serialize, Deserialize)]
37pub struct ProofNode {
38    /// Rule that produced this step.
39    pub rule: String,
40    /// Premise nodes in the proof graph.
41    pub premises: Vec<NodeId>,
42    /// Concluded axiom, when applicable.
43    #[serde(skip_serializing_if = "Option::is_none")]
44    pub conclusion_axiom: Option<ontologos_core::AxiomId>,
45    /// EL subsumption conclusion `sub ⊑ sup`.
46    #[serde(skip_serializing_if = "Option::is_none")]
47    pub conclusion_sub: Option<(ontologos_core::EntityId, ontologos_core::EntityId)>,
48    /// EL existential conclusion.
49    #[serde(skip_serializing_if = "Option::is_none")]
50    pub conclusion_existential: Option<(
51        ontologos_core::EntityId,
52        ontologos_core::EntityId,
53        ontologos_core::EntityId,
54    )>,
55    /// EL subproperty conclusion.
56    #[serde(skip_serializing_if = "Option::is_none")]
57    pub conclusion_subproperty: Option<(ontologos_core::EntityId, ontologos_core::EntityId)>,
58}
59
60/// Proof graph backing explanation traces.
61#[derive(Debug, Default, Serialize, Deserialize)]
62pub struct ProofGraph {
63    /// Nodes in topological construction order.
64    pub nodes: Vec<ProofNode>,
65}
66
67impl ProofGraph {
68    /// Export the proof graph as JSON.
69    pub fn to_json(&self) -> Result<String> {
70        serde_json::to_string_pretty(self)
71            .map_err(|e| Error::Core(ontologos_core::Error::Message(e.to_string())))
72    }
73
74    /// Number of proof nodes.
75    #[must_use]
76    pub fn node_count(&self) -> usize {
77        self.nodes.len()
78    }
79
80    /// Whether premise links form a directed acyclic graph.
81    #[must_use]
82    pub fn is_acyclic(&self) -> bool {
83        build::validate_proof_acyclic(&self.nodes).is_ok()
84    }
85}
86
87/// Collect inference trace with explanations enabled on `reasoner`'s ontology.
88pub fn collect_trace(reasoner: &mut Reasoner) -> Result<InferenceTrace> {
89    let route = resolve_route(reasoner.profile(), reasoner.ontology())?;
90    match route.kind {
91        EngineKind::El => Ok(ElClassifier::new()
92            .classify_with_options(reasoner.ontology(), true)?
93            .trace),
94        other => Err(Error::UnsupportedEngine(other)),
95    }
96}
97
98/// Generate proof graph for OWL EL classification traces.
99pub fn explain_el(ontology: &Ontology) -> Result<ProofGraph> {
100    let trace = ElClassifier::new()
101        .classify_with_options(ontology, true)?
102        .trace;
103    build_proof_graph(ontology, &trace)
104}
105
106/// Validate proof graph structure (acyclic, valid axiom ids, premise bounds).
107#[doc(hidden)]
108pub fn assert_valid_proof_graph(ontology: &Ontology, graph: &ProofGraph) {
109    assert!(!graph.nodes.is_empty(), "expected non-empty proof graph");
110    assert!(graph.is_acyclic(), "proof graph must be acyclic");
111    for node in &graph.nodes {
112        if let Some(id) = node.conclusion_axiom {
113            ontology
114                .axiom(id)
115                .unwrap_or_else(|_| panic!("valid conclusion axiom id {}", id.0));
116        }
117        for premise in &node.premises {
118            assert!(
119                (premise.0 as usize) < graph.nodes.len(),
120                "premise node id must exist"
121            );
122        }
123    }
124}
125
126/// Route explanation collection by resolved engine route.
127pub fn explain_with_profile(reasoner: &mut Reasoner) -> Result<ProofGraph> {
128    let trace = collect_trace(reasoner)?;
129    build_proof_graph(reasoner.ontology(), &trace)
130}
131
132#[cfg(test)]
133mod tests {
134    use ontologos_core::{Axiom, EntityId, EntityKind, Ontology};
135
136    use super::*;
137
138    fn class(ontology: &mut Ontology, iri: &str) -> EntityId {
139        ontology.entity_id(iri, EntityKind::Class).expect("class")
140    }
141
142    #[test]
143    fn explain_el_builds_graph() {
144        let mut ontology = Ontology::new();
145        let a = class(&mut ontology, "http://ex.org/A");
146        let b = class(&mut ontology, "http://ex.org/B");
147        let c = class(&mut ontology, "http://ex.org/C");
148        ontology
149            .add_axiom(Axiom::SubClassOf {
150                subclass: a,
151                superclass: b,
152            })
153            .unwrap();
154        ontology
155            .add_axiom(Axiom::SubClassOf {
156                subclass: b,
157                superclass: c,
158            })
159            .unwrap();
160
161        let graph = explain_el(&ontology).expect("graph");
162        assert!(graph.node_count() > 2);
163        assert_valid_proof_graph(&ontology, &graph);
164        assert!(graph.nodes.iter().any(|node| {
165            node.rule == "sub_trans_forward" && node.conclusion_sub == Some((a, c))
166        }));
167    }
168}
ontologos_explain/lib.rs

ontologos_explain/
lib.rs
