Recovering Explanations from Transformed Rule-Based Ontologies

Recovering Explanations from Transformed Rule-Based Ontologies⋆ Alex Ivliev(#) , Markus Krötzsch , and Maximilian Marx

arXiv:2608.06399v1 [cs.LO] 31 Jul 2026

Knowledge-Based Systems Group, TU Dresden, Dresden, Germany {alex.ivliev, markus.kroetzsch, maximilian.marx}@tu-dresden.de

Abstract 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. Keywords: Datalog · Proof transformations · Explainability

1

Introduction

Datalog and its numerous extensions form a family of rule languages that can express ontological knowledge in the Semantic Web context [42,10,28]. OWL RL and OWL EL, two profiles of the Web Ontology Language OWL 2 [49], can be captured by Datalog rules [59,39,40], and extensions of Datalog cover even larger subsets of OWL 2 [17,18]. Datalog is also used for query answering [15,16], for encoding ontological reasoning [40], for data extraction and analysis [52,25], and for transforming Knowledge Graphs [57,21]. A key benefit of Datalog as an ontology language is the inherent explainability of its consequences: any inferred fact can be justified by a proof tree that shows which rules were applied to which facts, tracing every inference back to the input. Computing such proof trees is well-studied for both OWL [38,33,2,3,5,47] and Datalog [23,60,30,14]. For Datalog, it usually takes the form of why-provenance, which asks for not one, but all proof trees of a fact; selecting the “most helpful” among them is a research topic in its own right [4,13]. Even when proof trees grow very large, summarisation and visualisation make them accessible to users [48,21,47]. Another major strength of Datalog is the availability of highly optimised engines that support efficient reasoning over knowledge graphs with billions of facts [50,58,37,35,45]. This efficiency is partly achieved by rewriting the input rules into an equivalent, ⋆

This is the technical report accompanying our ISWC’26 paper [36].

2

A. Ivliev et al. r(a, d) (2)

r(a, d) (4)

r(b, d) (2)

r(a, c) (4)

r(a, b) (1)

r(b, c) (1)

r(c, d) (1)

r(a, b) (3)

e(a, b)

e(b, c)

e(c, d)

e(a, b)

e(c, d)

e(b, c)

Figure 1. Proof trees for ontologies Π1 (left) and Π2 (right) in Example 1.

optimised ontology, using techniques such as program minimisation [55], the Magic Sets rewriting for goal-directed evaluation [8], removal of redundant parameters [53], folding and unfolding of rules [51], and propagation of filter conditions through recursive rules [32]. Some of these techniques were even discovered by studying transformations on proof trees [54,19]. Such transformations preserve the consequences of an ontology, but may substantially change the structure of its derivations, as demonstrated in the following example:

Example 1. The transitive closure r of a binary relation e can be defined by two equivalent ontologies Π1 and Π2 : Ontology Π1 (bushy):

Ontology Π2 (left-linear):

r(x, y) ← e(x, y)

(1)

r(x, y) ← e(x, y)

(3)

r(x, y) ← r(x, z), r(z, y)

(2)

r(x, y) ← r(x, z), e(z, y)

(4)

Both ontologies derive the same r-facts on any input database. However, the bushy rule (2) allows splitting a path at any intermediate node, which may result in balanced proof trees of logarithmic depth. The left-linear rule (4) extends a path by one edge at a time, producing left-leaning chains. Figure 1 shows proof trees for r(a, d) over D = {e(a, b), e(b, c), e(c, d)}. A Datalog engine may rewrite one of these ontologies into the other to evaluate it efficiently. Proof trees are then computed over the rewritten ontology, and thus fail to explain why a fact follows under the original one. We study the problem of recovering such an explanation, i.e., of constructing a corresponding proof tree for the original ontology from a proof tree for the transformed ontology. We establish the computational complexity of this task (Section 4) and, building on tree transducers [7] and Monadic Second-Order-definable transductions [20,24], identify two suitable formalisms for specifying proof tree transformations (Section 5). The appendix of this paper contains further examples.

Recovering Explanations from Transformed Rule-Based Ontologies

2

3

Preliminaries

We recall the syntax of Datalog (with built-in relations) and define its semantics based on proof trees. A recent survey [41] offers a broader treatment. Syntax We consider a vocabulary of mutually disjoint sets P of predicates, C of constants, and V of variables. We associate an arity ar(p) ≥ 0 with every predicate p ∈ P. A term is an element of the set T := C ∪ V. We use t̄ to denote a list of terms ⟨t1 , . . . , tk ⟩ where |t̄| = k. Similarly, we write, e.g., x̄ or ȳ for lists of variables. An atom has the form p(t̄) where p ∈ P and ar(p) = |t̄|. Atoms that do not contain any variables are called facts. The sets of all facts and all atoms are denoted F and A, respectively. A Datalog rule ρ is an expression of the form H ← B1 , . . . , Bn

(5)

where H and B1 , . . . , Bn are atoms. We call H the head and B1 , . . . , Bn the body of ρ. We use notation head(ρ) := H and bodyi (ρ) := Bi for 1 ≤ i ≤ n, and set |ρ| := n. We require that every variable in the head of ρ also appears in its body (safety). Rule bodies are allowed to be empty; in this case, the symbol ← is omitted. A program Π is a triple ⟨R, Pin , Pout ⟩ consisting of a finite set R of rules, and sets Pin and Pout of input and output predicates, respectively, such that input predicates may not appear in the head of a rule. Semantics and Proofs A (potentially infinite) set of facts D is a database. It is an input database for Π = ⟨R, Pin , Pout ⟩ if the predicate of every fact is from Pin . We allow for infinite databases D to express conceptually infinite built-in relations such as ≤ and ̸=. An ontology O = ⟨Π, D⟩ consists of a program Π together with an input database D. An assignment µ for a rule ρ maps every variable x in ρ to a constant µ(x) ∈ C. We extend µ to terms by setting µ(c) := c for constants c ∈ C, to lists of terms by µ(⟨t1 , . . . , tk ⟩) := ⟨µ(t1 ), . . . , µ(tk )⟩, and to atoms by µ(p(t̄)) := p(µ(t̄)). An ordered tree is a tuple T = ⟨V, root, ch⟩ where V is a finite set of nodes, root ∈ V is called the root node, and ch : V → V ∗ maps each node v to a finite sequence ch(v) = ⟨v1 , . . . , vn ⟩ of distinct children of v, such that every node except root appears in exactly one such sequence and root appears in none. We call v a leaf if ch(v) is empty. A proof tree for a fact f over a program Π = ⟨R, Pin , Pout ⟩ and a database D is an ordered tree T = ⟨V, root, ch⟩ together with labelling functions fact : V → F and rule : V → R ∪ {⊥}, such that 1. fact(root) = f ; 2. if ch(v) = ⟨v1 , . . . , vn ⟩ with n ≥ 1, then rule(v) ∈ R with |rule(v)| = n, and there exists an assignment µ for rule(v) such that µ(head(rule(v))) = fact(v) and µ(bodyi (rule(v))) = fact(vi ) for 1 ≤ i ≤ n; and 3. for every leaf v, either: (a) rule(v) = ⊥ and fact(v) ∈ D, or (b) rule(v) ∈ R with |rule(v)| = 0 and fact(v) = head(rule(v)).

4

A. Ivliev et al.

We say that a fact f is derived from Π and D, written Π, D ⊢ f , if there exists a proof tree T for f over Π and D. The leaf database DT of a proof tree T is the set of all facts fact(v) for leaves v of T with rule(v) = ⊥. Every proof tree T for f over Π and D is also a proof tree for f over Π and DT . The output of Π over D is the set out(Π, D) := {f | Π, D ⊢ f and the predicate of f is in Pout }. Remark 1. For finite input databases, out(Π, D) coincides with the set of output facts in the least fixpoint of the standard immediate-consequence operator. With infinite built-in relations, practical systems ensure termination by, e.g., requiring that every variable in a built-in also occurs in a body atom with a finite predicate. Such considerations do not affect our results. Containment Let Π1 = ⟨R1 , Pin , Pout ⟩ and Π2 = ⟨R2 , Pin , Pout ⟩ be programs over the same input and output predicates. We say that Π1 is contained in Π2 , written Π1 ⊑ Π2 , if out(Π1 , D) ⊆ out(Π2 , D) for every input database D. The two programs are equivalent, written Π1 ≡ Π2 , if Π1 ⊑ Π2 and Π2 ⊑ Π1 . A program transformation is a function t mapping programs Π to programs t(Π). It is sound if t(Π) ⊑ Π and complete if Π ⊑ t(Π) for all programs Π.

3

Proof Transformations

A sound program transformation produces a new program Π1 from an original program Π2 , such that Π1 ⊑ Π2 . This guarantees that for every proof tree T1 over Π1 there exists a proof tree T2 over Π2 deriving the same (output) fact over the same input database. The central question of this paper is how to obtain T2 from T1 , and which computational resources this requires. In a proof tree, the same fact may be derived multiple times in independent subtrees. A more compact representation merges such redundant derivations, yielding a directed acyclic graph. A proof DAG for a fact f over a program Π and database D is a tuple G = ⟨V, root, ch, fact, rule⟩ satisfying the same conditions as a proof tree, except that a node may appear as a child of multiple nodes. Notions such as the leaf database DG carry over from proof trees. The unfolding of a proof DAG G is the proof tree unfold(G) obtained by recursively duplicating shared nodes. Conversely, a proof tree may be compressed into a proof DAG by merging nodes labelled with the same fact and the same rule and whose subgraphs are isomorphic. For a fact f = p(t1 , . . . , tk ), Pwe define |f | := k. := The size of a proof tree T = ⟨V, root, ch, fact, rule⟩ is |T | v∈V |fact(v)|. The S := facts of a proof DAG G are facts(G) fact(v), and its size is |G| := v∈V P |{⟨v, w⟩ ∈ V × V | v ∈ ch(w)}| + t∈facts(G) |t|. Definition 1 (Proof transformation). Let Π1 = ⟨R1 , Pin , Pout ⟩ and Π2 = ⟨R2 , Pin , Pout ⟩ be programs with Π1 ⊑ Π2 . A proof transformation from Π1 to Π2 is a function τ that maps every proof tree T1 for a fact f with predicate p ∈ Pout over Π1 and input database D to a proof DAG τ (T1 ) for f over Π2 and D. The result of this transformation is the proof tree unfold(τ (T1 )).

Recovering Explanations from Transformed Rule-Based Ontologies

5

r(a) (9) p(b) (10) r(a) (7) r(b) (7) r(c) (6)

q(b) (11)

e(b, a)

r(b) (9)

e(b, a)

p(c) (10)

e(c, b)

q(c) (11)

e(c, b)

r(c) (8) s(c)

s(c)

Figure 2. Proof tree T1 for Π1 (left) and proof DAG τ (T1 ) for Π2 (right) of Example 2

We require that τ (T1 ) is a proof DAG instead of a proof tree because proof trees can be exponentially larger than the corresponding proof DAGs. The following example demonstrates such an unavoidable blowup. Example 2. Consider the following equivalent programs Π1 and Π2 with input predicates Pin = {s, e} and output predicate Pout = {r}. Program Π1 :

Program Π2 :

r(x) ← s(x)

(6)

r(x) ← s(x)

(8)

r(y) ← r(x), e(x, y)

(7)

r(y) ← p(x), q(x), e(x, y)

(9)

p(x) ← r(x)

(10)

q(x) ← r(x)

(11)

Both programs derive r(x) for exactly those x reachable from some s-fact along e-edges. However, Π2 duplicates each derivation of r(x) through the auxiliary predicates p and q. Consider D = {s(c), e(c, b), e(b, a)}. A proof transformation τ from Π1 to Π2 must map nodes for rules (6) and (7) to nodes for rules (8) and (9), respectively, and introduce two nodes for rules (10) and (11) below each node for rule (9). Figure 2 shows the proof tree T1 for r(a) over Π1 and D, and the proof DAG τ (T1 ) over Π2 and D. The unfolding unfold(τ (T1 )) is exponential in the size of T1 .

4

Complexity of Proof Transformations

We now focus on the computational problem of transforming a proof tree T1 over Π1 into a proof DAG T2 over Π2 for the same fact. A naive approach extracts the leaf database of T1 and evaluates Π2 from scratch, which takes time polynomial in the size of T1 . In this section, we show that producing a valid output is PTime-hard if T1 is encoded as a directed acyclic graph, matching the naive upper bound, and LogCFL-hard if T1 is encoded as a tree.

6

4.1

A. Ivliev et al.

The Transformation Problem

A proof transformation (Definition 1) assigns a fixed output proof to every input proof. Here, instead, we study the computational complexity of constructing some valid proof over Π2 from a proof over Π1 for the same fact, accepting any valid proof DAG as output. Intuitively, this captures the complexity of the best possible transformation algorithm: lower bounds apply to every proof transformation, while the upper bounds are established by a particular transformation algorithm. Formally, we define the search problem as follows. Problem: Transenc (Π1 , Π2 ) for programs Π1 ⊑ Π2 Input: A proof tree (if enc = Tree) or proof DAG (if enc = DAG) T1 for a fact f whose predicate is in Pout , over Π1 and input database DT1 . Output: A proof DAG T2 for f over Π2 and DT1 . Note that we fix the programs Π1 ⊑ Π2 in the problem definition, so complexity is measured only in terms of the size of the input. Consequently, algorithms for Transenc (Π1 , Π2 ) may exploit properties of the particular program pair. We consider both encodings enc ∈ {Tree, DAG} of the input proof tree (both given as adjacency lists), because they may differ exponentially in size (see Example 2). This difference stems solely from sharing identical subderivations, making the tree encoding the more informative measure when sharing is limited. A search problem associates every instance with a (non-empty) set of solutions. An algorithm solves such a problem if, for every instance, it computes a valid solution. To establish hardness, we use the following notion of reduction, adapted from the standard treatment of multivalued function problems in complexity theory [46]: An NC1 reduction from a decision problem L to a search problem S is a pair of functions g and h, computable by logspace-uniform NC1 circuit families [31], such that for every instance x of L: (1) g(x) is an instance of S, and (2) for every solution y of g(x), we have h(y) = 1 iff x ∈ L. Condition (2) quantifies over all solutions since an algorithm solving S may output any of them. A search problem S is C-hard under NC1 reductions for a complexity class C if every decision problem in C reduces to S via an NC1 reduction. We only consider NC1 reductions here, since they are sufficiently weak to establish L-hardness, yet expressive enough to admit L-complete problems to reduce from. 4.2

Complexity Results

The naive approach gives us an upper bound for the transformation problem: Proposition 1. Let Π1 ⊑ Π2 be programs. Then there exists a polynomial-time algorithm that solves Transenc (Π1 , Π2 ) for both encodings enc ∈ {Tree, DAG}. Proof. Given T1 , we compute the least fixpoint of Π2 over DT1 in polynomial time [1], storing for each fact the rule instance that was used to derive it. We get f ∈ out(Π2 , DT1 ) since Π1 ⊑ Π2 . Then, the stored rule instances, starting from f , form a proof DAG T2 for f over Π2 and DT1 . ⊔ ⊓

Recovering Explanations from Transformed Rule-Based Ontologies

7

For the corresponding lower bound, we reduce from the Circuit Value Problem, which is known to be PTime-complete for DAG-encoded circuits [31]. As an immediate corollary, we also obtain a L-hardness for TransTree (Π1 , Π2 ), as this problem is L-complete when the circuit is given as a tree [9]. We show a LogCFL lower bound later. Theorem 1. There is a pair of programs Π1 ⊑ Π2 for which the problem TransDAG (Π1 , Π2 ) is PTime-hard. Proof. We define programs Π1 and Π2 over the single output predicate goal and the set of input predicates Pin = {tin , fin , and, not, out}, where we use facts and(g, g1 , g2 ) and not(g, g1 ) to encode the structure of the circuit, tin (g) and fin (g) to declare the input gate g as true or false, and out(g) to mark the output gate. Program Π2 evaluates the circuit as expected: true(g) ← tin (g)

(12)

false(g) ← fin (g)

(13)

true(g) ← and(g, g1 , g2 ), true(g1 ), true(g2 ) false(g) ← and(g, g1 , g2 ), false(g1 ), true(g2 ) goal ← false(g), out(g)

(14) (15)

false(g) ← and(g, g1 , g2 ), true(g1 ), false(g2 ) false(g) ← and(g, g1 , g2 ), false(g1 ), false(g2 )

(17) (18)

true(g) ← not(g, g1 ), false(g1 ) (19) false(g) ← not(g, g1 ), true(g1 )

(20)

goal ← true(g), out(g)

(21)

(16)

Proof trees of Π2 correspond to evaluations of the circuit encoded by the input facts, where the result of the output gate is obtained by checking the rule label at the root of the proof tree. When constructing Π1 , we need to ensure that goal is only derived when Π2 can derive a valuation for an output gate: maybe(g) ← tin (g)

(22)

maybe(g) ← fin (g)

(23)

maybe(g) ← maybe(g1 ), maybe(g2 ), and(g, g1 , g2 )

(24)

maybe(g) ← not(g, g1 ), maybe(g1 )

(25)

goal ← maybe(g), out(g)

(26)

Proof trees of Π1 encode the structure of the circuit, but do not evaluate it. We can thus obtain a suitable input DAG T1 from an arbitrary circuit by a simple relabelling that maps the gate types to the corresponding rules in Π1 . ⊓ ⊔ We now show the LogCFL lower bound for TransTree (Π1 , Π2 ). As in the proof of Theorem 1, program Π1 merely validates the structure of the input, while Π2 decides a concrete problem. Here, we reduce from the word problem of a fixed context-free language. Theorem 2. There is a pair of programs Π1 ⊑ Π2 for which the problem TransTree (Π1 , Π2 ) is LogCFL-hard.

8

A. Ivliev et al.

Proof. Let L be a context-free language with grammar G = ⟨V, Σ, P, S⟩ and Σ ⊆ C. For this reduction, we pick L to be a language whose word problem is LogCFL-complete under NC1 reductions [43] and assume G to be given in quadratic Greibach normal form [6], i.e., each production p ∈ P is of the form A → σA1 · · · An for 0 ≤ n ≤ 2, a terminal symbol σ ∈ Σ, and nonterminal symbols A, A1 , . . . , An ∈ V . We use input predicates Pin = {first, next, last} and the output predicate goal, and encode a word w = σ1 · · · σℓ ∈ Σ + as the database Dw := {first(c1 ), next(c1 , σ1 , c2 ), . . . , next(cℓ , σℓ , cℓ+1 ), last(cℓ+1 )}, where next(x, σ, y) expresses that position y follows position x when reading the letter σ. Program Π1 consists of the following rules, where rule (27) is instantiated for every σ ∈ Σ: r(x, y) ← next(x, σ, y)

(27)

r(x, y) ← r(x, z), r(z, y)

(28)

goal ← r(x, y), first(x), last(y)

(29)

Program Π2 includes the rules of form (27) and rule (28). For each nonterminal A ∈ V , it uses binary predicates A and Ā, intended to hold on a span of the word iff A can, respectively cannot, produce that span. Program Π2 further contains the following two rules, which can be used to decide if w ∈ L: goal ← first(x), last(y), S(x, y)

(30)

goal ← first(x), last(y), S̄(x, y)

(31)

The predicates A are derived by the rules given below, which are instantiated for each production A → σA1 · · · An ∈ P : A(x, xn+1 ) ← next(x, σ, x1 ), A1 (x1 , x2 ), . . . , An (xn , xn+1 )

(32)

Deriving the complements Ā is more challenging, as Π2 must verify that no production of A can produce the span. For every production p ∈ P , we use binary predicate p̄ that holds on every span that cannot be produced by p. Then, Π2 contains for each nonterminal A ∈ V derived by productions p1 , . . . , pm ∈ P : Ā(x, y) ← p̄1 (x, y), . . . , p̄m (x, y)

(33)

A production p with leading terminal σ fails on every span that does not start with σ. We derive these spans using an auxiliary predicate σ̄: σ̄(x, y) ← next(x, σ ′ , y)

(34)

p̄(x, y) ← σ̄(x, y)

(35)

p̄(x, y) ← σ̄(x, z), r(z, y)

(36)

′

for all σ ̸= σ ∈ Σ and productions p ∈ P with lead terminal σ. The remaining causes of failure depend on the shape of p. A production p = A → σ additionally fails on every span of length at least two: p̄(x, y) ← next(x, t, z), r(z, y)

(37)

Recovering Explanations from Transformed Rule-Based Ontologies

9

A production p = A → σA1 additionally fails on spans of length one, which are too short, and on spans whose remainder after σ cannot be produced by A1 : p̄(x, y) ← next(x, t, y)

(38)

p̄(x, y) ← next(x, σ, z), Ā1 (z, y)

(39)

Finally, consider a production p = A → σA1 A2 . Spans of length one or two are again too short: p̄(x, y) ← next(x, t, y) p̄(x, y) ← next(x, t, z), next(z, t′ , y)

(40) (41)

On longer spans, p fails iff every way of splitting the word between A1 and A2 fails. We capture this condition with two auxiliary predicates. The first predicate p̄s (z, s, y) states that the span from z to y cannot be split at position s, since A1 fails on the part before s or A2 fails on the part after it. The second predicate p̄≤s (z, s, y) states that all split positions up to s fail: p̄s (z, s, y) ← Ā1 (z, s), r(s, y)

(42)

p̄s (z, s, y) ← r(z, s), Ā2 (s, y)

(43)

p̄≤s (z, s, y) ← next(z, t, s), p̄s (z, s, y)

(44)

p̄≤s (z, s′ , y) ← p̄≤s (z, s, y), next(s, t, s′ ), p̄s (z, s′ , y)

(45)

p̄(x, y) ← next(x, σ, z), p̄≤s (z, s, y), next(s, t, y)

(46)

For containment, consider an input database D with goal ∈ out(Π1 , D). Then there are constants c1 , . . . , cℓ+1 and s1 , . . . , sℓ such that D contains the facts first(c1 ), last(cℓ+1 ), and next(ci , si , ci+1 ) for all 1 ≤ i ≤ ℓ, spelling out the word w = s1 · · · sℓ . If w ∈ L, we can use rules of form (32) to simulate productions of G, deriving A(ci , cj+1 ) if the nonterminal A can produce the span si · · · sj . Hence, we have Π2 , D ⊢ S(c1 , cℓ+1 ), and thus Π2 , D ⊢ goal by rule (30). For the case w ∈ / L we show, by induction on the length of a span ci , . . . , cj+1 , that Π2 derives Ā(ci , cj+1 ) for every nonterminal A ∈ V that does not produce si · · · sj . It suffices by rule (33) to derive p̄(ci , cj+1 ) for every production p = A → σA1 · · · An ∈ P that cannot produce si · · · sj . If si ̸= σ, this follows from rules (35) and (36). Otherwise, we distinguish the three shapes of p. For n = 0, the production fails only if the span is longer than one letter, which is covered by rule (37). For n = 1, it fails if the span consists of a single letter (rule (38)), or if A1 does not produce the remainder si+1 · · · sj , in which case the induction hypothesis yields Ā1 (ci+1 , cj+1 ) and rule (39) applies. For n = 2, spans of one or two letters are too short (rules (40) and (41)); on longer spans, every split of the remainder must fail. By the induction hypothesis, rules (42) and (43) then derive p̄s (ci+1 , ck , cj+1 ) for every split position ck , so that rules (44) and (45) derive p̄≤s (ci+1 , cj , cj+1 ) and therefore rule (46) applies. We obtain Π2 , D ⊢ S̄(c1 , cℓ+1 ) for the full span, and hence goal ∈ out(Π2 , D) by rule (31). On the encoding Dw of a word w exactly one of S(c1 , cℓ+1 ) and S̄(c1 , cℓ+1 ) is derivable. Hence the rule at the root of every proof tree for goal over Π2 and Dw is determined by whether w ∈ L. ⊔ ⊓

10

5

A. Ivliev et al.

Proof Transformation Languages

We now turn to the question of how to specify proof transformations and identify two practical transformation languages. In Section 5.1, we show that the notion of uniform containment between programs admits local transformations defined by proof tree homomorphisms. We consider Monadic Second-Order Logic (MSO) interpretations as a transformation language in Section 5.2, which define transformations computable in logarithmic space for tree-encoded inputs. 5.1

Proof Tree Homomorphisms

A simple class of proof transformation arises from uniform containment, a notion introduced by Sagiv for minimising Datalog programs [55]. In this setting, an atom or a rule is considered redundant if removing it from the program results in an equivalent program. Checking containment between two Datalog programs is undecidable [56], so uniform containment can be used as a decidable alternative. Definition 2 (Uniform containment). Let Π1 = ⟨R1 , Pin , Pout ⟩ and Π2 = ⟨R2 , Pin , Pout ⟩ be programs over the same input and output predicates. Program Π1 is uniformly contained in Π2 , denoted Π1 ⊑u Π2 , if for every database D (not only input databases for Π1 or Π2 ), we have out(Π1 , D) ⊆ out(Π2 , D). Note that containment compares the output of the programs on input databases, while for uniform containment out(Π1 , D) ⊆ out(Π2 , D) must hold over all databases D. Hence, Π1 ⊑u Π2 implies Π1 ⊑ Π2 , but the converse does not hold in general. Let ω : V → C be an injective mapping from variables to constants. We can decide whether Π1 ⊑u Π2 by verifying for every rule ρ1 ∈ R1 , that its head can be derived from its body using Π2 , i.e., that Π2 , D ⊢ ω(head(ρ1 )) for D = {ω(bodyi (ρ1 )) | 1 ≤ i ≤ |ρ1 |} [55]. This leads to a class of proof transformations that replace each node of a proof tree for Π1 with the matching derivation of the same fact in Π2 . This corresponds naturally to the notion of tree homomorphisms [27], which we adapt for proof trees as follows. Definition 3 (Proof tree template). Let Π = ⟨R, Pin , Pout ⟩ be a program and ρ be a rule. A proof tree template T for ρ over Π is a tuple ⟨V, root, ch, atom, rule⟩ where ⟨V, root, ch⟩ is an ordered tree with labelling functions atom : V → A and rule : V → R, such that 1. atom(root) = head(ρ); 2. if ch(v) = ⟨v1 , . . . , vn ⟩ with n ≥ 1, then rule(v) ∈ R with |rule(v)| = n, and there exists a substitution θv : V → T such that θv (head(rule(v))) = atom(v) and θv (bodyi (rule(v))) = atom(vi ) for 1 ≤ i ≤ n; and 3. for every leaf node ℓ, there is an index ρℓ with 1 ≤ ρℓ ≤ |ρ| such that atom(ℓ) = bodyρℓ (ρ). Let T be a proof tree template for a rule ρ with |ρ| = n over Π and L ⊆ V the set of leaves of T . Furthermore, let T1 , . . . , Tn be proof DAGs over Π with

Recovering Explanations from Transformed Rule-Based Ontologies

11

Ti = ⟨Vi , rooti , chi , facti , rulei ⟩ that do not share nodes with T or with each other. If there is a substitution σ : V → C with σ(bodyi (ρ)) = fact(rooti ) for 1 ≤ i ≤ n, we write T [T1 , . . . , Tn ] to denote the proof DAG S that results from uniformly replacing each node in ⟨V ′ , root′ , ch′ , fact′ , rule′ ⟩ with a fresh copy, where Sn – V ′ := (V ∪ i=1 Vi ) \ L; ′ := – root root; Sn – ch′ := ch ∪ i=1 chi replacing every occurrence of a leaf node ℓ ∈ L by rootρℓ ; – fact′ (v) := σ(atom(v)) for v ∈ V and fact′ (v) := facti (v) for v ∈ Vi ; and – rule′ (v) := rule(v) for v ∈ V and rule′ (v) := rulei (v) for v ∈ Vi . Further, we use T|v to denote the subgraph of a proof DAG T rooted at v. We can now define proof tree homomorphisms as follows. Definition 4 (Proof tree homomorphism). Let Π1 = ⟨R1 , Pin , Pout ⟩ and Π2 = ⟨R2 , Pin , Pout ⟩ be programs with Π1 ⊑ Π2 , and let {Sρ }ρ∈R1 be a family of proof tree templates where Sρ is a proof tree template for ρ ∈ R1 over Π2 . The proof tree homomorphism induced by {Sρ }ρ∈R1 is a proof transformation τ defined as follows. Given a proof tree T = ⟨V, root, ch, fact, rule⟩ over Π1 and some database D, we obtain τ (T ) recursively: 1. if v is a leaf node, then τ (T|v ) := T|v ; 2. otherwise, if ch(v) = ⟨v1 , . . . , vn ⟩ and rule(v) = ρ, then τ (T|v ) := Sρ [τ (T|v1 ), . . . , τ (T|vn )] From the above characterisation of uniform containment, we immediately obtain: Theorem 3. Let Π1 and Π2 be programs. Then there exists a proof tree homomorphism from Π1 to Π2 if and only if Π1 ⊑u Π2 . Example 3. Recall the programs Π1 (bushy) and Π2 (left-linear) from Example 1. We have Π2 ⊑u Π1 , so we can obtain a proof tree homomorphism from Π2 to Π1 . For the base rule (3), the template T(3) applies the corresponding base rule (1) of Π1 directly: r(x, y) (1) e(x, y)

For the recursive rule (4), the template T(4) uses the bushy rule (2) at the root and derives r(z, y) from the second body atom e(z, y) via (1): r(x, y) (2) r(z, y) (1) r(x, z)

e(z, y)

Appendix A contains further examples of proof tree homomorphisms.

12

A. Ivliev et al.

5.2

Transformations Based on Monadic Second-Order Logic

Proof tree homomorphisms are restricted to local transformations and cannot consider the global structure of the input tree. For instance, the reverse direction of Example 3, transforming bushy proof trees of Π1 into left-linear proof trees of Π2 , cannot be realised by proof tree homomorphisms. MSO transductions [20,24] are a well-studied formalism for tree-to-tree transformations that can express such global restructurings. However, the output of MSO transductions is at most linear in the input, while proof transformations may require polynomial growth: Example 4. Consider the following programs Π1 and Π2 : Program Π1 : r(x) ← s(x) r(y) ← r(x), n(x, y) goal ← r(x), e(x)

Program Π2 : (47) (48) (49)

r(x, x) ← s(x)

(50)

′

′

′

′

r(x, y ) ← r(x, y), n(y, y ) ′

(51) ′

r(x , y ) ← r(x, y), n(x, x ), s(y ), e(y) (52) goal ← r(x, y), e(x), e(y)

(53)

Program Π1 derives goal if there is a path of n-edges from some s-fact to an e-fact. Program Π2 implements a counter, traversing all possible pairs of values along the n-chain. Hence, proof trees for goal over Π1 are of size linear in the input, while proof trees for goal over Π2 are of size quadratic in the input. We accommodate for such polynomial growth of degree k by using MSO interpretations [11], a generalisation of MSO transductions in which output elements are defined as k-tuples of input elements. Encoding proof trees as logical structures The goal is to define proof transformations as MSO formulae. With each proof tree, we therefore associate a relational structure consisting of the following relations over a universe of tree nodes and constants: – childi (x, y) if x is the ith child of y; – ruleρ (x) if rule ρ is applied to obtain x; and – argj (x, d) if the jth argument of the fact at x is d. We can now express proof trees as databases over this signature. Definition 5. Let T = ⟨V, root, ch, fact, rule⟩ be a proof tree over a program Π = ⟨R, Pin , Pout ⟩ and some database D. The associated interpretation of T is the database I(T ), which contains exactly the following facts: – childi (v, w) for every v, w ∈ V such that ch(w) = ⟨v1 , . . . , vn ⟩ with v = vi ; – ruleρ (v) for every v ∈ V and ρ ∈ R such that rule(v) = ρ; and – argj (v, d) for every v ∈ V such that fact(v) = p(d1 , . . . , dm ) with d = dj .

Recovering Explanations from Transformed Rule-Based Ontologies

13

MSO transformations We can now use MSO formulae to specify a proof transformation by defining the output structure over the nodes of the input proof tree. For an introduction to Monadic Second-Order Logic, we refer to Libkin [44]. The following definition for MSO interpretations is adapted to our setting from Gallot et al. [26]. Definition 6 (MSO interpretation). Let Π = ⟨R, Pin , Pout ⟩ be a program. Let n be the maximum arity of any rule in R and let m be the maximum arity of any atom occurring in R. A k-dimensional MSO interpretation for Π with k ≥ 1 consists of – a finite set C of components, – for each component α ∈ C, an MSO formula φα dom (x̄) with k free variables, – for each α ∈ C and ρ ∈ R, an MSO formula φα ρ (x̄) with k free variables, – for each α, β ∈ C and 1 ≤ i ≤ n, an MSO formula φα,β,i child (x̄, ȳ) with 2k free variables, and – for each α ∈ C, and 1 ≤ j ≤ m, an MSO formula φα,j arg (x̄, d) with k + 1 free variables. Conceptually, an MSO interpretation defines an output tree whose nodes are tuples of input nodes selected by φα dom (x̄) for each component α ∈ C. The remaining formulae define the labellings of children, rules, and facts. We write D, v̄ |= φ(x̄) to denote that the MSO formula φ is satisfied in the database D when the free variables x̄ are assigned to the elements v̄. Definition 7 (MSO proof transformation). Let Π1 = ⟨R1 , Pin , Pout ⟩ and Π2 = ⟨R2 , Pin , Pout ⟩ be programs with Π1 ⊑ Π2 . A proof transformation τ from Π1 to Π2 is an MSO proof transformation if there is a k-dimensional MSO interpretation for Π2 and some k ≥ 1 and some set of components C such that for every proof tree T1 = ⟨V1 , root1 , ch1 , fact1 , rule1 ⟩ for some fact f with predicate p ∈ Pout over Π1 and database D, there is a proof DAG G2 = τ (T1 ) = ⟨V2 , root2 , ch2 , fact2 , rule2 ⟩ for f over Π2 and D where – the nodes of G2 are pairs ⟨α, v̄⟩ ∈ C × V1k with I(T1 ), v̄ |= φα dom (x̄); – the rule at node ⟨α, v̄⟩ is the unique ρ ∈ R2 such that I(T1 ), v̄ |= φα ρ (x̄); – node ⟨β, w̄⟩ is the i-th child of ⟨α, v̄⟩ iff I(T1 ), v̄, w̄ |= φα,β,i (x̄, ȳ); and child – the j-th argument of the fact at ⟨α, v̄⟩ is d iff I(T1 ), v̄, d |= φα,j arg (x̄, d). Example 5. The proof transformation from bushy trees to left-linear trees from Example 1 can be described as a 1-dimensional MSO proof transformation with components C = {α} as follows. We assume a relation v ≤ w that holds whenever v = w or w is an ancestor of := ¬∃u. child(u, v) and Root(v) := ¬∃w. child(v, w) v and further define Leaf(v) W where child(u, v) := i childi (u, v). We then order the nodes above the leaves (derived by rule (1)) of the input tree from left to right: u <ℓ v := rule(1) (u) ∧ rule(1) (v) ∧ ∃p, a, b. child1 (a, p) ∧ child2 (b, p) ∧ u ≤ a ∧ v ≤ b

(54)

14

A. Ivliev et al.

We can check whether two nodes u and v are next to each other in the order Cons(u, v) := u <ℓ v ∧ ¬∃w. u <ℓ w ∧ w <ℓ v

(55)

We then identify the leftmost and rightmost nodes labelled with rule (1): First(v) := rule(1) (v) ∧ ¬∃w. Cons(w, v) Last(v) := rule(1) (v) ∧ ¬∃w. Cons(v, w)

(56) (57)

With this in place, we can define the structure of the output tree as follows: φdom (x) := ¬rule(2) (x)
1 φchild (x, y) := child1 (x, y) ∧ First(y) ∨ Cons(x, y) φ2child (x, y) := ¬First(y) ∧ rule(1) (y) ∧ child1 (x, y) φ(3) (x) := First(x) φ(4) (x) := ∃y. Cons(y, x) φ1arg (x, d) :=

Leaf(x) ∧ arg1 (x, d)
∨ rule(1) (x) ∧ ∃r. Root(r) ∧ arg1 (r, d)

φ2arg (x, d) := arg2 (x, d)

(58) (59) (60) (61) (62) (63) (64)

Complexity We now show that MSO proof transformations can be evaluated in logarithmic space when the input is encoded as a tree. Our argument uses the fact that MSO model checking over structures of bounded treewidth can be performed in logarithmic space [22]. We begin by recalling the relevant notions. Given a tree T with vertex set V and a subset X ⊆ V , we write T [X] for the subtree of T induced by X, that is, the tree obtained by restricting T to the nodes in X while preserving the child relationship among them. For a database D, we write A(D) for the set of all constants occurring in D. Definition 8 (Treewidth). Let D be a database. A tree decomposition of D is a labelled tree T = ⟨V, E, B⟩ with labelling function B : V → {X | X ⊆ A(D)} such that 1. for all a ∈ A(D), the induced subtree T [X] with X = {v ∈ V | a ∈ B(v)} is nonempty and connected; and 2. for every p(t1 , . . . , tk ) ∈ D, there is a node v ∈ V with {t1 , . . . , tk } ⊆ B(v). The width of a tree decomposition is maxv∈V |B(v)| − 1. The treewidth of D is the minimal width of any of its tree decompositions; the treewidth of a proof tree T is the treewidth of I(T ). The treewidth of a proof tree T over Π might grow arbitrarily large due to the presence of argj (v, d) facts in I(T ). However, we can find a proof tree T ′ for the same fact such that its treewidth only depends on Π. The key observation is that we can rename apart all constants in T such that two occurrences of a constant remain equal only when the validity of the proof tree requires them to be. This results in a tree where each constant appears only within a connected region: namely, within the subtree rooted at the rule instance that first introduced it.

Recovering Explanations from Transformed Rule-Based Ontologies

15

Lemma 1. For every program Π there exists a constant kΠ such that for every proof tree T = ⟨V, root, ch, fact, rule⟩ for f over Π and database D, there is a database D′ and a proof tree T ′ for f over Π and D′ with treewidth at most kΠ . Proof. In the following, we write vars(E) and terms(E) for the set of all variables and all terms, respectively, that appear in an expression E. We obtain T ′ = ⟨V, root, ch, fact′ , rule⟩ from T , where fact′ is defined recursively for each v ∈ V as follows: – If v = root, then fact′ (v) := fact(v). – If v is the i-th child of w ∈ V and rule(w) = ρ, let θ : vars(head(ρ)) → C be a substitution such that θ(head(ρ)) = fact′ (w). Given fact(v) = p(t1 , . . . , tk ) and bodyi (ρ) = p(s1 , . . . , sk ), we set fact′ (v) := p(t′1 , . . . , t′k ) where ( θ(sj ) if sj ∈ vars(head(ρ)) or sj ∈ C; and t′j = ⟨tj , w⟩ otherwise. Since the number of distinct constants in any single rule instance is bounded by the number of terms appearing in the rules of Π, we can construct a tree decomposition whose bags correspond to rule instances, each containing only the constants mentioned in that instance. Let D = ⟨V, E, B⟩ where {v, w} ∈ E if v is a child of w in T . We define B(ℓ) := terms(fact′ (ℓ)) ∪ {ℓ} for each leaf node ℓ in T ; for all other nodes v ∈ V with ch(v) = ⟨v1 , . . . , vn ⟩ we set [ B(v) := {v} ∪ {vi | 1 ≤ i ≤ n} ∪ terms(fact′ (v)) ∪ terms(fact′ (vi )) (65) 1≤i≤n

Then D defines a tree decomposition for T whose width depends only on the maximal number of distinct terms in a rule of Π, giving us the desired bound kΠ . Condition 1 of Definition 8 is satisfied because every constant is confined to a connected subtree; condition 2 holds because all constants of each fact are witnessed in the bag of the node where the corresponding rule is applied. ⊔ ⊓ Since MSO model checking over structures of bounded treewidth can be performed in logarithmic space [22, Theorem 1.2], we thus obtain the following. Theorem 4. Let τ be an MSO proof transformation from program Π1 to Π2 . For any proof tree T = ⟨V, root, ch, fact, rule⟩ for fact f over Π1 and database D, the proof DAG τ (T ) can be computed by an O(log |T |) space bounded transducer. Proof. If τ is an MSO proof transformation, there exists a k-dimensional MSO interpretation and set of components C satisfying Definition 7. For a proof tree T , we evaluate each MSO formula over I(T ′ ), where we obtain T ′ = ⟨V, root, ch, fact′ , rule⟩ as in Lemma 1. Note that we do not need to store T ′ as an intermediate step, since we can compute fact′ (v) for any v ∈ V on demand in logarithmic space. For each term position j in fact(v), we determine t′j by walking upward from v toward the root, following how the variable at position j is propagated through the heads of successive rule instances. If the

16

A. Ivliev et al.

variable appears in the head of the current rule, we continue upward, inheriting the corresponding position in the parent’s fact. Otherwise, the current node is the ancestor that introduced this constant, and we return the tagged pair ⟨tj , w⟩. By Lemma 1, I(T ′ ) has bounded treewidth, so each formula can be evaluated in logarithmic space [22, Theorem 1.2]. To instantiate each formula, we need k counters over the vertex set V for φdom (x̄) and φρ (x̄), 2k counters over V for φchild (x̄, ȳ), k counters over V , and 1 counter over the set of all terms occurring in fact labels for φarg (x̄, d). This yields a proof DAG τ (T ) for f over D′ . We rename each fresh constant ⟨t, w⟩ to t to get a proof DAG for f over D. ⊔ ⊓ While this suggests that there are program transformations that cannot be reversed using an MSO proof transformation (unless L = NL = LogCFL), we find that MSO proof tree transformations are expressive enough to capture many practical transformations. We have already seen that Example 5 can be expressed; we provide further examples in Appendix B.

6

Conclusions and Outlook

We have studied the problem of reversing program transformations at the level of proof trees and established PTime-hardness for the DAG-encoded case and LogCFL-hardness for the tree-encoded case. We have identified two practical transformation languages: Proof tree homomorphisms are characterised by uniform containment, and capture local transformations, such as transforming leftlinear proof trees into bushy proof trees (see Example 3). MSO proof tree transformations handle a strictly larger class of restructurings (such as transforming from bushy proof trees back to left-linear proof trees, see Example 5), but can still be evaluated efficiently in logarithmic space on tree-encoded input. For future work, several directions remain open. For tree-encoded inputs, there remains a gap between the LogCFL lower bound and the PTime upper bound. It is unclear whether this can be closed. Similarly, a characterisation of the program transformations that admit a reversal by an MSO proof transformation, along the lines of the characterisation of first-order tree-to-tree transductions by Bojańczyk and Doumane [12], is desirable. On the more practical side, we are implementing proof transformations in our Datalog engine Nemo [35,34] and plan to assess the practical overhead of proof tree reconstruction on realistic knowledge graphs and optimised rule sets. Lastly, it would be interesting to study how proof tree transformations generalise to extensions of Datalog such as existential rules, aggregates, or stratified negation. Acknowledgments. This work is supported by Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) in project number 389792660 (TRR 248, Center for Perspicuous Systems), by the Bundesministerium für Forschung, Technologie und Raumfahrt (BMFTR, Federal Ministry of Research, Technology and Space) in the Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI), and in DAAD project 57616814 (SECAI, School of Embedded Composite AI) as part of the program Konrad Zuse Schools of Excellence in Artificial Intelligence.

Recovering Explanations from Transformed Rule-Based Ontologies

17

Supplemental Material Statement. While the paper is self-contained, we provide further examples of proof transformations in the appendix. Declaration of use of Generative AI. Claude (Anthropic) was used for proofreading and preparing the figures. It also identified and helped correct an error in the proof of Theorem 2.

References 1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison Wesley (1994) 2. Alrabbaa, C., Baader, F., Borgwardt, S., Dachselt, R., Koopmann, P., Méndez, J.: Evonne: Interactive proof visualization for description logics (system description). In: Blanchette, J., Kovács, L., Pattinson, D. (eds.) Proc. 9th Int. Joint Conf. on Automated Reasoning (IJCAR’18). Lecture Notes in Computer Science, vol. 13385, pp. 271–280. Springer (2022). https://doi.org/10.1007/978-3-031-10769-6 3. Alrabbaa, C., Baader, F., Borgwardt, S., Koopmann, P., Kovtunova, A.: Finding small proofs for description logic entailments: Theory and practice. In: Albert, E., Kovács, L. (eds.) Proc. 13thInt. Conf. on Logic for Programming, Artificial Intelligence and Reasoning (LPAR’20). EPiC Series in Computing, vol. 73, pp. 32–67. EasyChair (2020). https://doi.org/10.29007/NHPP 4. Alrabbaa, C., Borgwardt, S., Herrmann, P., Krötzsch, M.: The shape of EL proofs: A tale of three calculi. In: Proc. 38th Int. Workshop on Description Logics (DL’25). CEUR Workshop Proceedings, vol. 4091. CEUR-WS.org (2025), https://ceur-ws. org/Vol-4091/paper45.pdf 5. Alrabbaa, C., Borgwardt, S., Koopmann, P., Kovtunova, A.: Explaining ontologymediated query answers using proofs over universal models. In: Governatori and Turhan [29], pp. 167–182. https://doi.org/10.1007/978-3-031-21541-4_11 6. Autebert, J., Berstel, J., Boasson, L.: Context-free languages and pushdown automata. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, Volume 1: Word, Language, Grammar, pp. 111–174. Springer (1997). https://doi.org/10.1007/978-3-642-59136-5_3 7. Baker, B.S.: Tree transducers and tree languages. Inf. Control. 37(3), 241–266 (1978). https://doi.org/10.1016/S0019-9958(78)90538-7 8. Bancilhon, F., Maier, D., Sagiv, Y., Ullman, J.D.: Magic sets and other strange ways to implement logic programs. In: Silberschatz, A. (ed.) Proc. 5th Symposium on Principles of Database Systems (PODS’86). pp. 1–15. ACM (1986). https:// doi.org/10.1145/6012.15399 9. Beaudry, M., McKenzie, P.: Circuits, matrices, and nonassociative computation. J. of Comput. Syst. Sci. 50(3), 441–455 (1995). https://doi.org/10.1006/JCSS.1995. 1035 10. Bellomarini, L., Sallinger, E., Gottlob, G.: The Vadalog system: Datalog-based reasoning for knowledge graphs. Proc. VLDB Endowment 11(9), 975–987 (2018). https://doi.org/10.14778/3213880.3213888 11. Bojanczyk, M.: Transducers of polynomial growth. In: Baier, C., Fisman, D. (eds.) Proc. 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS’22). pp. 1:1–1:27. ACM (2022). https://doi.org/10.1145/3531130.3533326 12. Bojanczyk, M., Doumane, A.: First-order tree-to-tree functions. In: Hermanns, H., Zhang, L., Kobayashi, N., Miller, D. (eds.) Proc. 35th Annual ACM/IEEE

18

A. Ivliev et al.

Symposium on Logic in Computer Science (LICS’20). pp. 252–265. ACM (2020). https://doi.org/10.1145/3373718.3394785 13. Borgwardt, S., Hirsch, A., Kovtunova, A., Wiehr, F.: In the eye of the beholder: Which proofs are best? In: Borgwardt, S., Meyer, T. (eds.) Proc. 33rd Int. Workshop on Description Logics (DL’20). CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020), https://ceur-ws.org/Vol-2663/paper-6.pdf 14. Calautti, M., Livshits, E., Pieris, A., Schneider, M.: The complexity of whyprovenance for datalog queries. Proc. ACM Manag. Data 2(2), 83 (2024). https: //doi.org/10.1145/3651146 15. Calì, A., Gottlob, G., Lukasiewicz, T.: A general Datalog-based framework for tractable query answering over ontologies. J. Web Semant. 14, 57–83 (2012). https: //doi.org/10.1016/j.websem.2012.03.001 16. Carral, D., Dragoste, I., Krötzsch, M.: Tractable query answering for expressive ontologies and existential rules. In: d’Amato, C., Fernández, M., Tamma, V., Lécué, F., Cudré-Mauroux, P., Sequeda, J.F., Lange, C., Heflin, J. (eds.) Proc. 16th Int. Semantic Web Conf. (ISWC’17), Part I. LNCS, vol. 10587, pp. 156–172. Springer (2017). https://doi.org/10.1007/978-3-319-68288-4_10 17. Carral, D., Dragoste, I., Krötzsch, M.: The combined approach to query answering in horn-alchoiq. In: Thielscher, M., Toni, F., Wolter, F. (eds.) Proc. 16th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’18). pp. 339–348. AAAI Press (2018), https://aaai.org/proceeding/kr-16-2018/ 18. Carral, D., Dragoste, I., Krötzsch, M.: Reasoner = logical calculus + rule engine. Künstliche Intell. 34(4), 453–463 (2020). https://doi.org/10.1007/ S13218-020-00667-6 19. Chaudhuri, S., Vardi, M.Y.: On the equivalence of recursive and nonrecursive datalog programs. In: Vardi, M.Y., Kanellakis, P.C. (eds.) Proc. 11th Symposium on Principles of Database Systems (PODS’92). pp. 55–66. ACM Press (1992). https://doi.org/10.1145/137097.137109 20. Courcelle, B.: Monadic second-order definable graph transductions: A survey. Theor. Comput. Sci. 126(1), 53–75 (1994). https://doi.org/10.1016/0304-3975(94) 90268-2 21. Dachselt, R., Gerlach, L., Hanisch, P., Ivliev, A., Krötzsch, M., Marx, M., Méndez, J.: Declarative debugging for datalog with aggregation. In: Krause, A., Pimentel, J.F. (eds.) Proc. Workshops of the EDBT/ICDT 2026 Joint Conf. CEUR WS Proceedings, CEUR-WS (2026), https://ceur-ws.org/Vol-4192/TGD-paper4.pdf 22. Elberfeld, M., Jakoby, A., Tantau, T.: Logspace versions of the theorems of bodlaender and courcelle. In: Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS’10). pp. 143–152. IEEE Computer Society (2010). https://doi.org/10.1109/FOCS.2010.21 23. Elhalawati, A., Krötzsch, M., Mennicke, S.: An existential rule framework for computing why-provenance on-demand for datalog. In: Governatori and Turhan [29], pp. 146–163 24. Engelfriet, J., Maneth, S.: Macro tree transducers, attribute grammars, and MSO definable tree translations. Inf. Comput. 154(1), 34–91 (1999). https://doi.org/10. 1006/INCO.1999.2807 25. Furche, T., Gottlob, G., Grasso, G., Guo, X., Orsi, G., Schallhart, C., Wang, C.: DIADEM: Thousands of websites to a single database. Proc. VLDB Endow. 7(14), 1845–1856 (2014). https://doi.org/10.14778/2733085.2733091 26. Gallot, P., Lhote, N., Nguyên, L.T.D.: The structure of polynomial growth for tree automata/transducers and MSO set queries. CoRR abs/2501.10270 (2025). https://doi.org/10.48550/ARXIV.2501.10270

Recovering Explanations from Transformed Rule-Based Ontologies

19

27. Gécseg, F., Steinby, M.: Tree Automata. Akadéniai Kiadó, Budapest, Hungary (1984) 28. González, L., Ivliev, A., Krötzsch, M., Mennicke, S.: Efficient dependency analysis for rule-based ontologies. In: Sattler, U., Hogan, A., Keet, M., Presutti, V., Almeida, J.P.A., Takeda, H., Monnin, P., Pirrò, G., d’Amato, C. (eds.) Proc. 21st International Semantic Web Conference (ISWC 2022). LNCS, vol. 13489, pp. 267– 283. Springer (October 2022). https://doi.org/10.1007/978-3-031-19433-7_16 29. Governatori, G., Turhan, A. (eds.): Proc. 2nd Int. Joint Conf. on Rules and Reasoning (RuleML+RR’22), LNCS, vol. 13752. Springer (2022) 30. Green, T.J., Karvounarakis, G., Tannen, V.: Provenance semirings. In: Libkin, L. (ed.) Proc. 26th Symp. on Principles of Database Systems (PODS’07). pp. 31–40. ACM (2007). https://doi.org/10.1145/1265530.1265535 31. Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: PCompleteness Theory. Oxford University Press (1995) 32. Hanisch, P., Krötzsch, M.: Rule rewriting revisited: A fresh look at static filtering for Datalog and ASP. In: ten Cate, B., Funk, M. (eds.) Proc. 29th Int. Conf. on Database Theory (ICDT’2026). LIPIcs, vol. 365. Dagstuhl Publishing (2026). https://doi.org/10.4230/LIPIcs.ICDT.2026.5 33. Horridge, M., Parsia, B., Sattler, U.: Laconic and precise justifications in OWL. In: Sheth, A., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T., Thirunarayan, K. (eds.) Proc. 7th Int. Semantic Web Conf. (ISWC’08). LNCS, vol. 5318, pp. 323– 338. Springer (2008) 34. Ivliev, A., Ellmauthaler, S., Gerlach, L., Marx, M., Meißner, M., Meusel, S., Krötzsch, M.: Nemo: First glimpse of a new rule engine. In: Pontelli, E., Costantini, S., Dodaro, C., Gaggl, S.A., Calegari, R., d’Avila Garcez, A.S., Fabiano, F., Mileo, A., Russo, A., Toni, F. (eds.) Proc. 39th Int. Conf. on Logic Programming (ICLP’23). EPTCS, vol. 385, pp. 333–335 (2023). https://doi.org/10.4204/EPTCS.385.35 35. Ivliev, A., Gerlach, L., Meusel, S., Steinberg, J., Krötzsch, M.: Nemo: Your friendly and versatile rule reasoning toolkit. In: Marquis, P., Ortiz, M., Pagnucco, M. (eds.) Proc. 21st Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’24). pp. 743–754. IJCAI Organization (2024). https://doi.org/10.24963/kr. 2024/70 36. Ivliev, A., Krötzsch, M., Marx, M.: Recovering explanations from transformed rulebased ontologies. In: Koubarakis, M., et al. (eds.) Proc. 25th Int. Semantic Web Conf. (ISWC’26). LNCS, Springer (2026), to appear 37. Jordan, H., Scholz, B., Subotic, P.: Soufflé: On synthesis of program analyzers. In: Chaudhuri, S., Farzan, A. (eds.) Proc. 28th Int. Conf. on Computer Aided Verification (CAV’16), Part II. LNCS, vol. 9780, pp. 422–430. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_23 38. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., Choi, K.S., Noy, N., Allemang, D., Lee, K.I., Nixon, L., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., CudréMauroux, P. (eds.) Proc. 6th Int. Semantic Web Conf. (ISWC’07). LNCS, vol. 4825, pp. 267–280. Springer (2007). https://doi.org/10.1007/978-3-540-76298-0_20 39. Krötzsch, M.: Efficient inferencing for OWL EL. In: Janhunen, T., Niemelä, I. (eds.) Proc. 12th European Conf. on Logics in Artificial Intelligence (JELIA’10). LNAI, vol. 6341, pp. 234–246. Springer (2010) 40. Krötzsch, M.: Efficient rule-based inferencing for OWL EL. In: Walsh, T. (ed.) Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11). pp. 2668– 2673. AAAI Press/IJCAI (2011). https://doi.org/10.5591/978-1-57735-516-8/ IJCAI11-444

20

A. Ivliev et al.

41. Krötzsch, M.: Modern Datalog: Concepts, methods, applications. In: Artale, A., Bienvenu, M., García, Y.I., Murlak, F. (eds.) Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). OASIcs, vol. 138. Dagstuhl Publishing (2025). https://doi.org/10.4230/OASIcs.RW.2024/2025.7 42. Krötzsch, M., Thost, V.: Ontologies for knowledge graphs: Breaking the rules. In: Groth, P.T., Simperl, E., Gray, A.J.G., Sabou, M., Krötzsch, M., Lécué, F., Flöck, F., Gil, Y. (eds.) Proc. 15th Int. Semantic Web Conf. (ISWC’16, Part I). LNCS, vol. 9981, pp. 376–392 (2016) 43. Lautemann, C., McKenzie, P., Schwentick, T., Vollmer, H.: The descriptive complexity approach to LOGCFL. J. of Comput. Syst. Sci. 62(4), 629–652 (2001). https://doi.org/10.1006/JCSS.2000.1742 44. Libkin, L.: Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https://doi.org/10.1007/ 978-3-662-07003-1 45. Logica Devs: Logica project webpage (Retrieved 04 Sept 2025), https://logica-web. github.io/ 46. Megiddo, N., Papadimitriou, C.H.: On total functions, existence theorems and computational complexity. Theor. Comput. Sci. 81(2), 317–324 (1991). https:// doi.org/10.1016/0304-3975(91)90200-L 47. Méndez, J., Alrabbaa, C., Koopmann, P., Langner, R., Baader, F., Dachselt, R.: Evonne: A visual tool for explaining reasoning with OWL ontologies and supporting interactive debugging. Comput. Graph. Forum 42(6) (2023). https://doi.org/10. 1111/CGF.14730 48. Méndez, J., Gerlach, L., Wieland, T., Ivliev, A., Krötzsch, M., Dachselt, R.: Evaluating a visual query tracer and builder for learning declarative logic programming. In: Proc. 37th IEEE Conf. on Visualization and Visual Analytics (VIS’26). IEEE (2026), to appear 49. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C. (eds.): OWL 2 Web Ontology Language: Profiles. W3C Recommendation (2009), available at http://www.w3.org/TR/owl2-profiles/ 50. Nenov, Y., Piro, R., Motik, B., Horrocks, I., Wu, Z., Banerjee, J.: RDFox: A highlyscalable RDF store. In: et al., M.A. (ed.) Proc. 14th Int. Semantic Web Conf. (ISWC’15), Part II. LNCS, vol. 9367, pp. 3–20. Springer (2015). https://doi.org/ 10.1007/978-3-319-25010-6_1 51. Pettorossi, A., Proietti, M.: Transformation of logic programs: Foundations and techniques. J. Log. Program. 19/20, 261–320 (1994). https://doi.org/10.1016/ 0743-1066(94)90028-0 52. Piro, R., Nenov, Y., Motik, B., Horrocks, I., Hendler, P., Kimberly, S., Rossman, M.: Semantic technologies for data analysis in health care. In: Groth, P.T., Simperl, E., Gray, A.J.G., Sabou, M., Krötzsch, M., Lécué, F., Flöck, F., Gil, Y. (eds.) Proc. 15th Int. Semantic Web Conf. (ISWC’16, Part II). LNCS, vol. 9982, pp. 400–417 (2016). https://doi.org/10.1007/978-3-319-46547-0_34 53. Ramakrishnan, R., Beeri, C., Krishnamurthy, R.: Optimizing existential datalog queries. In: Edmondson-Yurkanan, C., Yannakakis, M. (eds.) Proc. 7th Symposium on Principles of Database Systems (PODS’88). pp. 89–102. ACM (1988). https: //doi.org/10.1145/308386.308420 54. Ramakrishnan, R., Sagiv, Y., Ullman, J.D., Vardi, M.Y.: Logical query optimization by proff-tree transformation. J. of Comput. Syst. Sci. 47(1), 222–248 (1993). https://doi.org/10.1016/0022-0000(93)90025-R

