FO Rewritability for OMQ using Beth De nability and Interpolation

Abstract

We study rst-order (FO) rewritability for query answering in ontology mediated querying (OMQ) in which ontologies are formulated in Horn fragments of description logics (DLs). In general, OMQ approaches for such logics rely on non-FO rewriting of the query or on analogous completion of the data (ABox). In this paper, we study the problem of the existence of FO rewritings in terms of Beth de nability, and show how Craig interpolation can then be used to e ectively construct the rewritings, when they exist, from the Clark's completion of Datalog-like programs encoding a given DL TBox and optionally a query. We show how our construction can also be seen as an alternative to deriving perfect rewritings in the DL-Lite setting.

Introduction

We study rst-order (FO) rewritability for query answering in the setting of ontology mediated querying (OMQ) over a knowledge base (KB) formulated in terms of underlying Horn description logics (DLs) in the ALC family.

Typical OMQ approaches generally rely on either reformulating the query by incorporating the KB's terminological knowledge [ 10,11 ] and then executing the reformulated query over the explicit data in the KB as a relational query, or, for more expressive logics, on a Datalog completion of the explicit data with respect to the KB's terminological knowledge over which the OMQ is answered [ 24,25,27,28 ]. In the latter case, data completion is sometimes expressible in rstorder logic. This raises the FO rewritability problem: determining if a particular OMQ instance can be equivalently expressed as an FO query over the explicit data in the knowledge base.

Earlier work on OMQ for the FunDL family of DLs [ 31,32,34 ] has presented what was called a combined combined approach to OMQ, and has shown that it is essential to preserve tractability of OMQ in the presence of (limited) value restrictions. In this paper, we focus on the FO rewritability of OMQ when the underlying DL is Horn-SHIQ and its variants. We show that an adaptation of the combined combined approach leads to e cient OMQ query answering and to a solution to the FO rewritability problem for this family of DLs. In particular, we show how the combined combined approach, with the help of Beth de nability [ 4 ] applied on the Clark's completion [ 13 ] of the Datalog program used for the completion of the explicit data in the knowledge base, can be used to characterize FO rewritability of OMQs. We also show how Craig interpolation [ 14 ] can then be used to construct such an FO rewriting, when it exists. The existence of such a rewriting enables an OMQ front-end to a relational data source that underlies an ABox to operate entirely by a more re ned query reformulation of a given union of conjunctive queries (UCQ) that yields an SQL query over the relational data source, with no requirement to update tables beforehand.

Our contributions are as follows. 1. We show how to decide uniform FO rewritability of OMQ in Horn-SHIQ via Clark's completion of Datalog programs and Beth de nability; 2. We show how our framework extends to query speci c OMQ by extending existing results for Horn-DLF D; and 3. We show how a variant of the perfect rewriting approach to OMQ can be synthesized by appeal again to Beth de nability and Craig interpolation. This paper builds on earlier work that was the rst to consider FO rewritability of OMQ, but for the above mentioned FunDL family of DLs, via Beth de nability and Clark's completion [36]. FO rewritability for Horn logics in the ALC family has been studied by others, e.g., see [ 5,7 ]. This other work has also developed algorithms for generating such rewritings e ciently for logics in the E L family [ 19 ]. Our approach seems to provide an alternative path to detecting rewritability and to generating rewritings. A feature of our approach is its link to interpolation-based query optimization [ 21,33 ]. The link to query optimization reveals that minimal sized rewritings are often not optimal for query execution. However, establishing limits on the size of rewriting [ 6 ] does provide a guide on what rewritings are reasonable to consider during query optimization.

The use of database constraints, possibly combined with constraints implied by data mapping rules, has been explored in several systems that implement variants of perfect rewriting [ 11 ], such as Ontop and MASTRO [ 3,9 ] and others. One of the contributions in [36], inherited by this work, also shows how Beth de nability and Clark's completion seamlessly accommodate such constraints into the rewriting via interpolation (for space reasons we do not present the details here).

Beth de nability and Craig Interpolation have been used for other purposes, such as query reformulation under FO constraints [ 8,21,33,35 ]. That use, however, is orthogonal to the topic of this paper.

The remainder of the paper is organized as follows. Section 2 provides the necessary background and de nitions. Here, we review Horn-SHIQ and the combined combined approach to OMQ. Our main results then follow in Section 3 in which we show how the above-mentioned artifacts, Clark's completion of Datalog programs for example, can be employed to both decide FO rewritability and to synthesize FO rewritings of ABox completion in the combined combined approach to OMQ. In Section 4, we show how our framework is an alternative approach to perfect rewriting of queries for knowledge bases formulated in DLLite. In the conclusions we discuss several limitations and possible extensions of our approach.

