Recovering Explanations from Transformed Rule-Based Ontologies

The paper Recovering Explanations from Transformed Rule-Based Ontologies investigates the problem of reconstructing original derivations when Datalog-based ontologies have been optimized through rule rewriting. While rule reasoners use transformations to improve evaluation efficiency, "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. The authors study the problem of constructing, from a proof of entailment under the rewritten rules, a proof under the original ones."

Complexity of Proof Transformations

The authors define the search problem Trans enc(1, 2), which seeks to construct a valid proof DAG for a fact under an original program 1 given a proof (encoded as either a tree or a DAG) under a transformed program 2. The research establishes the following complexity results:

• Upper Bound: Proposition 1. Let 1 2 be programs. Then there exists a polynomial-time algorithm that solves Trans enc(1, 2) for both encodings enc in Tree, DAG.

• Lower Bounds: The problem is PTime-hard if T 1 is encoded as a directed acyclic graph... and LogCFL-hard if T 1 is encoded as a tree. Specifically, Theorem 1 states, There is a pair of programs 1 2 for which the problem Trans DAG(1, 2) is PTime-hard, and Theorem 2 states, There is a pair of programs 1 2 for which the problem Trans Tree(1, 2) is LogCFL-hard.

Proof Transformation Languages

The paper identifies two formalisms for specifying these transformations:

1. Proof Tree Homomorphisms: This class of transformations is characterised by uniform containment (1 u 2), a notion where 1 is contained in 2 over all possible databases. Theorem 3 establishes that there exists a proof tree homomorphism from 1 to 2 if and only if 1 u 2. These are described as local transformations capable of reversing operations such as Atom Permutation and Rule Unfolding.

2. MSO Proof Transformations: To handle global restructurings that homomorphisms cannot, the authors utilize Monadic Second-Order Logic (MSO) interpretations. While standard MSO transductions are limited to linear output growth, MSO interpretations accommodate for such polynomial growth of degree k required by proof transformations. This language can express more complex transformations, including Rule Folding, Filter Propagation, and Projection Pushing. Regarding computational efficiency, Theorem 4 states: Let tau be an MSO proof transformation from program 1 to 2. For any proof tree T for fact f over 1 and database D, the proof DAG tau(T) can be computed by an O(T) space bounded transducer.

1. Transparent High-Performance Reasoning Engines

Integrate a Proof Reconstruction Layer into optimized Datalog-based reasoning engines. This allows the system to use highly efficient, rewritten rule sets for fast computation while providing users with Why? explanations that are mapped back to the original, human-understandable ontology rules rather than the opaque, optimized ones.

2. Verifiable Neuro-Symbolic Optimizers

Develop a verification module for AI systems that use machine learning to optimize symbolic rule sets. By utilizing MSO (Monadic Second-Order) proof transformations, the system can ensure that any rule-rewriting suggested by a neural network is mathematically sound and can be reconstructed into a valid original proof, preventing black-box logic errors in symbolic reasoning.

3. Regulatory-Compliant Knowledge Graph Auditing

Implement an automated auditing subsystem for large-scale Knowledge Graphs (KGs) used in sensitive sectors like finance or medicine. This system can use the Trans enc algorithm to reconstruct the full derivation path of a fact—even if that fact was derived through complex global optimizations like Filter Propagation or Projection Pushing—ensuring a legally defensible and traceable audit trail for every inference.

4. Complexity-Aware Explainable AI (XAI) Interfaces

Build adaptive explanation generators that select the most computationally efficient reconstruction method based on the transformation type. The system would use fast, local Proof Tree Homomorphisms for simple rule permutations and switch to more intensive MSO-based reconstruction only when global restructurings are detected, minimizing the latency of generating explanations in real-time interactive systems.