Satisfaction and Implication of Integrity Constraints in Ontology-based Data Access

1 Introduction

Ontology-based data access (OBDA) is a popular approach for integrating heterogeneous data sources [Poggi et al., 2008; Calvanese et al., 2017; Kharlamov et al., 2017]. In OBDA, an ontology represents a global conceptual model reconciling the mismatches between the source schemas and providing users with the vocabulary for query formulation. The relationship between the ontology and the source schemas is declaratively specified using global-asview (GAV) mappings [Lenzerini, 2002], which assign to ontology predicates a set of views over the data sources.

Mappings (1)-(3) below are used to populate the ontology concept Property and roles heldBy and claims.

Axiom (4) below identifies anyone making an application as a Claimant, whereas (5) identifies anyone holding a property as a Landlord. Axioms (6)-(7) also state that everything claimed for by a claimant or held by a landlord is a property.

∃heldBy- ⊑ Landlord (5)

∃heldBy ⊑ Property (7)

When integrating data under a common schema, one may want to ensure that certain constraints are globally satisfied. In Example 1 we may want to ensure that (C1) each property is associated with a landlord; and (C2) landlords cannot apply for benefits related to a property they hold. Intuitively, constraint (C1) is violated since 30 Rossetti is not associated with a landlord; in contrast, constraint (C2) is satisfied since B. Lyndon (the only landlord) has not claimed any benefits.

