We propose summary proof trees as a way for explaining derivations in Datalog programs with aggregation. These combine structurally similar parts of proof trees into a single, easier to understand structure. We show how to query for such summaries, discuss the implementation in our rule engine Nemo, and empirically establish the feasibility of the method. We also briefly introduce a graphical interface for editing these proof queries and visualising the results.
As rule systems have matured to support large graphs (e.g., >100M edges on a laptop, >8B edges on a
server [5]), an important open challenge remains explainability of results. In spite of their declarative
(
In this paper, we therefore develop a new approach for explaining results of Datalog with (stratified) aggregates, and a prototype implementation that illustrates its feasibility. After clarifying preliminaries on Datalog with aggregates (Section 2), the starting point of our work is an extended notion of proof tree, or rather proof graph, which includes witnesses for all elements in sets over which aggregates have been computed (Section 3). This proof graph might be overwhelmingly huge, so we develop ways to select and summarise relevant content (Section 4). The main idea is to combine many individual proofs into a single tree structure that shows their common structure and has sets of inferences at each node. We define two types of queries for summarising proof graphs: type 1 queries start from a set of inferences and find their maximal common proof structures, and type 2 queries start from a given proof structure and find inferences that were produced in this way.
These queries form the basis of a prototype implementation for interactive proof graph exploration, which we develop by extending the Nemo graph rule engine [5]. Our algorithmic approach is explained in Section 5 and evaluated for (proof) query answering performance in Section 6. We finish with a brief overview of how this backend functionality is then used in an interactive user interface (Section 7), which can also be explored online at https://tools.iccl.inf.tu-dresden.de/nemo/tgd-2026.
All of our tools are free and open source (see https://github.com/knowsys/nemo, https://github.com/ knowsys/nemo-web, and https://github.com/imldresden/nev).
We start by introducing the syntax and semantics of the extension of Datalog that we consider in this work. A more gentle introduction can be found in recent literature [1].
Syntax We consider countably infinite, mutually disjoint sets of predicates P, constants C, and variables V, where C contains all integer numbers (and possibly more).1 A term is a constant or a variable, i.e., ∈ C ∪ V. Every predicate symbol ∈ P has an arity ar() ∈ N (possibly 0).
An atom has the form (1, . . . , ℓ) for predicate ∈ P and terms 1, . . . , ℓ with ℓ = ar(). List of terms are denoted in bold, e.g., = 1, . . . , ||, so we may write the previous atom as (). Similarly, , , etc. denote lists of variables. We treat lists as sets when order is irrelevant. A logical expression is ground if it does not contain variables.
Our syntax for aggregation is inspired by ASP engines like Clingo [19]. We consider the set of aggregation functions F = {COUNT, MAX, MIN, SUM} – further aggregates can easily be added without afecting our results. An aggregation atom is an expression of the form where ∈ V is the result variable, ⊆ C ∪ V a list of terms, ∈ F an aggregation function, and 1, . . . , ℓ a list of atoms, known as side conditions. The part in {. . .} is the aggregation set expression. A rule is of the form
= { : 1, . . . , ℓ}, ←
1, . . . , , 1, . . . , ,
1We adopt a weak typing approach where constants of diferent datatypes are part of a joint domain, as is typical for schema-less
graph languages like RDF.
(
Example 2. We extend Example 1 with the following rule that finds parents with multiple children (mC): mC() ← par(, ), = COUNT{ : par(, )}, ≥ 2 Here, the aggregation atom = COUNT{ : par(, )} counts the number of children for each parent , and stores it in the result variable . The set of outer variables is {, , }.
A program is a finite set of rules that is stratified in the following sense. There is a mapping
: P → N such that, for every rule ∈ of the form (
Any such partitions into disjoint strata, where the stratum for ∈ N is = {() ← ℬ ∈
() = }.
|
Semantics Variable-free (ground) atoms are also called facts, and a database is a finite set of facts.
Programs are evaluated over databases to obtain newly inferred facts as output.2 Aggregation functions
are applied to sets of tuples. Let ⊆ C be a set of -tuples of constants. We associate the following
partial function ⋃︀≥ 1 C → C with each aggregation function:
(
SUM() = ∑︀⟨,2,...,⟩∈,∈N
COUNT() = ||
Lines (
An assignment for a rule maps variables in to constants () ∈ C. For a list of terms , let
(⟨1, . . . , ⟩) = ⟨ (1), . . . , ()⟩ where () = if does not contain in its domain. We extend
this notation to (aggregation) atoms. Given an atom (), we set (()) = ( ()). Let be an
aggregation atom of form (
A rule is applicable over a given database if it has a match, defined next. Given an assignment for and an aggregation atom = { : 1, . . . , ℓ} in , we write { : 1, . . . , ℓ} for the set of all tuples of the form ′() where the ′ is an extension of to all variables in 1, . . . , ℓ such that 2In some contexts, it is useful to designate input and output predicates that define the intended “interface” of a program [ 1], but this is not relevant to our present work. ′() ∈ for all ∈ {1, . . . , ℓ}. In other words, ℰ is the set to which the aggregation set expression ℰ evaluates under the given bindings for outer variables. Let be an assignment for whose domain is exactly the set of outer variables of . Then is a match for over if, for every: 1. body atom of , () ∈ , and 2. aggregation atom = {ℰ } of , () = (ℰ ).
Note that condition 2 requires to be defined for ℰ .
A rule with head is applicable to if it has a match over and () ∈/ . The application of under then results in ∪ { ()}.
A program is evaluated based on some stratification . We assume without loss of generality that the non-empty strata of are exactly 1, . . . , ℓ. Let 0∞ = . For = 0, . . . , ℓ − 1, let ∞+1 be the database resulting in an arbitrary maximal sequence of applications of rules in +1 starting from ∞. The result () of over is () = ℓ∞. It is a standard fact in logic programming (and easy to verify) that (a) every ∞ is finite, (b) +1 does not depend on the order of rule applications, and (c) ∞ () does not depend on the chosen stratification.
Negation and Builtins It is not hard to extend our syntax and semantics to support builtin predicates for which defining facts are assumed given without being specified in the database. For example, a unary predicate · =0 can be defined by the single fact · =0(0) (we would usually prefer infix notation, as in = 0). There can also be infinite builtins, such as the binary <; in Datalog extensions, variables that occur with such infinite builtins are typically required to also occur in regular (finite) body atoms [1].
Using just a single finite builtin · = 0, we can express (stratified) negation. Indeed, a negated atom ¬() can be rewritten into two atoms = COUNT{ : ()} and = 0, where is a fresh variable. We allow to contain variables that are not used anywhere else: they are “inner” variables in the side condition, interpreted existentially. This is also how rule engines like Nemo and Clingo interpret such variables in negated atoms.
Every fact that is produced by a program over a database has at least one proof, which we will now define more concretely. The structure of proofs contains valuable information for explaining results, debugging programs, and certifying correctness [20]. While proof trees (or derivation trees) are common in logic programming, we must extend them here to cover aggregation. Moreover, we now consider directed acyclic graphs instead of mere trees, leading to a compact representation of proofs for all inferred facts.
To clarify the role of facts as preconditions of specific rule applications, we refer to specific body
atoms in rules: a body atom position is a pair ⟨, ⟩ where is a rule as in (
⟨ = COUNT{ : par(, )}, 1⟩
conditions, a side condition atom position is a pair ⟨, ⟩ with 1 ≤ ≤ ℓ. The set of all atom positions
(of either kind) of a program is denoted APos( ). To denote information about how aggregation
atoms were evaluated, we introduce evaluated aggregation atoms of the form = { : 1, . . . , ℓ}
where ∈ C and all other pieces are as in (
A derivation graph = ⟨, , ⟩ for program is a directed acyclic graph with the • vertex set , where each ∈ is either a ground atom (), an evaluated aggregation atom = {ℰ }, or an expression ∈ {ℰ } with a list of constants and ℰ an aggregation set expression, • edge set ⊆ × , and • edge labelling function : → APos( ) ∪ {*} .
Intuitively, each node of the derivation graph represents a derivation result, and its children represent
the data that it was derived from. For regular ground atoms, these will be the instantiated body atoms
of the relevant rule application (edges labelled by body atom position); for evaluated aggregation atoms,
they will be expressions ∈ {ℰ } for all elements of the evaluated aggregation set expression (edges
labelled by * ); and for expressions ∈ {ℰ }, they will be the instantiated atoms of the relevant side
conditions (edges labelled by side condition atom position). Figure 1 and Figure 2 show examples of
derivation graphs for Example 1 and Example 2, respectively. Note that kin(, ) has two diferent
proofs in Figure 1 (either by applying rule (
Definition 2. Consider a rule that was applied to a database using a match . The proof graph for this rule application is the derivation graph that contains exactly the following labelled edges (and associated vertices):
(A) if is the th (aggregation or regular) body atom of , and is the head of , then contains the edge
() →−⟨,⟩ (), where () denotes the expression obtained from by replacing each (necessarily outer) variable by ().
(B) if is an aggregation atom of form (
∈ { (ℰ )} →−* ().
Moreover, if ′ is the extension of that was used to establish ∈ ℰ ,3 then contains the edges for each ∈ {1, . . . , ℓ}.
Definition 3. The proof graph for a sequence of rule applications of a program starting from a database is the union of the proof graphs of all individual rule applications in the sequence.
Since rule application sequences are restricted to use previously derived facts, and since stratification ensures that any aggregation atom is only evaluated over side conditions of lower strata, we immediately get the following.
Proposition 1. The proof graph of any sequence of rule applications is a derivation graph, and in particular it is acyclic.
Example 3. Recall the rule for finding parents with multiple children from Example 2:
On the database from Example 1, consider the assignment with ↦→ , ↦→ , and ↦→ 2. We
ifnd extensions ′ with ′() = and ′′ with ′′() = of that witness {, } ⊆ { : par(, )} .
Indeed, these are the only two extensions, and thus is a match for rule (
In this section, we introduce conceptual means for users to select and summarise parts of proof graphs, which will form the basic backend operations in our implementation.
A proof graph for a maximal chain of rule applications ofers a complete account of all derivations in (), but it is very hard to inspect for real-world graph databases with millions of edges. Indeed, even a proof graph with a few hundred nodes can be hard to navigate or display. For structural simplification, we can “unravel” the directed acyclic graph into a tree if we recursively replace vertices with several outgoing edges by multiple nodes that each have one outgoing (parent) edge. After this operation, the proof graph is a disjoint union of trees, one for each fact in () that was not used in any rule application, and we might well allow users to select one such tree or a subtree of it (starting at a fact of interest). This is the classical “proof tree” view, extended with aggregates.
This classical view, however, neglects the set-based nature of rule-based computation and hides any regularities that emerge from this. Indeed, thousands of facts might be derived in exactly the same way, merely starting from diferent inputs, but viewing a thousand trees individually to compare them is not feasible. We therefore propose a summary proof tree that combines many (unravelled) proof trees with a similar structure. Nodes in such trees then are labelled by sets of vertices that occur in similar positions in the overall proof graph.
Definition 4. Let = ⟨, , ⟩ be a proof graph for a program . A summary proof tree ⟨, , , ⟩ for is given by a set of nodes, a set ⊆ × of edges that form a tree, a node labelling function : → 2 , and an edge labelling function : → APos( ) ∪ {*} , where we require that all edges that lead to the same parent node have mutually distinct edge labels.
The requirement of distinct edge labels is diferent from proof graphs, where evaluated aggregate atoms may have many children with the same label * . Merging these children into one set helps us to combine proof trees, as defined next. Figure 3 depicts the corresponding summary proof tree for the proof graph in Figure 2. 3Like for rule applications, we assume that every tuple considered in an aggregation was found in exactly one way, even if other ways might exist. This assumption is needed to obtain a unique proof. ∈ { : par(, )}, ∈ { : par(, )} ⟨ = COUNT{ : par(, )}, 1⟩ par(, ), par(, ) kin(, ), kin(, ) Definition 5. Let = ⟨, , ⟩ be a proof graph. For a vertex ∈ , let in-labels() = { (⟨, ⟩) | ⟨, ⟩ ∈ } and children(, ) = { | ⟨, ⟩ ∈ , (⟨, ⟩) = } for a label .
Given ⊆ , the summary proof tree for , denoted ( ), is defined recursively as follows: • The root of ( ) is a node with label () = . • If in-labels() is the same set for all ∈ , then, for every ∈ in-labels(), there is an edge →− such that is the root of a summary proof tree for ⋃︀∈ children(, ).
Intuitively, the summary proof tree determines the maximal common upper portion of the proof trees for the elements of , labelling each node by the set of all vertices that the individual proof trees use in this position. For sets of ground facts , the requirement of uniform in-labels() is satisfied exactly if the same rule was applied to derive all facts in (for sets of vertices from aggregation atoms or aggregated tuples, the requirement always holds). If no aggregates are used, the summary proof tree of a singleton set {()} corresponds to the classical proof tree for (). If present, however, the * -children of aggregate atoms are combined into a single node with a set of labels, whose children correspond to the aggregate’s side conditions, which in turn might have been derived in more than one way.
Definition 5 provides a powerful way to discover similarities in proof structures for many facts. Conversely, it is also useful to start from a proof structure of interest and find all the facts that were derived in a similar way.
Definition 6. Let = ⟨, , ⟩ be a proof graph. A summary tree query = ⟨, , , ⟩ has the same form as a summary proof tree (Definition 4), but with an additional possible value ⊤ (“no restriction”) for node labels.
Let ∈ be a vertex and ({}) = ⟨, , , ⟩ its summary proof tree. Then structurally matches if there is a mapping : → such that (a) the root of is mapped to the root of ({}); (b) if ⟨, ⟩ ∈ , then (⟨, ⟩) = (⟨ (), ()⟩); and (c) for every ∈ , either () = ⊤ or ( ()) ⊆ ().
Let be the set of all vertices of that structurally match . The result of over proof graph , denoted ℛ(), is obtained from the summary proof tree ( ) by deleting all nodes for which there is no corresponding node in .
In other words, ℛ() always has the same tree structure and edge labels as , but possibly diferent node labels, which are subsets of the upper bounds given in .
Example 4. Consider the program from Example 1. The summary proof tree ( ) for = {kin(, ), kin(, )}
is shown in Figure 4. Starting with = {kin(, ), kin(, )} instead would result in a tree containing
only the root node with label , since kin(, ) is derived from rule (
Now consider the summary tree query that is shown in Figure 5 with the same structure. The left child of the root is labelled by kin(, ), so only kin(, ) structurally matches the query, but not kin(, ). Therefore, the answer ℛ() only contains facts relevant for the derivation of kin(, ).
We refer to the queries of Definition 5 (based on vertex set ) as type 1 queries (T1), whereas those of Definition 6 (based on summary tree query ) are type 2 queries (T2). Together, they provide the two main ways for users to interact with proofs in our approach. It is important to note that answers for both query types are based on the concrete matches used during program evaluation, rather than all possible derivations of a fact. As a result, a query might have no answer even though other sequences of rule applications could have produced one.
Type 1 queries can be answered in a straightforward way by considering the summary proof trees for each fact in and merging them until they diverge. In the following, we therefore focus on the implementation of type 2 queries.
In this section, we show how to answer summary tree queries using Datalog programs. We also discuss how to extend this to language features provided by modern rule engines, and describe our own implementation in Nemo [5].
Modern engines usually implement a semi-naive evaluation strategy for Datalog that applies a given
rule to all matches without a corresponding head fact in a single step. We split a predicate into
predicates , grouping all -facts by the step in which they were derived. We also assume auxiliary
tables , for each aggregation atom of the form (
For the summary tree query = ⟨, , , ⟩, we use, for each node ∈ and derivation step , predicates (containing all facts satisfying the constraints imposed by the subtree rooted at ), (containing, for each fact in , an assignment of the outer variables witnessing the derivation for this fact) and (for the resulting node label of ). We write < for ⋃︀< (and similarly abbreviate ,< ). For node ∈ , we set to be all -facts in () if () ̸= ⊤, and to be the set of all derived -facts otherwise.
For the bottom-up phase, we first consider node with in-labels() only containing atom positions
for rule = ← 1, . . . , , 1, . . . , and child vertices for each body atom (1 ≤ ≤ ).
Let ℓ be a leaf node with associated predicate ℓ. We use the following rules, where (x, y) specifies
some arbitrary, but fixed map from x (outer variables occurring in the rule head) to y (outer variables
not occurring in the rule head). We write 1, 2 ← ℬ as an abbreviation for the two rules 1 ← ℬ
and 2 ← ℬ .
(
We extend the theoretical approach to all language features used in Nemo, including existential rules
and arithmetic operations. The latter are evaluated in the bottom-up phase as they would be during
rule applications. Existential rules extend Datalog with existentially quantified variables in rule heads.
Nemo uses the restricted chase [21] to evaluate such rules. The algorithm already supports such rules.
To avoid a Cartesian product in rule (
(x), <+1(x, y), <+1(x, y)
For aggregation, we consider vertices with an outgoing edge labelled by ⟨, ⟩ referring to aggregation atom . Let be the unique child with →− * and 1, . . . , be the child nodes of . We add the following rules: The rules for the top-down phase are as follows, where is the total number of derivation steps and is the root of :
mean max mean max
Tracing Matching in-labels() contains only body atom positions for rule with head atom that does not occur as the head atom of another rule, and all children of are also simple. If is simple and in-labels() only has body atom positions for rule such that all outer variables of occur in the head of , we have (x) = (x) = (x).
This section presents an evaluation of our approach. We demonstrate that (a) the proposed implementation outperforms a naive solution based on Nemo’s existing tracing functionality, and (b) the proposed implementation achieves performance suficient for real-time applications.
We base our performance evaluation on the benchmarks used by Ivliev et al. [5] that are publicly available.4 We replace LUBM-01k with LUBM-100 due to memory restrictions. The first section of Table 1 lists all the considered benchmarks together with the number of rules and the number of derived facts for each rule set. Galen is a Datalog implementation of EL-reasoning run on a medical ontology [22], while the rest are commonly used benchmarks for existential rules [21].
To generate the queries, we compute summary proof trees for a randomly chosen subset of all derived facts and construct the queries by omitting the fact restrictions. We limit the experiments to 1,000 queries per rule set. The second section of Table 1 shows the average node count of the generated queries and the amount of queries per rule set. With 16 nodes on average, Galen has large queries, while the other data sets average query sizes between 2 and 4.
We further compare our approach with a naive baseline implementation that uses the existing tracing implementation of Nemo. To answer proof queries, we first compute the proof trees for all derived facts. Note that Nemo optimises the computation of multiple traces by reusing previously computed results. We then match each proof tree to the provided query.
The runtime measurements for each experiment are repeated three times. Between each run, the state of the database was reset. All experiments were conducted on consumer hardware using a machine
with an AMD Ryzen 5900X CPU and 32 GB of RAM. The individual measurements are provided in the supplementary material.5 For the baseline experiments, we set a timeout (t.o.) of 10 minutes.
The third section of Table 1 shows the performance of our implementation, including the average number of answers per query, the average runtime in milliseconds, along with the percentage of queries answered in less than 1s and less than 5s, which we classify as "fast" and "acceptable" from a user perspective, respectively. The last section displays the average runtimes for the baseline implementation in milliseconds, divided into the time for computing the proof trees for all facts (Tracing) and the time for matching each proof tree against the query (Matching). Comparing our approach with the baseline, we notice a significant improvement. For Doctors-1M and Deep-100, our implementation achieves a speedup of approximately two orders of magnitude. For the remaining cases, the baseline implementation reaches the 10-minute timeout, whereas our implementation completes in under 5 seconds for the majority of instances. The baseline’s performance scales with the number of derived facts, making it infeasible for most of the rule sets evaluated here.
We now discuss the diferences in the runtimes for our implementation. For the existential rules benchmarks, all queries, except one in Doctors-1m and three in LUBM-100, can be evaluated in under 1s. For Galen, 58% of requests can be answered in under 1s, and 91% of requests in under 5s. We attribute the diferences in performance to two main factors. First, facts derived in the Galen benchmarks usually have large proof trees, which naturally increases the time required to answer the corresponding proof queries. Second, within the existential rules benchmarks, the derived facts are approximately evenly distributed across the possible proof query shapes (see supplementary material). This makes the queries more selective, so that fewer facts need to be considered during computation. Meanwhile, in Galen, we observe an uneven distribution, such that most inferences may be recomputed during the bottom-up phase.
Overall, we conclude that our prototype implementation is capable of answering complex queries for large-scale reasoning tasks eficiently in the majority of the cases, while improving significantly over the baseline implementation.
The web version of Nemo [5] integrates a visualisation tool called nev (Nemo Explain Visualizer6, inspired by pev2 [23]) that supports analysis and creation of T1 and T2 queries.
T1 queries function as nev’s entry point for building a query. The resulting summary proof tree can be manipulated by, e.g., adding or removing rules to issue T2 queries, which updates the facts in each tree node accordingly. 5https://github.com/knowsys/nemo-examples/tree/main/evaluations/tgd2026 6https://tools.iccl.inf.tu-dresden.de/nemo/tgd-2026
A T1 query initialising nev can be issued by clicking the magnifying glass next to a row in one of Nemo’s result tables. Then, a T2 query with the same tree shape can be issued with the “unrestrict” button. Also, one can manipulate the current tree shape by, e.g., adding or removing rules. Any such operation will trigger a summary tree query and update the node’s contents accordingly. Thus, arbitrary tree queries can be constructed.
In Figure 6, we present Example 2 in Nemo. Since Nemo’s syntax for aggregates is diferent from what we introduce in our theoretical considerations, we are forced to introduce an auxiliary rule for the aggregate storing the number of children for each parent on a new relation parCount. We can then trace the fact mC() in nev as can be seen in Figure 7. This shows a tree resembling Figure 3.
We present summary proof trees as a means to explain derivations (i.e., traces) of Datalog programs with aggregates. To navigate these potentially large structures, we also introduce summary tree queries, which overlay multiple partial derivations to allow the inspection of all derivations with a common shape. We enhance the reasoning engine Nemo with the capability of answering such queries and evaluate the feasibility of the approach using standard benchmarks. Furthermore, we show nev as a visualization tool for summary proof trees and as an interactive builder for summary tree queries.
An important direction for future work is the explanation of the absence of facts, which is a common use case for debugging Datalog programs. There exist semi-automated methods that explain missing facts by guiding users to select relevant rules and then to continue from the resulting partial instantiation of the rule [18]. Adapting such techniques to our setting raises several challenges. For one, aggregation introduces additional forms of failure (e.g., empty aggregation, or the aggreagation result fails to meet a condition). Second, it would be interesting to investigate how summary proof trees can be used to explain missing facts.
Finally, we plan to conduct a user study to validate the utility of having such explanatory features for the end user.
This work is funded by Deutsche Forschungsgemeinschaft (DFG) under Germany’s Excellence Strategy: EXC 2050/2, 390696704 – “Centre for Tactile Internet” (CeTI); by DFG grant 389792660 as part of TRR 248 – CPEC; by Bundesministerium für Bildung und Forschung (BMBF) and Saxon State Ministry for Science, Culture and Tourism (SMWK) in Center for Scalable Data Analytics and Artificial Intelligence (ScaDS.AI, SCADS22B); and by BMBF and German Academic Exchange Service (DAAD) in project 57616814 (SECAI, School of Embedded and Composite AI).
in: H. Kangassalo (Ed.), Proc. 9th Int. Conf. Entity-Relationship Approach (ER’09), ER Institute, 1990, pp. 189–203. [14] T. Arora, R. Ramakrishnan, W. G. Roth, P. Seshadri, D. Srivastava, Explaining program execution in deductive systems, in: S. Ceri, K. Tanaka, S. Tsur (Eds.), Proc. 3rd Int. Conf. Deductive and Object-Oriented Databases (DOOD’93), volume 760 of LNCS, Springer, 1993, pp. 101–119. doi:10. 1007/3-540-57530-8_7. [15] R. Caballero, Y. García-Ruiz, F. Sáenz-Pérez, A theoretical framework for the declarative debugging of Datalog programs, in: K. Schewe, B. Thalheim (Eds.), Proc. 3rd Int. Workshop on Semantics in Data and Knowledge Bases (SDKB’08), volume 4925 of LNCS, Springer, 2008, pp. 143–159. doi:10.1007/978-3-540-88594-8_8. [16] S. Köhler, B. Ludäscher, Y. Smaragdakis, Declarative datalog debugging for mere mortals, in: P. Barceló, R. Pichler (Eds.), Proc. 2nd Int. Workshop on Datalog in Academia and Industry (Datalog 2.0’12), volume 7494 of LNCS, Springer, 2012, pp. 111–122. doi:10.1007/978-3-642-32925-8_ 12. [17] A. Elhalawati, M. Krötzsch, S. Mennicke, An existential rule framework for computing whyprovenance on-demand for datalog, in: G. Governatori, A. Turhan (Eds.), Proc. 2nd Int. Joint Conf. on Rules and Reasoning (RuleML+RR’22), volume 13752 of LNCS, Springer, 2022, pp. 146–163. doi:10.1007/978-3-031-21541-4_10. [18] D. Zhao, P. Subotić, B. Scholz, Debugging large-scale Datalog: A scalable provenance evaluation strategy, ACM Trans. Program. Lang. Syst. 42 (2020). doi:10.1145/3379446. [19] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub, Multi-shot ASP solving with clingo, Theory
Pract. Log. Program. 19 (2019) 27–82. doi:10.1017/S1471068418000054. [20] J. Tantow, L. Gerlach, S. Mennicke, M. Krötzsch, Verifying datalog reasoning with Lean, in: Y. Forster, C. Keller (Eds.), Proc. 16th Int. Conf. Interactive Theorem Proving (ITP’25), volume 352 of LIPIcs, Dagstuhl Publishing, 2025. doi:10.4230/LIPICS.ITP.2025.36. [21] M. Benedikt, G. Konstantinidis, G. Mecca, B. Motik, P. Papotti, D. Santoro, E. Tsamoura, Benchmarking the chase, in: Proc. 36th Symp. on Principles of Database Systems (PODS’17), ACM, 2017, pp. 37–52. doi:10.1145/3034786.3034796. [22] Y. Kazakov, M. Krötzsch, F. Simančík, The incredible ELK: From polynomial procedures to eficient reasoning with ℰℒ ontologies, J. of Automated Reasoning 53 (2013) 1–61. doi:10.1007/ S10817-013-9296-3. [23] Dalibo, Pev2, https://github.com/dalibo/pev2, 2025. Accessed: 2025-07-01.