The Explanation Issue

In the realm of Artificial Intelligence, symbolic AI stands out for its ability to provide explainable results and predictions. In particular, knowledge and rule-based systems make it possible for users to trace the derivation of new knowledge back to the exact elements that have contributed to it. This traceability is crucial for applications where understanding the reasoning process is as important as the outcome itself, such as in healthcare or regulatory enforcement.

While the issue of computing explanations has long been studied for Description Logics (see e.g., [1,2,3,4,5]), the extension of the approach to mainstream rule languages such as Datalog has not been considered so far. Datalog is widely recognised as a language which leverages recursion for data processing [6] and plays a significant role in ontology-mediated query answering [7]. On the one hand, it encompasses RDF-Schema and OWL-RL ontologies. On the other hand, many reasoning tasks on ontologies can be reduced to query answering in this language [8]. Providing explanations for Datalog is thus a step towards more reliable data-intensive applications, and the goal of this work is to contribute to the explainability of Datalog.

Explaining reasoning in Datalog raises, however, two key challenges. The first is to choose a form of explanation that is suitable for the reasoning task. The second is to actually compute them, which is known to be expensive even for basic forms of explanations [9,10].

Choosing Explanations Let us illustrate the importance of choosing the "right" notion of explanation. Hereafter, we assume the reader is familiar with propositional and first order logic. Consider the knowledge base 𝒦 = ⟨ℛ, ℱ⟩ in Figure 1 with facts ℱ = {Boss(alice, alice)} and rules ℛ = {𝑟 1 , 𝑟 2 , 𝑟 3 }. Consider the task of explaining the fact 𝜙 = Manager(alice), which is entailed by 𝒦. As Figure 1 illustrates, 𝜙 can be derived in two different ways starting from ℱ. One is by applying 𝑟 1 . The other is by applying 𝑟 2 and then 𝑟 One possible form of explanation consists in computing the fact-support of 𝜙 with respect to ℱ, that is, the set of facts ℱ ′ ⊆ ℱ that can contribute to the derivation of 𝜙. The notion of fact-support corresponds to that of why-provenance [8,10,9,5]. For the example in Figure 1, this would yield ℱ ′ = ℱ. Here, fact-support provides an insufficient information as it does not show the role of rules in the reasoning task.

A meaningful notion of explanation here would be that of kb-support, that is, a subset 𝒦 ′ of 𝒦 which entails 𝜙. To be precise, we need to identify minimal subsets of the knowledge base that preserve the entailment since users typically prefer concise explanations. In the example of Figure 1, there are two kb-support explanations:

𝒦 ′ 1 = ⟨{𝑟 1 }, ℱ⟩ and 𝒦 ′ 2 = ⟨{𝑟 2 , 𝑟 3 }, ℱ⟩.

The interest in the notion of kb-support is that it better explains the roles taken by both the rules and the data in the reasoning task thereby giving the user more power to potentially take action and revise the knowledge base. In the context of Description Logics, kb-supports correspond to the notion of justifications with ABoxes (the standard version of justifications rather considering entailment axioms over TBoxes) [1,2]. In this work, we will thus consider this notion of kb-support which enables more detailed explanations for fact entailment over Datalog knowledge bases.

Computing Explanations An effective approach to tackling the expensive theoretical cost of computing explanations is to rely on the use of SAT-solvers [2,8]. Nowadays, these are considered mature and effective tools. The critical step of this reduction is that of encoding the input knowledge base and entailment (i.e., the inputs of the explanation problem) as a propositional formula. To illustrate, Figure 1 shows the SAT encoding of the explanation problem, which goes as follows. It associates every atom entailed by the knowledge base with a distinct propositional variable (here, 𝐴, 𝐵, and 𝐶). Then, a conjunctive formula is built. Its elements are either:

(i) a propositional variable corresponding to a fact in ℱ (e.g., 𝐴 represents Boss(alice, alice)), (ii) a grounded rule corresponding to a rule application (e.g., 𝐴 → 𝐵 represents Boss(alice, alice) → CEO(alice)) or (iii) a negated literal, whose propositional variable corresponds to the entailment (e.g., ¬𝐶 corresponds to ¬Manager(alice)).

