Effective Query Rewriting with Ontologies over DBoxes

1 Introduction

We address the problem of concept query answering on databases with ontologies. An ontology provides a conceptual view of the database and it is composed by constraints on a vocabulary extending the basic vocabulary (tables and attributes) of the data. Querying a database using the terms in such a richer ontology allows for more flexibility than using only the basic vocabulary of the relational database directly.

Description Logics [Baader et al., 2007] (DLs) are a prominent formalism for representing ontologies. However, DLs such as ALC or OWL or DL-lite were not originally developed with this use case in mind. In particular, the data in a DL knowledge base is represented using an ABox, which can be seen as an incomplete database. This means the extensions of the concepts and roles contain at least the data mentioned in the ABox, but may contain additional data, and this may vary among the models of the knowledge base. This is in contrast to relational databases, which are complete: the extensions of the predicates (i.e., the tables) contain exactly the data in the database and nothing more.

We introduce in this paper the notion of a DBox, which is syntactically similar to an ABox; it is a set of ground atomic concept and role assertions. However, semantically it behaves like a database, i.e., the extensions of the concepts and roles mentioned in the DBox are exactly defined by the contents of the DBox. We call the concepts and roles appearing in the DBox the DBox predicates. Observe that the DBox predicates are closed, i.e., their extensions are the same in every interpretation, whereas the other predicates in the knowledge base are open, i.e., their extensions may vary among different interpretations. This has been called also locally closed world [Etzioni et al., 1997] or exact views [Abiteboul and Duschka, 1998; Segoufin and Vianu, 2005; Nash et al., 2007].

The queries we consider in this paper are concept expressions (and the answers are their instances), and the ontologies are general ALC TBoxes. Our goals are (i) to check whether the answers to a given query under a TBox are solely determined by the extension of the DBox predicates and, if so, (ii) to find an equivalent rewriting of the query in terms of the DBox predicates to allow the use of standard database technology for answering the query. This means we benefit from the low computational complexity in the size of the data of answering first-order queries on relational databases. In addition, we would like as much as possible to use standard techniques for DL reasoning to find rewritings. As was pointed out recently also by Marx [2007], (i) corresponds to implicit definability [Tarski, 1956], and can be reduced to checking entailment and (ii) corresponds to explicit definability [Beth, 1953]. Inspired by the results of Craig [1957], this problem can be reduced to finding an interpolant.

Our contributions in this paper are as follows:

• We introduce the notion of DBoxes as a faithful encoding of databases, and show how to find a query rewriting over DBoxes, using Beth definability and interpolation;
• we present a procedure for calculating interpolants of ALC concepts under general TBoxes, using an adaptation of standard DL tableau techniques;
• we extend the procedure to deal with common tableau optimisation techniques found in implemented systems, in particular, non-atomic closure, semantic branching, lazy unfolding and absorption, and backjumping; and
• we show how abduction techniques can be used for amending TBoxes to gain definability of queries of interest.

2 ALC and DBoxes

ALC TBoxes. Let NC and NR be countably infinite sets of concept and role names, respectively. The set of ALC concepts is the smallest set that includes the atomic concepts NC ∪ {⊤}, and if C, D are concepts and R ∈ NR, then ¬C, C ⊓ D, and ∀R.C are concepts. As usual, ⊥, C ⊔ D, and ∃R.C are short for ¬⊤, ¬(¬C ⊓¬D), and ¬∀R.¬C, respectively. An ALC TBox T is a finite set of axioms of the form C ⊑ D, where C and D are ALC concepts.

An interpretation I is a pair 〈ΔI , ·I 〉 where ΔI is a nonempty set and ·I is a function that maps concept names A to subsets AI of ΔI and role names R to binary relations RI on ΔI ; ·I extends to concepts as follows: ⊤I = ΔI ; (¬C)I =ΔI \CI ; (C ⊓ D)I = CI ∩DI ; and (∀R.C)I = {δ ∈ ΔI | ∀δ′ (〈δ, δ′ 〉 ∈ RI → δ′ ∈ CI )}.

I is a model of a TBox T , written I |= T , iff CI ⊆ DI for all axioms C ⊑ D ∈ T . Since C ⊑ D is equivalent to ⊤ ⊑ ¬C ⊔ D, we assume that all axioms in T are of this form. We can thus view the TBox as a set of universal concepts {C | ⊤ ⊑ C ∈ T }.

