=Paper=
{{Paper
|id=Vol-1936/paper-01
|storemode=property
|title=News on Temporal Conjunctive Queries
|pdfUrl=https://ceur-ws.org/Vol-1936/paper-01.pdf
|volume=Vol-1936
|authors=Veronika Thost
|dblpUrl=https://dblp.org/rec/conf/semweb/Thost17
}}
==News on Temporal Conjunctive Queries==
https://ceur-ws.org/Vol-1936/paper-01.pdf
News on Temporal Conjunctive Queries
Veronika Thost
Center for Advancing Electronics Dresden (cfaed), TU Dresden
veronika.thost@tu-dresden.de
Abstract. Temporal query languages are important for stream process-
ing, and ontologies for stream reasoning. Temporal conjunctive queries
(TCQs) have therefore been investigated recently together with descrip-
tion logic ontologies, and the knowledge we have about the combined
complexities is rather complete. However, often the size of the queries
and the ontology is negligible, and what costs is the data. We prove a
new result on the data complexity of ontology-based TCQ answering and
close the gap between co-NP and ExpTime for many description logics.
Keywords: temporal queries, description logics, data complexity
1 Introduction
The temporal nature of data is important in many applications, and the Web of-
fers more and more streaming sources and datasets. Ontologies play an important
role in this context: by linking data from heterogeneous sources to the concepts
and relations described in an ontology, the integration and automated processing
of the data can be considerably enhanced. Queries formulated in the abstract
vocabulary of the ontology can then be answered over all the linked datasets.
Medical domain ontologies written in description logics (DLs) may, for exam-
ple, capture the facts that the varicella zoster virus (VZV) is a virus, that chick-
enpox is a VZV infection, and that a negative allergy test implies that no aller-
gies are present, by concept inclusions: VZV v Virus, Chickenpox v VZVInfection,
NegAllergyTest v ¬∃AllergyTo. Here, Virus is a concept name that represents the
set of all viruses, and AllergyTo is a role name, representing a binary relation con-
necting patients to allergies; ∃AllergyTo refers to the domain of this relation. A
possible data source storing patient data (e.g., allergy test results and findings)
could look as follows:
PID Name PID AllergyTest Date PID Finding Date
1 Ann 1 neg 16.01.2011 1 Chickenpox 13.08.2007
2 Bob 2 pos 06.01.1970 2 VZV-Infection 22.01.2010
3 Chris 3 neg 01.06.2015 3 VZV-Infection 01.11.2011
The data is then connected to the ontology by mappings [10], which in our exam-
ple may link the tuple (1, Chickenpox, 16.01.2011) to the facts HasFinding(1, x)
and Chickenpox(x). Conceptually, we thus regard a sequence of fact bases, one
for each time point we have data for.
Ontology-based query answering (OBQA) over the above knowledge can
then, for example, assist in finding appropriate participants for a clinical study,
by formulating the eligibility criteria as queries over the—usually linked and
heterogeneous—patient data. The following are examples of in- and exclusion
conditions for a recently proposed clinical trial:1 (i) the patient should have
been previously infected with VZV or previously vaccinated with VZV vaccine;
(ii) the patient should not be allergic to VZV vaccine. We focus on temporal con-
junctive queries (TCQs), which were originally proposed by [2, 4]. TCQs allow to
combine conjunctive queries (CQs) via the Boolean operators and the temporal
operators of propositional linear temporal logic LTL [9]. The above criteria can
be specified with the following TCQ Φ(x), to obtain all eligible patients x:
3P ∃y.HasFinding(x, y) ∧ VZVInfection(y) ∨ 3P ∃y.VaccinatedWith(x, y) ∧
VZVVaccine(y) ∧ ¬ ∃y.AllergyTo(x, y) ∧ VZVVaccine(y)
We here use the temporal operator “some time in the past” (3P ) and consider
the symbols AllergyTo and VZVVaccine to be rigid, which means that their in-
terpretation does not change over time; that is, we assume someone having an
allergy to have this allergy for his whole life. The OBQA scenario outlined above
is similar to the classical one [5], but we use temporal queries and consider a
(finite) sequence of fact bases. The ontology is written in a classical DL (i.e., one
can take one of the many existing ontologies) and assumed to always hold.
In contrast, so-called temporal DLs extend classical DLs by temporal opera-
tors, which then occur within the ontology (see [11] for an overview). But most
of these logics yield high reasoning complexities, even if the underlying atempo-
ral DL allows for tractable reasoning. Lower complexities are only obtained by
either considerably restricting the set of temporal operators or the DL.
The combined and data complexity of TCQ entailment have been studied
for various DLs in the past [4, 3, 7, 6]. In a nutshell, we have that the combined
complexity strongly varies—between PSpace and 2-ExpTime—depending on
the DL considered and the rigid names allowed, which often increase complex-
ity.2 The data complexity for the lightweight DLs between DL-Litecore and
DL-LiteH horn is generally ALogTime, and the one for EL without rigid sym-
bols is P, and co-NP with rigid symbols. For all other DLs investigated so far,
containment in co-NP has only been shown for the case without rigid roles. This
includes expressive DLs such as SHIQ and is interesting since already standard
conjunctive query entailment is co-NP-hard in these DLs, which means that we
get the temporal features “for free”. However, rigid roles are considered as an im-
portant feature for modeling and often expressive DLs are needed; for instance,
simple disjunctions of the form > v Male t Female (“everyone is male or female”)
cannot be expressed in DL-LiteH horn or EL. Yet, the proposed algorithms for such
combinations are at least exponential in the data.
In this paper, we first close the co-NP/ExpTime gap for the DL-LiteH krom —
which allows for disjunctions as in the example—and prove that TCQ entailment
1
https://clinicaltrials.gov/ct2/show/NCT01953900
2
For some very expressive DLs, we have co-2-NExpTime-hardness/decidability.
is in co-NP in data complexity, even with rigid roles. Then, we show that this
also holds for much more expressive DLs, such as ALCHI.
2 Preliminaries
Description logics focus on individual names, which are interpreted as constants;
concepts, which are interpreted as sets; and roles, which are interpreted as bi-
nary relations. Accordingly, DL signatures are based on three kinds of symbols:
individual names NI , concept names NC , and role names NR , all of which are
non-empty, pairwise disjoint sets. We focus on the DL DL-LiteH krom [1].
DL-LiteH H
krom . Let a, b ∈ NI , A ∈ NC , and P ∈ NR . In DL-Litekrom , the sets of
roles, basic concepts, and concepts are defined as follows:
R, S ::= P | P − , B, C ::= > | A | ∃R, D ::= B | ¬B
where ·− denotes the inverse role operator.
DL-LiteHkrom axioms are the following kinds of expressions: concept inclu-
sions (CIs) are of the form B v C, B v ¬C, or ¬B v C; role inclusions (RIs)
of the form R v S; and assertions of the form B(a), ¬B(a), P (a, b), or ¬P (a, b).
A DL-LiteH krom ontology is a finite set of concept and role inclusions, and an
ABox is a finite set of assertions. Together, an ontology O and an ABox A form
a knowledge base (KB) K := O ∪ A, written K = hO, Ai.
We sometimes also refer to the ABox as fact base or simply as the data.
Without loss of generality, we assume that, if the RI R v S is contained in O,
then we also have ∃R v ∃S ∈ O and ∃R− v ∃S − ∈ O; and that O contains
the trivial axioms ∃R v ∃R for all roles R occurring in O. The set of roles is
denoted by N− R . For a given KB K := O ∪ A, we denote by NI (K) and NI (A) the
set of individual names that occur in K and A; by NC (O) and NR (O) the sets of
concept and role names occurring in K; and by N− R (O) the set of roles occurring
in K. B(O) and C(O) denote the sets of all basic concepts and, respectively,
concepts that can be built from the symbols in NC (O) and N− R (O). We may also
use the abbreviation (P − )− := P for P ∈ NR .
A DL interpretation I = (∆I , ·I ) consists of a non-empty set ∆I , the domain
of I, and an interpretation function ·I , which assigns to every A ∈ NC a set
AI ⊆ ∆I , to every P ∈ NR a binary relation P I ⊆ ∆I × ∆I , and to every a ∈ NI
an element aI ∈ ∆I such that, for all a, b ∈ NI with a 6= b, we have aI 6= bI
(unique name assumption). The function is extended to all roles and concepts:
P − = {(y, x) | (x, y) ∈ P }, >I = ∆I , ∃RI = {x ∈ ∆I | ∃y ∈ ∆I , (x, y) ∈ RI },
(¬D)I = ∆I \ DI . An interpretation I satisfies (or is a model of) an axiom α,
written I |= α, if: α = X v Y is a CI or RI, and X I ⊆ Y I ; α = (¬)B(a)
and aI ∈ B I (aI 6∈ B I ); α = (¬)P (a, b) and (aI , bI ) ∈ P I ((aI , bI ) 6∈ P I ).
I satisfies (or is a model of) a KB K, written I |= K, if it satisfies all axioms
contained in it. A KB K is consistent (or satisfiable) if it has a model, and it is
inconsistent (or unsatisfiable) otherwise. K entails an axiom α, written K |= α,
if all models of K also satisfy α. This terminology and notation is extended to
(single) axioms, ontologies, and ABoxes by regarding each as a (singleton) KB.
We denote non-entailment by K 6|= α.
In the temporal setting, we assume that some concept and role names are
designated as being rigid (vs. flexible) as outlined in Section 1. If a concept
(axiom) contains only rigid symbols, then we may call it a rigid concept (axiom).
We denote by NRC ⊆ NC the rigid concept and by NRR ⊆ NR the rigid role names.
Temporal Semantics. An infinite sequence I = (Ii )i≥0 of interpretations
Ii = (∆, ·Ii ) is a DL-LTL structure if it respects rigid names, that is: X Ii = X Ij
for all X ∈ NI ∪ NRC ∪ NRR and i, j ≥ 0. Observe that the interpretations in a
DL-LTL structure share one domain (constant domain assumption). We may use
that terminology in other settings in that we consider interpretations I1 , . . . , I`
to respect rigid names if they agree on the interpretation of all rigid symbols.
Temporal Knowledge Bases. A temporal knowledge base (TKB) is of the
form K = hO, (Ai )0≤i≤n i with an ontology O and a non-empty, finite sequence
of ABoxes. We assume all concept and role names occurring in some ABox of a
TKB to also occur in its ontology. NI (K) denotes the set of all individual names
occurring in the TKB K. Note that every KB can be regarded as a TKB with
an ABox sequence of length one.
A DL-LTL structure I = (Ii )i≥0 over a domain ∆ is a model of a TKB K =
hO, (Ai )0≤i≤n i, written I |= K, if Ii |= O for all i ≥ 0 and Ii |= Ai for all
i ∈ [0, n]. A TKB is consistent (or satisfiable) if it has a model, and it is incon-
sistent (or unsatisfiable) otherwise.
Temporal Conjunctive Queries. Let NV be the set of variables, and NT :=
NI ∪NV be the set of terms. A conjunctive query (CQ) is of the form ∃y1 , . . . , ym .ψ,
where y1 , . . . , ym ∈ NV and ψ is a (possibly empty) finite conjunction of concept
atoms of the form A(t) and role atoms of the form R(s, t), where A ∈ NC ,
R ∈ NR and s, t ∈ NT . The set of temporal conjunctive queries (TCQs) is defined
as follows, where ϕ is a CQ:
Φ, Ψ ::= ϕ | ¬Φ | Φ ∧ Ψ | #F Φ | #P Φ | Φ U Ψ | Φ S Ψ
A TCQ Φ is a CQ literal if it is of the form (¬)ϕ with ϕ being a CQ; it is positive
if Φ = ϕ, and otherwise negative.
We denote the set of individuals occurring in a TCQ Φ by NI (Φ). As in propo-
sitional LTL, we may use abbreviations true 3 and false. The empty conjunction
and disjunction are interpreted as true and false, respectively.
As usual, the semantics is defined in a model-theoretic way, based on the
notion of homomorphisms. A mapping π : NT (ϕ) → ∆I is a homomorphism of
a CQ ϕ into an interpretation I = (∆I , ·I ) if π(a) = aI for all a ∈ NI (ϕ),
π(t) ∈ AI for all concept atoms A(t) in ϕ, and (π(s), π(t)) ∈ RI for all role
atoms R(s, t) in ϕ. I satisfies (or is a model of) ϕ, written I |= ϕ, if there is
such a homomorphism. For a given DL-LTL structure I = (Ii )i≥0 , an i ≥ 0,
and TCQ Φ, the satisfaction relation I, i |= Φ is defined by induction on the
3
For instance, true may denote a fix TCQ ϕ ∨ ¬ϕ, where ϕ is an arbitrary CQ.
TCQ Φ0 Condition for I, i |= Φ0
CQ ϕ Ii |= ϕ
¬Φ W, i 6|= Φ
Φ∧Ψ I, i |= Φ and I, i |= Ψ
#F Φ I, i + 1 |= Φ
#P Φ i > 0 and I, i − 1 |= Φ
ΦU Ψ there is a k ≥ i, such that I, k |= Ψ
and, for all j, i ≤ j < k, we have I, j |= Φ
ΦS Ψ there is a k, 0 ≤ k ≤ i, such that I, k |= Ψ
and, for all j, k < j ≤ i, we have I, j |= Φ
Fig. 1. Semantics of TCQs given a DL-LTL structure I = (Ii )i≥0 .
structure of Φ as specified in Figure 1. I is a model of Φ w.r.t. a TKB K if I |= K
and I, n |= Φ. A TCQ Φ is satisfiable w.r.t. a TKB K if it has a model w.r.t.
K; and Φ is entailed by a TKB K, written K |= Φ, if every model of K is also a
model of Φ w.r.t. K. We denote the fact that I, i |= Φ and K |= Φ do not hold
by I, i 6|= Φ and K 6|= Φ. Observe that a model of a TCQ must satisfy the query
at the current time point n, which is different for propositional LTL if n > 0.
Without loss of generality, we assume that the CQs contained in a TCQ Φ
use disjoint variables and denote by QΦ the set of exactly those CQs.4 We fur-
ther assume that TCQs contain only individual names that occur in the ABoxes,
and only concept and role names that occur in the ontology, and that all CQs
contained in TCQs are connected (i.e., the corresponding Gaifman graph is con-
nected); it is easy to show that this is without loss of generality.
Solving TCQ Satisfiability. The TCQ satisfiability problem can be split into
two separate ones: one in propositional LTL and one or several “atemporal” ones
in DL [4, Lemma 4.7]. The former tests the satisfiability of the propositional
abstraction of the given TCQ Φ at n, which is obtained from Φ by replacing the
CQs ϕ1 , . . . , ϕm ∈ QΦ by propositional variables p1 , . . . , pm , respectively. The
idea is that the worlds w0 , w1 , . . . in the LTL model characterize the satisfaction
of the CQs from QΦ in the respective DL interpretations I0 , I1 , . . . such that,
to obtain Ii , we only have to check the satisfiability of the conjunction of CQ
literals induced by wi w.r.t. the atemporal KB hO, Ai i, where Ai = ∅ for i > n.
From the latter it can be seen that, assuming k to be the number of different
worlds occurring in the LTL model, it is sufficient to look for n + 1 + k corre-
sponding DL interpretations. More precisely, the problems are linked by a set
W = {W1 , . . . , Wk } ⊆ 2{p1 ,...,pm } , which collects all worlds occurring in the LTL
model, and a mapping ι : [0, n] → [1, k] that maps time points to indexes from
W and points out the first n + 1 worlds, which have to reflect the knowledge
given in the respective ABoxes. The DL part is defined as r-satisfiability; the set
W is r-satisfiable w.r.t. ι and a TKB K iff there are interpretations I0 , . . . , In ,
J1 , . . . , Jk as follows:
4
If the variables were not disjoint, we could simply rename them.
– the interpretations share the same domain and respect rigid names,
models of O,V
– the interpretations are V
– Ji is a model of χi := pj ∈Wi ϕj ∧ pj ∈Wi ¬ϕj for all i ∈ [1, k],
– Ii is a model of Ai and χι(i) for all i ∈ [0, n].
Observe that, regarding data complexity, W and ι can be guessed in constant and
linear time, respectively. [4, Lem. 4.12] show that the LTL satisfiability problem
w.r.t. a given W and ι can be decided in polynomial time. However, regarding
r-satisfiability, [4] only show membership in ExpTime. The critical point with
r-satisfiability is the requirement that the interpretations for the n + k + 1 rel-
evant time points share a common domain, so the individual satisfiability tests
have to be done together. The trivial approach is to rename the flexible names
for all i ∈ [0, n + k]. This requires however that the ontology is extended by
corresponding axioms; that is, it grows with the data and impacts complexity.
3 Characterizing r-Satisfiablility
We regard a TCQ Φ, a TKB K = hO, (Ai )0≤i≤n i in DL-LiteH krom , a set W
⊆ 2{p1 ,...,pm } such that W = {W1 , . . . , Wk }, and a mapping ι : [0, n] → [1, k], as
described in the previous section. The goal is to propose a characterization of r-
satisfiability of W w.r.t. ι and K which, in contrast to existing characterizations,
is tailored to DL-LiteH krom and shows that the r-satisfiability problem is in NP.
Observe that the functions of the shared domain in the definition of r-
satisfiability are mainly two: (i) to synchronize the interpretation of rigid sym-
bols regarding the named individuals; (ii) to guarantee that the satisfiability
of the conjunctions χi , i ∈ [1, k], which is represented by the respective in-
terpretation Ji , is not contradicted by the interpretation of the rigid names
in the other interpretations, especially in no Ii with i ∈ [0, n]. The idea is
to look for similar interpretations I0 , . . . , In , J1 , . . . , Jk , but to not require a
shared domain: based on K, W, and ι, we specify a polynomial amount of ad-
ditional data—that hence can be guessed in polynomial time—, which captures
knowledge restricting the interpretation of the individual and rigid names and
simulates the shared domain; the additional data then allows us to check the
conditions for r-satisfiability for each of the interpretations independently of the
other interpretations—nondeterministically, in polynomial time. Without loss of
generality, we can restrict our focus to certain canonical interpretations, based
on the standard chase [8]; we introduce elements of the form uaR1 ...R` , a ∈ NI ,
H
R1 , . . . , R` ∈ N−
R . Note that we also apply this general approach for DL-Litehorn
and EL in [6, 7], but we do not have to deal with nondeterminism there; that is,
there is only one canonical interpretation for a KB.
Definition 1 (Canonical Interpretation). Let K = hO, Ai be a consistent
DL-LiteH
krom knowledge base. For all A ∈ NC and P ∈ NR , define:
A0 := {a | A(a) ∈ A},
P 0 := {(a, b) | P (a, b) ∈ A} ∪
{(a, uaP ) | ∃P (a) ∈ A} ∪ {(uaP − , a) | ∃P − (a) ∈ A}.
Then, iterate over all i ≥ 0: for all X ∈ NC ∪ NR define X i+1 := X i ; apply one
of the following rules for all A ∈ NC , P ∈ NR , R, S ∈ N− R , and B, C ∈ B(O);
and increment i; (d, e) ∈ (P − )i denotes the fact that (e, d) ∈ P i , and d ∈ (∃R)i
denotes the existence of an element e such that (d, e) ∈ Ri :
– If B v A ∈ O and e ∈ B i , then add e to Ai+1 .
– If B v ∃R ∈ O and e ∈ B i :
• if e ∈ NI (A), then add (e, ueR ) to Ri+1 ;
• if e = u% , then add (e, u%R ) to Ri+1 .
– If ∃R v A ∈ O, (d, e) ∈ Ri , then add d to Ai+1 .
– If R v S ∈ O and (d, e) ∈ Ri , then add (d, e) to S i+1 .
– If ¬B v C ∈ O, e 6∈ B i , e 6∈ C i , and every other rule (i.e., for a CI without
negation) that applies to e or a tuple containing e has been applied in a step
j < i, then add e to B i+1 or C i+1 .
The set ∆Iu K collects the above introduced new elements.
A canonical interpretation IK for K is then defined as follows based on such
a sequence of rule applications, for all a ∈ NI (A), A ∈ NC , and P ∈ NR :
∞
[ ∞
[
∆IK := NI (A) ∪ ∆uIK , aIK := a, AIK := Ai , P IK := P i.
i=0 i=0
Note that the assumptions in Section 2 about the additional axioms in the
ontology ensure that, whenever there is a named individual a ∈ (∃R)i for some
i ≥ 0, then a has an R-successor of the form uaR in the corresponding canonical
interpretation, and similar for unnamed elements. We denote the restriction of a
canonical interpretation I to a named individual a and its unnamed successors
by I|a . If K is consistent, then there is a canonical interpretation for K that is a
model of K. We denote the set of all those canonical models by IK .
In what follows, we specify the additional data to overtake the Functions
(i) and (ii). Specifically, we define a set of ABoxes containing assertions that
(i) (largely) fix the interpretations on the named individuals (i.e., relations to
unnamed successors are not fully taken into account yet), and (ii) ensure both
that the positive CQ literals are satisfied as required and that the negative CQ
literals are not satisfied if they must not. For simplicity, for i ∈ [1, k], we define
An+i := ∅ and extend ι such that ι(n + i) := i. For the synchronization of the
named individuals, we use name-ABoxes, which are similar to the ABox types
defined for DL-LiteH horn in [6], but we include flexible symbols. The idea is to then
guess n + k + 1 name-ABoxes and require them to agree on the rigid assertions.
Definition 2 (Name-ABox). A name-ABox for a set of individual names I
w.r.t. O is a set A of assertions formulated over I and all symbols in B(O) and
NR (O) such that α ∈ A iff ¬α ∈ / A.
Second, for all i ∈ [0, n + k], define Qi := {ϕj | pj ∈ Wι(i) }. Let the set
Naux
I ⊆ NI contain an individual name aix for each i ∈ [0, n + k] and each variable
x occurring in a CQ in Qi . Note that, because of our assumption that the
CQs in Φ have no variables in common, each aix ∈ Naux I can be unambiguously
associated to a CQ containing x. Then, AQi denotes the ABox obtained from Qi
by instantiating all variables with the corresponding names from NauxI . We use
these ABoxes to ensure that the positive CQ literals are satisfied as required.
While the former is similarly done in [6, 7], the nondeterminism allowed
in DL-LiteH krom requires a more careful construction of the unnamed parts of
I0 , . . . , In , J1 , . . . , Jk (i.e., since they have to satisfy all CIs of the form ¬B v C
in O, we have to specify them correspondingly): we must ensure that the inter-
actions of I0 , . . . , In , J1 , . . . , Jk in those parts, which are caused by the rigid
names, do not lead to the satisfaction of some ϕj ∈ QΦ in some Ji (Ii ) although
we have that pj ∈ Wi (pj ∈ Wι(i) ). The idea for the construction of I0 , . . . , In ,
J1 , . . . , Jk is to not consider arbitrary trees of unnamed successors for all the
individuals in all the interpretations, but to define prototypical ones whose size
is constant in the data, that fix the interpretations, and which we then copy for
all named individuals that are sufficiently similar. To this end, we define types,
which are generally independent of the data; for every interpretation and indi-
vidual name, there is however exactly one type characterizing the former on the
latter. A type captures the basic concepts satisfied on a name and, in particu-
lar, relevant homomorphisms of CQs from QΦ w.r.t. the named individual and
its unnamed successors; in particular, it does not explicitly refer to individual
names. A temporal type is a set of types. The idea is to consider prototypical
trees of unnamed successors for each temporal type as additional data: we use a
set of prototypical tree-ABoxes (one per type) over the same names, which agree
on the interpretation of the rigid names, and are such that every ABox repre-
sents some interpretation on the unnamed successors that fits to the respective
type. For instance, if a type specifies a CQ ϕ ∈ QΦ to be not satisfied (w.r.t. the
unnamed successors), then ϕ is not satisfied in the ABox. Our main contribution
is that we show that such tree-ABoxes whose size is independent of the data do
exist in the case of r-satisfiability and that we can assemble the interpretations
I0 , . . . , In , J1 , . . . , Jk from these ABoxes: for every individual name a and all
i ∈ [0, n + k], we guess a type Ta,i —a polynomial amount of information—that
represents Ii (or Ji ) on a; the set of all these types for a is a temporal type
and yields the prototypical successors to choose; that is, we copy the elements
in the corresponding set of tree-ABoxes and then specify Ii (or Ji ) on these
elements according to the ABox for Ta,i . Observe that we use finite ABoxes,
which means that every of the ABoxes contains enough information to define
the interpretations on other required successors (i.e., we may copy the elements
several times). Since the ABoxes capture all the rigid information from other
time points, this allows us to test the satisfaction of the negative CQ literals for
every of the n + k + 1 interpretations individually.
Definition 3 (Type). A basic type is a set B ⊆ C(O) such that B ∈ B iff
¬B 6∈ B for all B ∈ B(O); given such a basic type, the corresponding set of
assertions is defined as AB (a) := {D(a) | D ∈ B}. The basic type of an individual
name a in an interpretation I is the set BT(a, I) := {D ∈ C(O) | a ∈ DI }.
A type is a triple (B, M, Q) with a basic type B, a set M ⊆ ϕ∈QΦ 2NT (ϕ)
S
of term sets, and a set Q ⊆ QΦ of CQs. The type of an individual name a
in a canonical interpretation I is the triple T(a, I) := (BT(a, I), M, Q) where
Q ⊆ QΦ contains exactly the CQs that are satisfied in I|a , and M contains all
sets S of terms for which there are a CQ ϕ ∈ QΦ and a partial homomorphism
π : NT (ϕ) → ∆I|a of ϕ into I|a with a ∈ range(π) and dom(π) = S.
A temporal type is a set of types.
We assume every temporal type τ to be an ordered set and use τi to refer to the
i-th type in τ . We denote the set of all temporal types by T.
It is left to specify the prototypical tree ABoxes of unnamed successors for
a given temporal type τ . We first construct ABoxes for the types and, in a
second step, ensure that the conditions specified by the types are satisfied in
them, respectively. These ABoxes (Aτi )1≤i≤|τ | , initially empty, are constructed
iteratively, based on canonical interpretations, amongst others for these ABoxes.
During the iteration, we therefore assume that these interpretations are (non-
deterministically) extended correspondingly (i.e., to cover the new elements of
the ABoxes). Let s = |τ |. For all i ∈ [1, s], consider some Iτi ∈ IhO,Aτi ∪ABi (b)i ;
b is a fresh individual name and Bi the basic type in τi . Our procedure takes
the sequence (Iτi )1≤i≤s as input. It then repeatedly iterates over the (extended)
interpretations and extends the ABoxes (Aτi )1≤i≤|τ | until nothing changes any
more.
Example 1. We consider an ontology containing the inclusions ¬A v B, ¬B v C,
A v ∃R, C v ∃S, R v R0 , where only R0 is rigid. Let further |τ | = 3 and the
input canonical interpretations for τ1 , τ2 , τ3 be as follows.
A R C S A R A R A R
ubR0 b ubR ubR0 b ubS ubR0 b ubR ubRR ubRRR
Note that all elements that are no instances of A or C instantiate B, R0 is dotted.
After one iteration over the interpretations, the ABoxes Aτi for i ∈ [1, 3] are:
abR0 abR0 abS 2 abR0 abS 2
A C S A
b b b
R R
A abR3 A
abR1 abR1 a 1
R bR R
A a 1 3 abR3 R3 A
bR R
R R
abR1 R3 R3 abR3 R3 R3
Aτ1 is obtained from Iτ1 by introducing names representing the unnamed ele-
ments, flexible roles get a superscript. All names and the rigid assertions from
Aτ1 are then added to the other ABoxes, and the interpretations Iτ2 and Iτ3
are extended correspondingly. The above Aτ2 is then obtained from this Iτ2 ,
assumed to be as below. Then, again, all names and rigid assertions from Aτ2
are added to the other ABoxes, the interpretations are extended, and the above
Aτ3 is obtained from the extended Iτ3 , depicted below, where c = abR1 .
abR0 abR0 abS 2
C S A R A R A R
ubR0
ubR0 b ubS b ubR ubRR ubRRR
R A R A
abR1 ucRR ucR abR1
Note that we do not depict all R0 -successors; according to Definition 1, all ele-
ments instantiating ∃R must have such successors. We lastly show Iτ1 and Iτ3
extended for the above Aτ3 , where d = abR3 , e = abR1 R3 , and f = abR3 R3 . Ob-
serve that we assume that Iτ3 interprets udR in the same way as ubRR , both
udRR and uf R according to ubRRR , and ueR according to ucRR .
abR0 abS 2 abR0 abS 2
A R A R A R A R
b ubR0 b
ubR0 R ubR R AubRR AubRR ubRRR
R A R A R
abR3 abR3
abR1 ucRR ucR a 1 udR udRR
R R bR R R
abR1 R3 abR3 R3 A abR1 R3 abR3 R3 A
ueR R R uf R
abR1 R3 R3 abR3 R3 R3 abR1 R3 R3 abR3 R3 R3
In order to ensure that the size of the tree-ABoxes is finite, we specify a
termination criterion based on the maximal size m := max{|ϕ| | ϕ ∈ QΦ }
of a single of the CQs: we stop the introduction of new elements a%%0 ωR with
|%|, |ω| > m if those would, thereafter, occur in a subtree (of depth > m) with
root a%%0 that would be a copy of an already existing subtree of depth m with root
a% . This approach is correct if we extend the ABoxes in a breadth-first fashion
and, especially, regard all of the canonical interpretations before extending the
trees one level deeper.
We now specify the procedure TreeABox, which takes τ , the interpretation
sequence (Iτi )1≤i≤s , and b as input:
– For each domain element ub%R of Iτi , introduce an individual name ab%R
if R ∈ NRR , and otherwise ab%Ri ; we assume that such individual names
and role names containing superscripts do not occur in K. Similarly, for
each domain element uc%R of Iτi such that c = abσ ∈ Ntree
I , introduce a new
individual name abσ%R if R ∈ NRR and otherwise abσ%Ri .
Let R := N− − −
RR ∪ {Ri | R ∈ NR \ NRR , 1 ≤ i ≤ s}. The set NI
tree
collects the
new individual names, but (*) a name aυ is only added if there are no names
a% , and aσ in Aτ such that σ = %%0 ; υ = σσ 0 with |σ 0 | > m; and, for all
ω ∈ Rm , a%ω ∈ Ntree I iff aσω ∈ Ntree
I , and a%ω and aσω have the same basic
type in any of the interpretations Iτ` , ` ∈ [1, s]. For the next step, we capture
this relation using the function ν : ∆Iu τi → Ntree
I : for the above elements ub% ,
define ν(ub%R ) := ab%R(i) and, for the others, define ν(uc%R ) := abσ%R(i) .
Observe that this function may map several elements to the same name; as it
is the case for ubRR and udR in Example 1, where we have ν(ubRR ) = abR3 R3
and ν(udR ) = abR3 R3 . In these cases, we assume that the unnamed successors
of elements from Ntree I , such as udR , are interpreted in the same way as the
original unnamed elements, such as ubRR , for which ν was defined first (i.e.,
this must have happened when a was introduced, hence udR did not yet
exist); and that the successors of the former are interpreted in the same way
as the corresponding successors of the latter, and so on.
– For every a ∈ Ntree
I introduced in the previous step, let uσR ∈ ∆Iu τi be one of
the elements for which a was created. Add the following assertions to Aτi :
• for every B ∈ B(O) such that uσR ∈ B Iτi , the assertion B(a);
• for every S ∈ N− R such that (σ, uσR ) ∈ S
Iτi
, the assertion S(σ, a);
−
• for every S ∈ NR such that (uσ , uσR ) ∈ S Iτi , the assertion S(ν(uσ ), a).
Add all of the individual names and the rigid assertions added to Aτi also
to all other Aτj , j ∈ [1, s].5
– For every a ∈ NtreeI and B ∈ B(O) such that a ∈ B Iτi , further add the
assertion B(a) to Aτi . Again, add the rigid assertions to all Aτj , j ∈ [1, s].
The procedure outputs the sequence (Aτi )1≤i≤s . Regarding the last item, note
that it covers those names that were introduced for unnamed elements in other
canonical interpretations. For them, we only have to explicitly capture the non-
determinism, w.r.t. basic concepts. All relations on the corresponding named
individuals are completely determined by the assertions added in the item be-
fore (i.e., including those added in other iteration steps, maybe for some Iτj with
j 6= i). As mentioned above, we second have to ensure that the ABox created
for a type also satisfies the conditions specified by it.
Definition 4 (Tree-ABox). An ABox A produced by TreeABox given a name
b ∈ NI as input is a tree-ABox for a type τi = (B, M, Q) if:
– hO, A ∪ AB (b)i is consistent;
– for all ϕ ∈ S
QΦ , ϕ ∈ Q iff hO, A ∪ AB (b)i |= ϕ;
– for all S ∈ ϕ∈QΦ 2NT (ϕ) , S ∈ M iff there are a CQ ϕ ∈ QΦ and a partial ho-
momorphism π : NT (ϕ) → NI (A) of ϕ into A with b ∈ range(π), S = dom(π).
Because of (*), the sizes of the tree-ABoxes are finite, and they are independent
of the data: given v := max{|NT (ϕ)| | ϕ ∈ QΦ }, the maximal number of terms
occurring in one of the CQs, and t ≤ 2|B(O)|+|QΦ |+v∗|QΦ | , the number of possible
types, the depth of how far we specify the prototypical trees is bounded by
− t
d := |B(O)|t∗|NR (O)| ∗m + m; this follows from the facts that the names in Ntree
I
5
All names can be added, for example, by assuming > to be rigid.
are built from elements of N− R (O), sometimes with subscripts from [1, t], and
that we consider these names in t different interpretations.
Finally, the additional data is a tuple as follows, polynomial in the data:
((A0i )0≤i≤n+k , (Ta,i )a∈NI (K)∪Naux
I ,
, (Aτ,i ) τ ∈T, ), where
0≤i≤n+k 0≤i≤|τ |
– A0i is an name-ABox for NI (K) ∪ Naux
I for all i ∈ [0, n + k], and all A0i contain
the same rigid assertions;
(1)
– Ta,i is a type for all a ∈ NI (K) ∪ Naux
I and i ∈ [0, n + k], and Ta,i = BT(a, A0i ).
– (Aτj )1≤j≤|τ | is the result of applying TreeABox to τ , some sequence of cor-
responding canonical interpretations, and a fresh name b for all τ ∈ T; and
aux
Aτi is a tree-ABox
S for τi for all i ∈ [1, |τ |] if there is a name a ∈ NI (K) ∪ NI
such that τ = 0≤j≤n+k {Ta,j }.
For names a, b ∈ NI and a type τi , let Aτi [b/a] be the ABox obtained from a
tree-ABox Aτi by replacing every b by a, also within individual names. For a tuple
t as above, we define the ABox Attree,i for i ∈ [0, n+k] as the set that contains, for
all a ∈ NI (K)∪Naux I , all assertions from Aτj [b/a], where τ = {Ta,i | 0 ≤ i ≤ n+k}
and τj = Ta,i . Attree denotes the ABox that contains only the rigid assertions
from Attree,i , for all i ∈ [0, n + k], and all names occurring in these ABoxes6 ; by
construction, all of the latter ABoxes agree on those.
Lemma 1. W is r-satisfiable w.r.t. ι and K iff there is a tuple
t = ((A0i )0≤i≤n+k , (Ta,i )a∈NI (K)∪Naux
I ,
, (Aτ )τ ∈T )
0≤i≤n+k
as specified above such that, for all i ∈ [0, n + k]:
(C1) KRi := hO, A0i ∪ Ai ∪ AQι(i) ∪ Attree,i i is consistent and,
(C2) for all pj ∈ Wι(i) , we have KRi 6|= ϕj .
Proof. (⇒) As outlined in Section 2, we can consider the n+k +1 interpretations
from the definition of r-satisfiability integrated within a single interpretation if we
rename the flexible symbols accordingly. The advantage of this approach is that
we can, w.l.o.g., assume that this interpretation is a canonical interpretation,
which is not possible with the single interpretations from the definition of r-
satisfiability because of the shared domain. Hence, for every i ∈ [0, n + k + 1]
and every flexible name X in NC (O) ∪ NR (O), we introduce a fresh name X (i)
called the i-th copy of X. If X is a more complex expressions (an axiom, CQ, or
conjunction of CQ literals), X (i) is obtained by replacing every occurrence of a
flexible name by its i-th copy. By [4, Lem. 4.14], W is r-satisfiable w.r.t. ι and K
iff the conjunction χW,ι of CQ literals has a model I w.r.t. hOW,ι , Ai, where:
^ (n+1+i) ^ (i) ^ (i)
^ (i)
χW,ι := χi ∧ χι(i) , χ(i) := ϕj ∧ ¬ϕj ,
1≤i≤k 0≤i≤n pj ∈Wi−n−1 pj ∈W i−n−1
[
(i) (i)
OW,ι := {α | α ∈ O, 0 ≤ i ≤ n + k}, A := {α }.
0≤i≤n,
α∈Ai
6
As above, this can be ensured, for example, by assuming > to be rigid.
For simplicity, we often focus on some i ∈ [0, n + k] and consider the i-th copies
of concept and role names as the (original) flexible names and disregard all other
copies (but not the rigid names); in the following, we refer to those parts of I, in
which the signature is smaller and renamed, as Ii . Similarly, we consider T(a, Ii )
to be the type of a in I for i ∈ [0, n + k], and may refer to the set of all these
types as the temporal type of a in I.
We then can define the components of the required tuple t for i ∈ [0, n + k]
and c ∈ NI (K) ∪ Naux
I easily: Tc,i := T(c, Ii ) and
A0i := {(¬)B(a) | a ∈ NI (K) ∪ Naux Ii Ii
I , B ∈ B(O), a ∈ B (a 6∈ B )} ∪
{(¬)R(a, b) | a, b ∈ NI (K), R ∈ NR (O), (a, b) ∈ RIi ((a, b) 6∈ RIi )}.
For all τ ∈ T, we choose an arbitrary a ∈ NI (K)∪Naux I with temporal type τ in I;
for each i ∈ [1, |τ |], define Iτi to be some Ij|a with τi = T(a, Ij ); and then define
(Aτi )1≤i≤|τ | := TreeABox(τ, (Iτi )1≤i≤|τ | , a); if there is no such element a, the
ABoxes are empty. We can assume the latter algorithm to iterate only once over
the types because the interpretations of the new names in all the interpretations
are given already, by the interpretations of the elements for which they were
introduced, respectively (i.e., we do not have to extend interpretations).
It is easy to see that the tuple is as required—that is, Ii represents the model
of KRi —if (∗) we assume I to be such that (1) the trees of unnamed successors
for two names a, b ∈ NI (K) ∪ Naux I that have the same temporal type in I are
isomorphic w.r.t. the rigid symbols and that (2) it interprets those successors
the same in Ii and Ij if T(a, Ii ) = T(a, Ij ). This is the case because Attree,i
then is trivially satisfied for all i ∈ [0, n + k]: the interpretations that can be
selected for the construction of a prototypical ABox Aτ then all are isomorphic;
that is, the construction neither depends on the name chosen as prototype for
the temporal type nor on the indexes i whose interpretation Ii is chosen as
prototype for a type. We lastly show that (∗) is a valid assumption. The proof
is by contradiction. We hence assume that such a given model I cannot be
simplified in the described way without loosing the property that it satisfies
both the KB and the conjunction of CQ literals. Let J be a corresponding
adaptation of such a model I, constructed as follows:
– For every temporal type τ for which there is an individual name a such that
τ is the temporal type of a in I, and for every j ∈ [1, |τ |], select one index
ij ∈ [0, n + k] such that τj = T(a, Iij ), and let Aτ,j be the (possibly infinite)
set of assertions representing Iij on all unnamed successors of a. That is, Aτ,j
covers all the successors contained in I, but it only describes I w.r.t. the rigid
names and the ij -th copies of flexible names.
– Adapt I as follows. For every a ∈ NI (K) ∪ Naux I with temporal type τ in I,
replace all unnamed successors by copies of the elements occurring in Aτ,j (for
an arbitrary j ∈ [1, |τ |]). For every i ∈ [0, n + k], the interpretation of the i-th
copies of names on these elements in J is then given by the corresponding flexible
assertions in the one set Aτ,j for which we have τj = T(a, Ii ). The interpretation
of the rigid names is also given by these ABoxes since they all agree on those
names. As with I, we use interpretations Ji to refer to J on the rigid names and
on the i-th copies; that is, we consider the i-th copies as the (original) flexible
names and disregard all other copies.
– The construction of J maintains the types, meaning that T(a, Ji ) = T(a, Ii )
0 0 0
for all a ∈ NI (K) ∪ Naux
I , i ∈ [0, n + k]. Let (B, M, Q) := T(a, Ii ), (B , M , Q ) :=
T(a, Ji ). Note that, to replace the unnamed successors of a in I, we chose un-
named successors of some b ∈ NI (K) ∪ Naux I of the same temporal type as a in I;
and that the interpretation in Ji on a and its unnamed successors is given by
the one on b and its unnamed successors in some Ij with T(b, Ij ) = T(a, Ii ).
Clearly, for every homomorphism of some ϕ ∈ Q0 into Ji|a , there is a corre-
sponding one into Ij|b if a does not occur in ϕ, by the definition of Ji . This
especially holds because the interpretation of the rigid symbols on a and its
unnamed successors in the whole interpretation J is fully determined by the
interpretation of the rigid symbols in Ij|b . If a occurs in ϕ, then the definition
of T(a, Ii ) yields {a} ∈ M, and T(b, Ij ) = T(a, Ii ) hence implies a = b by the
definition of T(b, Ij ). The construction of Ji|a then, as before, yields Q0 ⊆ Q.
For the other direction, we consider a homomorphism of some ϕ ∈ Q into Ii .
But then we also have one of ϕ into Ij which, in turn, yields a corresponding
one into Ji . M = M0 follows by analogous arguments. We show B = B 0 . Since
we do not adapt the interpretation of the concept and role names w.r.t. only
named individuals, it is left to focus on basic concepts of the form ∃R. The only
critical case is thus the one where there is an element uaR in I but not in J
and a has no named R-successor (in both I and J ) either; that is, there is no
element ubR in I, but b has a named R-successor (again in both I and J ) by
BT(a, Ii ) = BT(b, Ij ). However, note that we assume the ontology to contain
all CIs of the form ∃R v ∃R. Hence, the element ubR must exist in I by Defi-
nition 1. By construction, we thus get that uaR exists in J , which contradicts
the assumption. The case where an element uaR exists in J but not in I is not
critical w.r.t. possible changes of the basic type.
Since we do not adapt the interpretation of the concept and role names w.r.t.
only named elements, J |= A. Regarding the named elements, J also satisfies
OW,ι since the adaptation retains the basic types. Regarding an unnamed ele-
ment e, observe that it is valid to argument based on the single interpretations
Ji , i ∈ [0, n + k], instead of on J as a whole because the ontology contains no
axioms where different kinds of copies occur in and Ji represents the interpreta-
tion of rigid names in J . The interpretation of e in such a Ji corresponds to the
interpretation of an isomorphic element in some Ij , j ∈ [0, n + k]. But we have
I |= OW,ι , and OW,ι contains all copies (i.e., also the j-th) of all axioms in O.
So Ji satisfies all axioms in O, which yields J |= OW,ι . J also satisfies all CQ
literals ϕ(i) satisfied in I. This is clear if only named individuals are considered
because I and J agree on the interpretation of concept and role names w.r.t.
only named individuals and the basic types are maintained. For the other cases,
observe that we can argument based on single interpretations Ii /Ji , again, since
the copies of the CQs only contain one kind of copies of names, and all these
interpretations for I/J agree on the rigid symbols. We consider the case where
there is a homomorphism that maps to maximally one named individual. All
the unnamed elements in the range must form a tree structure with a named
individual a ∈ NI (K) ∪ Naux I as root. Assuming T(a, Ii ) = (B, M, Q), we must
have ϕ ∈ Q by Definition 3. From T(a, Ii ) = T(a, Ji ), we get that ϕ(i) also in J
is satisfied based on a and its unnamed successors. If there is a homomorphism
π mapping to both several named and unnamed elements, then a corresponding
homomorphism π 0 into J can be obtained based on the type. By Definition 3,
for all a ∈ (NI (K) ∪ Naux I ) ∩ range(π), there is a set of terms Va in T(a, Ii )
(2)
containing exactly the terms t ∈ NT (ϕ) with π(t) = a or π(t) being an unnamed
successor of a. From T(a, Ji ) = T(a, Ii ), we get Va ∈ T(a, Ji )(2) , which means
that there must be a corresponding partial homomorphism πa of ϕ into Ji ,
again by Definition 3. Now, we define π 0 : (i) π 0 (t) := π(t) if π(t) ∈ NI (K ∪ Naux I ).
(ii) π 0 (t) := πa (t) for all a ∈ (NI (K) ∪ Naux
I ) ∩ range(π) and t ∈ V a . Regarding the
(i)
negative CQ literals, we proceed by contradiction and assume that J |= ϕj for
some pj ∈ Wι(i) . Again, we can consider single interpretations Ii /Ji . Since we
do not adapt the interpretation of the names on only named elements the corre-
sponding homomorphism π must map to unnamed elements. It can neither map
to only unnamed elements and maximally to one named element: the arguments
correspond to those given above for the corresponding case for the positive CQ
literals if Ii and Ji and I and J are switched, respectively. The same holds for
the case where π maps to several named and to unnamed elements.
(⇐) We regard a tuple t that satisfies the conditions from Lemma 1 and
construct interpretations I0 , . . . , In , J1 , . . . , Jk as required based on the KBs in
Condition (C1), which contain all the necessary information (i.e., KRi yields Ii for
i ∈ [0, n] and Ji for i ∈ [n + 1, n + k]): we have the name-ABoxes for the named
individuals in the TKB, and Attree,i for all i ∈ [0, n+k] for those successors (up to
some “depth” d0 ≤ d) of the latter individuals that must exist given O. The shared
domain of our interpretations contains all of the names occurring in these KBs
and additional unnamed elements, to include the required successors of depths
greater than d0 . The idea is to inductively introduce elements by continuing the
repetition we have given the construction of the tree-ABoxes.
The ontology and the ABoxes Ai for i ∈ [0, n + k] are clearly satisfied by the
respective interpretations, since the KBs KRi are consistent and our interpreta-
tions are completely defined based on canonical ones (i.e., the ones used to con-
struct the ABoxes Attree,i ; these ABoxes describe the interpretations completely
in the sense that they capture all the necessary rigid knowledge and nondeter-
ministic decisions). The additional ABoxes AQι(i) ensure that the positive CQ
literals are satisfied as required. By contradiction, it can easily be shown that no
negative CQ literal is satisfied. By (C2), a corresponding homomorphism π must
map to unnamed elements and, since we untangle the interpretations during the
construction of Attree,i to depth ≥ 2m, it cannot map to elements in NI (K) ∪ Naux I .
This yields a contradiction to (C2) because there are isomorphic named elements
for all those π maps to, since the repeating trees are of depth m. t
u
Regarding complexity: W and ι can be guessed in polynomial time, and the
LTL satisfiability testing w.r.t. a given W and ι can be done in polynomial time
[4, Lem. 4.12]. Similarly, the tuple from Lemma 1 can be guessed in polynomial
time; note that the tests if the ABoxes for the temporal types are tree-ABoxes are
data independent. Since both KB consistency and CQ non-entailment are in NP
in DL-LiteHkrom [1, Thm. 8.2], (C1) and (C2) can be decided nondeterministically
in polynomial time. TCQ satisfiability is thus in NP [4, Lem. 4.7].
Theorem 1. TCQ entailment regarding a TKB in DL-LiteH
krom is in co-NP.
The expressivity of TCQs allows to reduce TCQ entailment in much more
expressive DLs to TCQ entailment in DL-LiteH krom [6], without an impact on
the data. For example, CIs7 as ∃R.A1 v A2 and A1 v A2 t A3 can be encoded
using TCQs ¬∃xy.R(x, y) ∧ A1 (y) ∧ A2 (x) and ¬∃x.A1 (x) ∧ A2 (x) ∧ A3 (x) if the
ontology is extended by the CIs ¬A2 v A2 and ¬A3 v A3 . This yields:
Corollary 1. TCQ entailment regarding a TKB in ALCHI is in co-NP.
4 Conclusions
We have shown that the data complexity of TCQ entailment w.r.t. temporal
knowledge bases in expressive DLs is in co-NP, even if rigid symbols are con-
sidered. This result is interesting since already standard conjunctive query entail-
ment is co-NP-hard, which means we get the temporal features “for free”. Yet, it
remains to design deterministic algorithms to translate the result into practice.
References
1. Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family
and relations. Journal of Artificial Intelligence Research 36, 1–69 (2009)
2. Baader, F., Borgwardt, S., Lippmann, M.: Temporalizing ontology-based data ac-
cess. In: Proc. of CADE. pp. 330–344 (2013)
3. Baader, F., Borgwardt, S., Lippmann, M.: Temporal conjunctive queries in expres-
sive description logics with transitive roles. In: Proc. of AI. pp. 21–33 (2015)
4. Baader, F., Borgwardt, S., Lippmann, M.: Temporal query entailment in the de-
scription logic SHQ. Journal of Web Semantics 33, 71–93 (2015)
5. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applica-
tions. Cambridge University Press, 2 edn. (2007)
6. Borgwardt, S., Thost, V.: Temporal query answering in DL-Lite with negation. In:
Proc. of GCAI. pp. 51–65 (2015)
7. Borgwardt, S., Thost, V.: Temporal query answering in the description logic EL.
In: Proc. of IJCAI. pp. 2819–2825 (2015)
8. Deutsch, A., Nash, A., Remmel, J.B.: The chase revisited. In: Proc. of PODS. pp.
149–158 (2008)
9. Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS. pp. 46–57 (1977)
10. Poggi, A., Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.:
Linking data to ontologies. Journal on Data Semantics 10, 133–173 (2008)
11. Thost, V.: Using Ontology-Based Data Access to Enable Context Recognition in
the Presence of Incomplete Information. Ph.D. thesis, TU Dresden (2017)
7
The syntax and semantics of many DLs extending DL-LiteH
krom are described in [5].