Intensional and Extensional Views in DL-Lite Ontologies

1 Introduction

Views have numerous applications in data and knowledge bases. For example, they can provide the user with virtual data collections derived from elementary objects, thus improving abstraction. Views can also represent a selection of the underlying data that limits the exposure of sensitive information. Indeed, users of a given class may have permission to query the knowledge base only through a set of views, effectively limiting their access to only specific parts of the data. Additionally, views may serve as a specification mechanism for data and knowledge exchange and integration. For example, a set of views can specify the portion of the source data that populates the target knowledge base in an exchange task, or the so-called global schema in data integration.

Generally speaking, the notion of view adapts naturally to ontological knowledge bases. In this paper, we focus on knowledge bases expressed in Description Logics (DL) and, specifically, in the lightweight DL DL-LiteR [Calvanese et al., 2007b]. Intuitively, DLs are logical formalisms representing the domain of interest in terms of concepts, i.e., sets of individuals, and roles, i.e., binary relations between objects. Surprisingly, few papers deal directly with views in DL knowledge bases. In [Buchheit et al., 1998], the authors propose to split the axioms of a DL knowledge base into two sets, one for standard intensional knowledge regarding concepts and roles of interest (forming the schema) and one for defining views, i.e., new unary predicates with an associated definition. While intensional axioms may refer only to schema elements, view definitions may refer to both schema and view elements. In this context, views may be recursive, i.e., their definition may contain (either direct or indirect) references to themselves, thus beyond first-order logic. The authors advocate fixpoint semantics for dealing with cycles in the definitions. Another seminal work on views for DLs is [Beeri et al., 1997], where the authors introduce the problem of rewriting queries using views. Intuitively, the latter asks for a query expression that uses only a set of views defined over a DL knowledge base and is equivalent to the input query. While query rewriting aims at computing a query over the views that is equivalent to the original one, viewbased query answering has the goal of computing the answers to a query by relying only on the pre-computed extensions of a set of views. Observe that rewriting is a technique for addressing view-based query answering, but the latter is a much more general problem. Algorithms and complexity for view-based query answering in DLs, including DL-Lite, have been investigated in [Calvanese et al., 2000; Calvanese et al., 2012].

In this paper, we present a novel framework for including views in DL knowledge bases following an approach similar to the one adopted in [Buchheit et al., 1998], but with the following differences. (i) View definitions in our framework consist of epistemic logic formulae rather than just DL concept expressions. Thus, they can use joins, projections, selections, and differences and the modal operator K to talk about what is "known" in the knowledge base, i.e., answers for queries. (ii) We do not limit views to unary or binary predicates, and thus each view symbol has an associated arity, which corresponds to the number of distinguished variables of the formula constituting its definition. (iii) We disallow recursion in view definitions and base our semantics upon epistemic logic.

Example 1. Assume a DL knowledge base K storing HR data. K defines the following concepts and roles: Emp, for employees, Mng, for managers, Dep, for departments, hasDep, connecting employees to their departments; and hasMng, connecting departments to their managers. The axioms of K define the relationships between the concepts and roles introduced above.

A fundamental notion for the users of K is the relationship between employees, their department, and their managers. This relation is ternary, and its definition requires joins, and therefore it is beyond the expressive power of DLs. However, we can define the desired relationship using a view V . However, to define V properly, we first need to clarify the users' intended meaning for this view.

For example, users may want to define the ontological concept isMngOf of being the manager of an employee in a department. The following formula ϕmng(x, y, z) defines this view: Emp(y) ∧ hasDep(y, z) ∧ hasMng(z, x).

Also, users may be interested in restricting the concept isMngOf only to the employees, managers, and departments known to the system. That is, those obtained by the certain answers of the query ϕmng to K. We call this view qMngOf. Observe that, while isMngOf is just a handy shortcut for ϕmng, qMngOf is grounded upon an extra-logical concept, i.e., query answers. In this sense, qMngOf is closer to the standard notion of views for databases, and it requires an epistemic extention of first-order logic to be defined in a DL knowledge base. For its definition, we can use the following formula ϕqmng(x, y, z) of epistemic modal logic: K(ϕmng(x, y, z)). Intuitively, ϕqmng(m, e, d) holds in some model of K if only if ϕmng(m, e, d) holds in all the models of K.