The importance of representing integrity constraints in the unified schema has been stressed in many works on data integration (e.g., see [Lenzerini, 2002; Cal`ı et al., 2004]). Faithfully representing such constraints in OBDA is, however, challenging due to the well-known mismatch between the closed-world semantics of integrity constraints in databases and the open-world semantics of ontology languages [Sequeda et al., 2012; Calvanese et al., 2014].

Integrity constraints in relational databases are used to check whether the given data satisfies certain conditions. For instance, one may introduce a functional dependency (C3) in Table S stating that no one can claim benefits on two different properties, which holds in our example. During database updates, a check is performed to see whether a person is now claiming for different properties, in which case the update is rejected; if the update is accepted, however, the constraint can be safely disregarded for the purpose of query answering.

The obvious representation of global constraints (C1) and (C3) using ontology axioms (8) and (9) below, however, yields a markedly different behaviour.

In particular, adding axiom (8) to the ontology would not raise an error in the data; instead, it would trigger the inference that 30 Rossetti is associated with some (unknown)

landlord. Furthermore, in contrast to database integrity constraints, axiom (8) affects query answering; e.g., when given a query asking for all properties associated to some landlord, an OBDA system will return 30 Rossetti as part of the answer even though the owner of this property is not given in the data. Ontology languages used in OBDA are thus closely related to incomplete databases, where data is assumed to be partially specified and dependencies are used to extend the database with missing information.

The problem of combining ontology languages with integrity constraints has received significant attention in the literature [Donini et al., 2002; de Bruijn et al., 2005; Calvanese et al., 2007a; Motik et al., 2009; Motik and Rosati, 2010; Tao et al., 2010; Patel-Schneider and Franconi, 2012; PatelSchneider, 2015]. In this paper, we explore in the context of OBDA the formalism by Motik et al. (2009), where knowledge bases consist of a description logic (DL) TBox and an integrity constraints component where constraints are interpreted as checks over minimal models of the TBox and the data. The framework ensures that, once constraints have been satisfied, they can be safely disregarded for query evaluation. This is a very desirable property in the context of OBDA: constraint satisfaction can be checked whenever the source data is updated, whereas state-of-the-art OBDA systems can continue to be used for query answering without modification.

Our contributions are as follows. In Section 3 we extend the framework by Motik et al. (2009) to OBDA. In addition to a TBox T , mappings M, and source database D typically considered in the OBDA literature, we also consider sets of source constraints Σ and target constraints C. Satisfaction of Σ is defined as usual in databases, by requiring D |= Σ. In contrast, satisfaction of C requires that the constraints hold in a suitable minimal model of T ∪M ∪D. We argue that all the desirable properties proved in [Motik et al., 2009] seamlessly extend to OBDA. In our framework, there is also a clear need to understand the semantic relationship between sets of source and target constraints; for instance, when bootstrapping a source schema, we may want to check whether the source constraints have been faithfully propagated to the target schema [Sequeda et al., 2012; Calvanese et al., 2014; Console and Lenzerini, 2014; Console, 2016]. To this end, we define the source-to-target implication problem, which is to check whether a target constraint γ is satisfied (with respect to T and M) by all databases D satisfying Σ, in which case γ does not impose additional requirements to the data. Conversely, we define target-to-source implication, which is to check whether a source constraint σ is satisfied by all databases D satisfying the target constraints C with respect to T and M, in which case σ is captured by C. These problems are strongly related to dependency propagation-a classical problem in databases [Klug, 1980; Klug and Price, 1982; Sagiv, 1987; Abiteboul and Hull, 1988; Fan et al., 2008]; indeed, many of our lower bounds hold for the empty TBox and thus transfer to the database setting.

In Section 4 we study the satisfaction problem for target constraints consisting of disjunctive tuple-generating dependencies and show that it is Πp2 -complete if the TBox is expressed in DL-LiteR. We also study the data complexity of this problem by assuming that the TBox, mappings, and constraints are fixed, and establish tractability in LOGSPACE, which suggests feasibility in practice. To the best of our knowledge, these are the first complexity bounds for constraint satisfaction as defined in [Motik et al., 2009].

In Section 5 we show that, for DL-LiteR TBoxes, sourceto-target implication is decidable whenever the language of source constraints Σ has decidable finite entailment problem. Furthermore, we establish tight 2EXPTIME and EXPTIME bounds for Σ consisting of frontier-guarded tuple-generating dependencies [Baget et al., 2011] and for Σ consisting of full dependencies, respectively. We also establish PSPACEcompleteness for Σ a set of linear dependencies, and Πp2 - completeness for Σ a set of functional dependencies.

Finally, in Section 6 we study target-to-source implication and establish complexity bounds for the case where constraints and mappings are frontier-guarded, and T is a DL-LiteR TBox satisfying certain restrictions. Our upper bounds are obtained via reduction to satisfiability of guardednegation (GNFO) first-order sentences [B´ar´any et al., 2015].

2 Preliminaries

We adopt standard notions in first-order logic with equality (≈). Entailment and satisfaction of sentences by interpretations (|=) are defined in the standard way. The size |ϕ| of a formula (or set of formulas) ϕ is also defined as usual.

Dependencies. A dataset is a finite set of ground atoms not mentioning equality or function symbols. A disjunctive tuple-generating dependency (DTGD) is a function-free sentence σ of the form ∀xy. (ϕ(x, y) → ∨ni=1 ∃zi. (ψi(x, zi))), where n ≥ 1, x, y, z1, . . . , zn are pairwise disjoint tuples of variables, and ϕ(x, y), ψ1(x, z1), . . . , ψn(x, zn) are conjunctions of equality-free atoms over all the given variables and possibly also constants. Formula ϕ(x, y) is the body of σ, whereas formula ∨ni=1 ∃zi. ψi(x, zi) is the head. If n = 1, then σ is called a TGD and if, in addition, ϕ(x, y) comprises at most one atom, then it is called linear. A full dependency is a TGD without existentially quantified variables and where the head consists of a single atom. An inclusion dependency is a linear TGD with a single atom in its head. 1 A DL-LiteR dependency is an inclusion dependency with predicates of arity one or two and atoms mentioning no constants or repeating variables. A functional dependency (FD) on an n-ary predicate P between two sets of positions ∅ ⊂ X, Y ⊆ {1, . . . , n} is a function-free sentence of the form ∀xy. (P(x) ∧ P(y) → ∧j∈Y xj ≈ yj), with x = x1, . . . , xn, y = y1, . . . , yn, and yi = xi iff i ∈ X. A dependency σ is a DTGD or an FD. The frontier of σ is the (possibly empty) set of universally quantified variables occurring in both the body and the head. We say that σ is frontierguarded (respectively, guarded) if the body has an atommentioning all frontier variables (respectively, all its variables). The schema of a set of dependencies Σ is the set Sch(Σ) of predicates in Σ different from ≈. From now onwards, universal quantifiers in dependencies are omitted for brevity. We use Skolemisation to interpret dependencies in Herbrand interpretations. In particular, for each dependency σ with frontier x and each existentially quantified variable zi, we define a globally unique function symbol f iσ of arity |x|, and we let substitution θsk map each zi in σ to its corresponding functional term f iσ (x). The Skolemisation of σ is the sentence obtained by applying θsk to σ; the Skolemisation sk(Σ) of a set of dependencies Σ is defined in the obvious way.

1 Our definition is more general than the standard one, as it allows for atoms with constants and multiple occurrences of a variable; this facilitates exposition and has no impact on lower bounds.

QueryAnswering. Aconjunctive query (CQ) is a functionfree and equality-free first-order formula q(x) constructed using conjunction and existential quantification only. A union of conjunctive queries (UCQ) is a formula ∨ni=1 qi(x), where each qi(x) is a CQ. The schema of a UCQ q is the set Sch(q) of predicates used in q. A certain answer to a UCQ q(x) over dependencies Σ and a dataset D is a tuple c of constants satisfying Σ ∪ D |= q(c); the set of such certain answers is denoted as q(Σ,D) . If Σ consists of TGDs only, sk(Σ)∪D admits a unique minimal Herbrand model H such that, for each UCQ q(x) and tuple c of constants, H |= q(c) iff c ∈ q(Σ,D) .

OBDA. We assume countably infinite and pairwise disjoint sets S and T of source and target predicates respectively. Dependency σ is a source dependency if it satisfies Sch(σ) ⊆ S, and it is a target dependency if Sch(σ) ⊆ T. Source and target datasets are defined analogously. As usual in OBDA, we restrict ourselves to DL-LiteR ontologies and GAV mappings. A TBox is a finite set T of DL-LiteR target dependencies. A mapping set M is a finite set of constant-free full dependencies with non-empty frontier where all body predicates belong to S and all head predicates belong to T. We say that M is injective if no two dependencies share a head predicate and that M is trivial if it is injective and has only dependencies of the form P(x1, . . . , xn) → P ′ (x1, . . . , xn). The virtual image of a mapping set M and a source dataset D is the target dataset VM,D consisting of all atoms P(c) such that ϕ(x, y) → P (x) is in M and D |= ∃y. ϕ(c, y). The certain answers q(T ∪M,D) to a query q over the target vocabulary coincide with q(T ,VM,D) . The unfolding of a formula ϕ with respect toM, where Sch(ϕ) ⊆ T, is the formula unfoldM(ϕ) obtained from ϕ by replacing each atom P(t) with ⊥ (if M does not mention P) or with ∨ni=1 ∃yi. ϕi(t, yi), where ϕ1(x1, y1) → P(x1), . . ., ϕn(xn, yn) → P(xn) are all mappings in M for P. The unfolding of a set of formulas is defined in the obvious way.

GNFO. We also consider the guarded-negation fragment of first-order logic (GNFO) [B´ar´any et al., 2015] consisting of formulas ϕ specified by the following grammar, where α ranges over atoms, and expressions α(x, y) and ϕ(x) denote that x∪y and x are the free variables in α and ϕ, respectively:

The restriction over first-order logic is the requirement that all free variables of a negated expression must be guarded by an atom. GNFO enjoys the finite model property, and satisfiability checking is 2EXPTIME-complete [B´ar´any et al., 2015].

3 OBDAwith Integrity Constraints

We next present our extension of OBDA with integrity constraints, and define the relevant reasoning problems. In addition to a TBox T , mappings M, and source dataset D, we also consider finite sets of source dependencies Σ (the source constraints) and target dependencies C (the target constraints). Satisfaction of Σ is defined as usual in databases, by assuming that source data is complete and requiring D |= Σ. In contrast, satisfaction of target constraints C must be consistent with the open-world semantics of OBDA, where query answering is defined in terms of all models of T ∪ VM,D.

Motik et al. (2009) proposed a formalism that combines a DL ontology consisting of TBox T and target dataset A with integrity constraints C. Constraints C are satisfied if they hold in all minimal Herbrand models of sk(T ) ∪ A, in which case they do not influence query answering. Skolemisation is introduced to address the semantic difficulties posed by existential quantifiers in the TBox: it ensures that equivalent TBoxes satisfy the same constraints. The following definition extends the semantics by Motik et al. to OBDA in the obvious way.

Definition 1. A source dataset D satisfies a set C of target constraints with respect to a TBox T and a mapping set M, written D |=[M,T ] C, if the minimal Herbrand model of sk(T ) ∪ VM,D is also a model of C.

Example 2. Let D, M, and T be as in Example 1, and let C = {γ1}, where γ1 formalises constraint (C1) as the dependency Property(x) → ∃z. heldBy(x, z) ∧Landlord(z). Then, as intuitively expected, D ̸|=[M,T ] C since the minimal Herbrand model of sk(T )∪VM,D satisfies Property(30 Rossetti) and does not satisfy ∃z. heldBy(30 Rossetti, z).

As in [Motik et al., 2009], the definition of constraint satisfaction ensures that target constraints satisfied by the data can be safely disregarded for query answering.

In contrast to Motik et al. (2009), our OBDA framework defines two types of constraints, which are satisfied according to different semantics. In this setting, there is a clear need to analyse the semantic relationship between source and target constraints, e.g., to understand whether a source constraint is propagated via the mappings to the target. To this end, we next formalise the notion of constraint implication.

Definition 2. Let Σ and C be sets of source and target constraints respectively, let T be a TBox and M a mapping set.

We say that Σ implies a target constraint γ with respect to T and M, written Σ |=[M,T ] γ, if, for every source dataset D, it holds that D |=[M,T ] γ whenever D |= Σ.

Conversely, C implies a source constraint σ with respect to T and M, written C |=[M,T ] σ, if, for every source dataset D, it holds that D |= σ whenever D |=[M,T ] C.

Example 3. Let D, M, and T be as in Example 1, and let Σ = {σ1} where σ1 formalises constraint (C3) in the introduction as S(x, x1) ∧ S(x, x2) → x1 ≈ x2. For the target constraint γ1 from Example 2, we have that D ̸|=[M,T ] γ1 and because D |= Σ, we derive that Σ ̸|=[M,T ] γ1. However, if we extend Σ with the inclusion dependency σ2 = S(y, x) → ∃z1, z2. T(x, z1, z2), we can then verify that Σ |=[M,T ] γ1.

Let γ2 = claims(x, x1) ∧ claims(x, x2) → x1 ≈ x2 and γ3 = Claimant(x) → ∃z1, z2. claims(x, z1)∧heldBy(z1, z2). For C = {γ2, γ3} one can verify that C |=[M,T ] σ1 as a result of γ2 being in C, and also that C |=[M,T ] σ2.

4 Constraint Satisfaction

In this section we study the complexity of checking D |=[M,T ] C for T a DL-LiteR TBox.

Motik et al. (2009) proved decidability of constraint satisfaction for T an ALCHI TBox and C consisting of arbitrary first-order sentences. Although decidability extends to our setting, the proof in [Motik et al., 2009] is by reduction to satisfiability of MSO formulae on infinite k-ary trees (SkS) and thus only provides a non-elementary upper bound.

We next show that the problem becomes Πp2 -complete if T is DL-LiteR and C consists of DTGDs. The lower bound follows from a result by Pichler and Skritek (2011), who showed that the problem of checking whether a dataset satisfies a TGD is Πp2 -hard. To establish the upper bound we rely on [Cal`ı et al., 2012] and show that, if a target constraint γ does not hold in the minimal Herbrand model H of sk(T )∪VM,D (and hence D ̸|=[M,T ] γ), then γ is violated already in a fragment of H where the depth of all functional terms is bounded by a polynomial in the size of T , γ, and M.

Definition 3. Let T be a DL-LiteR TBox, let A be a target dataset, and let γ = ϕ(x, y) → ∨ni=1 ∃zi. ψi(x, zi) be a target constraint. A counter-example to γ with respect to T ∪ A is a mapping λ of x to terms in the Herbrand Universe of sk(T ) ∪ A such that sk(T ) ∪ A |= ∃y.ϕ(λ(x), y) but sk(T ) ∪ A ̸|= ∨ni=1 ∃zi. ψi(λ(x), zi).

Lemma 1. Assume that D ̸|=[M,T ] γ, for γ a target constraint of the form ϕ(x, y) → ∨ni=1 ∃zi. ψi(x, zi). Let H be the minimal Herbrand model of T ∪ VM,D and let Hd be the subset of H involving terms of functional depth at most d = 16 · p · |γ|, with p the number of target predicates in T , M, and γ. Then, there exists a counter-example λ to γ with respect to T ∪ VM,D such that Hd |= ∃y. ϕ(λ(x), y).

The result in the lemma immediately suggests a nondeterministic algorithm for checking the complement of constraint satisfaction. To check that D ̸|=[M,T ] γ, we

• guess a mapping λ from the frontier variables x of γ to ground terms of functional depth at most d involving constants fromD; and
• check that sk(T ) ∪ VM,D |= ∃y. ϕ(λ(x), y) and sk(T ) ∪ VM,D ̸|= ∨ni=1 ∃zi. ψi(λ(x), zi) using two NP oracles.

Theorem 2. Checking D |=[M,T ] C is Πp2 -complete if T is DL-LiteR and C consists of DTGDs; the lower bound holds already if we require T = ∅, and C to consist of a single TGD.

We conclude this section by showing that constraint satisfaction is in LOGSPACE in data complexity under the assumptions of Theorem 2. The result also relies on Lemma 1, where the depth d is now constant since T , M, and C are fixed. Furthermore, VM,D and the relevant model fragment Hd can be generated using logarithmic space. Finally, checking Hd |= γ is clearly feasible in LOGSPACE for fixed γ.

Theorem 3. For T a fixed DL-LiteR TBox, C a fixed set of DTGDs, and M a fixed mapping set, checking D |=[M,T ] C for an input source dataset D is in LOGSPACE.

5 Source-to-Target Constraint Implication

We now turn our attention to the problem of checking whether Σ |=[M,T ] γ for T a DL-LiteR TBox.

We show decidability for any class of source constraints with decidable finite entailment problem. Furthermore, we establish tight complexity bounds showing that source-totarget implication is no harder than finite entailment for the following classes of source dependencies: (i) frontierguarded TGDs, (ii) full dependencies, and (iii) linear dependencies. We also show Πp2 -completeness for Σ consisting of FDs. All our lower bounds hold for T = ∅, which allows us to obtain new results for the dependency propagation problem in databases. Finally, we show that considering TBoxes based on full dependencies immediately leads to undecidability.

We next describe an algorithm for checking Σ ̸|=[M,T ] γ when Σ is an arbitrary set of dependencies, T is a DL-LiteR TBox, and γ is a DTGD of the form ϕ(x, y) → ∨ni=1 qi(x) with each qi a CQ. Our algorithm searches for a witness source dataset Dw satisfying Σ but not γ with respect to T andM. In doing so, it relies on two main observations.

First, each counter-example λ to γ w.r.t. T ∪VM,Dw is justified by a subset D of Dw containing linearly many constants and atoms in the size of γ and M. Our algorithm will check D |=[M,T ] γ for all D up to the relevant size; as discussed in Section 4, this check can be done by considering a shallow fragment of the minimal Herbrand model H of sk(T )∪VM,D.

Second, any such source dataset D with D ̸|=[M,T ] γ as per counter-example λ may not satisfy Σ, in which case we need to extend D to a (finite) model D′ of Σ. Such extension, however, may also yield an extended virtual image VM,D′ which may invalidate λ if sk(T ) ∪VM,D′ |= qi(λ(x)) for some CQ qi in the head of γ. Thus, our algorithm checks whether D can be extended to a dataset D′ satisfying Σ and preserving the counter-example λ (and hence still violating γ). To this end, we next introduce the notion of a λ-witness.

Definition 4. Let T be a DL-LiteR TBox, let q(x) be a CQ over T, and let λ map x to ground terms. A λ-witness for T and q(x) is a Boolean CQ q′ = ∃y. ξ(y) over predicates in T such that sk(T ) ∪ ξ(λ′ (y)) |= q(λ(x)) for some injective mapping λ′ from y to constants.

Intuitively, a λ-witness for T and a CQ qi(x) in the head of γ specifies a pattern in the target data, the presence of which is sufficient to invalidate λ. Thus, to ensure that a candidate D not satisfying γ as per λ can be extended to a (finite) model of Σ that preserves λ, it suffices to show that Σ ∪ D does not finitely entail the unfolding of any λ-witness. Finally, since T is DL-LiteR, the size of the relevant λ-witnesses to consider can be bounded by the size of γ.

With these ingredients at hand, we are ready to formalise our algorithm. Let mv and ma be the maximum number of variables and atoms in a mapping from M, and γ = ϕ(x, y) → ∨ni=1 qi(x). We then apply the following steps.

1. Do the following for each source dataset D with at most ma · |γ| atoms defined over the predicates fromM and the constants in γ extended with mv · |γ| fresh constants.
2. Compute the subset Hd of the minimal Herbrand model H of sk(T ) ∪ VM,D involving terms of functional depth at most d, where d is the quantity defined in Lemma 1 for M, T , and γ.
3. For each counter-example λ to γ w.r.t. T ∪ VM,D involving only terms in Hd do the following.
4. Compute the set W of all λ-witnesses q′ for T and a CQ qi(x) in γ such that |q′ | ≤ |qi| and q′ uses only target predicates from M, constants from qi(λ(x)), and quantified variables y1, . . . , y2·|qi|.
5. ii) Compute Qλ = unfoldM(∨q′∈W q′ ).
6. iii) If Σ∪D does not finitely entail Qλ, return true.