Recovering Explanations from Transformed Rule-Based Ontologies

21

55. Sagiv, Y.: Optimizing datalog programs. In: Minker, J. (ed.) Foundations of Deductive Databases and Logic Programming, pp. 659–698. Morgan Kaufmann (1988). https://doi.org/10.1016/B978-0-934613-40-8.50021-X 56. Shmueli, O.: Decidability and expressiveness aspects of logic queries. In: Vardi, M.Y. (ed.) Proc. 6th Symposium on Principles of Database Systems (PODS’87). pp. 237–249. ACM (1987). https://doi.org/10.1145/28659.28685 57. Skvortsov, E.S., Xia, Y., Bowers, S., Ludäscher, B.: Logica-TGD: Transforming graph databases logically. In: Boehm, M., Daudjee, K. (eds.) Proc. Workshops of the EDBT/ICDT 2025 Joint Conf. CEUR WS Proceedings, vol. 3946. CEUR-WS (2025), https://ceur-ws.org/Vol-3946/TGD-4.pdf 58. Urbani, J., Jacobs, C., Krötzsch, M.: Column-oriented Datalog materialization for large knowledge graphs. In: Schuurmans, D., Wellman, M.P. (eds.) Proc. 30th AAAI Conf. on Artificial Intelligence (AAAI’16). pp. 258–264. AAAI Press (2016). https://doi.org/10.1609/aaai.v30i1.9993 59. Urbani, J., Piro, R., van Harmelen, F., Bal, H.E.: Hybrid reasoning on OWL RL. Semantic Web 5(6), 423–447 (2014). https://doi.org/10.3233/SW-130120 60. Zhao, D., Subotic, P., Scholz, B.: Debugging large-scale datalog: A scalable provenance evaluation strategy. ACM Trans. Program. Lang. Syst. 42(2), 7:1–7:35 (2020). https://doi.org/10.1145/3379446