An important detail here is that negating the fact to explain in the encoded formula allows one to solve the explanation problem by looking at its minimal unsatisfiable sets (MUSes) [11]. As Figure 1 shows, each MUS of the encoded formula provides an explanation.

Computing All Explanations Computing explanations via MUS for Datalog can lead to potential pitfalls. The main issue is that two distinct rule applications can "conflict" by resulting in the same SAT-encoding. This case is illustrated in Figure 2. Here, we can see that the applications of 𝑟 1 and 𝑟 2 are both encoded as 𝐴 → 𝐶. As a result, the MUS enumeration no longer yields a (minimal) explanation. The situation becomes even more complex when many recursive rules share the same groundings. To address these issues, we present an encoding into group-SAT formulas [11] which allows us to establish a precise correspondence between explanations and group-MUSes.

Computing All Explanations Efficiently While solvers are efficient, MUS computation remains hard. Therefore, significant challenges may arise in terms of scalability as the size and complexity of the knowledge base increase. The main reason for this is that in more complex knowledge bases there may be a larger number of atoms and rules which are not relevant for the entailment to explain. This is illustrated in Figure 3: atoms s(c) and s(d), as well as rule 𝑟 4 , are irrelevant for explaining goal(a).

Considering irrelevant atoms will slow down both the encoding computation and the MUS enumeration task. Hence, we introduce a filtering technique that reduces the size of the encoded formula while preserving its soundness and completeness.

Contribution

The contributions of this paper are the following:

From Datalog Explanations to Group-MUS