Background and De nitions

Horn-SHIQ and its variants. Our primary focus will be on KBs with underlying DLs that are a variant of Horn-SHIQ. We begin by de ning the relevant roles, concepts and their semantics presumed by such DLs.

De nition 1 (Horn-SHIQ Concepts and Roles)

Let R, PC and IN be disjoint sets of primitive role names, primitive concept

names and individual names respectively. Horn-SHIQ roles R are of the form P and P for P 2 R, and concepts C are of the form A for A 2 PC, C1 u C2, ?, >, 8R:C, 9R:C, ( n R:C), or ( n R:C) for n 0. The semantics is with respect to a structure I = (4I ; I ) in which 4I is a domain of objects and I an interpretation function seeded by xing the interpretations of primitive concept names A to be subsets of 4I , primitive role names R to be subsets of 4I 4I , and individual names a to be elements of 4I , and is extended to derived concepts

C and roles R in the standard way [2]. Subsumption between concepts and roles, assertions, knowledge bases and their consistency, logical implication, and other reasoning problems are also de ned in the standard way.

The following de nition of a Horn-SHIQ KB appeals to a simpli ed normal form for subsumption constraints presented in [ 16 ]. For more general but expressively equivalent syntax, e.g., that allows other forms of quali ed number restrictions, see [ 22 ].

De nition 2 (Horn-SHIQ TBoxes and ABoxes [16])

A Horn-SHIQ knowledge base K consists of a TBox T and an ABox A. A TBox T (in normal form) consists of role subsumptions of the form R1 v R2 that de ne a role hierarchy, transitivity assertions trans(R), and concept subsumptions that adhere to one of the following forms:1

A u B v C, A v 8R:B, A v 9R:B, 9R:A v B, or