22

A

A. Ivliev et al.

Examples of Proof Tree Homomorphisms

In this section, we give further examples of program transformations that can be reversed using proof tree homomorphisms. Let Π1 = ⟨R1 , Pin , Pout ⟩ be a program. We consider several common classes of program transformations that produce a program Π2 = ⟨R2 , Pin , Pout ⟩ with Π2 ⊑ Π1 , and provide proof tree homomorphisms from Π2 to Π1 . A.1

Atom Permutation

A simple program transformation swaps atoms within rule bodies [51]. This has no effect on the derived facts but may affect evaluation order in a reasoner. Formally, an atom permutation is a family {πρ }ρ∈R1 , where πρ : [n] → [n] is a permutation with |ρ| = n for each ρ ∈ R1 , and [n] := {1, . . . , n}. For a rule ρ = H ← B1 , . . . , Bn , we define πρ (ρ) := H ← Bπρ−1 (1) , . . . , Bπρ−1 (n) . The transformed program is Π2 with R2 = {πρ (ρ) | ρ ∈ R1 }. To reverse this transformation, we define, for each πρ (ρ) ∈ R2 , the proof tree template Sπρ (ρ) for the rule πρ (ρ) over Π1 : H ρ

B1

A.2

···

Bn

Rule Unfolding