A concept C is satisfiable w.r.t. T iff there is some model I of T such that CI ̸= ∅; D subsumes C w.r.t. T , written C ⊑T D, iff CI ⊆ DI for all models I of T . We write C ≡T D if CI ⊆DI and DI ⊆ CI .

For ease of presentation, we assume all concepts to be in negation normal form (NNF), which means the negation signs appear only in front of atomic concepts. The negation normal form of the complement of a concept C is written ˙¬C.

With sig(C) (resp. sig(T )) we denote the set of all concept and role names occurring in C (resp. T ), i.e., the signature of C (resp. T ). With sig(C, T ) we denote the set of all concept and role names occurring in C or T .

DBoxes. Let NI be a countably infinite set of individual names. A DBox D is a set of assertions of the forms A(a) and R(a, b), where A ∈ σD(C), R ∈ σD(R), and a, b ∈ σD(I). The signature σD of D consists of the DBox concepts σD(C) ⊆ NC, the DBox roles σD(R) ⊆ NR, and the DBox individuals σD(I) ⊆ NI; we call DBox predicates the set σD(P) = σD(C) ∪ σD(R). The active domain of D is the set of individuals in σD(I) appearing in the assertions of D.

An interpretation I = 〈ΔI , ·I 〉 is a model of D, written I |= D, iff aI = a for every DBox individual a ∈ σD(I), and for every concept (resp., role) name P in σD(P) and every u ∈ ΔI (resp., (u, v) ∈ ΔI ×ΔI ), we have that u ∈ P I iff P(u) ∈ D (resp., (u, v) ∈ P I iff P(u, v) ∈ D). In other words, in every model of D the extensions of the DBox predicates are given by the contents of the DBox, and are the same in every model. Please note that the domain ΔI of a model of D is not fixed, but it includes all the DBox individuals in σD(I), which in turn includes the active domain of D.

A DBox D is satisfiable with respect to a TBox T iff there is a model of D that is also a model of T . An interpretation I is a model of C(a), where C is a concept and a an individual name, written I |= C(a), iff aI ∈ CI . A pair (T , D) entails a membership expression C(a) - this is the instance checking problem, or concept querying problem - written (T ,D) |= C(a), iff for every model I of T and D it holds that I is a model of C(a). Finally, D entails C(a), written D |= C(a), iff (∅,D) |= C(a).

The unique names assumption (UNA) holds for a DL L if for any interpretation I considered in L , aI ̸= bI whenever a ̸= b, for any two a, b ∈ NI . If we assume UNA, reasoning in a DL with DBoxes can be reduced to reasoning in the same DL extended with nominals - i.e., concept expressions of the form {a}, where a is an individual name, such that {a}I = {aI } - and vice versa.

Proposition 1. Given a description logic L with UNA that includes ALC, for every DBox D and TBox T in L there exists a TBox T D in L extended with nominals with size polynomially bounded by the size of T ∪D, such that D is satisfiable with respect to T iff T D is satisfiable, and vice versa.

Proof sketch. (⇒) T D is obtained fromT by adding completion and closure axioms. For every DBox concept A add the axiom A ≡ {a1}⊔· · ·⊔{an}, such that A(a1), . . . , A(an) are the assertions involving A in D. For every DBox role R add the axioms {ai} ⊑ ∃R.{bj}, {ai} ⊑ ∀R.{b1} ⊔ · · · ⊔ {bn}, and ∃R.⊤ ⊑ {a1} ⊔ · · · ⊔ {am}, such that R(ai, bj) for i = 1, · · · ,m and j = 1, · · · , n are the assertions involving R in D.

(⇐) For every occurrence of {a} in T D , the assertion Aa (a) is added to D, where Aa is a new DBox concept name, and every occurrence of {a} in T D is replaced with Aa .

Please note that this reduction encodes the entire DBox into a TBox, and that, although concept querying in ALCO has the same combined complexity as in ALC, if we consider more expressive logics such as SHIQ we do get an increase in combined complexity when nominals are added (from EXPTIME to NEXPTIME). It can also be shown that the data complexity of query answering with DBoxes (i.e., with closed data predicates) is at least as hard as query answering with ABoxes (i.e., with open data predicates), and that it is strictly harder if we consider conjunctive query answering in simple description logics such as DL-lite (it increases from LOGSPACE to CONP-hard, which can be shown by a reduction from non-existence of 3-colourings).