2) Return false.

Correctness follows from our previous observations. If the algorithm returns true, then it has found a source dataset D and counter-example λ to γ such that D can be extended to a model D′ of Σ not satisfying Qλ; the construction of Qλ and the properties of unfolding ensure that VM,D′ does not contain a pattern that can make some CQ qi(λ(x)) true in sk(T ) ∪ VM,D′ , thus, λ remains a counter-example. Conversely, Σ ̸|=[M,T ] γ is justified by a D and a counterexample λ involving functional terms of polynomial depth; our algorithm will consider (an isomorphism of) λ and determine existence of a dataset satisfying Σ and preserving λ. The following decidability result immediately follows.

Theorem 4. Checking Σ |=[M,T ] γ is decidable if T is DL-LiteR, γ is a DTGD, and Σ is in a class of dependencies for which UCQ entailment w.r.t. finite models is decidable.

Our algorithm considers exponentially many source datasets of polynomial size; for each of them, the relevant part of the corresponding minimal Herbrand model can be constructed in exponential time. Furthermore, there are exponentially many counter-examples λ to consider and also exponentially many λ-witnesses. Thus, the algorithm performs exponentially many finite query entailment tests. This shows that source-to-target implication is no harder than finite query entailment if we consider classes of source dependencies for which the latter problem is EXPTIME-hard. Thus, our analysis provides 2EXPTIME (resp., EXPTIME) upper bounds for Σ consisting of frontier-guarded TGDs (resp., full dependencies). Furthermore, by considering a simple variant of our algorithm which avoids the explicit construction of Hd in Step 1a and of W in Step 1(b)i, we can establish a PSPACE upper bound for Σ consisting of linear dependencies. The matching lower bounds are obtained via a reduction from finite entailment, and hold for T = ∅ and trivial mappings.