Rule unfolding replaces a body atom with the body of a rule that derives it, eliminating one level of indirection in the derivation [51]. For a rule ρ and a substitution σ, we write σ(ρ) for the rule obtained by applying σ to each atom. Let r = H ← B1 , . . . , Bn ∈ R1 be a rule and Bk be a body atom of r for some 1 ≤ k ≤ n. Let d = A ← C1 , . . . , Cp ∈ R1 be another rule (with d ̸= r) such that the head of d unifies with Bk via a most general unifier σ. The unfolding of r at position k using d is the rule unfoldr,k (d) := σ H ← B1 , . . . , Bk−1 , C1 , . . . , Cp , Bk+1 , . . . , Bn

(66)

A transformation from Π1 to Π2 is a rule unfolding if for every ρ ∈ R2 , either ρ ∈ R1 holds, or there are r, d ∈ R1 and 1 ≤ k ≤ |r| such that ρ = unfoldr,k (d). To reverse unfolding, consider an unfolded rule ρ′ = unfoldr,k (d). The template Sρ′ reconstructs the original two-step derivation:

Recovering Explanations from Transformed Rule-Based Ontologies

23

σ(H) r

σ(A) d

σ(B1 )

···

σ(Bk−1 )

σ(C1 )

···

σ(Cp )