Finally, users may want to define complex views by means of a sophisticated use of the notion of query answers. For example, they may be interested in employees and managers of known departments, where the latter are the certain answers of Dep(x) over K. The latter view, that we call kMngOf, can be defined by the formula ϕkmng(x, y, z) defined as follows: ϕmng(x, y, z) ∧ K(Dep(z)).

The above example shows that views can enrich a DL knowledge base with new powerful abstractions. Such abstractions can play a crucial role in ontology exploration and query answering. The introduction of view predicates may also help overcome some intrinsic characteristics of Ontology-based Data Access (OBDA) systems. The first characteristic has to do with the nature of the ontology languages used in OBDA, which typically allow only unary and binary predicates. The use of views provides the possibility of using n-ary predicates in modelling the domain. The second characteristic is related to the restricted expressive power of DL axioms required for decidability. For example, no such languages allow the free use of joins in concepts and role expressions. Once again, views may help to mitigate such restrictions. Moreover, views can be used to introduce a lightweight mechanism for distinguishing truth from knowledge, i.e., being a given query's certain answer. The latter requires a modal mechanism, whose use through views remains controlled, avoiding intractability.

Views in knowledge bases can enhance all standard reasoning tasks of OBDA, including query answering and query containment. Moreover, there are specific reasoning tasks of interest on views, including checking consistency and containment. In this paper, we present several forms of view definitions, and we study the complexity of fundamental reasoning tasks involving them.

The rest of this paper is organized as follows. Section 2 introduces some preliminary notions; in Section 3 we present our framework; in Section 4 we study the complexity of reasoning with positive views; in Section 5 we discuss the impact of negation on view definitions; in Section 6 we conclude.

2 Preliminaries

We briefly review the main concepts used in the technical development of this paper.

Logic and Complexity We will assume basic familiarity with the standard notions of computational complexity and first-order logic, and refer the reader to [Arora and Barak, 2009] for a detailed account. Given a formula φ and a vector of variables ¯x, we will sometimes use φ(¯x) to say that ¯x are the free variables of φ. A substitution ν for ¯x is a mapping from ¯x to a given set of symbols, and ν(φ) is the formula obtained from φ by substituting each x ∈ ¯x with ν(¯x).

Description Logics Knowledge Bases Let NI, NC, and NR be countably infinite sets of individual, concept, and role names, respectively. A DL-LiteR knowledge base (KB), or ontology, is a pair 〈T ,A〉, where T and A are, respectively, a DL-LiteR TBox and a Description Logic ABox, i.e., finite sets of logical axioms of the form

where a, b are individual names, A and P are concept and role names, respectively, B1,B2 are basic concepts, i.e., expressions of the form A, ∃R, and R, R1, and R2 are basic roles, i.e., expressions of the form P or P -. Intuitively, T and A consist of the intensional and extensional information captured by the KB, respectively. As customary, semantics of DL-LiteR are defined via Description Logic interpretations (interpretations for short). An interpretation is a pair I = 〈∆I , ·I 〉, where ∆ is a countable set, called the domain of I, and ·I is a function such that aI ∈ ∆I , for each a ∈ NI, A ⊆ ∆I , for each A ∈ NC, and P ⊆ ∆I ×∆I , for each P ∈ NR. For interpretations, we assume standard names [Levesque and Lakemeyer, 2000], i.e., we assume that ∆I = NI and aI = a, for every interpretation I and a ∈ NI . In other words, we assume that constants are always interpreted into themselves, effectively blurring out the difference between constants and the individuals they represent. The standard name assumption is very common in OBDA, and it implies the unique name assumption. An interpretation I satisfies an axiom α ⊑ β if αI ⊆ βI ; it satisfies α ⊑ ¬β if αI ∩ βI = ∅; and it satisfies A(a), resp. P(a, b), if a ∈ AI , resp. (a, b) ∈ P I . We say that I satisfies 〈T ,A〉, written I |= 〈T ,A〉, if I satisfies all the axioms in the KB.