Theorem 5. Checking Σ |=[M,T ] γ for T a DL-LiteR TBox and γ a DTGD is:

1. 2EXPTIME-complete for Σ frontier-guarded TGDs;
2. EXPTIME-complete for Σ full dependencies; and
3. PSPACE-complete for Σ linear dependencies.

The lower bounds hold already for M trivial and T = ∅.

We next show that source-to-target implication becomes Πp2 -complete for Σ consisting of functional dependencies. The lower bound follows by a reduction from CQ containment w.r.t. a DL-LiteR TBox [Bienvenu et al., 2012]. The key observation to establish the upper bound is that it suffices to consider source datasets D of polynomial size. Hence, to decide the complement of our problem, we can guess D and accept if D |= Σ and D ̸|=[M,T ] γ. The former can be checked in polynomial time; the latter can be checked by applying the algorithm in Section 4, which involves additional (existential) guesses and two NP oracle calls.

Theorem 6. Checking Σ |=[M,T ] γ is Πp2 -complete if Σ consists of FDs, T is DL-LiteR, and γ is a DTGD. The lower bound holds already for M a trivial mapping set and Σ = ∅.

We conclude this section by showing that extending the ontology language can easily lead to undecidability. In particular, if T is Datalog (i.e., consists of full dependencies) then we can easily establish a reduction from the non-uniform containment problem for Datalog programs [Shmueli, 1993].