σ(Bk+1 )

···

σ(Bn )

For rules ρ ∈ R2 ∩ R1 that were not unfolded, the template Sρ is the identity: a root node deriving the head of ρ connected to the leaf nodes that are labelled by the body atoms of ρ.

24

A. Ivliev et al.

B

Examples of MSO Proof Transformations

In this section, we present examples of program transformations that can be reversed using MSO proof transformations. We let Π1 = ⟨R1 , Pin , Pout ⟩ be a program and define program transformations obtaining Π2 = ⟨R2 , Pin , Pout ⟩, which can be reversed by proof transformations from Π2 to Π1 . B.1

Rule Folding

Rule folding replaces multiple rules whose bodies share a common pattern by a single rule that uses an auxiliary predicate [51]. Let c1 , . . . , cn and d1 , . . . , dn be pairwise distinct rules in R1 , and let A and H be atoms and B̄ a list of atoms such that: – head(di ) is unifiable with A using most general unifier σi , – ci = σi (H ← B̄, body(di )), and – the head of every rule r ∈ / {d1 , . . . , dn } is not unifiable with A. The folding of c1 , . . . , cn using d1 , . . . , dn is the rule r := H ← A, B̄. The transformed program Π2 is obtained from Π1 by replacing {c1 , . . . , cn } with {r}. We can reverse this transformation using a 1-dimensional MSO proof transformation with a single component. The idea is to replace the rule r with rule ci if the A was derived by rule di . φdom (x) :=