3 Definability and Query Answering

We introduce in this Section implicit and explicit definability for queries, and discuss how explicit definitions can be used for concept query rewriting. In the following, given a TBox T and a DBox D, let Q be a query concept (i.e., a query asking for all the instances of the concept) and let sig(Q, T ) = {B1, . . . ,Bm,D1, . . . ,Dn} be the combined signature where {D1, . . . ,Dn} ⊆ σD(P) and {B1, . . . ,Bm} ∩ σD(P) = ∅; {D1, . . . ,Dn} is the set of DBox predicates appearing in T or in Q.

Definition 1 (Implicit definability). Let a concept ϕ′ (resp. a TBox T ′ ) be like ϕ (resp. T ) but with occurrences of B1, . . . ,Bm replaced by distinct occurrences of B′1 , . . . ,B′m ̸∈ sig(Q, T ). Then, Q is implicitly definable from D1, . . . ,Dn in T iff Q ≡T ∪T ′ Q′ .

In other words, given a TBox, a concept Q is implicitly definable if the set of all its instances depends only on the extension of the DBox predicates. This means that it may be possible to find an expression using only predicates in the DBox whose instances are the same as in the original concept: this would be its explicit definition.

Definition 2 (Explicit definability). Q is explicitly definable from D1, . . . ,Dn in T iff there is some concept C such that Q ≡T C and sig(C) ⊆ {D1, . . . ,Dn}.

Clearly, explicit definability implies implicit definability. Beth [1953] shows that the converse also holds for the case of first-order logic: if Q is implicitly definable fromD1, . . . , Dn in T , then it is explicitly definable. To prove this property for ALC with general TBoxes, we exploit interpolation.

Lemma 1 (Interpolation for ALC with TBoxes). Let Q be an ALC concept and let T be an ALC TBox such that Q ⊑T ∪T ′ Q′ , where Q′ and T ′ are obtained as above. Then, there exists some concept C, called the interpolant of Q and Q′ under T and T ′ , such that sig(C) ⊆ sig(Q, T ) ∩ sig(Q′ , T ′ ), Q ⊑T ∪T ′ C, and C ⊑T ∪T ′ Q′ .

Theorem1 (Beth Definability for ALC with TBoxes). If Q is implicitly definable fromD1, . . . , Dn in T then Q is explicitly definable fromD1, . . . ,Dn in T .

Proof. We have that Q ≡T ∪T ′ Q′ . Now, by Lemma 1 there is an interpolant C of Q and Q′ under T and T ′ . Since it is an interpolant, sig(C) ⊆ sig(Q, T ) ∩ sig(Q′ , T ′ ) ⊆ {D1, . . . ,Dn}, and both (a) Q ⊑T ∪T ′ C and (b) C ⊑T ∪T ′ Q′ . By (a) and Q′ ⊑T ∪T ′ Q, we have C ⊑T ∪T ′ Q, from which Q ≡T ∪T ′ C follows by (b). From the structure of T ′ and the fact that sig(Q), sig(C) ⊆ sig(T ) straightforwardly follows that Q ≡T C.

This proof of Beth definability for ALC with general TBoxes is constructive, provided we have a constructive method of finding interpolants as defined in Lemma 1. In Section 4 we present such a method, and we prove its correctness and completeness.

We can now combine these results to reduce answering definable queries to query answering using only the DBox.

Theorem 2. Let D be a DBox that is satisfiable with respect to a TBox T , let Q be a concept and let a ∈ σD(I) be a DBox individual. If Q is implicitly definable from σD(P), then there is an ALC concept C with sig(C) ⊆ σD(P) such that (T ,D) |= Q(a) iff D |= C(a).

To enable rewriting C(a) to standard database query languages we first need to prove its domain independence.

Definition 3 (Domain independence). Let C be a concept and let a be an individual name. C(a) is said to be domain independent if for every interpretation I = 〈ΔI , ·I 〉 such that I |= C(a) it is the case that I ′ |= C(a) for every interpretation I ′ = 〈ΔI′ , ·I′ 〉 with ΔI′ ⊇ΔI and ·I = ·I′ .