Theorem 7. Checking Σ |=[M,T ] γ is undecidable if T and γ are full dependencies, and even if Σ = ∅ and M is trivial.

6 Target-to-Source Constraint Implication

We finally study the implication problem of checking whether C |=[M,T ] σ. We show decidability for the case where σ, M, and C are frontier-guarded, and T consists of full DL-LiteR dependencies; we leave for future work the investigation of the problem for T an arbitrary DL-LiteR TBox.

To check C |=[M,T ] σ we proceed as follows:

1. We rewrite C with respect to T to obtain a new set C ′ of target constraints. This allows us to eliminate T since we can show that C |=[M,T ] σ if and only if C ′ |=[M,∅] σ.
2. We unfold C ′ with respect to the mappings M.
3. We check finite satisfiability of unfoldM(C ′ ) ∪ {¬σ}.

In Step 1, we rewrite each DTGD γ = ϕ(x, y) → ∨ni=1 qi(x) with respect to T using standard rewriting techniques [Calvanese et al., 2007b]; in particular, we compute a UCQ rewriting ρ2 of the head UCQ ∨ni=1 qi(x) and a UCQ rewriting ρ1 of the body query ∃y.ϕ(x, y) to obtain the set of DTGDs of the from q → ρ2, with q a CQ in ρ1.