EpistemicKnowledge Bases We assume the standard epistemic logic based on the modal logic S5 and extend this concept to DL-LiteR ontologies in the spirit of [Calvanese et al., 2007a]. An epistemic formula is a standard first-order formula over NI , NC, and NR that can use the unary modal operator K with the intuitive meaning of 'it is known' or 'it is certain'. Epistemic formulae are interpreted over epistemic interpretations, i.e., pairs 〈w,W〉, where w is an interpretation and W is a set of interpretations that contains w. An epistemic interpretation W = 〈w,W〉 satisfies an epistemic formula φ (written 〈w,W〉 |= φ) if the following hold:

• φ = P(¯ c), with ¯ c ∈ NI , and w |= φ;
• φ = φ1 ∧ φ2 andW |= φ1 andW |= φ2;
• φ = φ1 ∨ φ2 andW |= φ1 or W |= φ2;
• φ = ¬φ1 andW ̸|= φ1;
• φ = ∃x.φ1(x) and W |= φ1(c), for some c ∈ NI .
• φ =K(φ1) and 〈w,W〉 |= φ1, for every w ∈W.

An epistemic interpretation W = 〈w,W〉 is compatible with a KB K if w |= K. Compatible interpretations represent the possible epistemic states of K, i.e., what K might know for sure. Among compatible interpretations, we want those that carry correct and minimal knowledge. Intuitively, given an interpretation W compatible with K, to enforce correctness we require that every possible world of W satisfies the statements of K, and to enforce minimality we require that every interpretation that satisfies the statements of K is a possible world of W. In light of these considerations, we define the epistemic models of a DL-LiteR KB K as follows. An interpretation W = 〈w,W〉 is an epistemic model for K if W is compatible with K and w′ ∈ W if and only if w′ |= K. With a slight abuse of notation, we write W |= K for W is a model of K and use Mod(K) to denote the epistemic models of K. A DL-LiteR KB K is satisfiable if Mod(K) ̸= ∅. Observe that the epistemic models of a DL-LiteR KB K extend the standard notion of models of K, i.e., the set of all interpretations that satisfy K. Therefore, we can naturally extend reasoning tasks of standard DL-LiteR ontologies to the case of epistemic models. Assume an epistemic formula q(¯x) over the alphabet of K with n free variables ¯x. The certain answers of φ over K are the set of substitutions ν for the free variables of φ such that W |= ν(φ), for every W ∈ Mod(K). Given a DL-LiteR KB 〈T , A〉, an epistemic formula φ, and a substitution ν for the free variables of φ, Query Answering is the following decision problem: is ν a certain answer for φ over 〈T , A〉? The data complexity of Query Answering is the complexity of checking whether ν is a certain answer for φ over 〈T ,A〉, for fixed T and φ, and input A and ν. It is easy to see that, if φ does not contain the operator K, Certain Answers defined above coincide with standard certain answers for queries over Description Logics ontologies. Complexity of Query Answering in this context is known in the literature for many interesting cases. For example, when φ is a union of conjunctive queries, i.e., the union of a set of existentially quantified conjunction of atoms without K, Query Answering is NP-complete, and in AC 0 in data complexity ([Calvanese et al., 2007b]). Query Answering for queries expressed via epistemic formulae was first studied in [Calvanese et al., 2007a], where the authors show a broad class of epistemic formulae with AC 0 data complexity.

3 Views for Knowledge Bases