Theorem 3. Let C be an ALC concept and let a be an individual name. Then, C(a) is domain independent.

Proof sketch. Let I = 〈ΔI , ·I 〉 and I ′ = 〈ΔI′ , ·I′ 〉 be two interpretations as in Definition 3, and let δ be in both ΔI and ΔI′ . We will show by induction on the structure of concept D in negation normal form that δ ∈ DI implies δ ∈ DI′ .

The atomic cases are trivial: if D = A or D = ¬A, for some atomic concept A, clearly δ ∈ DI iff δ ∈ DI′ , since AI = AI′ . Suppose now D = C1 ⊓ C2. By the inductive hypothesis, δ ∈ (C1)I implies δ ∈ (C1)I′ , and δ ∈ (C2)I implies δ ∈ (C2)I′ . But then δ ∈ (C1 ⊓ C2)I implies δ ∈ (C1 ⊓ C2)I′ . Analogous for when D = C1 ⊔ C2. Suppose D = ∃R.E. Since RI = RI′ , there is some δ′ ∈ ΔI such that 〈δ, δ′ 〉 ∈ RI iff δ′ ∈ ΔI′ and 〈δ, δ′ 〉 ∈ RI′ . Moreover, by the induction hypothesis we have that δ′ ∈ EI implies δ′ ∈ EI′ . Analogous for D = ∀R.E.

Consider a query C(a) with a ∈ σD(I) and sig(C) ⊆ σD(P). Since C(a) is domain independent, deciding D |= C(a) can be reduced to checking aI ∈ CI for an arbitrary model I of D; in particular we choose the smallest model I D = 〈ΔID , ·ID 〉 of D, where ΔID is equal to the set of the DBox individuals in σD(I) and ·ID considers only the set of DBox assertions. In other words, the entailment check reduces to model checking over I D and a standard database query language over the DBox database can be used for deciding D |= C(a).

Given a query concept Q, a TBox T , and a DBox D, in order to find the answer set {a | (T ,D) |= Q(a)} by means of the rewriting {a | D |= C(a)}, one can use the equivalent database query Q(x) :- C FO(x) ∧ ⊤D(x) over the database D, where CFO is the standard first order translation of C and ⊤D is the relation containing exactly the DBox individuals σD(I). It is possible to pre-compute offline the rewriting of all definable atomic concepts in the ontology as materialised SQL views, so that at run time query answering on ALC ontologies with DBoxes is reduced to answering SQL queries over the DBox database with materialised views.

4 Constructive Interpolation for ALC

Fitting [1983] and Rautenberg [1983] give constructive proofs using symmetric Gentzen systems, respectively tableau calculi. Schlobach [2004] provides an algorithm for calculating interpolants between ALC concepts; however, he does not consider TBoxes, nor does he provide a reference with standard or optimised implemented tableau algorithms.

Let NV be a countably infinite set of variable names and < a well-order relation on NV . A biased constraint is an expression of the form (x : D)λ where x ∈ NV , D is a concept, and λ ∈ {l, r} is a bias. A biased constraint system S for 〈C, T 〉 is a finite, non-empty set of biased constraints.

We say a variable x ∈ NV is in S if S contains a mention of x; x is fresh for S if x is not in S and y < x for all y in S. We assume that when a variable x is in S, the constraints (x : ⊤)l , (x : ⊤)r are also in S.

Let x be a variable in S. The set of x-constraints of S is defined as {x : C ∈ S}. For a role name R, with succ(x, R, S) we denote the set {Cλ | (x : ∀R.C)λ ∈ S}. If X is a set of labelled concepts, then x : X is a shorthand for {(x : C)λ | Cλ ∈ X}.

S is said to contain a clash if for some variable x and some concept name A, {(x : A)λ , (x : ¬A)κ} ⊆ S.

The R⊓ rule

The R⊔ rule

The R∃ rule

Condition: (x

: ∃R.C)λ ∈ L(g), there is no variable y in L(g)

such that y

Effect: L(g′ ) =

: {Cλ } ∪ succ(x, R, S) ⊆ L(g)

L(g) ∪ y

: {Cλ } ∪ succ(x, R, S) ∪ T ,

where y is fresh for S

Figure 1: Biased completion rules for ALC