Definition 5. Let q(x) be a UCQ and let T be a DL-LiteR TBox. A UCQ ρ(x) is a T -rewriting of q if, for every target dataset A, it holds that q(T ,A) = ρ(∅,A) .

Lemma 2. Let T consist of full DL-LiteR dependencies and let C consist of DTGDs. For each γ ∈ C, let ργ1 and ργ2 be T -rewritings of the body and head of γ respectively, let C ′γ = {q → ργ2 | q a CQ in ργ1 }, and let C ′ = ⋃γ∈C C ′γ .

Then, for each source dataset D, it holds that D |=[M,T ] C if and only if D |=[M,∅] C ′ .

Lemma 2 immediately implies that C |=[M,T ] σ if and only if C ′ |=[M,∅] σ, and hence we have reduced our problem to the particular case where the TBox is empty. As shown in the following example, however, Lemma 2 may not hold if T is a DL-LiteR TBox with existentially quantified dependencies.

Example 4. Consider mapping set M = {A(x) → B(x)}, TBox T = {B(x) → ∃y.R(x, y)}, and target constraint C = {R(y, x) → F(x)}. One can check that C ′ = C, where C ′ is the rewritten constraints as in Lemma 2. Consider D = {A(c)}. Clearly, D |=[M,∅] C ′ ; however, the minimal Herbrand model of sk(T ) ∪ VM,D consists of atoms B(c), R(c, f(c)), and hence D ̸|=[M,T ] C.