We proceed to introduce our framework for view-enriched KBs. Assume a countably infinite set NV of predicate symbols with an associated arity, pairwise disjoint with NI , NC, and NR. We call NV the set of view names. In what follows, we use N and NO to denote the set of all symbols, i.e., NI ∪ NC ∪ NR ∪ NV , and the set of ontological symbols NI ∪NC ∪NR, respectively. A view definition V (view for short) is a pair 〈v(¯x), φ(¯x)〉, where v is a view name from NV , called the name of V , ¯x is a tuple of distinct variables, and φ(¯x) is an epistemic formula with free variables ¯x, called the definition of V . Observe that, since φ is an epistemic formula, it cannot contain predicates from NV . A View Box V (VBox for short) is a finite set of view definitions such that, for every distinct U,U ′ ∈ V, the name of U is different from the name of U ′ . A view-enriched DL-LiteR intensional specification (intensional specification for short) is a pair 〈T , V〉, where T is a DL-LiteR TBox and V is a VBox. Finally, a view-enriched DL-LiteR KB (KB for short) is a triple 〈T , V, A〉, where 〈T , V〉 is an intensional specification, and A is an ABox.

Example 2. Assume the KB of Example 1. Relevant intensional knowledge is: (i) hasDep connects employees to departments; (ii) departments with a manager have at least one employee; (iii) all managers direct at least one department. The following TBox captures this information.

The ABox A represents relevant extensional information.

Views in the example can be defined by the following VBox

Finally, we write Khr for the triple 〈T , V, A〉 in this example.

Semantics of view-enriched KBs extend the notion of epistemic models of DL-LiteR KBs. A view-enriched interpretation is a triple W = 〈w,W, f〉, where 〈w,W〉 is an epistemic interpretation over NO, and f is an interpretation for NV with domain NI. Given a view V = 〈v(¯x), φ(¯x)〉, we say that W satisfies V if,

where ν is a substitution for ¯x. We call vf the extension of v in W (sometimes denoted by vW ). In simple words, W satisfies V if the extension of V inW is defined according to φ. Assume a view-enriched DL-LiteR KB K = 〈T , V, A〉. We say that W is a model for K if 〈w,W〉 satisfies 〈T ,A〉 and every V ∈ V. We write Mod(K) for the set of all models of K and K |= φ if W |= φ, for each W ∈ Mod(K). We illustrate semantics of view-enriched KBs in the following example.

Example 3. Assume formulae ψi(x) = ∃y∃zRi(x, y, z) with R1 = isMngOf, R2 = kMngOf, and R3 = qMngOf. Intuitively, each ψi asks for managers of departments with at least one employee via the view Ri. Since every department with a manager has at least one employee, and every manager directs a department, we have KHR |= ψ1(x) for x = Alice, x = Cora, and x = Dylan. Moreover, since Dylan and Cora direct departments D1 and D2, respectively, and D1 and D2 are known in the KB, we have KHR |= ψ2(x) for x = Cora, and x = Dylan. On the other hand, while Alice is known to be a manager in the KB, the department she directs is not, and therefore KHR ̸|= ψ2(Alice). Finally, since Bob works in D1, we have KHR |= ψ3(Dylan). On the other hand, Alice and Cora direct no known employee. Therefore, KHR ̸|= ψ3(x), for x = Alice, and x = Cora.

3.1 Reasoning with Views

In a view-enriched KB, it is of interest to study several forms of reasoning involving views to enhance the conceptual analysis as well as our understanding of the data. Below we investigate these forms of reasoning.

View Consistency A fundamental reasoning task in DL KBs is concept and role consistency, i.e., checking whether the extension of a given concept or role is non-empty in some of the possible worlds described by the KB. Consistency allows designers to discover hidden properties of the model and automatically recognize possibly ill-defined concepts and roles. We extend consistency to view definitions with the notion of View Consistency. Given an intensional specification S and a view definition V from S, we say that V is consistent in S if there exists an ABox A and an interpretation W ∈ Mod(〈S,A〉) such that the extension of V in W is not empty. View Consistency is the following decision problem: given S and V as above, check whether V is consistent in S.

ViewContainment Another fundamental reasoning task in DLKBs is concept and role containment. Intuitively, containment asks whether a concept or role extension is contained inside another in all the possible worlds described by K. We extend containment to view definition with the notion of View Containment. Intuitively, a view V is contained in a view V ′ under the KB K if the extension of V is all the models of K. View Containment could be used, for instance, to check for redundancy in view definitions and optimize query answering. Perhaps more interestingly, view containment can be used to check whether a given view enjoys specific properties. For example, View Containment can type the components of a view, i.e., check whether they are subsumed by a given ontological concept.