Let H, J be ALC concepts and T = T l ∪T r a set of biased concepts with T l being l- and T r being r-labelled concept. A biased tableau for 〈H ⊓ ˙¬J, T 〉 is a triple T = 〈V, E, L〉, where 〈V, E〉 is a finite tree, with g0 ∈ V being the root node, and L is a labelling function associating with each node g ∈ V a biased constraint system for 〈H ⊓ ˙¬J, T 〉 and with each edge 〈g, g′ 〉 ∈ E a biased completion rule Rχ from Figure 1. In addition, we require L(g0) = x0 : {Hl }∪{( ˙¬J)r }∪T ∪ T ′ . A biased tableau T0 for 〈H ⊓ ˙¬J, T 〉 that contains only the root node is called the initial biased tableau for 〈H ⊓ ˙¬J, T 〉. A completion rule is applicable in a node g if its condition is satisfied in g.

A branch of a tableau is a path from the root down to a leaf. If in a tableau there is some successor g′ of g such that L(〈g, g′ 〉) = R⊔, then g is called a branching point in the tableau. A branch is closed if the label of its leaf node contains a clash; otherwise it is open. A tableau is closed if all its branches are closed; otherwise it is open. A tableau is complete if no completion rule is applicable in the leaf nodes of any of its open branches.

The biased tableau algorithm takes as input the initial biased tableau T0 for 〈H ⊓ ˙¬J, T 〉. T0 is then expanded by repeatedly applying the completion rules given in Figure 1 with the following strategy: R∃ is applied only when R⊔ is not applicable which in turn is applied only when R⊓ is not applicable. If the obtained complete tableau is closed, the algorithm returns false, otherwise true.

If the biased tableau algorithm returns false, then a second phase is initiated to extract an interpolant I.

Definition 4. Let g be a node in a tableau and let {(x : C1)l , . . . , (x : Cn)l , (x : D1)r , . . . , (x : Dm)r } be the xconstraints of L(g). A concept I is called an interpolant for this set under T if I is an interpolant for C1 ⊓ . . . ⊓ Cn and ¬D1 ⊔ . . . ⊔ ¬Dm under T l and T r . (Take the empty intersection to be ⊤ and the empty union to be ⊥.)

Let C and D be concepts. We define the binary infix operator ·⊔ as follows: C ·⊔ D = C ⊔ D, C ·⊔ ⊥ = ⊥ ·⊔ C = C, C ·⊔ null = null ·⊔ C = C, and null ·⊔ null = null. If ht1 and ht2 are hash tables, ht′ = ht1 ·⊔ ht2 is defined as: ht′ (x) = ht1(x) ·⊔ ht2(x), for every variable x. The operator ·⊓ is defined analogously.

Interpolants at nodes g are stored in hash tables int(g).

Figure 2: Atomic interpolant calculation rules for ALC

Figure 3: Propositional interpolant calculation rules for ALC

Every key in int(g) is a variable in L(g) and every value is a concept or the special symbol null. With int(g)(x) we denote the value associated with the key x. The algorithm used in the second phase starts from the leaves of the tableau tree and applies the interpolant calculation rules Cχ(λ) in Figures 2, 3, and 4, which are if-then rules. If the rules do not assign a value, it is assumed to be null.

We need to show that our interpolant calculation algorithm is correct and that it terminates. The latter is a consequence of the complete tableau being finite, which in turn is a consequence of our tableau calculus being a decision procedure for ALC [Baader et al., 2007]. We show correctness in two steps: first we prove that our interpolant calculation rules are sound, i.e., they compute interpolants; second we prove completeness, i.e., that we always find an interpolant.

Lemma 2 (Soundness). Let T be a closed biased tableau for 〈H ⊓ ˙¬J, T 〉, g a node in the tableau, and x a variable in L(g). If int(g)(x) is not null, it is an interpolant for the x-constraints of L(g).

Proof sketch. We proceed by induction on the tableau tree. For each leaf node g, L(g) must contain a clash involving some variable x. Assume (x : A)l , (x : ¬A)r ∈ L(g), then clearly · · · ⊓ A ⊑T A ⊑T · · · ⊔ A, and so int(g)(x) = A is an interpolant; similar for the other atomic rules.

