In order to meet usability requirements, most logic-based applications provide explanation facilities for reasoning services. This holds also for DLs, where research focused on the explanation of both TBox reasoning and, more recently, query answering. Besides explaining the presence of a tuple in a query answer, it is important to explain also why a given tuple is missing. We address this latter problem for (conjunctive) query answering over DL-Lite ontologies, by adopting abductive reasoning, that is, we look for additions to the ABox that force a given tuple to be in the result. As reasoning tasks, we consider existence and recognition of an explanation, and relevance and necessity of a certain assertion for an explanation. We characterize the computational complexity of these problems for subset minimal and cardinality minimal solutions.
Conjunctive Queries. Let V be a countably infinite set of variables. Expressions A(t) and P (t, t ) are called atoms, where t, t ∈ V ∪ C. A conjunctive query (CQ) q is an expression q(x 1 , . . . , x n ) ← a 1 , . . . , a m , where each a i , 1 ≤ i ≤ m, is an atom. Let V(q) denote the set of variables occurring in q, C(q) the set of constants in q, and let at(q) = 1≤i≤m {a i }. A match for q in an interpretation I is a mapping π : V(q) ∪ C(q) → ∆ I such that π is the identity on constants, π(t) ∈ A I for each 3 We ignore here the distinction between data values and objects, since it is immaterial for our results. As a consequence, we do not consider value domains and attributes, which are present in DL-LiteA.
Query answering over ontologies formulated in Description Logics (DLs) has received considerable attention both in research and industry. Given an ontology, users typically pose queries over the conceptual schema and get answers that take into account the constraints specified at the conceptual level. Many efforts have concentrated on lightweight description logics. For instance, DL-Lite A has been tailored for query answering over large data sets [7]. For this reason, expressive power is traded in favor of a better computational behavior in terms of data-complexity. In fact, conjunctive query answering in DL-Lite A enjoys FOL-rewritability, i.e., it can be reduced to the problem of evaluating a suitably constructed FOL query over a database instance.
In order to meet usability requirements set by domain users, most logic-based applications provide explanation algorithms for reasoning services. This holds also for DLs, where research focused on the explanation of both TBox reasoning [12,6,14,3] and, more recently, query answering [5]. In addition, the latter paper advocates the importance of tackling the problem of explaining the absence of a tuple in the answers to a query over an ontology. This problem stems from the database community, where it has been solved in the context of databases extended with provenance information [9]. We address this problem by considering explanations for the absence of a tuple in the context of query answering over DL-Lite A ontologies. We adopt abductive reasoning [10,11], that is, we consider which additions need to be made to the ABox to force the given tuple to be in the result. More precisely, given a TBox T , an ABox A, and a query q, an explanation for a given tuple t is a new ABox U such that the answer to q over T , A ∪ U contains t. An important aspect in explanations is to provide the user with solutions that are simple to understand and free of redundancy, hence as small as possible. To address this requirement, we study various restrictions on solutions, in particular, we focus on subset minimal and cardinality minimal ones. We consider standard decision problems associated to logic-based abduction: (i) existence of an explanation, (ii) recognition of a given ABox as being an explanation, and (iii) relevance and (iv) necessity of an ABox assertion, i.e., whether it occurs in some or all explanations. After motivating such problems and formalizing them, we provide algorithms to solve them and a precise characterization of their computational complexity for DL-Lite A . The complexity results for the various reasoning tasks are summarized in Table 1.
DL-Lite A . DL-Lite A is a member of the DL-Lite family of DLs [7], which have been designed for dealing efficiently with large amounts of extensional information. In DL-Lite A , concept expressions C, denoting sets of objects, and role expressions R, denoting binary relations between objects, are formed as follows:
where A denotes an atomic concept and P an atomic role 3 . In a DL-Lite A ontology O = T , A , the TBox T consists of axioms of the form
and the ABox A consists of assertions of the form A(c) and R(c, c ), where c, c are constants (or, individuals) from a countably infinite set C. An interpretation is a pair I = ∆ I , • I , where ∆ I is a non-empty domain, and the interpretation function • I is defined as usual. We adopt here the unique name assumption (UNA), i.e., c I 1 = c I 2 for all c 1 , c 2 ∈ C with c 1 = c 2 . We refer to [7] for more details. A(t) ∈ at(q), and π(t), π(t ) ∈ P I for each P (t, t ) ∈ at(q). The tuple x 1 , . . . , x n is the tuple of answer variables of q. The answer to q over I, denoted ans(q, I), is the set of all n-tuples d 1 , . . . , d n ∈ C n such that d I 1 , . . . , d I n = π(x 1 ), . . . , π(x n ) for some match π for q in I. A union of conjunctive queries (UCQ) is a set of CQs with the same answer variable tuple. For a UCQ q, we let ans(q, I) = q ∈q ans(q , I). The certain answer to a CQ or a UCQ q over O is defined as cert(q, O) = {c ∈ C n | c ∈ ans(q, I) for each model I of O}.
We now define the problem considered in this paper: Definition 1. Let O = T , A be an ontology, q a UCQ, and c a tuple of constants. We call P = O, q, c a query abduction problem (QAP). A solution to P (or an explanation for P) is any ABox U such that the ontology O = T , A ∪ U is consistent and c ∈ cert(q, O ). The set of all explanations for P is denoted expl(P).
∈ cert(q, O), then we call c a negative answer to q over O. Note that a query over the ontology can have a negative answer only if the ontology is satisfiable. Differently, if the ontology is unsatisfiable then the QAP P does not have any solution.
In the following, we will examine various restrictions to expl(P) to reduce redundancy in explanations. This is achieved by the introduction of a preference relation among explanations. This relation is reflexive and transitive, i.e., we have a pre-order among solutions.
Definition 2. Assume a QAP P. Let denote a pre-order on the set expl(P) of solutions. We write U ≺ U if U U and U U. The preferred explanations expl (P) of a QAP P under the pre-order are defined as follows: expl (P) = { U ∈ expl(P) | there is no U ∈ expl(P) s.t. U ≺ U }, i.e., expl (P) contains all the -explanations that are minimal under .
Two preference orders are considered here: the subset-minimality order, denoted by ⊆, and the minimum explanation size order, denoted by ≤. The latter order is defined by U ≤ U iff |U| ≤ |U |. Observe that expl ≤ (P) ⊆ expl ⊆ (P).
We define now four decision problems related to (minimal) explanations, which are parametric w.r.t. the chosen preference order . Given a QAP P:
--EXISTENCE: Does there exist a -explanation for P? --RECOGNITION: Is a set U of ABox assertions a -explanation for P? --RELEVANCE: Does an assertion α occur in some -explanation for P? --NECESSITY: Does an assertion α occur in all -explanations for P? In the following, whenever no preference is applied (i.e., when is the identity) we omit to write in front of the problem's names. We provide an example, in which we highlight the consequences of choosing among the various orderings. That is, there are two different kinds of students, PostGrad and UnderGrad . Moreover, PartTime students are tutored by Tutor s, who are particular professors. Additionally, the university offers some Advanced courses. Let the ABox A consist of the assertions teaches(rob, SWT ), hasTutor (peter , rob). Now, assume that a user is interested in finding all those who both teach an advanced course and tutor a student. Then, she would write the query q(x) ← teaches(x, y), Advanced (y), hasTutor (z, x).
Moreover, she may expect rob to be part of the result, i.e., rob ∈ cert(q, O), but this is not the case. Intuitively, rob satisfies all the constraints imposed by the query, except that the SWT course is not known to be Advanced . One can easily see that {teaches(rob, TOC ), Advanced (TOC ), hasTutor (john, rob)} is an explanation, {teaches(rob, ALG), Advanced (ALG)} is a ⊆-minimal explanation, while {Advanced (SWT )} is a ≤-minimal explanation.
In the next section, the complexity of the four main problems is studied in the light of the different preference relations.
Table 1 provides an overview of our complexity results. Recall that the class Σ P 2 is a member of the Polynomial Hierarchy [13]; it is the class of all decision problems solvable in non-deterministic polynomial time using an NP oracle. Moreover, the class P NP contains all the decision problems that can be solved in polynomial time with an NP oracle, where all oracle calls must be first prepared and then issued in parallel. The class DP contains all problems that, considered as languages, can be characterized as the intersection of a language in NP and a language in CONP [13]. Note that: PTIME ⊆ NP ⊆ DP ⊆ P NP ⊆ Σ P 2 is believed to be a strict hierarchy of inclusions and here we make such an assumption.
Our results can be explained as follows. We show in the next section that EX-ISTENCE can be reduced to the PTIME-complete satisfiability problem for DL-Lite A without the UNA [1], which justifies our PTIME upper bound. This result can then be used to characterize the complexity of RELEVANCE, NECESSITY, and ⊆-NECESSITY. ≤-RELEVANCE and ≤-NECESSITY are harder. The reason being that in order to solve these problems one has to compute first the minimal size of a solution and, then, inspect all the solutions of that size. Additionally, there is another increase in complexity when dealing with ⊆-RELEVANCE. The intuition is that there is an exponential number of candidate solutions to examine and for each of them one has to check that none of its subsets is itself a solution, which requires a CONP computation. Due to space limitations, the results on -RECOGNITION are not detailed in this paper (see [8] for more details). The intuition for the NP bound for RECOGNITION is that one needs simply to check consistency and perform query evaluation to solve the problem. In case a preference order is in place, one has to check minimality as well, which is a CONP check for ⊆and ≤-minimal explanations that leads to completeness for DP.
For -EXISTENCE note first that the existence of an explanation for P implies the existence of an explanation under the ⊆ and ≤ orderings. Thus, we only consider EX-ISTENCE. Our first task is to show that we can restrict ourselves to explanations built from the original signature of the input QAP plus a small number of fresh constants.
Proposition 1. If P = O, q, c has a solution, then P has a solution U with concepts, roles, and attributes only from O and at most m = max qi∈q |at(q i )| fresh ABox individuals.
Proof. Assume an arbitrary solution U to P. Given the consistency of O = T , A ∪ U , it follows that there exists a model I of O under the UNA. W.l.o.g. we assume that ∆ I = C with c I = c for each c ∈ C. Additionally, the interpretation I admits a match π for some q i (x) ∈ q, such that π(x) = c. Let U = {A(o) | A(t) ∈ at(q i ) and π(t) = o} ∪ {R(o, o ) | R(t, t ) ∈ at(q i ) and π(t) = o and π(t ) = o }. Observe that U has no more individuals than q i has variables. It remains to see that U is a solution. Clearly the original match π witnesses also c ∈ ans(q i , A ∪ U ). It remains to see that O = T , A ∪ U is consistent. But this follows from the fact that I is a model of O and that the atoms in U hold in I
The above restriction allows us to consider canonical explanations, i.e., explanations resulting from suitable instantiations of the bodies of CQs q i ∈ q. Keeping in mind that CQs, seen as FOL formulae, are always satisfiable, an explanation does not exist only if the structure of the query is not compliant with the constraints expressed in the ontology. That is, for all the interpretations J of q with ans(q, J ) = ∅, there is no model I of O, such that I ∪ J |= O. To check whether a UCQ is compliant with the ontological constraints, a naïve method is to iteratively go through all the CQs in q and instantiate them in the ABox. If for none of the CQs we obtain a consistent ontology, then the query violates some of the constraints imposed at the conceptual level.
Proposition 2. For DL-Lite A ontologies, EXISTENCE is PTIME-complete.
Proof. (MEMBERSHIP) Note that P = O, q, c , with q a UCQ, has a solution iff P q = O, q , c has a solution for some q ∈ q. Hence, it suffices to show the upper bound for CQs. To this end, we provide a logspace reduction from EXISTENCE to consistency in DL-Lite A without UNA, which in turn is PTIME-complete [1]. Assume a QAP P = O, q, c , where q is a CQ and O = T , A . We argue that P has a solution iff O = T ∪ T , A ∪ U q ∪ A is consistent, where O is an ontology obtained from O and q(c) as follows. The ABox U q is obtained from at(q(c)) by replacing each variable x with a fresh individual name a x . The ABox A consists of assertions A o (o) for all constants o occurring in T , A and U q , where each A o is a fresh concept name. The TBox T consists of axioms A o ¬A o for all pairs o = o of constants occurring in A and q(c). We now show that P has a solution iff O is consistent.
Assume that P has a solution U. Then, due to consistency of O = (T , A ∪ U), there is a model I of O under the UNA. Additionally, I admits a match π for q(c). Let I be the extension of I that additionally interprets (i) constants in U q as a I x = π(x) for all variables x in q, and (ii) A I o = {o I } for all freshly introduced A o . It remains to show that I is a model of O . Observe that since I is under the UNA, we have that
Thus I satisfies all the disjointness axioms A o ¬A o in T . The assertions in A are satisfied due to (ii), while the assertions in U q due to (i) above.
The other direction of the proof is obvious and we omit it here. (HARDNESS) Let us reduce consistency in DL-Lite A without UNA to EXISTENCE. Given O = T , A , we create QAP P = O , q(), simply by encoding the ABox A in the CQ q by replacing each constant a ∈ A by a distinct variable name x a in q, while the ontology O consists only of the TBox T .
The existence of an explanation is most of the times not very informative to the user. In fact, given a negative answer to a query, it is important to delineate the fundamental reasons leading to the absence of the expected tuple. That is, users would like to know which assertions occur in all the solutions to a QAP P. Proposition 3. For DL-Lite A ontologies, the NECESSITY and ⊆-NECESSITY problems are PTIME-complete.
Proof. (MEMBERSHIP) We assume a QAP P = O, q, c with O = T , A , an assertion ϕ(t) and consider NECESSITY first. This problem can be reduced to non-EXISTENCE, which was shown to be in PTIME in the previous section. We build O = T , A such that ϕ(t) occurs in all explanations for P iff P = O , q, c has no explanation. We define O by setting A = A ∪ { φ(t)} and T = T ∪ { φ ¬ϕ}, where φ is a fresh predicate name. It is easy to see that if P has no explanation, then either P has no explanation as well, or, all the explanations for P must contain ϕ(t). For ⊆-NECESSITY, observe that ϕ(t) occurs in all explanation for P iff ϕ(t) occurs in all ⊆-minimal explanations for P. Thus ⊆-NECESSITY can be decided in polynomial time using our algorithm for NECESSITY.
(HARDNESS) The lower-bound can be proved through a logspace reduction from EXISTENCE to non-NECESSITY, that is, deciding whether there exists a solution to a QAP that does not contain the given assertion. Let P = O, q, c be a QAP with q a CQ, we build P, α such that P has a solution iff P, α is a negative instance to NECESSITY. Let α = A(o), for some fresh concept A and constant o not occurring in P. Now, assume P has a solution U. By Proposition 1, we know that there exists a solution U to P containing only concept and role names from O. Hence, A(o) ∈ U , since concept name A is not in the ontology. Therefore, one can conclude that A(o) is not a necessary assertion to P.
The other direction is straightforward.
Let us now show the complexity of necessity under the ≤ preference order.
Theorem 1. For DL-Lite A ontologies, ≤-NECESSITY is P NP -complete.
Proof. (MEMBERSHIP only, HARDNESS in [8]) Let's assume a QAP P = O, q, c and an assertion α. By the use of canonical explanations, we know that the size m of the largest solution to P corresponds to the size of the largest CQ in q. Observe that (P, α) is a negative instance of ≤-NECESSITY iff there is an 0 ≤ i ≤ m such that (a) P has an explanation U with |U| = i and α ∈ U, and (b) U is ≤-minimal. Thus, we use an auxiliary problem SIZE-OUT, which is to decide given a tuple P , α , n , where P is a QAP, α is an assertion, and n is an integer, whether there exists an explanation U for P such that |U | = n and α ∈ U . Furthermore, the problem NO-SMALLER is to decide given a tuple P , n of a QAP and an integer whether there is no explanation U for P such that |U | < n . Observe that SIZE-OUT is in NP, while NO-SMALLER is in CONP. Take the tuple S = A 0 , B 0 , . . . , A m , B m , where (a) A i = (P, α, i), for all 0 ≤ i ≤ m, and (b) B i = (P, i), for all 0 ≤ i ≤ m. Due to the above observation, α occurs in all ≤-minimal explanations U for P iff for all 0 ≤ i ≤ m, one of the following holds: (i) A i is a negative instance of SIZE-OUT, or (ii) B i is a negative instance of NO-SMALLER. Note that S can be built in polynomial time in the size of the input, while the positivity of the instances in S can be decided by making 2m parallel calls to an NP oracle. Thus we obtain membership in P NP .
A domain user faced with a negative answer to a query may ask herself whether, the absence of a certain ABox assertion α in the ontology is related with the lack of the tuple in the results. That is, she would like to know whether α occurs in some explanation to QAP P.
Proposition 4. For DL-Lite A ontologies, RELEVANCE is PTIME-complete.
Proof. (MEMBERSHIP) We assume a QAP P = O, q, c with O = T , A and an assertion φ(t). We now provide a reduction from RELEVANCE to EXISTENCE. We construct O = T , A , where A = A∪φ(t). Then, P has an explanation U with φ(t) ∈ U iff there exists an explanation to P = (O , q, c). This is because, any explanation to P can be extended by adding φ(t). It is simple to see that any such explanation is an explanation to P, as well. Finally, if P does not admit explanations, then φ(t) is a source of inconsistency in P.
(HARDNESS) Hardness can again be proved with a reduction from EXISTENCE in a similar way as done in Section 4.2.
Let us now tackle the problem of ⊆-RELEVANCE, for which we recall the FOLrewritability of query answering in DL-Lite A . Given an ABox A, let DB(A) be the following interpretation: (i) ∆ DB(A) is the set of constants occurring in A, (ii) A DB(A) = {o ∈ ∆ DB(A) | A(o) ∈ A}, for each atomic concept A, and (iii) P DB(A) = { o, o ∈ ∆ DB(A) | P (o, o ) ∈ A}, for each atomic role P . Proposition 5 ([7]). Let PerfectRef(q, T ) be the perfect reformulation of q w.r.t. T , which is a UCQ obtained by applying the rewrite rules given in [7]. Then, cert(q, O) = r∈PerfectRef (q,T ) ans(r, DB(A)).
In other words, the certain answers to a UCQ can be computed by rewriting the query into a FOL query to be evaluated over the ABox.
Theorem 2. For DL-Lite A ontologies, ⊆-RELEVANCE is Σ P 2 -complete.
Proof. (MEMBERSHIP) The membership in Σ P 2 is clear from Algorithm 1, which works as follows. An explanation U containing φ(t) is non-deterministically computed by guessing an instantiation of a subquery in PerfectRef(q(c), T ), where Anon is a set of fresh ABox individuals (see Proposition 1). Let HAS-SUBEXPL solve the problem of deciding whether a solution U has a subset which is itself an explanation. The problem can be easily proved to be in NP. Then, the algorithm checks the complement of HAS-SUBEXPL in order to assure that none of the subsets of U is itself an explanation, from which it follows that φ(t) is ⊆-relevant. Checking the complement of HAS-SUBEXPL requires the power of a CONP machine. For this reason, the algorithm is solvable in non-deterministic polynomial time by a TM with an NP oracle.
(HARDNESS) We prove it by a reduction from the Σ P 2 -complete problem co-CERT3COL [15] (see also [4]). An instance of co-CERT3COL is given by a graph G = (V, E) with vertices V = {0, . . . , n − 1} such that every edge is labeled with a disjunction of two literals over the Boolean variables {p (i,j) | i, j < n}. G is a positive instance if there is a truth value assignment t to the Boolean variables such that the graph t(G) Algorithm 1
INPUT: QAP P = q, O, c and ABox assertion φ(t) OUTPUT: yes iff φ(t) is relevant to P 1: Guess qi ∈ {q1, . . . , qn} = q 2: Guess the derivation of one rewriting r(c) in PerfectRef(qi(c), T ) 3: Guess a set of atoms U ⊆ at(r) 4: Guess a mapping π from V(q) to constants in DB(A) and Anon 5: Check that (T , A ∪ U) |= ⊥, where U is the instantiation of U through π. 6: Check that φ(t) ∈ U and π is a match for r(c) over DB(A ∪ U) 7: Check that HAS-SUBEXPL (P, U) = no.
update. If this is the case, then q G can be matched in A G without the ABox from (A3), i.e. in the triangle part. Then t(G) is 3-colorable, which contradicts the assumption. "⇐" Let U be a ⊆-minimal explanation containing B(b). Due to the presence of q e1 ∪ . . . ∪ q e k in q G and the assumption, the role W p cannot occur in U for any proposition p. Since U is an explanation, by the definition of q and (A5) we have that A p (c p ) ∈ U or A p (c ¬p ) ∈ U for all propositions p. Since for any proposition p we have that A p occurs in q G with one and only variable z p , we know that exactly one of A p (c p ) ∈ U and A p (c ¬p ) ∈ U holds. Due to the atoms W p (z p , z p ) in q G , we also have that individuals of the form c p and c ¬p are the only ones that can get an A p label. Consider the assignment t defined as follows: t(e) = t if A p (c p ) ∈ U, and t(e) = f if A p (c ¬p ) ∈ U. It is not difficult to argue that t(G) is not 3-colorable and thus G is a positive instance of co-CERT3COL. Indeed, if t(G) was 3-colorable, Q should be mappable into the triangle part obtained in (A1)-(A3). Then U \ {B(b)} would be a smaller update, which would mean a contradiction. Note that the above lower bound holds already for empty TBoxes. Proposition 6. For DL-Lite A ontologies, ≤-RELEVANCE is P NP -complete.
Proof. (MEMBERSHIP only, HARDNESS in [8]) ≤-RELEVANCE can be tackled in a way similar to ≤-NECESSITY. In fact, the algorithm described in Theorem 1 can be modified in order to solve this problem. Let SIZE-IN solve the following problem: given a tuple P, α, n , where P is a QAP, α an assertion, and n an integer, decide whether there exists an explanation U, with |U| = n and α ∈ U. Then, we change the positivity condition of the ≤-NECESSITY algorithm as follows: α occurs in some ≤-minimal explanations U for P iff for some i, 0 ≤ i ≤ m, it holds that: (i) A i is a positive instance of SIZE-IN, and (ii) B i is a positive instance of NO-SMALLER. It is easy to see that SIZE-IN is solvable in NP, hence the whole problem is again in P NP .
In this paper we have provided the formalization of a new problem, namely the explanation of negative answers to user queries over ontologies. A tuple is said to be a negative answer, if the user expects it to be part of cert(q, O) but the tuple is actually not. In our framework, an explanation consists of an ABox that when added to the ontology leads the negative answer to be returned in the results of the query. We define various problems that help us in characterizing the complexity of finding explanations, such as the existence of explanations and relevance/necessity of assertions. We further consider a minimality criterion to be applied over explanations, such as subset-minimal and minimum-size preference orders. Within this framework, we provide a characterization of the computational complexity of the various problems for the DL DL-Lite A .
Future work includes studying the application of this framework to other lightweight description logics, starting with the EL-family. We would also like to investigate the problem in the case where the ontology signature and the explanation signature may be different. That is, the signature over which explanations can be constructed is restricted only to a subset of the ontology signature [2].
obtained from G by including only those edges whose label evaluates to true under t is not 3-colorable. Assume an instance G of co-CERT3COL. We show how to build in polynomial time a QAP P G = (T G , A G ), q G , c G and an ABox assertion α G such that: G is a positive instance of co-CERT3COL iff α G is ⊆-relevant for P G . We use an empty TBox and a Boolean query, thus T G = ∅ and c G = . The query q G is a UCQ q G = q e1 ∪ • • • ∪ q e k ∪ q , where {e 1 , . . . , e k } = E, each q ei is an atomic query q ei () ← W ei (x, y), and q is defined as follows. Assume B = {t, f } to be the set of truth values. The query q has the following atoms for each edge e = (i, j) in E: (a) B(x i ), R e (x i , y e ), R e (y e , x j ), B(x j ), and (b) P (y e , z pi ), A pi (z pi ), W pi (z pi , z pi ), where p i ∈ {p 1 , p 2 } and p 1 , p 2 are the first and the second proposition in the labeling of e, respectively. The query q simply incorporates G together with the disjunctions on the edges. Observe that if two edges have the same proposition in their label, then this will be reflected in q by some shared variables z pi .
To build A G we use individuals c p and c ¬p for the truth value of proposition p. Intuitively, the truth value of p will be determined by either A p (c p ) or A p (c ¬p ) being in the update. Assume a tuple t = e, v 1 , v 2 , a, b , where e ∈ E, {v 1 , v 2 } ⊆ B, and a, b are individuals. Let p 1 , p 2 be the first and the second propositions of e. For i ∈ {1, 2} and v i = t , let l i = p i if p i is positive and l i = ¬p i otherwise. Similarly, for i ∈ {1, 2} and v i = f , let l i = ¬p i if p i is positive and l i = p i otherwise. Then, the ABox A(t) consists of the assertions R e (a, d T ), R e (d T , b), P (d T , c l1 ) and P (d T , c l2 ) depending on the boolean values in input.
The ABox A G is the union of the following ABoxes: (A1) A( e, v, v , a i , a j ) for all e ∈ E, v, v ∈ B, 0 ≤ i, j ≤ 2, and i = j; (A2) A( e, f, f, a i , a i ) for all e ∈ E, and 0 ≤ i ≤ 2; Let α G = B(b). It is not too difficult to see that G is a positive instance of co-CERT3COL iff there exists an ⊆-explanation U to P such that α G ∈ U. Basically, definitions (A1)-(A3) encode a triangular structure T in which edges in G that evaluate to false according to a given truth assignment can be mapped on any edge of T , reflexive edges included. If an edge of G evaluates to true, then it must be mapped to one of the non-reflexive edges. This ensures that if G can be mapped to T under truth assignment t, then t(G) is 3-colorable. Instead, definitions (A4)-(A5) define a cyclic structure C into which any graph G can be embedded. It has to be noted that the node b is not asserted to be a member of B, hence q G cannot be mapped there directly with any truth assignment. We see this more formally next: "⇒" Suppose there is a truth assignment t such that t(G)
It remains to argue that U is a ⊆-explanation to P. It is not hard to see that U is an explanation. Indeed q G matches already in the ABox obtained by point (A3) (hint: since B(b) ∈ U, we match q G by mapping all variables of q G to (interpretation of) b). Suppose there is a smaller update U ⊂ U. Observe that U 1 ⊆ U . This is because for all propositions p, the symbol A p does not occur in A G but does occur in q G . Then, U \ {B(b)} must be an