We formalize the notion of view containment as follows. Given an intensional specification S and view definitions V and V ′ from S, V is contained in V ′ under S, written V ⊑S V ′ , if for every ABox A and model W ∈ Mod(〈S,A〉), the extension of V inW is contained in the extension of V ′ inW. View Containment is the following decision problem: given S, V , and V ′ as above, check whether V ⊑S V ′ .

Query Answering Given a formula ψ over N and a viewenriched interpretation W, we can define naturally when W satisfies ψ, written W |= ψ. In light of this consideration, given a KB K, it is natural to talk about the Certain Answers for ψ over K and therefore Query Answering. To formalize Query Answering in this context, we introduce two classes of formulae over N. A View-Enriched Conjunctive Query (VE-CQ) is an existentially-quantified conjunction of atoms with predicates from N . A View-Enriched Union of Conjunctive Query (VE-UCQ) is the union of finitely-many VE-CQs. Given K and a VE-UCQ Q(¯x), Certain Answers for Q(¯x) over K are defined as customary, and we use ans(Q,K) to denote the set of certain answers of Q over K. VE-UCQ Answering is the following decision problem: for input a viewenriched DL-LiteR KB 〈T , V, A〉, VE-UCQ Q(¯x), and substitution ν for ¯x, check whether ν ∈ ans(Q, 〈T , V,A〉). The data complexity of VE-UCQ Query Answering is the complexity of checking whether ν ∈ ans(Q, 〈T , V, A〉), for input A and ν, and fixed Q, T , and V. We call VE-CQ Answering the restriction of VE-UCQ Answering to VE-CQs.

Query Containment The basic reasoning task in query optimization is Query Containment, i.e., checking whether, given queries Q and Q′ , Q subsumes Q′ . We can naturally extend Query Containment to view-enriched KBs as follows. Given VE-UCQs Q and Q′ and an intensional specification S, we say that Q is contained in Q′ under S, written Q ⊆S Q′ , if ans(Q, 〈S, A〉) ⊆ ans(Q′ , 〈S, A〉), for every ABox A. VEUCQ Containment is the following decision problem: for input Q, Q′ , and 〈T , V〉 as above, check whether Q ⊆S Q′ . We call VE-CQ Containment the restriction of VE-UCQ Containment to VE-CQs.

Computability Before concluding this section, we briefly discuss the decidability of the decision problems defined above.

Assume a VBox V and a VE-CQ Q of the form ∧i Ri(¯ zi)∧ ∧j Sj(¯ zj), where each Ri is an ontological symbol fromNO, and Sj is a view name from NV such that 〈Sj(¯x), φj(¯x)〉 ∈ V. The unfolding of Q according to V is the formula unf(Q, V) ≡ ∧i Ri(¯ zi) ∧ ∧j ψj(¯ zj), where each ψj(¯ zj) is obtained from φj(¯x) by

• Renaming apart the variables in φj(¯x); and
• Substituting ¯ zj to ¯x in φ.

Intuitively, the unfolding described above is a simplified version of the standard notion of mapping unfolding (see, e.g., [Poggi et al., 2008]). The unfolding of a VE-UCQ Q according to V is simply the union of the unfolding of all the conjunctive queries composing Q.

Proposition 1. Assume a VE-UCQ Q, a VBox V, and an interpretation W that satisfies V. W satisfies Q if and only if it satisfies unf(Q, V).