For reasons of space we further only show soundness of C∃(l). We have that y is not in L(g). For any other variable z ̸= x, we have that int(g)(z) is an interpolant, by induction. If int(g′ )(y) = null, int(g)(x) must be an interpolant (if it is not null): if X ⊑T int(g)(x), then clearly X ⊓ ∃R.C ⊑T int(g)(x). Now assume int(g′ )(x) = null and int(g′ )(y) ̸= ⊥. If (y : D)λ ∈ L(g′ ) for some concept D ̸= C, either (x : ∀R.D)λ ∈ L(g) or (D)λ ∈ T .

Figure 4: Modal interpolant calculation rules for ALC

In the former case we have that C ⊓ D ⊑T int(g)(y) implies ∃R.C ⊓ ∀R.D ⊑T ∃int(g)(x) and int(g′ )(y) ⊑T ¬D implies ∃R.int(g′ )(y) ⊑T ¬∀R.D. For the latter case, observe that ∀R.D ≡T ⊤. The cases int(g′ )(x) ̸= null and/or int(g′ )(y) = ⊥ can be shown analogously.

Lemma 3 (Completeness). Let T be a closed biased tableau for 〈H ⊓ ˙¬J, T 〉 with root node g0. Then, int(g0)(x0) ̸= null.

Proof sketch. Since our biased tableau algorithm is sound and complete, H ⊑T J iff there exists a closed biased tableau T = 〈V, E, L〉 for 〈H ⊓ ˙¬J, T 〉. Since T is closed, all labels of its leaves contain clashes. Let g be such a leaf. Then, there is some y in L(g) such that {y : A, y : ¬A} ⊆ L(g) and y is introduced by a (possibly empty) series of R∃ applications. Clearly, int(g)(y) ̸= null. One can verify by induction on the rule applications that int(g0)(x0) ̸= null.

We are now ready to prove interpolation for ALC with general TBoxes.

Proof of Lemma 1. Let T l = {Cl | C ∈ T } and T r = {Cr | C ∈ T ′ }. By Lemma 3 we have that int(g0)(x0) is an interpolant for the x0-constraints of L(g0) under T l ∪ T r . But L(g0) = x0 : {Hl }∪{( ˙¬J)r }∪T l ∪T r and so int(g0)(x0) is an interpolant for H and J under T and T ′ .

Finally, we remark that the interpolant calculation algorithm can be made more space-efficient by integrating it into the satisfiability checking algorithm (one-pass) and generating the tableau in a depth-first manner: interpolants are constructed for each subbranch while backtracking, so that the subbranch may be discarded from memory before exploring the next subbranch. Interpolants are combined at the branching points using the C⊔(λ) rule. Please note that, in this way, the final algorithm to compute the interpolant can be obtained by simply adorning a standard tableau algorithm for ALC.

5 Integrating Tableau Optimisations

In this section, we extend the tableau algorithm with commonly used optimisations, which can be applied to the onepass algorithm sketched above, so that the process to compute the interpolant is just an adorned variant of the standard and optimised implemented tableau algorithm for ALC.

Figure 5: Interpolant calculation rules for non-atomic clashes

Non-atomic Closure. One can relax the definition of the closure condition for a tableau such that a constraint system S is said to contain a clash if for some variable x and some concept C, {x : C, x : ˙¬C} ⊆ S. For example the unsatisfiability of the constraint system S ⊇ {C ⊓ D, ˙¬(C ⊓ D)} can be detected without branching for ˙¬(C ⊓ D). Figure 5 depicts the calculation rules for non-atomic clashes, replacing the ones in Figure 2. Correctness is proved analogously to the atomic case.

Semantic Branching. The standard definition of R⊔ (cf. Figure 1), which is based on syntactic branching, does not prevent the recurrence of unsatisfiable disjuncts in different branches of the tree. Semantic branching is a technique that allows the subtrees introduced by non-deterministic rules to be distinct in the sense that the satisfiability of a disjunct is searched only in a single subtree [Horrocks, 2003]. This requires a slight change in the R⊔ rule: the second effect becomes L(g′′ ) = L(g) ∪ {x : ˙¬C1, x : C2}, obtaining the new rule R⊔′ . Replacing R⊔ with R′⊔ in our tableau calculus requires modifying the third condition of C⊔(λ) in Figure 3 with L(g′′ ) = L(g) ∪ {(x : ˙¬C1)λ , (x : C2)λ}. However, the way the interpolants are calculated does not change.