n ^

¬ ruledi (x)

(67)

i=1

φci (x) := ruler (x) ∧ ∃w. child1 (w, x) ∧ ruledi (w) φρ (x) := ruleρ (x) for ρ ∈ / {c1 , . . . , cn }

(68) (69)

The child formula rewires the children of an r-node, placing the B̄-children first and then the children inherited from the absorbed di -node:
φjchild (x, y) := ¬ ruler (y) ∧ childj (x, y) (70)
∨ ruler (y) ∧ childj+1 (x, y) if 1 ≤ j ≤ |B̄|
φjchild (x, y) := ¬ ruler (y) ∧ childj (x, y) (71)
∨ ruler (y) ∧ ∃w. child1 (w, y) ∧ childj−|B̄| (x, w) if j > |B̄| φjarg (x, d) := argj (x, d) B.2

(72)

Filter Propagation

Filter propagation is a technique that moves filter conditions such as x = 3 through the rules of a program, so that they are checked as early as possible during bottom-up evaluation [32]. Formally, a filter propagation is a mapping f that assigns to each body atom of each rule in R1 a new rule and body position in which it should appear.

Recovering Explanations from Transformed Rule-Based Ontologies

25

That is, f maps atom positions ⟨ρ, i⟩ with ρ ∈ R1 and 1 ≤ i ≤ |ρ| to tuples ⟨ρ′ , j, σ⟩, where ρ′ ∈ R1 , j ≥ 1 and σ is a substitution adapting the variables. Atom positions with f (ρ, i) = ⟨ρ, i, id⟩ are stationary; all others are moved. The transformed program Π2 = ⟨R2 , Pin , Pout ⟩ has, for each ρ′ ∈ R1 , a rule f (ρ′ ) whose head is head(ρ′ ) and whose j-th body atom is σ(bodyi (ρ)) for the unique ⟨ρ, i⟩ with f (ρ, i) = ⟨ρ′ , j, σ⟩. We set R2 := {f (ρ) | ρ ∈ R1 }. Example 6. Consider the program Π1 : ρ1 : r(x, y) ← e(x, y) ρ2 : r(x, y) ← r(x, z), e(z, y)