Proposition 1 follows from the fact that Q and unf(Q, V) are logically equivalent under V. Given a VE-UCQ Q and a VBox V, it is clear that unf(Q, V) can be computed in polynomial time w.r.t. Q and V. In spite of this result, all the decision problems defined above are undecidable for unrestricted view definitions due to the the unrestricted use of first-order formulae. We say that an intensional specification is viewonly if it is of the form 〈∅, V〉, i.e., S has no ontological axioms. It is easy to see that View Containment, View Consistency, VE-UCQ Answering, and VE-UCQ Containment are undecidable even for view-only DL-LiteR intensional specifications. Therefore, in order to achieve decidability, we need to restrict the language allowed in view definitions. In the subsequent sections, we present meaningful decidable languages for view definitions and examine the complexity of relevant decision problems.

4 Lightweight Views

In this section, we introduce a class of view definitions that we dubbed lightweight. Lightweight views represent an interesting conceptual extension of DL-LiteR KBs while having a very limited impact on their computational characteristics. A lightweight epistemic conjunction ϕ(¯x) is an epistemic formula of the form

where α and βi, for each i, are conjunctions of relational atoms, ¯x = ¯xo ∪ ¯xk, with ¯xk = ⋃i ¯xi, occur free in ϕ(¯x), ¯ y = ⋃i ¯ yi, and ¯ yo ⊆ ¯ y. A view definition 〈v(¯x), ϕ(¯x)〉 is lightweight if ϕ(¯x) is a lightweight epistemic conjunction, and a knowledge base is lightweight if its views are. Observe that all the views in Example 2 are lightweight. We proceed to analyse the complexity of reasoning with lightweight views. First, given ϕ(¯x) as above, we define the following formulas.

• ϕo (¯xo, ¯ yo) = ∃¯u.α(¯xo, ¯ yo, ¯u);
• ϕk (¯xk, ¯ y) = ∧ni=1 ∃¯ zi.βi(¯xi, ¯ yi, ¯ zi), with ¯xk = ⋃i ¯xi;
• ϕ+(¯x, ¯ y) ≡ ϕo (¯xo, ¯ yo) ∧ ϕk (¯xk, ¯ y)

The canonical ABox A of ϕ+(¯x), resp., ϕk and ϕo , is an ABox obtained from ϕ+(¯x), resp., ϕk and ϕo , by replacing each variable with a distinct individual name. When not otherwise specified, we will assume, w.l.o.g., that each variable z of q is replaced with cz ∈ NI in A, and denote by ¯ cx the image of ¯x in A. In the reminder of this section, we assume a DL-LiteR intensional specification S = 〈T , V〉, lightweight views V = 〈v(¯x), ϕ(¯x)〉 and V ′ = 〈v′ (¯x), ϕ′ (¯x)〉 in V, and VE-UCQ Q and Q′ .

View Consistency Consistency of lightweight views is tractable as the following theorem shows.

Theorem 1. For input S and V as above, View Consistency is in PTime.

To prove the claim, we observe the following. For every W satisfying V, vW ̸= ∅ if and only if W contains a homomorphic copy of the canonical ABox A of ϕ+(¯x). Therefore, one can prove that V is consistent in 〈T , V〉 if and only if 〈T ,A〉 is satisfiable, being T a DL-LiteR TBox. The desired complexity follows from the fact that satisfiability of DL-LiteR KBs can be checked in PTime.

View Containment View Containment is decidable for lightweight views as the following theorem shows.

Theorem 2. For input S, V and V ′ as above, View Containment is NP-Complete.

To prove the claim, we observe the following. Given an ABox A, an epistemic witness of V ′ in 〈S, A〉 is a substitution occurring in ans(ϕ′k , 〈T ,A〉). Assume W ∈ Mod(S,A). Intuitively, a tuple ν(¯x) is in v′W only if ν can be extended to become an epistemic witness. Let Aϕ+ and Aϕk be the canonical ABox of ϕ+ and ϕk , respectively. One can prove that V ⊑S V ′ if and only if there exists an epistemic witness of ϕ′ in 〈S,Aϕk〉 such that ν ′ ∈ ans(〈T ,Aϕ+〉), for some extension ν ′ of ν such that ν(¯x) = ¯ cx. The desired complexity upper bound follows from the fact that we can guess, in nondeterministic polynomial time, Certain Answers for conjunctive queries over DL-LiteR KBs. The lower bound can be obtained with a reduction from Query Answering for DL-LiteR KBs.