A v ( 1 R:B), where A; B; C 2 PC [ f>; ?g. Roles R are called simple when neither they nor any of their subroles are transitive. To avoid a well known source of undecidability, we require that any number restriction occurring in T will mention only simple roles.

An ABox A consists of concept assertions, role assertions, equality axioms and inequality axioms with the respective forms A(a), R(a; b), a = b and a 6= b.

A Horn-ALCHQI KB is a Horn-SHIQ KB without any transitivity assertions. 1 Note that subsumptions of the form \A1 u uAn v B" are also allowed in [ 16 ]. Here, we are appealing to an obvious conservative extension to replace such subsumptions with strictly binary use of conjunction to further simplify our presentation. Conjunctive queries and OMQ. Conjunctive queries are, as usual, formed from atomic queries (or atoms) of the form \A(x)" and \R(x; y)", where x and y are variables, using conjunction and existential quanti cation (in prenex normal form). As usual, we con ate conjunctive queries with the set of its constituent atoms and a list of answer variables to simplify notation.

De nition 3 (Conjunctive Query) Let now be a set of atoms A(xi) and R(xi1 ; xi2 ), where A is a primitive concept name or >, R a role name, and x a tuple of variables. We call the expression ' = fx j g a conjunctive query (CQ). A CQ ' is also a notational variant of the formula \9y: V 2 " in which y contains all variables appearing in but not in x.2 We also omit set braces when explicitly listing atoms in to improve readability. With this understanding, the usual de nition of certain answers is assumed and given as follows: De nition 4 (Certain Answer) Let K be a Horn-SHIQ knowledge base and ' = fx j g a CQ. A certain answer to ' over K is a tuple of constant symbols a, such that K j= '(a) (where '(a) is short for '[x 7! a]).

Our primary concern is then given by the following problem: De nition 5 ((uniform) FO Query Rewritability) Given a Horn-SHIQ TBox T , the problem of uniform query rewritability is to determine if there is a query reformulation 'T for every CQ ' such that, for every ABox A and tuple of constant symbols a, (T ; A) j= '(a) i A j= 'T (a). Later in the paper, we brie y consider a query-speci c variant of this problem: whether such a rewriting exists for a given CQ. The following observations will also be useful in regard to this problem.

Observation 6 (Transitivity) Consider a Horn-SHIQ knowledge base with a TBox ftrans(R)g. Then the CQ f(x; y) j R(x; y)g cannot be FO rewritable since this would one allow to answer the connectivity question with respect to any ABox considered as a graph of R-edges.

Analogously to transitive roles, allowing equality between ABox objects, and therefore not adopting the unique name assumption (UNA), leads immediate to non-rewritability: Observation 7 (Equality) Consider a Horn-SHIQ KB in which T = ; and a CQ f(x; x) j >(x)g. Again, this query solves the (undirected) connectivity problem in an ABox with explicit equalities between individuals and thus cannot have an FO rewriting. 2 Note that it is not necessary to place any restrictions on the variables x. Indeed, one can add additional atoms >(xi) to ensure variables in x also appear in , if desired, without any impact on the remaining results.

Hence, hereon, we focus on the Horn-ALCHQI sub-dialect of Horn-SHIQ without transitive roles, and also adopt UNA.

Observation 8 (Boolean Queries) Consider a Boolean CQ '. Such a query,

when equivalent to a concept, can be entailed not only due to matches in an

ABox, but also due to matches in the anonymous part of the models of the knowledge base. However, these matches only depend on the existence of certain patterns (types) in the given ABox that can be enumerated and this way converted to a UCQ [31,32,34].

Hence, hereon as well, we focus on CQs with (1) at least one answer variable, and (2) that are connected. The combined combined approach that we now outline can be extended to all CQs, although the details of doing so lie outside the scope of this paper since they do not a ect query rewritability. Finally, we assume that the KBs under consideration are consistent. Hence, it will be unnecessary to check for at most number restrictions (functionality) in our constructions. The Combined Combined Approach. To study FO rewritability of conjunctive queries over Horn-ALCHQI knowledge bases, we begin with the following manifestation of a combined combined approach to OMQ originally developed for the feature logic Horn-DLF D [ 31,32,34 ].3 Our objective is to modify the approach to suit Horn-ALCHQI, and to show how such can be used to decide query rewritability with respect to knowledge bases expressed in terms of such dialects.

Proposition 9 (Combined Combined Approach for Horn-ALCHQI)

Let K = (T ; A) be a consistent Horn-ALCHQI knowledge base and ' a conjunctive query. Then there is a UCQ query 'T and a Datalog program T , both of which can be e ectively constructed from T , such that

K j= '(a) ()

T (A) j= 'T (a) for any tuple of constant symbols a, and where

T when evaluated over A.

T (A) is the minimal model of In the rest of this section, we give the de nition of T (A) and 'T .

Datalog programs and clauses that follow use the standard syntax and semantics, and, in particular, predicates used in such programs are classi ed as either EDB (extensional predicates), those for which we have explicit data, and IDB (intensional predicates), predicates whose interpretation is de ned by the minimal model semantics of Datalog [37,38,39]. 3 Note that the original combined approach [ 24,29 ] used the TBox subsumptions to complete the ABox but not to rewrite the CQ. The approach presented here combines this combined approach with a variation on perfect rewriting [ 11 ]; hence we call it the combined combined approach.

De nition 10 (Datalog Program T ) The Datalog program T used in

Proposition 9 consists of completion rules obtained by translating subsumptions that are logical consequences of T . The form of these subsumptions and their translation are given as follows: (consequences of T ) A1 u A2 v B A v 8R:B 9R:A v B R v S (completion rule in CB(x) CB(x) CB(x) RS(x; y)

T ) CA1 (x); CA2 (x) CA(y); RR(y; x) CA(y); RR(x; y) For every primitive concept B and role R, we introduce an unary EDB predicates PB(x) and PR(x; y) together with additional clauses CB(x) PB(x), RR(x; y) PR(x; y), and RR (x; y) PR(y; x) (accounting for explicit data of the form A(a) and R(a; b) in an ABox ), and IDB predicates CB(x) and RR(x; y) corresponding to the completion of the ABox w.r.t. T .

Note that the subsumptions for existential restrictions do not contribute to the de nition of an ABox completion since they do not generate additional ABox assertions for ABox individuals. Similarly, number restrictions (at most restrictions) do not play any role here as we assume that ABoxes we try to complete are always consistent with the TBox T (as we already mentioned above). Also note that, unlike in the classical combined approach [ 24,28 ], our combined combined approach does not introduce any new constants in the ABox, similarly to [ 32 ]. The following de nition is an adaptation of the approach to query reformulation to Horn-ALCHQI: De nition 11 (Query Reformulation) Let ' = fx j g be a CQ. We write FoldT (') to denote the set of CQs obtained by applying the following when initialized with the singleton set