Lazy Unfolding and Absorption. Absorption is a TBox rewriting technique that has been developed to address the problem of the high level of non-determinism caused by general TBox axioms [Horrocks, 2003]. Being a rewriting technique, absorption of general axioms into simple axioms is performed before the satisfiability algorithm starts. For this reason, we are only concerned here with the structure of the output TBox. Given a general TBox T , the absorption process rewrites and partitions T into the general TBox TG and the unfoldable TBox TU [Horrocks, 2003] such that a concept is satisfiable w.r.t. T iff it is satisfiable w.r.t. TU ∪ TG.

The implicit definability problem takes as input two TBoxes T and T ′ . Therefore, we assume w.l.o.g. that the absorption process is only applied to T , resulting in TU and TG, and T ′U and T ′G are obtained analogously to T ′ . R∃ is modified to use only TG and T ′G and, in addition, we need the rules in Figure 6 that handle unfoldable TBoxes. In the literature, these rules constitute what is known as the lazy unfolding optimisation [Horrocks, 2003].

To complement these rules we use the interpolant calculation rules given in Figure 7. One needs to verify the soundness of these rules. We show only CU1(l) for TU. Suppose X = {(x : C1)l , . . . , (x : Cn)l , (x : D1)r , . . . , (x : Dm)r }, g′ is the result of applying RU1 to g for A ≡ C ∈ TU, and X ∪ {(x : A)κ , (x : C)l } are the x-constraints of L(g′ ).

The RU1 rule

Condition: (x

(x

:

:

A)κ ∈ L(g), A

C)l ̸∈ L(g) (or (x

Effect: L(g′ ) =

L(g) ∪ {(x

The RU2 rule

Condition: (x

:

≡

:

C is in TU (or T ′U), and

C)r ̸∈ L(g))

C)l } (or {(x

: ¬A)κ ∈ L(g), A

(x

:

≡

˙¬C)l ̸∈ L(g) (or (x

:

:

C)r })

C is in TU (or T ′U), and

˙¬C)r ̸∈ L(g))

The RU3 rule

Figure 6: Lazy unfolding rules

Note that although κ may not be equal to l, we can assume w.l.o.g. that κ = l since A ∈ sig(TU). By our assumption, int(g′ )(x) is an interpolant for the x-constraints of L(g′ ) and by Definition 4, A ⊓ C ⊓ C1 ⊓ . . . ⊓ Cn ⊑T int(g′ )(x) ⊑T ¬D1 ⊔ . . . ⊔¬Dm. CU1 assigns int(g′ )(x) to int(g)(x). We have that (i) A ⊓ C1 ⊓ . . . ⊓ Cn ⊑T int(g′ )(x) follows from (A ⊓ C ⊓ C1 ⊓ . . . ⊓ Cn)I = (A ⊓ C1 ⊓ . . . ⊓ Cn)I , for all models I of T , since A ≡ C ∈ TU and (ii) int(g′ )(x) ⊑T ¬D1 ⊔ . . . ⊔ ¬Dm follows from the fact that L(g) has the same r-labelled x-constraints as L(g′ ).

Backjumping. Our tableau decision procedure for ALC, upon discovering a clash, backtracks to the last branching point to which R⊔ is applicable. Blindly progressing in this way may be very inefficient if the given concept causes a lot of branching but the source of unsatisfiability does not depend on this branching (cf. [Horrocks, 2003]). Backjumping addresses this problem by identifying the causes of clashes and it is one of the most effective optimisation techniques, along with absorption + lazy unfolding, to deal with nondeterminism. It works by associating a constraint to a branching point in the tableau such that the introduction of the constraint depends on that branching point. Because of this, tableau rules are equipped with dependency propagating information [Horrocks, 2003]. When a clash {x : A, x : ¬A} is discovered, the dependencies of both of these constraints are combined, and the algorithm backjumps to the deepest branching point in the set. As a consequence, backjumping is an optimisation that modifies the shape of the tableau generated by the satisfiability checking algorithm by eliminating redundant branches from the tree. For this reason, no modification is required in our interpolant calculation rules.

6 Abduction

In our framework, finding the rewriting of a query in terms of the DBox predicates is possible only if the query is implicitly definable. However, not always a given query concept is implicitly definable given a TBox. To gain definability of queries of interest, it is necessary to modify the ontology by adding axioms to the TBox such that they become implicitly definable. We propose to use techniques from the area of abduction to find such axioms.