(74)

ρ3 : out(y) ← r(x, y), x = a

(75)

(73)

The filter x = a at position (ρ3 , 2) is propagated to the base case, yielding: f (ρ1 ) : r(x, y) ← e(x, y), x = a f (ρ2 ) : r(x, y) ← r(x, z), e(z, y) f (ρ3 ) : out(y) ← r(x, y) Here f (ρ3 , 2) = ⟨ρ1 , 2, id⟩ and all other positions are stationary. In a proof tree for Π2 , the filter appears at every base-case leaf; in a proof tree for Π1 , it appears only at the root. An MSO proof transformation from Π2 to Π1 can be defined using a 1dimensional MSO interpretation with a single component. φdom (x) := ⊤ φρ (x) := rulef (ρ) (x) _ φichild (x, y) :=

(76) (77) rulef (ρ) (y) ∧ ∃p. childj (x, p)

f (⟨ρ,i⟩)=⟨ρ′ ,j,σ⟩

∧ rulef (ρ′ ) (p) ∧ p ≤ y j φarg (x, d) := argj (x, d)

(78) (79)

The domain formula retains all nodes and the rule formula recovers the original rule name. The argument formula is inherited directly, since filter propagation does not change rule heads. The child formula links a filter that has been pushed down in the tree to its original ancestor. B.3