ffx j gg: (computing 'T ) Update FoldT (') for a CQ fy j g 2 FoldT (') according to the following rewrite rules (top-down) until no such rewrite is possible: 1. If fA(x); B(x)g and T j= AuB v ? then FoldT (') := FoldT (') ffy j gg: 2. If fA(x); B(x)g

and T j= A v B then FoldT (') := FoldT (') ffy j gg [ ffy j fB(x)ggg: 3. If fR(x; y); R0(x; y)g

and T j= R v R0 then FoldT (') := FoldT (') ffy j gg [ ffy j fR0(x; y)ggg:

4. If x and y are variables in then

FoldT (') := FoldT (') [ ffy j g[x=y]g: and

FoldT (') := FoldT (') [ ffy j 0gg for all 0 of the form fR1(x; y); : : : ; Rn(x; y); R10(y; x); : : : ; Rm0(y; x); A1(y); : : : ; Ak(y)g [ fB1;i1 (x); : : : ; Bk;ik (x)g that are generated by sets fB1;i1 (x); : : : ; Bk;ik (x)g such that (i) for some Bi;ij and B 2 PC [ f>g we have T j= Bi;ij v 9Ri:B or T j= Bi;ij v 9Ri0 :B and (ii) such that each of the Ai concepts for which T 6j= B v Ai there is a concept Bi;ij for which T j= Bi;ij v 8Ri:Ai or T j= Bi;ij v 8Rj0 :Ai, where Bi;ij is maximal w.r.t. v.4 The reformulation of ' w.r.t. T , 'T , is then given by the UCQ W 2Fold(') .

Note that, for our purposes, the existence of 'T is su cient since we are concerned with rewritability and not query answering. The existence of 'T also indicates that the non-rewritability of CQs is con ned to the interaction of the TBox with explicit data given by an ABox. 3

Classi cation of TBoxes

To test for FO de nability of the completion (i.e., all predicates that stand for the completed ABox instance), we use the following construction: De nition 12 (Clark's Completion of T is given by a set of formulas T ) The Clark's Completion [ 13 ]

T CB(x) $ PB(x) _ (9y: 1) _ : : : _ (9y: n)

RR(x; y) $ PR(x; y) _ 1 _ : : : _ m corresponding to all clauses CB(x) their heads).

i and RR(x; y) j in

T (grouped by The bodies i ( i) are introduced in De nition 10. Note also that the Clark's Completion is no longer a Datalog program. This completion, however, closes the original Datalog program in the following sense: Proposition 13 ([ 13 ], simpli ed for this paper) { {

T [ Adb j= CB(a) implies T [ Adb 6j= CB(a) implies

T [ Adb j= CB(a), and

T [ Adb j= :CB(a). 4 This rule allows one to remove atoms over quanti ed variables (y in our case) in a query by adding atoms over the remaining variables (x in our case) that imply the existence of the original atoms with the help of the TBox. (and similarly for RR(a; b) consequences) for every ABox A and constant a (and b), where Adb is the closed world variant of A, a set of ground facts such that all facts not in Adb are false.

Note that Clark's result works in the much more general setting of logic programs with function symbols and possibly in nite resolution proofs and under the Negation As Failure semantics. Since Clark's completion makes all IDB predicates closed, we can now use standard tools for testing for explicit de nability.

Also note that, had we used T instead, none of the de nability results could possibly hold, and that, in the absence of role/feature subsumptions (such as role hierarchies), there is no need to apply the completion to the RR atoms. Proposition 14 (Projective Beth De nability [ 4 ]) Let be an FO theory over symbols in L and L0 L. Then the following are equivalent: 1. For M1 and M2 models of such that M1jL0 = M2jL0 , it holds that M1 j= '[a] i M2 j= '[a] for all M1, M2, and a tuples of constants, and

2. ' is equivalent under to a formula in L0 (we say ' is Beth de nable

over and L0).

This gives us a complete characterization of FO rewritability of the ABox closure of individual primitive concept names with respect to Horn-ALCHQI TBoxes as follows: Theorem 15 Let T be a Horn-ALCHQI TBox over the primitive concept names fA1; : : : ; Akg and role names fR1; : : : ; Rng. Then the completion of the primitive concept Ai (role Ri) w.r.t. T is FO de nable if and only if CAi (x) (RRi (x; y)) is Beth de nable over T and L0 = fPA1 ; : : : ; PAk ; PR1 ; : : : ; PRn g. Proof (sketch): Follows immediately from the properties of Beth de nability (Proposition 14) and the de nition and properties of the Clark's completion (Proposition 13).

Observe that one can restrict the alphabet of the ABox (L0) to target only ABoxes over restricted signature(s).

Given T , one can now reformulate (1) in Proposition 14 as a logical implication problem by making a copy of all formulas of T in which all non-logical symbols not in fPA1 ; : : : ; PAk ; PR1 ; : : : ; PRn g are starred. Hence, the de nability question for CA(x) and RR(x; y) can be expressed as a logical implication question of the form:

T [ T [

T j= 8x:CA(x) ! CA(x) T j= 8x; y:RR(x; y) ! RR(x; y) (1) Note that, without role constructors, there is no need to check for the de nability of RR(x; y) atoms since they are always de nable (we elaborate on the role of role constructors in Section 5). Note also that, on closer inspection, all formulas in T can be written as ALCI subsumptions. Hence: Theorem 16 Let T be a Horn-ALCHQI TBox. Then the existence of 1. the FO rewritability of the A completion with respect to T , and 2. the uniform query rewritability over T are decidable and in EXPTIME.

Proof (sketch): The rst claim follows immediately from Theorem 15 applied to all atoms of the form CB and the decidability and complexity of reasoning in ALCI. The second claim follows by observing that (i) de nability of atomic queries implies de nability of arbitrary UCQs using the combined combined approach, and that (ii) non-de nability of a single atomic query exhibits the need for a non FO ABox completion for queries containing/consisting of this atom.

In the second case, one can restrict the de nability conditions to atoms that can appear in the query 'T . A matching lower bound can be obtained for expressive fragments of Horn-ALC (for which the reasoning complexity is EXPTIMEcomplete).5 However, since the size (and the construction) of rewritings will dominate this cost (even for the simplest ontology languages [ 23 ]), exact complexity bounds are mostly of academic interest.

Construction of rewritings. To obtain an algorithm that constructs rewritings from our characterization of FO rewritability, we utilize Craig Interpolation: Proposition 17 (Craig Interpolation [ 14 ]) Let ' and be FO formulas such that j= ' ! . Then there is an FO formula , called Craig interpolant, containing only symbols common to ' and such that j= ' ! and j= ! . Moreover, the interpolant can be extracted, typically in linear time, from a proof of j= ' ! , as long as a reasonably structural proof system, such as resolution, (cut-free) sequent calculus, and/or analytic tableau is used. Combining the above construction with the rewriting 'T we get: Theorem 18 Let K = (T ; A) be a consistent Horn-ALCHQI knowledge base. Then the data complexity of uniform conjunctive query answering is in AC0 whenever the A completion with respect to T is FO de nable with respect to T . Proof (sketch): Let A(x) be an FO de nition of CA w.r.t. T . Then K j= '(a) i Adb j= 'T [ A[y=x]=A(y) j A 2 PC](a): The claim follows since 'T [ A[y=x]=A(y) j A 2 PC] is an FO formula, in particular a UCQ.

Our approach also provides decidability for the non-uniform (query-speci c) problems. Also, while one can explicitly construct 'T , to decide FO rewritability of a CQ, one only needs to determine the atomic formulas for which interpolants are needed in the reformulation. This yields our desired result: 5 It was noted in [36] that the exact complexity is open for PTIME fragments of

Horn-DLF D, such as CF Dnc and CF DI8kc .

Theorem 19 Let T be a Horn-ALCHQI TBox and ' a CQ. Then the following are equivalent: 1. ' is FO rewritable with respect to T and 2. T [ T j= 8x:CA(x) ! CA(x) for all CA appearing in 'T and 8x; y:RR(x; y) ! RR(x; y) for all RR appearing in 'T . The exact complexity again depends on the complexity of (2) above. In the general case, an EXPTIME bound follows from [ 20 ], but again, a more re ned analysis is in order for fragments of Horn-ALCHQI. 4

A One-step Construction of Rewritings

We have been considering the test for existence of rewritings and the construction of such rewritings as a two part process: (i) the construction of an ABox completion, and (ii) subsequent query reformulation. We have already noted that non-rewritability can always be traced to part (i) of this process. An interesting question that emerges, however, is whether such a two-part process is needed. In this section we outline a one-step approach to the problem that continues to be based on Clark's completion and on Beth de nability, optionally followed by Craig interpolation. Now, however, we apply both techniques to the full TBox, i.e., including existential restrictions that may generate anonymous objects, and to the user query, (to save space, in Horn-ALC only).

De nition 20 (Logic Program for Horn-ALC TBox)

(entailed by T ) (completion rule in

T ) A v ? A1 u A2 v B A v 8R:B 9R:A v B A v 9R:B

C?(x) CA(x) CB(x) CA1 (x); CA2 (x) CB(x) CA(y); RR(y; x) CB(x) CA(y); RR(x; y) RR(x; fR(x)) CA(x); and

CB(fR(x)) CA(x) Note that the construction of a Datalog program in Section 3 omitted the last rule (for A v 9R:B) since the e ect of that subsumption has been accommodated by query reformulation. The clauses stemming from the existential restrictions contain Skolem functions fR and hence the resulting set of clauses is no longer a Datalog program. To de ne the Clark's completion, observe that the clauses for A v 9R:B can be equivalently written as as shown in [ 13 ]. Now, since the heads of the clauses in T have a uniform format, we can create the completion T as in De nition 12. (This requires adding the standard equality axioms or assuming equality is an interpreted predicate.) For a given CQ ' of the form fx j g, extend the completion with T ;' =

T [ fQ(x) $ g (with Q a new symbol). Then one can apply the de nability test as in the previous case to obtain the rewritability test: Theorem 21 Let T be a Horn-ALC TBox and ' a CQ. Then the following are equivalent: 1. T ;' [ T ;' j= 8x:Q(x) ! Q (x), and 2. ' is FO rewritable with respect to T .

The theorem provides a direct, sound and complete test for FO rewritability of CQs with respect to Horn-ALC TBoxes. However, unlike in the case of Datalog, we need to ensure that the test is still decidable and has a reasonable computational complexity. Note that the actual complexity in this case is tied to the proof system used to prove (1) in Theorem 21: as in DL reasoners, not every proof system achieves the optimal complexity bound. For Horn-ALC, a reduction to the Ackermann pre x with equality [ 1 ] seems feasible, with the aim of obtaining the complexity bound using Furer's result [ 18 ]. However, if one is interested in generating the rewriting in the form of an interpolant, a suitable proof system that supports interpolant generation, such as Analytic Tableau [ 17 ], (cut-free) Sequent Calculus, or Resolution, is needed. Alternative blocking-style techniques used in DL tableau reasoners are very likely to apply here as well. An intriguing possibility is to also just limit the depth of terms in a general high-performance theorem prover along the lines described by Chomicki for DatalognS [ 12 ]. Both of these options are subjects of future research.

An interesting application of Theorem 21 emerges when the given TBox is formulated in DL-Lite variants, for which interpolants will then correspond to the result obtained by perfect query reformulation developed in [ 10,11 ]. It is relatively easy to observe that the one-step interpolation-based approach always succeeds and produces essentially the perfect rewritings of conjunctive queries. 5

Summary and Extensions

In this section, we brie y discuss several common extensions of Horn-ALC that we have omitted so far in our development to keep the presentation of the main ideas cleaner. In the light of Theorem 21, it is relatively immediate that any extension that leads to Horn T can be accommodated. Note that, to extend the two-step combined combined approach, we would need to modify, often in non-trivial manner, the query reformulation algorithm. (For an example that accommodates inverse features and a variety of equality generating dependencies called path-functional dependencies, see [ 31 ].)

Additional concept and role constructors, and the induced subsumptions, can be classi ed in three groups: 1. Constructors that lead to full Horn rules, i.e., without existential quanti ers in their heads, that preserve the tree model property. Rules corresponding to these constructors can simply be added in De nition 10 and De nition 20 without any major impact on the query reformulation in De nition 11; 2. Constructors that lead to embedded Horn rules with existential quanti ers in their heads that continue to preserve the tree model property. Here, both De nition 10 and 11 need to be extended to account for the possibility of additional anonymous individuals. Alternatively, one can capture all of the e ects by naturally extending De nition 20 and proceeding with a one-step de nability test; and 3. Constructors that break the tree-model property. Examples relate to transitivity assertions and nominals; here, it is not always clear how to modify De nition 11 to make Proposition 9 hold. However, extending De nition 20 and subsequently using Theorem 21 will still work.

However, using Theorem 21, while sound and complete for determining rewritability, does not come for free. With each extension, one needs to revisit the decidability and complexity of the de nability test which, ultimately, becomes undecidable. This happens even in cases when only unary function symbols are needed but where unrestricted use of binary predicates, such as roles, are allowed.

Extensions that are unlikely to be possible. There are limits to the de nability

based approach: (beyond Horn logics ) The approach for Horn logics relies crucially on the existence of a unique minimal model (called the universal model in DL circles) that can be characterized using the Clark's completion. This insight then makes Beth de nability and Craig interpolation work. It remains unclear how this idea could generalize to logics without the minimal model property (i.e., non-Horn). For these reasons PTIME-coNP boundaries [ 30 ] are unlikely to be resolved using these techniques. (beyond FO logics ) The synthesis of the rewritings is tied to Craig Interpolation. Hence synthesizing, e.g., linear Datalog or dealing with dichotomies on the NLPTIME [ 26 ] boundary seems also to be beyond the capabilities of the techniques used in this paper. Applying results on interpolation in non- rst order logics, such as the -calculus [ 15 ], will be the focus of future research. However, the combined combined approach already gives one a Datalog rewriting, so the space to be explored seems to be rather limited. 34. David Toman and Grant E. Weddell. Conjunctive Query Answering in CF Dnc: A PTIME Description Logic with Functional Constraints and Disjointness. In Australasian Conference on Arti cial Intelligence, pages 350{361, 2013. 35. David Toman and Grant E. Weddell. An interpolation-based compiler and optimizer for relational queries (system design report). In IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, Maun, Botswana, May 7-12, 2017, 2017. 36. David Toman and Grant E. Weddell. First order rewritability for ontology mediated querying in horn-dlfd. In Proceedings of the 33rd International Workshop on Description Logics (DL 2020), volume 2663 of CEUR Workshop Proceedings.

CEUR-WS.org, 2020. 37. J.D. Ullman. Principles of Database Systems. Computer Science Press, 1982. 38. J.D. Ullman. Principles of Database and Knowledge-Base Systems, volume 1. Computer Science Press, 1988. 39. J.D. Ullman. Principles of Database and Knowledge-Base Systems, volume 2. Computer Science Press, 1989.

References

1. W. Ackermann . Uber die Erfullbarkeit gewisser Zahlausdrucke . Mathematische Annalen , 100 : 638 { 649 , 1928 .

2. Franz Baader , Diego Calvanese, Deborah L. McGuinness , Daniele Nardi , and Peter F. Patel-Schneider . The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, 2003 .

3. Timea Bagosi , Diego Calvanese, Josef Hardi, Sarah Komla-Ebri, Davide Lanti, Martin Rezk, Mariano Rodriguez-Muro, Mindaugas Slusnys , and Guohui Xiao . The ontop framework for ontology based data access . In The Semantic Web and Web Science - 8th Chinese Conference, CSWS 2014, Revised Selected Papers , pages 67 { 77 , 2014 .

4. Evert Willem Beth . On Padoa's method in the theory of de nition . Indagationes Mathematicae , 15 : 330 { 339 , 1953 .

5. Meghyn Bienvenu , Peter Hansen , Carsten Lutz, and Frank Wolter . First orderrewritability and containment of conjunctive queries in horn description logics . In Proceedings of the 29th International Workshop on Description Logics , Cape Town, South Africa, 2016 .

6. Meghyn Bienvenu , Stanislav Kikot, Roman Kontchakov, Vladimir V. Podolskii , Vladislav Ryzhikov, and Michael Zakharyaschev . The complexity of ontologybased data access with OWL 2 QL and bounded treewidth queries . In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2017 , pages 201 { 216 , 2017 .

7. Meghyn Bienvenu , Balder ten Cate, Carsten Lutz, and Frank Wolter . Ontologybased data access: A study through disjunctive datalog, csp, and MMSNP . ACM Trans. Database Syst ., 39 ( 4 ): 33 :1{ 33 : 44 , 2014 .

8. Alexander Borgida , Jos de Bruijn, Enrico Franconi, Inanc Seylan, Umberto Straccia, David Toman, and Grant E. Weddell . On nding query rewritings under expressive constraints . In SEBD , pages 426 { 437 , 2010 .

9. Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, Antonella Poggi, Mariano Rodriguez-Muro, Riccardo Rosati, Marco Ruzzi, and Domenico Fabio Savo. The MASTRO system for ontology-based data access . Semantic Web , 2 ( 1 ): 43 { 53 , 2011 .

10. Diego Calvanese, Giuseppe De Giacomo, Domenico Lembo, Maurizio Lenzerini, and Riccardo Rosati . DL-Lite: Tractable description logics for ontologies . In Proc. of the 20th Nat. Conf. on Arti cial Intelligence (AAAI 2005 ), pages 602 { 607 , 2005 .

11. Diego Calvanese, Giuseppe de Giacomo, Domenico Lembo, Maurizio Lenzerini, and Riccardo Rosati . Tractable Reasoning and E cient Query Answering in Description Logics: The DL-Lite Family . J. of Automated Reasoning , 39 ( 3 ): 385 { 429 , 2007 .

12. Jan Chomicki . Depth-bounded bottom-up evaluation of logic program . J. Log. Program. , 25 ( 1 ):1{ 31 , 1995 .

13. Keith L. Clark . Negation as failure . In Logic and Data Bases, Symposium on Logic and Data Bases , Centre d'etudes et de recherches de Toulouse, France, 1977 , pages 293 { 322 , 1977 .

14. William Craig . Three uses of the Herbrand-Genzen theorem in relating model theory and proof theory . Journal of Symbolic Logic , 22 : 269 { 285 , 1957 .

15. Giovanna D'Agostino and Marco Hollenberg . Logical questions concerning the mu-calculus: Interpolation, lyndon and los-tarski . J. Symb. Log. , 65 ( 1 ): 310 { 332 , 2000 .

16. Thomas Eiter , Magdalena Ortiz, Mantas Simkus, Trung-Kien Tran , and Guohui Xiao . Query rewriting for horn-shiq plus rules . In Proceedings of the Twenty-Sixth AAAI Conference on Arti cial Intelligence, July 22-26 , 2012 , Toronto, Ontario, Canada., 2012 .

17. Melvin Fitting . First-Order Logic and Automated Theorem Proving, Second Edition . Graduate Texts in Computer Science. Springer Publishers, 1996 .

18. Martin Furer. Alternation and the Ackermann Case of the Decision Problem . L'Enseignement Math., 27 : 137 { 162 , 1981 .

19. Peter Hansen , Carsten Lutz, Inanc Seylan, and Frank Wolter . E cient query rewriting in the description logic EL and beyond . In Proceedings of the TwentyFourth International Joint Conference on Arti cial Intelligence , IJCAI 2015 , pages 3034 { 3040 , 2015 .

20. Ian Horrocks , Ulrike Sattler, Sergio Tessaris, and Stephan Tobies . How to decide query containment under constraints using a description logic . In Logic for Programming and Automated Reasoning , 7th International Conference, LPAR 2000, Reunion Island , France, November 11-12 , 2000 , Proceedings, pages 326 { 343 , 2000 .

21. Alexander K. Hudek , David Toman, and Grant E. Weddell . On enumerating query plans using analytic tableau . In Automated Reasoning with Analytic Tableaux and Related Methods - 24th International Conference, TABLEAUX 2015 , Wroclaw, Poland, September 21-24 , 2015 . Proceedings, pages 339 { 354 , 2015 .

22. Ullrich Hustadt , Boris Motik, and Ulrike Sattler . Data complexity of reasoning in very expressive description logics . In Proc. Int. Joint Conf. on Arti cial Intelligence (IJCAI) , pages 466 { 471 . Professional Book Center, 2005 .

23. Stanislav Kikot , Roman Kontchakov, Vladimir V. Podolskii, and Michael Zakharyaschev. Long rewritings, short rewritings . In Proceedings of the 2012 International Workshop on Description Logics, DL-2012 , Rome, Italy, June 7-10, 2012 , 2012 .

24. Roman Kontchakov , Carsten Lutz, David Toman, Frank Wolter , and Michael Zakharyaschev . The combined approach to query answering in DL-Lite . In Proc. KR , pages 247 { 257 , 2010 .

25. Roman Kontchakov , Carsten Lutz, David Toman, Frank Wolter , and Michael Zakharyaschev . The combined approach to ontology-based data access . In Proc. Int. Joint Conf. on Arti cial Intelligence (IJCAI) , pages 2656 { 2661 , 2011 .

26. Carsten Lutz and Leif Sabellek . Ontology-mediated querying with the description logic EL: trichotomy and linear datalog rewritability . In Proceedings of the TwentySixth International Joint Conference on Arti cial Intelligence , IJCAI 2017 , pages 1181 { 1187 , 2017 .

27. Carsten Lutz , Inanc Seylan, David Toman, and Frank Wolter . The combined approach to OBDA: Taming role hierarchies using lters . In ISWC (1) , pages 314 { 330 , 2013 .

28. Carsten Lutz , David Toman, and Frank Wolter . Conjunctive query answering in the description logic EL using a relational database system . In Proc. Int. Joint Conf. on Arti cial Intelligence (IJCAI) , pages 2070 { 2075 , 2009 .

29. Carsten Lutz , David Toman, and Frank Wolter . Conjunctive query answering in the description logic EL using a relational database system . In Proc. IJCAI , pages 2070 { 2075 , 2009 .

30. Carsten Lutz and Frank Wolter . Non-uniform data complexity of query answering in description logics . In Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012 , 2012 .

31. Stephanie McIntyre , Alexander Borgida , David Toman, and Grant E. Weddell . On limited conjunctions and partial features in parameter-tractable feature logics . In The Thirty-Third AAAI Conference on Arti cial Intelligence , AAAI 2019 , pages 2995 { 3002 , 2019 .

32. Jason St. Jacques , David Toman, and Grant E. Weddell . Object-relational queries over CF DInc knowledge bases: OBDA for the SQL-Literate . In Proc. IJCAI , pages 1258 { 1264 , 2016 .

33. David Toman and Grant E. Weddell. Fundamentals of Physical Design and Query Compilation . Synthesis Lectures on Data Management . Morgan & Claypool Publishers, 2011 .