Steps 2 and 3 are then justified by the following lemma.

Lemma 3. For σ a DTGD and C consisting of DTGDs, we have that C |=[M,∅] σ if and only if unfoldM(C) ∪ {¬σ} does not admit a finite model.

Correctness of our approach follows from Lemmas 2 and 3. Analysis of Steps 1-3 also provides a 3EXPTIME upper bound. On the one hand, a rewritten set of constraints C ′ of exponential size satisfying Lemma 2 can be computed in exponential time using standard techniques [Calvanese et al., 2007b]; furthermore, if C is frontier-guarded we can ensure that so is C ′ . On the other hand, if C ′ , M, and σ are frontierguarded, then unfoldM(C ′ )∪{¬σ} can be written as a GNFO formula ϕ; finite satisfiability can be checked in 2EXPTIME in |ϕ|, which in turn is exponential in T , C, and M.

Theorem 8. Checking C |=[M,T ] σ is in 3EXPTIME for σ a frontier-guarded DTGD, M a frontier-guarded mapping set, T consisting of full DL-LiteR dependencies, and C consisting of frontier-guarded DTGDs. The problem is 2EXPTIME-hard even if T = ∅ and one of the following holds: either (i) σ is an inclusion dependency, M is trivial, and C is a set of guarded TGDs; or (ii) σ is a linear dependency, M is linear, and C consists of full and linear dependencies.