Query Answering In light of Proposition 1, checking whether ν ∈ ans(Q,K) amounts to checking whether ν ∈ ans(unf(Q, V), 〈T ,A〉). Therefore, we can prove decidability of VE-UCQ.

Theorem 3. For input K and Q as above, VE-UCQ Answering is NP-Complete and AC 0 in data complexity.

To prove the claim, we observe the following. By a slight abuse of notation, given unf(Q, V), we use q ∈ unf(Q, V) to denote the disjuncts of unf(Q, V). Observe that, for each such q, unf(q, V) is a lightweight epistemic conjunction. In light of these considerations, one can prove that ν ∈ ans(Q,K) if and only if there exists an extension ν ′ of ν such that ν ′ ∈ ans(q+,K), for some q ∈ unf(Q, V). The desired complexity follows from the fact that answering conjunctive queries over DL-LiteR KBs is NP-Complete and in AC 0 in data complexity.

QueryContainment Checkingwhether Q ⊆S Q′ amounts to checking whether unf(Q, V) is contained in unf(Q′ , V) under T . Once again, this is a consequence of Proposition 1. In light of these considerations, we can prove the following.

Theorem 4. For input S, Q and Q′ as above, VE-UCQ Containment is in NP-Complete.

To prove the claim, we observe the following. One can prove that Q ⊆S Q′ if and only if for every q1 ∈ unf(Q, V) there exists q2 ∈ unf(Q′ , V) such that ν ∈ ans(q+ 2 , 〈T ,Aq〉), where Aq is the canonical ABox of q+ 1 and ν(¯x) = ¯ cx. The desired complexity upper bound follows from the fact that one can guess an answer for q+ 2 in nondeterministic polynomial time. To prove the lower bound, we can show a reduction from Query Answering for UCQ under DL-LiteR KBs.

5 Adding Negation

An important feature of ontological languages is the ability to express negative information, i.e., information about what should not hold for a given set of individuals. Unfortunately, several fundamental reasoning tasks become undecidable as soon as we allow unrestricted forms of negation in ontological KBs (see, e.g., [Guti´errez-Basulto et al., 2015]). A standard solution to restore decidability consists in restricting the occurrence of negation to specific syntactic positions. This is the case, e.g., of DL-LiteR KBs where negation can occur only in disjointness axioms. One may wonder whether a less restricted form of negation could be recovered using views. We explore this possibility in what follows, showing that, if we settle for epistemic negation, i.e., negation occurring only in front of the K operator, it is possible to define expressive decidable languages of view definitions.

Intensional Negation We start our analysis of negation in view definitions with intensional negation, i.e., negation occurring only in front of non-epistemic atoms. An intentional conjunction with safe negation is a formula of the form ∃¯ y. ∧i Ri(¯xi, ¯ yi) ∧ ∧j ¬Rj(¯xj, ¯ yj), where ¯x = ⋃i ¯xi, ¯ y = ⋃i ¯ yi, ¯xj ⊆ ¯x and ¯ yj ⊆ ¯ y, for every j, and Ri and Rj are predicates in NO. A conjunctive view definition with safe negation is a view definition 〈v(¯x), ϕ(¯x)〉 such that ϕ is an intentional conjunction with safe negation. Conjunctive views with safe negation have a deep negative impact on decidability of query answering as the following proposition shows.

Proposition 2. For conjunctive views with safe negation, VECQ Answering is undecidable.

The claim follows from the fact that Query Answering for conjunctions with safe negation defined above is undecidable over DL-LiteR KBs ([Guti´errez-Basulto et al., 2015]).

Epistemic Negation A possible way to mitigate the negative effects of negation is to allow it in front of the K operator only. A lightweight epistemic conjunction with negation is an epistemic formula ϕ(¯x) of the form