[Colucci et al., 2004; Elsenbroich et al., 2006] define abductive reasoning tasks in DLs. Among these, we consider

Figure 7: Lazy unfolding interpolant calculation rules

TBox abduction problems.

Definition 5 (TBox Abduction Problem). Let T be a TBox, and let C and D be concepts such that both are satisfiable w.r.t. T and C ̸⊑T D. A TBox abduction problem (TAP) is denoted by 〈T ,C,D〉. A TBox TA is a solution to a TAP 〈T , C, D〉 if T ∪ TA is satisfiable and C ⊑T ∪TA D.

We look for solutions with particular syntactic shapes.

Definition 6 (Sub-concept Solution). Let P = 〈C,D, T 〉 be a TAP. We say that a solution TA to P is a sub-concept solution to P iff TA is a set of axioms of the form E1 ⊑ ¬E2, where concepts E1, E2 are sub-formulae of C, D, or T .

Since the concepts in sub-concept solutions appear in the abduction problem, we conjecture that such amendment to the TBox are more easily understandable than amendments involving arbitrary concepts. Moreover, among sub-concept solutions we identify semantically minimal ones - i.e., the ones that minimally change the TBox in order to obtain definability of a query. With subSol(P) we denote the set of all sub-concept solutions to a TAP P and with M(T ) the set of all models of the TBox T .

Definition 7. Let P = 〈C,D, T 〉 be a TAP, let ≺ be a preference order, and let TA, TB ∈ subSol(P). Then TA ≺ TB iff M(T ) \ M(TA) is a subset of M(T ) \ M(TB). A subconcept solution TA is minimal iff there is no other subconcept solution TB such that TA ≺ TB.

The idea behind this minimality criteria is that it favours a solution TA over TB whenever TA has more common models with the original TBox T than TB. In a way, TA, when added to T , changes the models of T in a minimal way. Note that ≺ is a partial order since (M(T ) \ M(TA)) ⊆ (M(T ) \ M(TB)) does not always hold for arbitrary two sub-concept solutions TA and TB

A thorough study of abduction in DLs is given in the master's thesis by Klarman [2008], in which the author solves the more generic problem of ABox abduction using both tableau and resolution, and proposes novel techniques. A minimality criteria similar to ours is also formulated. Since we do not consider ABoxes, our approach requires less involved techniques.

7 Outlook

In this paper we considered the basic propositionally closed DL ALC. However, several languages currently in use, e.g., OWL, are based on more expressive DLs, with constructs such as inverse roles and qualified cardinality restrictions. For example, in the presence of inverse roles, standard DL tableau algorithms may propagate concepts back and forth between individuals. Therefore, proving interpolation constructively by induction over the tableau is problematic. But one can overcome this problem by adapting a calculus with analytic cut rules [Goré and Nguyen, 2007] for inverse roles. Techniques like algebraic reasoning seem promising in the case of qualified cardinality restrictions [Haarslev et al., 2001]. In the presence of nominals, the logic loses the interpolation property and requires additional constructs in the concept language to regain this property [Ten Cate et al., 2006]. In future work we plan to extend our techniques towards such expressions Description Logics.

The high computational complexity of these DLs might make one question the practicality of such techniques. However, the schema of a database in contrast to its instance is not exposed to many changes. Hence the explicit definitions can be computed offline as SQL views once the ontology has been developed.

Another interesting research direction is to increase the expressiveness of the query language beyond concept expressions towards, e.g., conjunctive queries. Deciding implicit definability reduces to checking query containment under Description Logic constraints [Calvanese et al., 2008]. However, standard Description Logic tableau techniques are not easily extended in this direction. One would need to develop new interpolation calculation methods or use techniques for first-order logic (e.g., Craig [1957]).

Another direction we plan to pursue is a case study of real world ontologies to check how many queries of interest are definable in terms of a given set of DBox predicates and how hard it is to amend such ontologies to make queries definable.

Acknowledgements

We wish to thank Alex Borgida, Tommaso Di Noia, Umberto Straccia and David Toman with whom we are studying a more general framework on query rewriting based on Beth definability and abduction, and the anonymous reviewers for insightful comments. The work presented in this paper has been partially funded by the European project ONTORULE.