Justifications are a very useful tool for explaining DL consequences. They highlight parts of the ontology that are responsible for the consequence, and can serve as the basis for more detailed explanations such as proofs. In this paper, we present an approach that can compute ABox justifications, i.e., justifications restricted to assertions, for answers to conjunctive queries, assuming that these queries are Datalogrewritable over the input ontology. We implemented the approach based on the rewriting tool Clipper and ProvSQL, which can be used to compute provenance information, including justifications, for SQL queries. The potentially recursive nature of Datalog rewritings does not allow a direct translation into SQL queries, but requires some additional processing steps, depending on the cyclic structure of the Datalog program and the ABox. We show that the set of all ABox justifications can be computed in reasonable time, and compare the performance with Souflé, a Datalog engine that also supports explanations.
Despite the reputation of description logics and other logic-based formalisms of supporting
the inspection and understanding of large and complex domain knowledge, sometimes DL
entailments are far from understandable by themselves. For this reason, research on explanation
approaches for DLs already has a long history. Justifications , which point out the responsible
axioms, are the most popular tool and often enough to understand a given entailment [
Related areas of research include provenance for databases [
In this paper, we consider a type of justifications for conjunctive query answering in
Datalogrewritable description logics. We report on an implementation that combines the Datalog
rewritings computed by Clipper, which supports Horn-ℋℐ ontologies [
The runtime of this approach is substantially larger than what is required for query answering
in the first place, which is mainly due to ProvSQL computing the provenance for all query
answers at once. In practice, we expect that such explanations are usually only computed
upon request by a user, and only for single answers at a time. We compare the performance of
our approach with Souflé, a Datalog engine that supports proofs for query atoms [
We assume that the reader is familiar with the basics of DLs [
ℎ :– 1, 2, . . . , where ≥ 0, ℎ, 1, . . . , are atoms, ℎ is the head of the rule, and the conjunction of 1, 2, . . . , is the body of the rule. The predicate in the rule head depends on each predicate occurring in the body. A program is recursive if the transitive closure of the “depends on”-relation is cyclic.
A conjunctive query (CQ) is a first-order formula of the form (⃗) = ∃⃗.(⃗, ⃗), where is a
conjunction of concept and role atoms using the variables in ⃗ and ⃗. The variables in ⃗ are the
answer variables of . An answer to over an ontology (, ) with ABox and TBox is a
|⃗|-tuple ⃗ of individual names from such that every model of (, ) satisfies (⃗) under the
usual semantics of first-order logic (written , |= (⃗)). A Datalog rewriting of w.r.t. is a
tuple (, , ), where , is a Datalog program with the |⃗|-ary query predicate , such that,
for all ABoxes over the signature of and , it holds that , |= (⃗) if ∪ , |= (⃗).
Clipper is a tool that can compute Datalog rewritings for arbitrary CQs and TBoxes formulated
in Horn-ℋℐ [
Example 1. In a scenario where a human operator oversees a collection of drones, each drone can be connected to an individual describing its surroundings via the role environment. Since sensor readings are often imperfect, the description can contain additional confidence information. Consider a CQ () = ∃. environment(, ) ∧ LowVisiblity() ∧ HighConfidence() over a TBox
The query returns a set of individuals (drones) that are likely in a low-visibility environment. The ontology additionally specifies that rain decreases visibility and, if a drone is wet, it is likely raining. A Datalog rewriting of the query and ontology could look as follows.
An ABox justification for a query answer , |= (⃗) is a minimal subset ⊆ for
which , |= (⃗) holds. Using a Datalog rewriting (, , ), this can be reformulated to
∪ , |= (⃗). The latter problem can be solved in the closed-world setting of databases,
and therefore we will apply database provenance computation to solve it. The why-provenance
for a database query answer |= (⃗) is the set of all minimal subsets of that yield the same
answer. ProvSQL is a plugin for the Postgres relational database system [
In the setting of ontology-based data access, databases often come equipped with so-called
mappings that associate data from the data sources with concepts in the ontology. In particular,
they can define unary and binary relations in terms of SQL queries over an input database that
may contain tables with more than two attributes. This type of mappings is usually referred to
as global-as-view [
In this paper, we assume these mappings to be pre-materialized into unary and binary tables that correspond to DL concepts and roles, respectively. In some cases, splitting a large table into smaller ones also allows for more fine-grained justifications.
Example 2. Using mappings, a database entry of a (ProvSQL-enabled) SensorData table can be transformed into separate facts sensor(123, camera), Rain(123), time(123, 15:43),
′() = ∃. environment(, ) ∧ Rain() ∧ HighConfidence() that has the answer = d2 w.r.t. the TBox from Example 1. The only justification for this answer is {environment(d2, 123), Rain(123), HighConfidence(123)}, which allows pinpointing the reasons for the query answer more precisely than by just returning the full original tuple SensorData(123, d2, camera, rain, 15:43, 0.8).
In this section, we describe the building blocks of our approach for computing ABox justifications
for CQ answers.
3.1. ProvSQL
ProvSQL2 [
Example 3. Returning back to Example 2 above, using ProvSQL, we can trace the DL-ified tuples back to the original SensorData table, since the facts such as environment(d2, 123) can be obtained by an SQL query over the materialized environment table: drone d2 id 123
provsql 6bb9bd38-4ef8-bb6d where the UUID ’6bb9bd38-4ef8-bb6d’ refers to a circuit that encodes the projection operation over the original entry ’a0eebc99-9c0b-4ef8’.
To obtain the set of all justifications J = {1, . . . , } for a specific output tuple, we then
need to suitably evaluate its provenance circuit. Each UUID corresponding to an input fact
gets replaced by {{ }} (the set containing only the trivial justification for ), and the operators
⊗ , ⊕ are translated into element-wise set union and simple set union, respectively, which
corresponds to a step-wise combination of the sets of justifications for intermediate query
results [
was detected at a nearby location, then it is also raining at the current location, will be rewritten as environmentSomeRain() :– near(, ), environmentSomeRain() environmentSomeRain() :– environment(, ), Rain()
In the next section, we explain how we can transform a possibly recursive Datalog program into a series of SQL statements, whose provenance can be traced using ProvSQL. 3.3. Compiling Datalog Rules Into SQL Statements The algorithm proceeds as follows. First, the “depends on”-relation of the Datalog program is represented as a graph, denoted by = (, ), where each node in corresponds to a predicate that occurs in the ontology. The edge relation is defined using the body and the head of each rule: for each rule ℎ :– 1, . . . , , there exist edges (ℎ, 1 ), . . . , (ℎ, ) in . Furthermore, each node is associated with the set of all rules in the Datalog program that have in their head. In Datalog rewritings produced by Clipper, no other predicate depends on the query predicate , and thus for most of the following descriptions we will ignore the node and process it separately at the end.
If is acyclic, its nodes can be partitioned into levels according to the length of the longest path to any leaf node (a node without outgoing edges). The algorithm processes all nodes on the same level one after the other, starting from the lowest level, i.e., the leafs. Processing a node translates all rules associated with (which all have the same head predicate) into SQL statements.
Example 5. For example, the rules ℎ(1) :– 1(1, 2), 2(2), ℎ(1) :– 3(1) would be translated into the query CREATE TABLE ℎ AS ((SELECT 1.1 FROM 1 JOIN 2 ON 1.2 = 2.1) UNION (SELECT 1 FROM 3)).
In case a table for a predicate ℎ already exists and has to be updated with new tuples, in order for ProvSQL to recognize a change in the data, first a dummy table needs to be created that holds the union of the data contained in the old table and the new query results:
CREATE TABLE dummy AS (. . . UNION SELECT * FROM ℎ) 3https://github.com/ghxiao/clipper 4https://www.dlvsystem.it/dlvsite/ 5https://github.com/potassco/clingo Afterwards, the old table is deleted and re-created with the content of the dummy table: DROP TABLE ℎ
CREATE TABLE ℎ AS SELECT * FROM dummy
However, the dependency graph of the rules created by Clipper from a Horn-ℋℐ ontology
can actually be cyclic (see Example 4). To handle cyclic dependency graphs, all strongly
connected components (SCCs) are first identified using Kosaraju-Sharir’s algorithm [
For an SCC and a new cycle node , the dependency graph = (, ) is updated to ′ = ( ′, ′) with ′ = ( ∖ ) ∪ {} and (1) (2) (3) (4) ′ = {(, ) | (, ) ∈ , , ∈ ′} ∪ {(, ) | (, ) ∈ , ∈ ′, ∈ } ∪ {(, ) | (, ) ∈ , ∈ , ∈ ′}.
The rules previously associated to the nodes in are thereafter associated to . The algorithm
then proceeds as in the non-recursive case, but processes cycle nodes diferently, depending on
the associated rules. Due to the shape of the Datalog programs produced by Clipper, all rules
involved in a cycle either have only unary predicates in the head (e.g. as in Example 4), or they
have only binary predicates in the head [
By Horn-ℋℐ syntax, when binary head atoms are involved, all rules must be of one of the following shapes: (, ) :– (, ) (, ) :– (, ) (, ) :– (, ), (, ) If all rules in the cycle are of the form (2), they can be processed as in the case of unary head atoms. If rules of shape (3) are involved, we need to double the number of executions of the SQL statements since it may require 2ℓ iterations to propagate all involved pairs of individuals (, ) and their inverses (, ) to all involved binary predicates.
Finally, transitivity rules of the form (4) need to be processed diferently, since their application involves a potentially unbounded number of individuals, and thus the necessary number of iterated SQL statements now depends on the length of the longest (undirected) path in the current database that involves only the roles from the cycle node. Therefore, every transitivity rule (potentially as part of a larger cycle node) increases the number of iterated applications of SQL statements for the whole cycle node by log2 , where is the length of this path.
At the very end of the algorithm, the query predicate is populated using the same approach as in Example 5, since we do not have to worry about cycles at this stage.
Algorithm 1: Generating SQL updates w.r.t. a Datalog program for ABox tables . 1 = (, ) is the “depends-on” relation graph of 2 foreach ∈ do 3 rule() = { ∈ | is in the head of } 4 ′ = 5 while ′ has a SCC do 6 create a new cycle node 7 rule( ) = { ∈ | ∈ rule() for some ∈ } 8 update ′ according to (1) for
The above-described procedure is summarized in Algorithm 1.
Theorem 1. Let = ( , ) be a Horn-ℋℐ ontology, a CQ with Datalog rewriting (, , ) w.r.t. , and ′ the set of facts resulting from Algorithm 1 w.r.t. the Datalog program , and . Then |= (⃗) if (⃗) ∈ ′.
Proof. For soundness, it sufices to observe that the algorithm faithfully applies the rules in the rewriting, which is correct for query answering over . To show completeness, we have to show that ∪ , |= (⃗) implies (⃗) ∈ ′. If ∪ , |= (⃗), there exists a derivation D (i.e., a tree of rule applications) deriving (⃗) from the facts in using the rules in , . In the following, we assume that D is minimal, and in particular that no fact is derived twice and only facts that are required to derive (⃗) are derived. For every fact (⃗) derived in D, we prove that (⃗) ∈ ′ by induction over the order in which the node representing is processed by the main loop in Lines 11–25. Hence, we assume that the claim is satisfied for all predicates represented by the nodes reachable from in the original graph ′ (after the introduction of the cycle nodes in Lines 5–8). We distinguish two cases.
• If is an ordinary node or a cycle node associated with only unary or only binary head predicates (including ), but rules of the form (3) or (4), then we consider the last rule applications in D involving the predicates in . For any premises ′(⃗′) of these rules involving predicates from previous stages, we know by induction that ′(⃗′) ∈ ′ has already been derived previously by Line 24. The remaining premises must be of the form ′(⃗) with ′ represented by the current cycle node . Assume that the depth of these last rule applications is larger than the length ℓ of the longest acyclic path in the SCC represented by . Then the rule applications contain a cycle, i.e., at least one fact ′(⃗) is derived twice, which contradicts our assumption on the derivation D. Thus, since the depth of the last rule applications to derive (⃗) is bounded by ℓ, we have (⃗) ∈ ′ by our construction. • If involves binary predicates and at least one rule of the form (3), but no rule of the form (4), then we can apply the same arguments as above, but have to consider all facts of the form ′(, ) and ′(, ) that are involved in the derivation of (⃗) = (, ), which means that the length of the derivation could be doubled in the worst case (see Line 16). • If is a cycle node involving a transitive binary predicate (cf. Lines 17–20), then (⃗) = (, ) and we consider all applications of the rule (, ) ← (, ), (, ) up to the derivation of (, ) (or (, )). Since D is non-redundant, the original -facts (not derived by the transitivity rule) must form an -path (, 1), (1, 2), . . . , (, ) from to without repeating constants. If this path is of length , then the fact (, ) is derived after at most log2 nested applications of (, ) ← (, ), (, ). By similar arguments as above, each of the -facts (, +1) must have been derived after 2ℓ rule applications from other binary facts (or their inverses) whose predicates are involved in the cycle. This shows that (, ) ∈ ′ and (, ) ∈ ′.
Note that Algorithm 1 does consider the query predicate : the ABox tables are updated until no more facts are derived. In the implementation, this procedure is optimized by terminating once the node has been processed by the loop in Lines 12–25. Further iterations are redundant, since they cannot create new facts for .
In order to evaluate our approach, we compare our implementation with Souflé, a
state-ofthe-art tool for Datalog reasoning that can also compute proofs [
We also wanted to compare the performance of a recent approach for computing provenance
for Datalog programs based on Rulewerk and Vlog [
The Query Time for our approach already includes the time taken by ProvSQL to compute the provenance circuits for each intermediate answer, which could also be seen as part of the Explanation Time, which is why we also report the Total Time for each tool. Nevertheless, the comparison is still biased since ProvSQL always computes the full provenance, i.e., we obtain all possible justifications for a query answer, whereas Souflé outputs only a single proof, from which we can extract one (possibly non-minimal) set of input facts responsible for the answer. By construction, our approach cannot compute the provenance of just a single query answer on demand without pre-computing the provenance for all answers. Similarly, ProvSQL does not support computing only a single ABox justification.
We can see that with the provenance components our algorithm mostly compares favorably to Souflé, except for queries that have a lot of answers (which requires ProvSQL to compute many provenance circuits) and for answers whose provenance is very large due to the cycles in the Datalog program. Since we only want to compute justifications, these provenance circuits contain a lot of redundancies that could be eliminated at intermediate steps by a more dedicated algorithm in the future.
We presented a possible approach for computing ABox justifications, or why-provenance, for
relatively expressive ontology-mediated queries that have Datalog rewritings. This can be useful
to compute further, more detailed explanations of query answers by restricting the set of facts
needed for computing them [
We thank Islam Hamada for his contributions to the implementation. This work was supported by the DFG grant 389792660 as part of TRR 248 (https://perspicuous-computing.science). Proceedings, volume 13752 of Lecture Notes in Computer Science, Springer, 2022, pp. 146–163. doi:10.1007/978-3-031-21541-4_10. [32] C. Alrabbaa, S. Borgwardt, A. Hirsch, N. Knieriemen, A. Kovtunova, A. M. Rothermel, F. Wiehr, In the head of the beholder: Comparing diferent proof representations, in: G. Governatori, A. Turhan (Eds.), Rules and Reasoning - 6th International Joint Conference on Rules and Reasoning, RuleML+RR 2022, Berlin, Germany, September 26-28, 2022, Proceedings, volume 13752 of Lecture Notes in Computer Science, Springer, 2022, pp. 211– 226. doi:10.1007/978-3-031-21541-4_14.