where ∃¯ y.ψ(¯x, ¯ y) is a lightweight epistemic conjunction of the form ∃¯ y∃¯u. α(¯xo, ¯ yo, ¯u) ∧ ∧ni=1 K(∃¯ zi. βi(¯xi, ¯ yi, ¯ zi)), and ¯ yj ⊆ ¯ y and ¯xj ⊆ ⋃i ¯xi, for each j. A lightweight view with negation is a view definition 〈v(¯x), ϕ(¯x)〉 where ϕ is a lightweight epistemic conjunction with negation. Views in this class can express meaningful properties, e.g., difference between certain answers of conjunctive queries, while preserving query answering decidability. The following theorem defines the computational complexity of query answering with this class of views.

Theorem 5. For lightweight views with negation, VE-CQ answering is Σp2 -complete and AC 0 in data complexity.

To prove the claim, we simply observe that we can unfold Q according to V and obtain a lightweight epistemic conjunction with negation unf(Q, V). Therefore, the desired complexity upper bounds are a direct consequence of the results presented in [Calvanese et al., 2007a]. To prove hardness, we can show an encoding of (the negation of) tuple-generating dependencies(tgds) as lightweight epistemic conjunctions with negation. The desired lower bounds follow from the fact that satisfaction of binary tgds is Π2p -hard ([Pichler and Skritek, 2011]).

While VE-CQ Answering remains decidable for lightweight views with negation, this is not the case of several other relevant reasoning tasks. A notable example is VE-UCQ Containment, as the following theorem shows.

Theorem 6. VE-UCQContainment is undecidable for intensional specifications with lightweight views with negation.

To prove the claim, one can show a reduction from finite tgd entailment, i.e., the problem of checking whether Σ entails τ over finite models, for input a set Σ of tgds and a single tgd τ. Checking finite tgd entailment is a notoriously undecidable problem also in the case of binary tgds ([Beeri and Vardi, 1981]).

Lightweight Epistemic Negation Is it possible to preserve computability of relevant decision problems while still having a restricted form of negation in view definitions? Before concluding this section, we present a meaningful class of views with these characteristics. A lightweight negative epistemic conjunction is a lightweight epistemic conjunction with negation where wj is empty, for each j. In simple words, lightweight negation forbids the use of existentially quantified variables inside the scope of ¬K. A lightweight negative view is a view definition 〈v(¯x), ϕ(¯x)〉 where ϕ is a lightweight negative epistemic conjunction. Lightweight negative views have a limited impact on the decidability of relevant reasoning tasks as the following theorem shows.

Theorem7. For lightweight negative views, VE-CQContainment is in Πp3 .

To prove the claim, one can show that a counter-example of containment, i.e., an ABox A such that ans(Q′ , 〈T , V, A〉) is not contained in ans(Q, 〈T , V,A〉), has size at most polynomial in the input. With this upper bound in place, an algorithm can guess such A in non-deterministic polynomial time, and check whether A is an actual counterexample of containment simply by evaluating queries Q and Q′ over 〈T , V, A〉. The latter can be done using the result presented in Theorem 5. With similar arguments, one can prove decidability of View Containment.

Theorem 8. For lightweight negative views, View Containment is in Πp3 .

Finally, we can show that View Consistency is decidable for lightweight views with lightweight negation. To prove this claim, we can once again show a polynomial upper bound on the size of a counter-example.

Theorem 9. For lightweight negative views, View Consistency is in coNP .

6 Conclusions

We presented a novel framework for enriching DL KBs with views. We defined languages for view definitions that can capture several interesting properties. For views defined in these languages, we studied the complexity of several reasoning tasks and showed that, under reasonable restrictions, views do not impact the overall complexity of reasoning with DL-LiteR KBs. The directions for future work are many. From the practical standpoint, it is of interest to implement our framework in real OBDA systems. From the theoretical standpoint, it is of interest to further investigate negation in view definitions, also considering relationship with the work on merging DLs and rules (e.g. [Rosati, 2008]).

Acknowledgements

This work has been partially supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), by the ANR AI Chair INTENDED (ANR-19-CHIA-0014), and by the MIUR PRIN 2017 project "HOPE" (prot. 2017MMJJRE).