The Logical Setting We assume a first-order signature with functions. We consider mutually disjoint sets of variables, constants, and functions. We call term any variable, constant, or functional term of the form 𝑓 (𝑡

= ⟨ℛ 1 , ℱ 1 ⟩ and 𝒦 2 = ⟨ℛ 2 , ℱ 2 ⟩ we write 𝒦 1 ⊆ 𝒦 2 when ℛ 1 ⊆ ℛ 2 and ℱ 1 ⊆ ℱ 2 .

Fact Entailment

The chase is a standard method for computing universal models of knowledge bases that can in turn be used for tasks like fact entailment [12]. A substitution is a partial function mapping variables to ground terms. A trigger for a fact set ℱ and a rule set ℛ is a tuple 𝜏 = ⟨𝑟, 𝜎⟩ where 𝑟 ∈ ℛ, and 𝜎 is a substitution such that 𝜎(body(𝑟)) ⊆ ℱ. The trigger outputs out(𝜏 ) = 𝜎(head(𝑟)).

For a KB 𝒦 = ⟨ℛ, ℱ⟩, let Chase 0 (𝒦) = ℱ; and, for every 𝑖 ≥ 1, let Chase 𝑖 (𝒦) be the minimal fact set that includes Chase 𝑖−1 (𝒦) and out(𝜏 ) for every trigger 𝜏 of Chase 𝑖−1 (𝒦) and ℛ. Moreover, let Chase(𝒦) = ⋃︀ 𝑖≥0 Chase 𝑖 (𝒦). A KB 𝒦 entails a fact 𝜙, denoted 𝒦 |= 𝜙, if and only if 𝜙 ∈ Chase(𝒦). From now on, every knowledge base considered in this section is Datalog. Knowledge bases with functions will be employed in Section 3. At this point, we can formally define the notion of explanation for Datalog knowledge bases.

Definition 1 (Explanation). For a Datalog knowledge base 𝒦 = ⟨ℛ, ℱ⟩ and a fact 𝜙, a kb-support explanation of 𝒦 |= 𝜙 is a KB 𝒦 ′ ⊆ 𝒦 such that 𝒦 ′ |= 𝜙 but 𝒦 ′′ ̸ |= 𝜙 for every 𝒦 ′′ ⊂ 𝒦 ′ . We denote by Expl(𝒦, 𝜙) the set of all explanations of 𝒦 |= 𝜙.

From Explanations to Group-MUS We now show how to reduce the explanation problem to group-MUS (GMUS) enumeration. Group-SAT (GSAT) formulas are natural extensions of SAT formulas where constraints are modeled as sets or groups [13]. The underlying idea is that all clauses in a group must hold together. Below, we assume the standard notion of literal (positive or negative propositional variable) and clause (disjunction of literals). A group 𝒢 is a set of clauses. To keep the formalisation concise, we slightly enrich the standard definition and also assume that every group 𝒢 has a unique identifier 𝑖 denoted by 𝒢 𝑖 . Otherwise said, we consider two groups with the same clauses but with different identifiers to be different. A GSAT formula F is a set of groups F = {𝒢 1 , . . . , 𝒢 𝑛 }. A GSAT formula is satisfiable if the conjunction of all the clauses in the union of its groups is satisfiable. A GMUS of F is a minimal set of the groups of F that is unsatisfiable. We write GMUS(F) for the set of all GMUS of F. Figure 2 illustrates the GSAT formula stemming from the encoding of the input facts and rules. In the formula, we have two groups which contain the same (set of) clauses; these are denoted as {𝐴 → 𝐶} 𝑟 1 and {𝐴 → 𝐶} 𝑟 2 where the identifier of each group corresponds to the rule that generates it. Also note that with this encoding every GMUS in Figure 2 corresponds to one explanation.

To reduce the computation of the explanations for a fact 𝜓 over a KB 𝒦 to group-MUS enumeration, our goal is to produce a GSAT formula which encodes the derivations enabled by the KB as well as the (negation of) the fact to explain. Let 𝒦 = ⟨ℛ, ℱ⟩, we define GSAT(𝒦 ∧ ¬𝜓) as the minimal set containing:

• the group 𝒢 𝑟 with 𝒢 = Grounding 𝒦 (𝑟), for every 𝑟 ∈ ℛ

• the group 𝒢 𝜙 with 𝒢 = {𝜙}, for every 𝜙 ∈ ℱ

• the group 𝒢 𝜓 with 𝒢 = {¬𝜓} Above, Grounding 𝒦 (𝑟) is the set containing the grounded rule 𝜎(body(𝑟)) → 𝜎(head(𝑟)) for every trigger 𝜏 = ⟨𝑟, 𝜎⟩ over Chase(𝒦). Given a set of groups F, we denote by KBs(F) the knowledge base built by using all facts and rules that are identifiers of the groups in F. Proposition 1 establishes a precise correspondence between the explanations for 𝒦 |= 𝜓 and the group-MUSes of GSAT(𝒦 ∧ ¬𝜓).

Proposition 1. Expl(𝒦, 𝜓) = ⋃︁

F∈GMUS(GSAT(𝒦∧¬𝜓))

KBs(F).

Knowledge-Base Filtering via Relevance

To explain an entailment of a knowledge base, it is often the case that only a portion of the knowledge base's facts and rules are necessary or relevant to that entailment. In this section, we present a formal definition of relevance and introduce a rule-based technique for filtering out facts that are irrelevant for explaining a given fact. This technique can drastically reduce the size of the encoded formula to be solved.

Relevance We say that a fact 𝜓 is relevant for the entailment of a fact 𝜙 in a knowledge base 𝒦 if there exists an explanation 𝒦 ′ ∈ Expl(𝒦, 𝜙) that contains 𝜓. This definition naturally extends to rules. Consider the knowledge base in Figure 3 with facts ℱ = {p(a), q(a), t(b, a), s(c), s(d)} and rules ℛ = {𝑟 1 , 𝑟 2 , 𝑟 3 , 𝑟 4 }. The entailment 𝜙 = goal(a) can be derived in two ways. The first is by applying 𝑟 1 , which yields t(a, a); this atom allows for the application of 𝑟 3 to derive 𝜙. The second is by applying 𝑟 3 on the results of 𝑟 1 and 𝑟 2 . The fact 𝜙 has, however, only one explanation, namely, 𝒦 ′ = ⟨{𝑟 1 , 𝑟 3 }, {p(a)}⟩. Indeed, 𝒦 ′′ = ⟨{𝑟 1 , 𝑟 2 , 𝑟 3 }, {p(a), q(a), t(b, a)}⟩ is not minimal as 𝒦 ′ ⊂ 𝒦 ′′ (see Definition 1). As a result, with Expl(𝒦, 𝜙) = {𝒦 ′ }, the only elements relevant to the entailment of 𝜙 in 𝒦 are p(a) and 𝑟 1 , 𝑟 3 . Despite its apparent simplicity, it turns out that deciding relevance is hard. This holds true even if one focuses only on deciding the relevance of facts, for a fixed rule set. By a reduction from SAT, we have the following proposition. Proofs can be found in Appendix A.

Proposition 2. For a fixed ruleset ℛ, deciding if a fact 𝜓 ∈ ℱ is relevant for 𝜙 on ⟨ℛ, ℱ⟩ is NP-complete.

Approximating Relevance Considering this hardness result, we turn our attention to the task of approximating relevant facts and rules. This is achieved using a two-step rule-based approach: a static step which preprocesses the input knowledge base, followed by a dynamic step for tracing each individual entailment. The static step builds an entailment graph which tracks all relationships between any entailed atoms and rules. This entailment graph allows us to compute an approximation of relevant facts. For instance, as illustrated in Figure 3, the relevance approximation includes atoms p(a), q(a), t(b, a) and rules 𝑟 1 , 𝑟 2 , 𝑟 3 . We now present our approach and give a construction for the entailement graph based on rules with function symbols, which can be deployed on reasoners supporting the formalism. Before detailing each step, we introduce the following notation. Given a predicate 𝑃 , we denote by 𝑃 + and 𝑓 𝑃 a fresh predicate and a function unique for 𝑃 , respectively; below, the same will hold for predicates 𝐵 and 𝐻. Moreover, given a rule 𝑟 we respectively denote by E 𝑟 and 𝑓 𝑟 a fresh predicate and a function unique for 𝑟. The aim of the static step is to produce the entailment graph, i.e. a hypergraph representing the links (in terms of entailment) between the atoms. In order to do that, we first need to be able to reference the atoms in Chase(𝒦). This is done by rules of type (1) which infer, for any atom 𝑃 (𝑡 ¯) of arity 𝑘, an atom 𝑃 + (𝑡 ¯, 𝑓 𝑃 (𝑡 ¯)) of arity 𝑘 + 1 where 𝑓 𝑃 (𝑡 ¯) is a functional term representing 𝑃 (𝑡 ¯) itself. Then, every rule 𝑟 is transformed into a rule of type (2) which, once applied, uses the functional terms to link all images of the body atoms to the image of the head atom via an hyperedge relation E 𝑟 proper to 𝑟. Let us emphasise that this step is done only once, for every input 𝒦.

Static step (entailment graph building)

Figure 4 illustrates the rules for the static step EntGraph(ℛ) for the rule base of Figure 3, as well as their applications starting from p(a). First, the rule 𝑟 𝑝 produces the atom p + (a, f p (a)), where 𝑓 p (a) represents p(a). Consider then rule 𝑟 1 . This is transformed in the following way: the body p(𝑥) and the head t(𝑥, 𝑥) are respectively replaced by p + (𝑥, 𝑓 p (𝑥)) and t + (𝑥, 𝑥, 𝑓 t (𝑥, 𝑥)), and an hyperedge atom E r 1 (𝑓 p (𝑥), 𝑓 t (𝑥, 𝑥)) is added to the head to represent the link between the two atoms in the entailment graph. Note that this edge atom uses the functional terms corresponding to the atoms appearing in the rule. Since we have p + (a, f p (a)), the rule 𝑟 ′ 1 produces both t + (a, a, f t (a, a)) and the edge predicate E r 1 (f p (a), f t (a, a)) representing the fact that p + (a, f p (a)) is used to derive t + (a, a, f t (a, a)). Finally, 𝑟 ′ 3 is obtained from 𝑟 3 in a similar way, and it is used to derive goal + (a, f goal (a, a)).

Dynamic Step (tracing)

For any fact 𝜙 to explain, we define 𝒟 = Chase(⟨relPropag(ℛ, 𝜙), 𝒮⟩) where 𝒮 is the result of the static step and relPropag(ℛ, 𝜙) is the minimal set containing the following rules:

1. → Rel(𝑓 𝑃 (𝑥 ¯)) if 𝜙 = 𝑃 (𝑥 ¯)

2. E r (𝑦 Rel(f goal (a))

𝑟 𝑟𝑒𝑙𝑔𝑜𝑎𝑙 Rel(f t (a, a)) 𝑟 𝑟𝑒𝑙3 E r3 (f t (a, a), f t (a, a), f goal (a))

RelEdge(f r3 (f t (a, a), f t (a, a), f goal (a)))

Rel(f p (a))

𝑟 𝑟𝑒𝑙1 E r1 (f p (a), f t (a, a))

RelEdge(f r1 (f p (a), f t (a, a))) in the static step, and Rel and RelEdge are reserved predicates. Intuitively, these rules recursively trace a fact back to the ancestor atoms which belong to the input fact base. Figure 5 illustrates the rules for the dynamic step relPropag(ℛ, 𝜙) for the rule base of Figure 3 and the entailment 𝜙 = goal(a), as well as their applications. In a nutshell, the atom to be is marked as relevant thanks to the (empty body) rule → Rel(f goal (a)). Then the relevance relation is propagated back using the edge atoms produced during the static step. In order to do this, we need the "propagation rule" 𝑟 𝑟𝑒𝑙 1 -𝑟 𝑟𝑒𝑙 4 . For instance, since we have E r 3 (f t (a, a), f t (a, a), f goal (a)) from the static step, and goal(a) is relevant (i.e., Rel(f goal (a))), then by rule 𝑟 𝑟𝑒𝑙 3 we have that both t(a, a) and 𝑟 3 are relevant (i.e, Rel(f t (a, a)) and RelEdge(f r 3 (f t (a, a), f t (a, a), f goal (a))), respectively). The same process applies for deeming p(a) and rule 𝑟 1 as relevant by the application of 𝑟 𝑟𝑒𝑙 1 .

Finally, for 𝒦 = ⟨ℛ, ℱ⟩, we define the approximation of the relevant KB as SupRel 𝜙 (𝒦) = ⟨ℛ ′ , ℱ ′ ⟩ where ℱ ′ = {𝑃 (𝑡 ¯) ∈ ℱ | 𝒟 |= Rel(𝑓 𝑃 (𝑡 ¯))} and ℛ ′ = {𝑟 ∈ ℛ | 𝒟 |= RelEdge(𝑓 𝑟 (𝑡 1 , . . . , 𝑡 𝑛 , 𝑡 ′ ))}. Note that both 𝒮 and 𝒟 knowledge bases always admit a finite (terminating) chase. Soundness and completeness below state that this approximation provides the same explanations as the exact relevance. Proposition 3. Expl(𝒦, 𝜙) = Expl(SupRel 𝜙 (𝒦), 𝜙)

Experimental Analysis

We have implemented our approach by using the MARCO tool for group-MUS enumeration [11] (Section 2) and InteGraal [14] for approximating relevance (Section 3).

Benchmarks

We selected 24 interesting ontologies from the MOWL corpus [15]. These ontologies were in the EL profile and have been translated into Datalog programs using the Java OWL API [16] and the translation presented in [17]. We made sure that each ontology has at least 5 extensional facts and produces at least 5 intensional facts. For each ontology, we picked 5 entailment queries to explain among the atoms with the greatest reasoning depth (and that are hence, intuitively, more challenging to explain), that is, atoms that are derived in the last (breadth-first) step of the saturation of the ontology.

Protocol For each ontology, we compute the entailment graph using InteGraal [14] and the rules for the static step presented in Section 3; recall that this step is done only once per ontology. Subsequently, for each entailment query, we again use InteGraal [14] and the rules for the dynamic step presented in Section 3 to compute a knowledge base that consists only of the part of the input ontology relevant to that particular entailment query. This relevant knowledge base is then translated into a GSAT formula as described in Section 2 and fed to the MARCO tool [11]. The tool returns all MUSes which, when translated back to Datalog knowledge base statements, constitute the explanations. We compared against the OWL API [16] which is the only tool we are aware of which computes kb-support explanations (i.e., ontology axioms corresponding to facts and rules). We implemented our benchmarking protocols using the B-Runner library [18] and made them available online [19].

Setup All our experiments are run on a server with AMD Ryzen 9 3900XT 12-Core Processor @4.7GHz, 128GB of RAM @2.4GHz, and 2TB of SSD NVME. Analysis Figure 6 reports the time taken by the static step, which corresponds to the entailment graph construction, vs the dynamic step which is further divided into filtering (via InteGraal) and MUS enumeration (via MARCO). For the dynamic step, we report the average time for the 5 queries we considered. Times are in milliseconds.

As expected, we can observe that the time taken by the static step (even if within tenths of a second) is significantly longer than that of the dynamic step. Interestingly, we found that the time required for constructing the entailment graph depends on the number of possible rule groundings as well as on the depth (in a breadth-first sense) of the chase. This cost, being fixed, is however amortised when multiple explanation queries are submitted.

Concerning the dynamic step, we can observe that this is much faster than the static step, more in the order of tens of milliseconds. Again, we found that a crucial aspect here is the depth of the derived atom: the deeper an atom is in the entailment graph the more one has to propagate relevance. Our results also indicate that the group-MUS enumerator is very fast (in the order of milliseconds), which further validates this approach for computing explanations. Note also that the generality of our method makes that it can be implemented with any reasoner supporting the rules described in Section 3, and any group-MUS enumerator.

We conclude with a comparison with the explanation facility provided by the OWL API. We can see that our approach is generally more competitive if we consider only the dynamic step, and can even be more competitive depending on the cases for one-of explanations including both the static and dynamic step as a single operation.

Related Work & Conclusion

We have introduced the first comprehensive approach for computing kb-support explanations for fact entailments over Datalog knowledge bases. Our method leverages on group-MUS enumeration for computing explanations as well as on a rule-based approach to filter irrelevant atoms for the task. Our approach has been implemented and experimentally evaluated.

Our work considers explanations in the form of kb-support (a.k.a, justifications with ABoxes), which, to the best of our knowledge, has not been investigated so far for Datalog [9,8,10]. Indeed, existing methods for Datalog focus on the notion of why-provenance which corresponds to that of fact-support. The recent work of [8] studies the use of SAT-solvers for computing why-provenance on Datalog based on so called non-ambiguous proof trees. Rule-based approaches for on-demand computation of Datalog provenance have been studied in [10]. The recent work of [5] considers provenance computation for the EL Description Logic [20,21]. In the context of answer set programming (ASP), the work of [21] considers a notion of graph-explanation; this can be seen as an extension of fact-support including all inferred facts (but no rules). While these approaches are close to ours in spirit, the technical development remains different. Notably, considering kb-supports allows us to obtain more explanations than whyprovenance, and thus a better understanding of the entailed facts. On the other hand, this also required us to establish a new correspondence between group-MUSes and kb-support explanations.

In the context of Description Logics, reasoning explanations have long been studied. Justifications, also called minimal axiom sets, and their computation are referred to as axiom pinpointing. The approaches closest to ours are the following. [1] and [2] consider the problem of computing axiom explanation for EL TBoxes (hence, without data). [1] studies the complexity of computing relevant axioms while [2] presents a reduction to GMUS enumeration. However, in contrast to our work, none of these approaches consider data (ABoxes). The problem of filtering the knowledge base to a set of relevant facts has been considered in [8,10,3,4]. All of these approaches employ a notion akin to that of a dependency graph. However, our work differs in that it considers a different notion of explanation. Moreover, our work is the only one that studies the complexity of deciding the relevance of atoms (NP-complete).

Through this work we demonstrated the practical applicability of group-SAT solvers for knowledge bases, paving the way for more efficient and explainable AI systems. Future work includes the extension of our setting to richer rule languages, including suitable forms of functions, negation, and disjunction.

(Soundness) We show that if Source is relevant for the entailment of Target with 𝒦 then the CNF formula Φ is satisfiable. a ○ By hypothesis there is an explanation ⟨ℛ ′ , ℱ ′ ⟩ ⊆ ⟨ℛ, ℱ⟩ such that Source ∈ ℱ ′ and ⟨ℛ If a rule of the form (1) has been applied then there is a constant 𝑣 𝑘 such that T(𝑣 𝑘 ) ∈ ℱ ′ and T(𝑣 𝑘 ) → T(𝑐 𝑖 ) ∈ ℛ ′ . Let 𝑉 𝑘 be the corresponding variable of 𝑣 𝑘 and 𝐶 𝑖 the clause corresponding to 𝑐 𝑖 in Φ, then by the construction of the rules in (1) we have that 𝑉 𝑘 ∈ 𝐶 𝑖 and by c ○ we know that 𝜎 ℱ ′ (𝑉 𝑘 ) = True, thus 𝜎 ℱ ′ (𝐶 𝑖 ) = True.

If a rule of the form (2) has been applied then there is a constant 𝑣 𝑘 such that F(𝑣 𝑘 ) ∈ ℱ ′ and F(𝑣 𝑘 ) → T(𝑐 𝑖 ) ∈ ℛ ′ . Let 𝑉 𝑘 be the corresponding variable of 𝑣 𝑘 and 𝐶 𝑖 the clause corresponding to 𝑐 𝑖 in Φ, then by the construction of the rules in (2) we have that ¬𝑉 𝑘 ∈ 𝐶 𝑖 and by c ○ we know that 𝜎 ℱ ′ (𝑉 𝑘 ) = False thus 𝜎 ℱ ′ (𝐶 𝑖 ) = True. There is a positive literal 𝑉 𝑘 ∈ 𝐶 𝑖 such that 𝜎(𝑉 𝑘 ) = 𝑇 𝑟𝑢𝑒. In this case, let 𝑣 𝑘 and 𝑐 𝑖 be the constants corresponding to 𝑉 𝑘 and 𝐶 𝑖 respectively. By a ○ we have that T(𝑣 𝑘 ) ∈ ℱ ′ , and T(𝑣 𝑘 ) → T(𝑐 𝑖 ) ∈ ℛ by the construction of rules in (1).

There is a negative literal ¬𝑉 𝑘 ∈ 𝐶 𝑖 such that 𝜎(𝑉 𝑘 ) = 𝐹 𝑎𝑙𝑠𝑒. Let 𝑣 𝑘 and 𝑐 𝑖 be the constants corresponding to 𝑉 𝑘 and 𝐶 𝑖 respectively. By a ○ we have that F(𝑣 𝑘 ) ∈ ℱ ′ , and F(𝑣 𝑘 ) → T(𝑐 𝑖 ) ∈ ℛ by the construction of rules in (2).

In both cases, ⟨ℛ, ℱ ′ ⟩ |= T(𝑐 𝑖 ) for every 1 ≤ 𝑖 ≤ 𝑚. c ○ Let ℱ ′′ be a minimal subset of ℱ ′ and ℛ ′ a minimal subset of ℛ (obtained in linear time by deletion, i.e., by removing on fact/rule until the entailment is lost) such that ⟨ℛ ′ , ℱ ′′ ⟩ |= Target. We know that (3) and ( 4) are the only rules that can infer Target. However, (4) can not be applied on ℱ ′′ . Indeed, ℱ ′ is built from an assignment 𝜎 and therefore either T(𝑣 𝑖 ) or F(𝑣 𝑖 ) belongs to ℱ ′′ for any constant 𝑣 𝑖 corresponding to a variable 𝑉 𝑖 in Φ. Hence the rule (3) has been applied to derive Target. d ○ To conclude, note that to apply (3) the atom Source must belong to ℱ ′′ and ⟨ℛ ′ , ℱ ′ ⟩ is an explanation of Target. Hence, Source is relevant for Target.

(Polynomiality) We show the size of 𝒦 is polynomial with respect to the size of Φ. In the fact set ℱ we have 2𝑛 + 1 atoms with 𝑛 being the number of propositional variables in Φ. Then the rule set contains at most 𝑘 × 𝑚 + 2 rules where 𝑚 is the number of clauses in Φ and 𝑘 the largest number of literals in a clause. Thus the instance 𝒦 is polynomial with respect to Φ and the translation can be computed in polynomial time.