Theorem 8 provides only 2EXPTIME lower bounds via reductions from query answering under guarded (D)TGDs [Cal`ı et al., 2013; Bourhis et al., 2016]. However, we obtain a 2EXPTIME upper bound if we can ensure the set C ′ of rewritten target constraints computed in Step 1 is of polynomial size. This is so if C consists of inclusion dependencies: CQs with a single atom admit polysize T -rewritings whenever T consists of linear dependencies. The matching 2EXPTIME lower bound is provided by case (ii) in Theorem 8.

Theorem 9. Checking C |=[M,T ] σ is 2EXPTIME-complete for σ a frontier-guarded DTGD, M consisting of frontierguarded mappings, T consisting of full DL-LiteR dependencies, and C consisting of inclusion dependencies.

We conclude by showing that allowing for arbitrary full dependencies in C immediately leads to undecidability, even for the empty TBox. This follows by a straightforward reduction from the fact entailment problem for arbitrary TGDs.

Theorem 10. Checking C |=[M,T ] σ is undecidable if C and σ are full dependencies, and even if T = ∅ and M is injective.

7 RelatedWork

Although there have been many proposals for combining ontologies with integrity constraints, there is no consensus around any specific semantics. As discussed in Section 3, we adopted the one in [Motik et al., 2009] as it provides a number of nice theoretical guarantees; it would be interesting to study OBDA constraint satisfaction and implication under alternative semantics, and the work by Console (2016) could be an interesting starting point in this direction.

Source-to-target constraint implication in the absence of a TBox has been widely studied in the database literature under different names, such as view dependency inference and dependency propagation. The problem is EXPTIME-complete for full dependencies [Fan, 2009], and we showed in Section 5 that the EXPTIME upper bound extends to DL-LiteR TBoxes and target DTGDs. The problem is NP-complete for FDs and join dependencies [Klug and Price, 1982; Fan, 2009] and becomes tractable if the sets of constraints consist of FDs and multi-valued dependencies [Fan, 2009]. Undecidability for the case where mappings are allowed to contain arbitrary algebra expressions in the body and all dependencies are FDs was shown by Klug (1980). Finally, Abiteboul and Hull (1988) showed decidability for FDs and "TBoxes" consisting of non-recursive full dependencies, where undecidability is obtained if recursion is allowed. Source-to-target implication for a generalisation of FDs has been recently studied in the context of data quality [Fan et al., 2008].

Console and Lenzerini (2014) study the protection problem, which is to check whether the virtual image of every source dataset satisfying the given source constraints can be extended to a model of a given DL-LiteA TBox. This problem is closely related to source-to-target implication since, under the Unique Name Assumption, disjointness and functionality axioms in the TBox behave like integrity constraints. They also study the analogue problem of target-to-source implication, called faithfulness. Console and Lenzerini establish EXPTIME upper bounds for both problems when source dependencies are weakly-acyclic sets of TGDs and equalitygenerating dependencies.

Finally, the problem of bootstrapping source schemas into an ontology has been studied in [Sequeda et al., 2012; Calvanese et al., 2014], where certain transformations are proposed for propagating the database constraints to the ontology with the aim of preserving their original semantics.

8 Conclusions and FutureWork

We have proposed an extension of OBDA with source and target integrity constraints and studied the relevant reasoning problems. Our complexity results for constraint satisfaction and source-to-target implication are applicable to the ontology and mapping languages typically used in OBDA, and cover a wide range of constraint languages. Our results on target-to-source implication, however, leave a few gaps that we plan to close in future work; in particular, we will extend our results to arbitrary DL-LiteR TBoxes and investigate whether our 3EXPTIME upper bound in Theorem 8 is tight. Finally, it would be interesting to study constraint satisfaction and implication for the alternative semantics of integrity constraints in ontologies mentioned in the related work section.

Acknowledgements

Research supported by the SIRIUS Centre for Scalable Data Access and the EPSRC projects DBOnto, MaSI3 , and ED3 .