Projection Pushing

Projection pushing removes argument positions in predicates such that the output of the program is unaffected [53]. Formally, let Π1 = ⟨R1 , Pin , Pout ⟩ be a program. A position elimination assigns to each IDB predicate p a set of retained positions U (p) ⊆ {1, . . . , ar(p)} such that all positions of output and input predicates are retained. For an

26

A. Ivliev et al.

atom p(t1 , . . . , tm ), we write p|U (t1 , . . . , tm ) for the atom p′ (tj1 , . . . , tjk ) where U (p) = {j1 < · · · < jk } and p′ is a fresh predicate of arity k. For a rule ρ = H ← B1 , . . . , Bn , the reduced rule is ρ|U := H|U ← B1 |U , . . . , Bn |U

(80)

provided ρ|U is safe. The transformed program is Π2 = ⟨R2 , Pin , Pout ⟩ with rule set R2 = {ρ|U | ρ ∈ R1 }. Example 7. Consider the program Π1 computing the transitive closure of e: r(x, y) ← e(x, y) r(x, y) ← r(x, z), e(z, y) out(y) ← r(x, y) If we are only interested in the output predicate out, the first position of r can be eliminated. Setting U (r) = {2} yields Π2 : r′ (y) ← e(x, y) r′ (y) ← r′ (z), e(z, y) out(y) ← r′ (y) This transformation can be reversed using a 1-dimensional MSO interpretation with a single component. The tree structure is preserved and the rule labelling recovers the original rule from the reduced one for each ρ ∈ R1 : φdom (x) := ⊤

(81)

φichild (x, y) := childi (x, y)

(82)

φρ (x) := ruleρ|U (x)

(83)

Defining the argument formula is a bit more involved. For retained positions, the argument value is read directly from the reduced representation. For eliminated positions, we trace the value downward through the tree. Fix a rule ρ ∈ R1 with head predicate p and let j ∈ / U (p) be an eliminated position. Let xj denote the variable at position j in head(ρ). By safety, xj occurs in at least one body atom of ρ. For each body atom bodyi (ρ) with predicate q in which xj occurs at position j ′ , exactly one of the following holds: 1. q is an input predicate, or j ′ ∈ U (q): the value can be read at the i-th child of x. 2. q is an IDB predicate and j ′ ∈ / U (q): position j ′ is itself eliminated, and we must recurse at the i-th child. To encode this recursive computation, we define a fixed finite graph that captures how variable bindings propagate through rules. The predicate position graph of Π1 is the labelled directed graph GΠ whose vertices are predicateposition pairs ⟨p, j⟩ with p a predicate and 1 ≤ j ≤ ar(p). It contains an edge

Recovering Explanations from Transformed Rule-Based Ontologies

27

⟨p, j⟩ → ⟨q, j ′ ⟩ labelled ⟨ρ, i⟩ whenever ρ ∈ R1 has head predicate p, the variable at position j in head(ρ) also appears at position j ′ in bodyi (ρ), and that body atom has predicate q. A vertex ⟨q, j ′ ⟩ is terminal if q ∈ Pin or j ′ ∈ U (q). The MSO formula Φp,j (x, d) quantifies over a downward path in the proof tree together with a run of GΠ along that path. For each vertex ⟨q, j ′ ⟩ of GΠ , we introduce a monadic variable Xq,j ′ representing the set of tree nodes on the path that are visited in graph node ⟨q, j ′ ⟩. Let V (GΠ ) be the set of vertices in GΠ and let X̄q,j ′ be a list of monadic second-order variables Xq,j ′ for each vertex ⟨q, j ′ ⟩ in GΠ .  Φp,j (x, d) := ∃X̄q,j ′ . ∃y.

x ∈ Xp,j ∧ ∀v.



^

v ∈ Xq,j ′ ⇒

⟨q,j ′ ⟩∈V (GΠ )

 ruler|U (v) ∧ ∃w. childi (w, v)

_ ′

′

(84)

′′

⟨q,j ⟩→⟨q ,j ⟩ labelled ⟨r,i⟩

( ∧

w = y ∧ argj ′′ (y, d) w ∈ Xq′ ,j ′′

if ⟨q ′ , j ′′ ⟩ terminal otherwise

!

At the start, node x is in state ⟨p, j⟩. At each step, a node v in state ⟨q, j ′ ⟩ picks an edge ⟨q, j ′ ⟩ → ⟨q ′ , j ′′ ⟩ labelled ⟨ρ, i⟩, verifies that v uses rule ρ|U , and descends to child i. If ⟨q ′ , j ′′ ⟩ is terminal, the value d is read at position j ′′ of that child. Otherwise, the child enters state ⟨q ′ , j ′′ ⟩ and the process continues. The argument formula distinguishes retained and eliminated positions: ( _ argj ′ (x, d) if j ∈ U (p) j φarg (x, d) := ruler|U (x) ∧ (85) Φp,j (x, d) if j ∈ / U (p) r∈R 1

head pred. p

where j ′ = |{k ∈ U (p) | k ≤ j}| is the position of j in the reduced predicate. For retained positions, the value is read directly from the reduced representation (adjusting for the change in indexing). For eliminated positions, the value is recovered via Φp,j .

Related documents

• Specification Oracles#1071205
• Credo: Reusable Declarative Primitives for Agentic Workflows#618647
• Subsumption in $\mathcal{FL}_{\bot \mathit{reg}}$ with TBoxes Is in ExpTime#1123087
• Against idiosyncrasy in ontology development#768804
• From Interpretation to Compilation: A Compilation-Based Execution Engine for Semantic Operator Systems#440455