# Recovering Explanations from Transformed Rule-Based Ontologies

arXiv: https://arxiv.org/abs/2608.06399 · HTML: https://mlsanity.com/paper/2608.06399/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 61 references that are in the map.
- First posted on arXiv 31 Jul 2026.

## Builds on (most cited first, 12 of 12)

- [The Vadalog System: Datalog-based Reasoning for Knowledge Graphs](https://mlsanity.com/paper/1807.08709/) (2018)
- [Column-Oriented Datalog Materialization for Large Knowledge Graphs (Extended Technical Report)](https://mlsanity.com/paper/1511.08915/) (2015)
- [Finding Small Proofs for Description Logic Entailments: Theory and Practice (Extended Technical Report)](https://mlsanity.com/paper/2004.08311/) (2020)
- [Explaining Ontology-Mediated Query Answers using Proofs over Universal Models (Technical Report)](https://mlsanity.com/paper/2208.14381/) (2022)
- [Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version](https://mlsanity.com/paper/2205.09583/) (2022)
- [Efficient Dependency Analysis for Rule-Based Ontologies](https://mlsanity.com/paper/2207.09669/) (2022)
- [The Complexity of Why-Provenance for Datalog Queries](https://mlsanity.com/paper/2303.12773/) (2023)
- [Nemo: First Glimpse of a New Rule Engine](https://mlsanity.com/paper/2308.15897/) (2023)
- [The structure of polynomial growth for tree automata/transducers and MSO set queries](https://mlsanity.com/paper/2501.10270/) (2025)
- [Logica-TGD: Transforming Graph Databases Logically](https://mlsanity.com/paper/2503.00568/) (2025)
- [Rule Rewriting Revisited: A Fresh Look at Static Filtering for Datalog and ASP](https://mlsanity.com/paper/2601.05108/) (2026)
- [Evaluating a Visual Query Tracer and Builder for Learning Declarative Logic Programming](https://mlsanity.com/paper/2607.18864/) (2026)

## Abstract (arXiv)

Datalog rules are often used to define ontologies over Knowledge Graphs. Rule reasoners routinely optimise such ontologies by rewriting their rules into a form that can be evaluated more efficiently. These transformations preserve the entailed facts, but not the structure of the underlying derivations. A proof tree under the rewritten rules explains why a fact holds, but does not readily yield an explanation in terms of the original rules. We study the problem of constructing, from a proof of entailment under the rewritten rules, a proof under the original ones: we establish its computational complexity and identify two practically relevant languages for specifying proof transformations.