We study first order (FO) rewritability for query answering in the setting of ontology mediated queries (OMQ) in which ontologies are formulated in the Horn fragments of the feature description logic DLFD. In general, OMQ approaches for logics such as DLFD rely on non-FO completion of the data (ABoxes) that can commonly be expressed as Datalog programs. In this paper, we study the problem of the existence of FO rewritings for a given Horn-DLFD theory (TBox) in terms of Beth definability, and show how Craig interpolation can then be used to effectively construct the rewritings (when they exist) from the Clark's completion of Datalog programs for computing ABox completions. In addition, since data that populates OMQ is commonly residing in relational database systems, we show how constraints enforced by such systems can be used to expand the scope of rewritable queries.
In earlier work [25,27], we presented a combined-combined approach to ontology mediated querying (OMQ) of backend relational data sources when ontologies are formulated as TBoxes in the Horn fragments of the description logic (DL) DLFD and where ABoxes are induced by data residing in the data sources. The logic DLFD is the most expressive member of the FunDL family of feature-based DLs [26], which are particularly well suited for capturing relational schemata by virtue of being feature-based and also by virtue of including the path functional dependency (PFD) concept constructor. PFDs makes it possible to capture a variety of equality generating dependencies commonly occurring in relational schemata, such as primary keys, uniqueness constraints and functional dependencies. To illustrate, we show in the next section how the relational schema in Figure 1 can be captured as a Horn-DLFD TBox, the FunDL dialect that will be the focus of the remainder of this paper. This example also serves to illustrate how the parts of a TBox that reflect a relational schema could in principle be automatically generated, and thereby make it unnecessary to author so-called mapping rules in ontology based data access (OBDA) (again see [25,27]).
The combined-combined approach is so named because any of the Horn fragments of DLFD in the FunDL family will require using ontological knowledge, a Horn-DLFD TBox in our case, for two steps in OMQ. The first step, as with the combined approach to OMQ [19,20,22,23], is to complete the ABox via a Datalog program that adds tuples to tables in the backend relational database. Note that this first step depends only on the TBox. The second step, as with the perfect rewriting approach to OMQ and OBDA [9], is to rewrite a query to account for such artifacts as inheritance and attribute typing in the TBox.
In this paper, we show how Beth definability can be used to resolve the problem of recognizing when a first order (FO) rewriting of the Datalog program needed in the first step exists, and then how Craig interpolation can be used to effectively construct such a rewriting. A key insight is to employ the Clark's completion of the Datalog program in both the diagnosis and synthesis of FO expressibility of ABox completion.
The existence of such a rewriting enables an OMQ frontend to a relational data source to operate entirely by a more refined query reformulation that, for a given user query, ultimately yields an SQL query over the data source, that is, with no requirement to update tables in the data source beforehand. An additional advantage of our approach is that it also becomes straightforward to incorporate the benefits of integrity constraints such as foreign key constraints that are enforced by a relational database management system to simplify query reformulation. Indeed, such integrity constraints can enable FO rewriting of data completion that would otherwise not be possible.
In summary, our contributions are as follows.
1. We show how to decide FO rewritability of OMQ in Horn-DLFD via Clark's completion of Datalog programs and Beth definability; 2. We show how an equivalent non-recursive Datalog program can be derived via Craig's theorem and interpolation in cases where ABox completion for a given TBox is indeed FO expressible; 3. We illustrate how integrity constraints in backend relational schema can enable FO rewritability of OMQ that would otherwise not be possible; and 4. We show how our framework extends to query specific OMQ in a straightforward manner.
The remainder of the paper is organized as follows. Section 2 immediately following provides the necessary background and definitions. Here, we review Horn-DLFD and the combined combined approach to OMQ. Our main results 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 The most expressive member of the FunDL family is the dialect DLFD. In this paper, we consider Horn-DLFD, the most expressive Horn fragment of DLFD, assuming in particular that an ontology is given as a Horn-DLFD TBox. 1 To simplify our presentation, we also assume features are interpreted as total functions. Definition 1 (Horn-DLFD) A path function Pf is a word in F * , with the empty word denoted by id , and concatenation by ".". Concept descriptions of two kinds, C and D, are defined by the grammar rules on the left-hand-side of Figure 2, where A ∈ PC, f ∈ F and Pf (possibly subscripted) refers to a path function. An instance of the final production is called a path functional dependency (PFD).
Semantics is defined in the standard way with respect to an interpretation I = ( , (•) I ) that fixes the meaning of symbols in PC, IN and F. Here, features are interpreted as total functions. We also assume the unique name assumption (UNA) whereby, for any distinct individuals a and b, a I = b I .
The interpretation function I is extended to path expressions by interpreting id (the empty word) as the identity function λx.x, concatenation as function composition, and to complex concept descriptions C or D as given on the righthand-side of Figure 2. An interpretation I satisfies a subsumption C D if Syntax Semantics: "(•) I " A knowledge base (KB) K = (T , A) consists of a TBox T of subsumptions, and an ABox A of assertions. I satisfies K if it satisfies each subsumption and assertion in K.
Although incorporating features deviates from the normal practice of using binary predicate symbols called roles, features make it easier to incorporate concept constructors suited to the capture of relational data sources that include various dependencies by a straightforward reification of n-ary predicates. Thus, e.g., a role R can be reified as a primitive concept R C and two features domR and ranR in Horn-DLFD, and a subsumption A ∀R.B can then be captured as a subsumption ∀domR.A ∀ranR.B.
As usual, to ensure decidability in the presence of ABoxes [28] and reasonable computational properties of the logic, one looks for additional restrictions on the PFD concept constructors. One restriction, which has been investigated (e.g., [17,27]), is to limit the PFD constructor to one of the following two forms:
We can allow a more complex variant of (2) if the ABox completion admits/requires creating additional constant symbols; for details-beyond the scope of this paper-see [27]. Also, in this paper we will not explore the parameter tractable fragments of Horn-DLFD nor the issues connected with interpreting features as partial functions. Both these issues were studied in [25] which shows, among other things, how partiality can be easily simulated in Horn-DLFD.
Example 2 Figure 3 lists the subsumptions for a Horn-DLFD TBox that provides an ontological view of the relational schema illustrated in Figure 1. Part (a) are subsumptions that capture column definitions and data dependencies manifest in the schema itself. This part of an ontology can be automatically generated (for an outline of a procedure to do this, see [25]). Observe in particular how the name attached to a foreign key constraint, such as headRef, is mapped to a feature with the same name. Part (b) illustrates how additional data dependencies not expressible without appeal to general assertions in SQL can also be captured in Horn-DLFD. Here, the (presumed) fact that name values of employees are disjoint from name values of departments is captured by appeal to an asymmetric use of PFDs. Finally, Part (c) illustrates how an ontology can be enhanced by adding further subsumptions, in this case relating to the virtual concept of a manager.
Conjunctive queries are, as usual, formed from atomic queries (or atoms) of the form "A(x)" and "x.f = y", where x and y are variables, using conjunction and existential quantification. To simplify notation, we conflate conjunctive queries with the set of its constituent atoms and a set of answer variables: Definition 3 (Conjunctive Queries and Certain Answers) Let A(x i ) and x i1 .f i = x i2 be (first-order) atoms, where A is a primitive concept , f i is a feature, and x and ȳ tuples of variables. A conjunctive query (CQ) ϕ is an expression of the form ∃ȳ. ψ with free variables x, that is constructed from the above atoms ψ using conjunctions and existential quantification.
Let K be a Horn-DLFD knowledge base and ϕ a CQ. A certain answer to
As usual, UCQ stands for a union of CQs. To study the first-order rewritability of conjunctive queries over Horn-DLFD TBoxes, we use the following version of the combined combined approach to OMQ in our setting.
Proposition 4 (Combined Combined Approach to OMQ [25,27,30]) Let K = (T , A) be a Horn-DLFD knowledge base and ϕ a conjunctive query.
Then there is a UCQ query ϕ T and a Datalog program Π T , both of which can be effectively constructed from T , such that
for a tuple of constant symbols ā and where Π T (A) is the minimal model of Π T when evaluated over A.
The proposition uses a Datalog program Π T to define an ABox completion over which the query ϕ T , the rewriting of the original user query, is evaluated to compute the certain answers. The Proposition also shows that the data complexity of OMQ in Horn-DLFD is complete for PTIME.
To simplify the presentation, we assume that Horn-DLFD TBoxes are in a normal form given as follows:
Definition 5 (Normal Form of Horn-DLFD TBoxes) Let T be a Horn-DLFD TBox. We say that T is in normal form if all subsumptions adhere to one of the following six forms: (consequences of T ) (completion rule in Π T )
For every primitive concept B, we introduce an unary EDB predicate P B (x) together with an additional clause C B (x) ← P B (x) that captures explicit data in an ABox of the form A(a), and an IDB predicate C B (x) corresponding to the completion of the ABox w.r.t. T . For features, we use R f (x, y) as a synonym for ABox assertion f (x) = y to conform with standard Datalog syntax. We also define an auxiliary symbol C ⊥ (x) that will be used to test for ABox consistency.
Note that the subsumptions for unqualified inverse features (5) and PFDs (6) do not contribute to the definition of an ABox completion since they do not generate additional ABox assertions for primitive concepts. Also note that, unlike in the classical combined approach [19,23], our combined combined approach does not introduce any new constants in the ABox [27].
To test for first-order definability of the completion (i.e., all predicates that stand for the completed ABox instance), we use the following construction: Note that Clark's result works in the much more general setting of logic programs with function symbols and possibly infinite 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 definability. Note that had we used Π T instead, none of the definability results could possibly hold. Note that in absence of role/feature subsumptions (such as role hierarchies) we do not need to apply the completion to the R f atoms.
Proposition 9 (Projective Beth Definability [3]) Let Σ be an FO theory over symbols in L and L ⊆ L. Then the following are equivalent:
, and a tuples of constants, and 2. ϕ is equivalent under Σ to a formula ψ in L .
Theorem 10 Let T be a Horn-DLFD TBox over the primitive concepts and features {A 1 , . . . , A k , f 1 , . . . , f n }, and let T be a conservative extension of T in normal form. Then the completion of the primitive concept A w.r.t. T is first-order definable if and only if C Ai (x) is Beth definable over Σ T and L = {P A1 , . . . , P A k , R f1 , . . . , R fn }.
Proof. Follows immediately from the properties of Beth definability (Proposition 9) and the definition and properties of the Clark's completion (Proposition 8).
Observe that one can restrict the alphabet of the ABox (L ) to target only ABoxes over restricted signature(s).
Given Σ T , one can now reformulate (1) in Proposition 9 as a logical implication problem by making a copy of all formulas of Σ T in which all non-logical symbols not in {P A1 , . . . , P A k , R f1 , . . . , R fn } are starred. Hence, the definability question for C A (x) can be expressed as a logical implication question of the form:
Note that, on closer inspection, all formulas in Σ T can be written as ALCI subsumptions. 2 Hence:
Theorem 11 Let T be a Horn-DLFD TBox. Then the existence of 1. the first order rewritability of the A completion with respect to T , 2. the consistency of T , and 3. the uniform query rewritability over T are all decidable and in EXPTIME.
Proof. The first claims follow immediately from Theorem 10 applied to all atoms of the form C B and the decidability and complexity of reasoning in ALCI. The second claim relies on definability of C ⊥ (x) and, in the presence of key PFDs of the form A B : Pf 1 , . . . , Pf k → Pf, on the definability of C A (x) and C B (x) since the remaining consistency check for PFD satisfaction can then be expressed as a first-order query with respect to these explicit definitions. The last claim follows by observing that (i) definability of atomic queries implies definability of arbitrary (U)CQs using the combined-combined approach [25], and that (ii) non-definability of a single atomic query exhibits the need for a non first-order ABox completion for queries containing/consisting of this atom.
Note that in the third case one can restrict the definability conditions to atoms that can appear in the query ϕ T . A matching lower bound can be obtained for expressive fragments of Horn-DLFD (for which the reasoning complexity is EXPTIME-complete). However, the exact complexity is open for PTIME fragments, such as CF D nc and CF DI ∀− kc . Note, however, that since the size (and the construction) of rewritings will dominate this cost (even for the simplest ontology languages [18]), exact complexity bounds are mostly of academic interest.
Example 12 Returning to our introductory example, we find out that neither C EMP (x) nor C DEPT (x) nor the TBox-derived C MAN (x) atom are first-order definable. We confirmed this using a tableau-based depth-limited interpolant generator [16,31]. One of the reasons is that an ABox can contain a chain of alternating deptRef/empRef features without having the objects along this chain alternately belonging to the EMP and DEPT concepts, save the individual at the beginning of this chain. The Datalog completion rules are needed to propagate these concept assertions along such a chain.
To obtain an algorithm that constructs rewritings from our characterization of FO rewritability, we utilize Craig Interpolation: Proposition 13 (Craig Interpolation [12]) Let ϕ and φ be first order formulas such that |= ϕ → φ. Then there is a first order formula ψ, called Craig interpolant, containing only symbols common to ϕ and φ such that |= ϕ → ψ and |= ψ → φ.
Moreover, the interpolant can be extracted, typically in linear time, from a proof of |= ϕ → φ, as long as a reasonably structural proof system, such as resolution, (cut-free) sequent calculus, and/or analytic tableau is used.
The formulation (1), after a minor manipulation of the formulas, can thus be used to construct a Craig interpolant for C A (x) from a (analytic) tableau proof of the above logical implication statement (if one exists): one can construct, with the help of blocking [1,13], a finite analytic tableau for (1). The size of the rewriting, however, will depend crucially on the proof system used and on the presentation of the rewriting. However, by using an optimal tableau for ALC [13] (modified for ALCI), one can construct an exponential representation of the rewriting by sharing common subexpressions in the same way the tableau algorithm caches already unsatisfiable sets. However, plain first-order representation of the formula will suffer from additional exponential blowup, as one would expect.
Combining the above construction with the already existing rewriting ϕ T from [25] we get: Theorem 14 Let K = (T , A) be a Horn-DLFD knowledge base. Then the data complexity of conjunctive query answering is in AC 0 whenever the A completion with respect to T is first-order definable with respect to Σ T .
Proof. Let ψ A (x) be a first order definition of
is a first order formula, in particular a UCQ in the case of Horn-DLFD.
For ABoxes constructed from relational instances (see the discussion in our Introduction and Background Sections), relational systems commonly enforce integrity constraints such as primary and foreign keys. The effect of these database constraints is that parts of the corresponding ABox are not only consistent with such constraints but are a model. This observation is in particular helpful in the case of foreign keys since they stipulate that parts of the ABox completion are no longer necessary: for a foreign key to hold in an instance of a relational database, either its target exists in the appropriate table or the source is NULL, which can then be interpreted as value unknown and is taken care of by query rewriting ϕ T .
Definition 15 (Adding Foreign Keys) Let A B and A ∀f.B be subsumptions corresponding to foreign keys that capture ISA and attribute typing, respectively. For each such constraint, add P B (x) ← C A (x) and P B (x) ← C A (y), R f (x, y), respectively, to Σ A .
This definition allows us to sidestep parts of the ABox completion that are mandated by the database constraints and thus already exist in the original instance of the ABox. As a consequence, we have the following extension of Theorem 14:
Theorem 16 Let K = (T , A) be a Horn-DLFD knowledge base. Then the data complexity of conjunctive query answering is in AC 0 whenever the A completion with respect to T is first-order definable with respect to the theory Σ T ∪ Σ A .
Example 17 Continuing with our example, adding the constraints
to Σ A , both C EMP (x) and C DEPT (x) become definable with the expected interpolants C EMP (x) and C DEPT (x) found by the above-mentioned interpolant generator [16,31]. Moreover, C MAN (x) also becomes definable by ∃y.P EMP (x)∧R manRef (y, x) (again, using the interpolant found by the interpolant generator).
Our approach also provides decidability for the non-uniform (query-specific) problems:
Theorem 18 Let T be a Horn-DLFD TBox and ϕ a (U)QC. Then the following are equivalent:
1. Σ T ∪ Σ * T |= ∀x.ϕ T → ϕ * T (x), and 2. ϕ is first-order rewritable with respect to T .
The exact complexity again depends on the complexity of (1) above. In the general case, an EXPTIME bound follows from [15], but again, a more refined analysis is in order for fragments of Horn-DLFD.
We have shown how the combined combined approach to OMQ can be used to determine when query answering mediated by a Horn-DLFD TBox can be reduced to a first order query over a plain ABox (or, in turn, over the underlying data source), and when a non-first order (Datalog-based) completion of the data is needed. Interestingly enough, and unlike other approaches that aim on determining first-order rewritability, our approach links the problem to well studied issues of explicit definability [3], interpolation [12], and to Clark's completion of logic programs [11]. In addition, our approach naturally and seamlessly incorporates database constraints that hold in the data source to improve our chances of finding a first order rewriting.
Further extensions of this work along the following lines is needed:
-Performing a fine-grained analysis of computational complexity for tractable members of Horn-DLFD, such as CF D nc . (We conjecture that the rewritability problem will remain intractable.) -Determining if a dichotomy holds, in particular, if non-rewritability implies NL hardness of OMQ in data complexity. (We conjecture that this is the case since blocked branches of a tableau proof signal non-rewritability and can be used to simulate, e.g., s-t connectivity similarly to the approach in [21].) -Extensions to situations in which ABox closure requires a finite number of additional auxiliary constants. (The approach itself can immediately use Skolem functions to deal with such constants while retaining completeness. However, decidability and complexity issues stemming from the use of Skolem functions remain to be determined.) -Extensions to DLs outside of the FunDL family, such as the various members of the EL family and to more expressive logics such as Horn-SHIQ. -And integration with an interpolation-based relational query optimizer [16,31] via depth-limited tableau construction, which, for a sufficiently large depth, leads to completeness as in [10].
An additional issue arises from the assumption of UNA. Indeed, this assumption is implicit in [21], where explicit equality among constant symbols is simply not considered, and also in most of the other approaches to OMQ via query rewriting, including the original approach introduced in [9]. In the case of Horn-DLFD, UNA is needed explicitly to accommodate keys and PFDs. We conjecture that some form of UNA is necessary, but whether restricted variants could suffice is unknown.
First order rewritability for Horn logics in the ALC/SHIQ family has been studied by others, e.g., see [4,6]. This earlier work has also developed algorithms for generating such rewritings efficiently for logics in the EL family [14]. 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 [16,29]. 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 [5] does provide a guide to what rewritings are reasonable to consider during query optimization.
The use of database constraints, or constraints implied by data mapping rules and database constraints, has been explored in several systems that implement variants of perfect rewriting [9], such as Ontop and MASTRO [2,8] and others. Our approach, however, seamlessly accommodates such constraints into the rewriting via interpolation and, again, could serve as an unifying approach between perfect rewriting-based approaches and the combined approach, even for DL-Lite based approaches to OMQ/OBDA.
Our approach cannot deal with rewritings to Datalog/and or Linear Datalog and with dichotomies on the NL-PTIME [21] and PTIME-coNP boundaries [24]: extensions of definability/interpolation beyond first order theories do not seem to exist at present and it is unclear whether similar approaches can be developed due to the close ties between interpolation and compactness of first order theories.
Finally, note that Beth definability and Craig Interpolation have been used for other purposes, such as query reformulation under first-order constraints [7,16,29,31]. That use, however, is orthogonal to the topic of this paper.