Answering Conjunctive Queries over a Temporally-Ordered Finite Sequence of ABoxes Sharing one TBox Natalya G. Keberle ? Zaporozhye National University, Dept. of Information Technologies 66, Zhukovskogo str. 69063, Zaporozhye, Ukraine nkeberle@gmail.com Abstract. Ontology-based data access (OBDA) assumes that data in a database are mediated with a conceptual layer, available for clients and hiding data storage details. Ontologies are good candidates for such a conceptual layer presentation, whereas databases are good for huge data storage. One of the interesting appli- cations of OBDA is checking a finite set of constraints defined in some language against a temporally-ordered sequence of ABoxes sharing one TBox, where each constraint is considered as a conjunctive query. Presented is one algorithm of con- junctive query answering for such a language, proved are its termination, sound- ness and completeness. Keywords. Ontology-based data access, temporal conjunctive query language, description logic knowledge base Key terms. KnowledgeEvolution, KnowledgeManagementProcess, DecisionSup- port 1 Introduction Ontology-based data access (OBDA) [1] assumes that data in a database are mediated with a conceptual layer, available for clients and hiding data storage details. Ontologies are good candidates for such a conceptual layer presentation, whereas databases are good for huge data storage. The benefits from combination of databases and knowledge bases are as follows: – database management is the mature field of research, there is a lot of commercially and freely avaliable DBMSs, showing good-to-excellent performance on large datasets. It is an obvious place to store the assertional part of some knowledge base, i.e. an ABox; – a TBox often requires a reasoning support to deduce additional assertions, axioms and to check the consistency of a knowledge base. ? The work done during the research visit to Dresden University of Technology, sponsored by The Ministry of Education and Science, Youth and Sport of Ukraine 80 N. G. Keberle At the same time, employing such an approach is rather challenging due to signifi- cant differences between relational database systems and ontology languages, based on Description Logics, such as OWL. At first, relational databases adopt a closed-world semantics, i.e. all facts that are not explicitly stated to be true are assumed to be false. In contrast, OWL is based on an open world semantics which does not requre one to fix the truth value of every fact and is more similar to an incomplete database. Second, relational databases are unaware of the intensional part of a knowledge base (called a TBox). Research has been done so far in the OBDA field considers only one ABox stored in a data source, that is an actual set of assertions on individuals and their pairs. However, real applications show that ABox is changing over time. The examples of such dynamic systems can be easily found in practice: environmental conditions, air traffic load, com- puter system load and performance, health control for the people suffering from serious diseases. Therefore, in some applications of situation awareness [2], there is a need to store an archive of ABoxes, keeping ABoxes actual at different time points. Temporal logics are often used as the means to formulate constraints a dynamic system should obey during its work. The main results of the paper are: – for the point-based linear finite time structure elaborated is the language of unions of temporal conjunctive queries, which allows to evaluate atemporal unions of con- junctive queries at different time points; – proposed is an algorithm of answering a union of temporal conjunctive queries, which harnesses set-theoretic operations on atomic queries answer sets. Proved are its termination, soundness and completeness; The paper is organized as follows: in the next section a language of unions of temporal conjunctive queries is introduced and the definitions of main reasoning tasks available for such a query language are presented. In the section 3 the algorithm of answering temporal unions of conjunctive queries is presented and illustrated in examples. The section 4 is dedicated to the proofs of logical properties of the algorithm. The section 5 discusses the related work in the field of conjunctive queries answering. 2 Conjunctive Queries: Syntax, Semantics Assume there is a knowledge base K = (A, T ), where T is a set of concept axioms (a TBox), A is a set of assertional axioms (an ABox). Fix a language of a knowledge base to ALC [3]. An interpretation of K, named I, is a pair (·I , ∆), where ∆ is a domain of individuals, obeying unique name assumption (UNA) and ·I is an interpretation func- tion, which assigns every concept C a set C I ⊆ ∆, every atomic role R a binary relation RI ⊆ ∆ × ∆, and every individual name a an individual aI ∈ ∆. Assertional axioms are C(a) - concept assertion and R(a, b) - role assertion. Query answering is the extension of a well known task of instance checking: given a knowledge base K and an assertion α. Check whether this assertion is entailed by an ABox of K. Answering Conjunctive Queries over a Temporally-Ordered ... 81 2.1 Conjunctive Queries Basics Let Vars(Q) be a set of all distinguished and non-distinguished variables which appear in a query Q, let Inds(Q) to denote the set of all individual names which appear in query Q and Terms(Q) to denote the set of all terms in Q, i.e. Vars(Q) ∪ Inds(Q). Let us formally define conjunctive queries and Boolean conjunctive queries for a well- elaborated language ALC [3]. Definition 1 (Conjunctive query, Union of conjunctive queries). Let x, y, c are re- spectively tuples of distinguished variables (answer variables), of non-distinguished variables and of individual names, and t, t1 , t2 are terms in Terms(Q). A conjunctive query (CQ) is an expression of the form conj(x, c) = ∃y.q1 ∧ . . . ∧ qm , where qi ::= C(t) | r(t1 , t2 ) A Boolean conjunctive query is a CQ without answer variables. A union of conjunctive queries (UCQ) is a disjunction of conjunctive queries (CQs) of the form Q(x) = {x | conj1 (x, c) ∨ . . . ∨ conjn (x, c)} Example 1. The example of a query asking about all students that attend some courses and take some exams could be as follows: Q(x) = {x | ∃y.takeCourse(x, y) ∧ takeExam(x, y)} This query can be modified to a Boolean query by substitution of x with an individ- ual name: Q(x) = {| y.takeCourse(”Eldora”, y) ∧ takeExam(”Eldora”, y)} We use |Q| to denote the size of Q - the number of symbols required to build the query. The arity of a query will be the number of answer variables in the query. If all terms in Q are individual names, we say Q is ground. We write Q(c) for a query whose answer variables x are substituted by c, Q(x) for a conjunctive query and simply Q for a Boolean conjunctive query. Sometimes we write x1 , . . . , xn instead of x, and similarly for y and c. Given an ALC-knowledge base K = hT , Ai, an interpretation I satisfies a query Q(x) iff the interpretation function can be extended to the variables in Q(x) in such a way that I satisfies every term in Q(x). A query Q(x) is true w.r.t. K (written K |= Q) iff every interpretation that satisfies K also satisfies Q. Definition 2 (Query answering, query entailment). Given a query Q(x) with a tuple of answer variables x, and a knowledge base K, a tuple of individuals c with the same arity of x is an answer for Q in K if I |= Q(c) for every model I in K. Given a Boolean conjunctive query Q, and a KB K, query entailment is a task to decide whether K |= Q if I |= Q for every model I of K. Given a conjunctive query Q(x), a tuple of individuals a, and a KB K, query an- swering is a task to decide whether a is an answer for Q(x) in K. 82 N. G. Keberle 3 Temporal Conjunctive Queries Let K = hT , (Ai )0≤i≤n i be a knowledge base with a sequence of ABoxes sharing one TBox. Let’s describe a query language extending the language of conjunctions of positive existential formulae built from query atoms. Having in mind linear temporal logic LT L (see e.g. [4]), this language allows for the following temporal operators: # (next), #− (previous), U (until), S (since). Definition 3. Temporal conjunctive query (TCQ) Ψ is an expression tconj(x, c) = ∃y.q1 ∧ . . . ∧ qm , where qi ::= ϕ | Ψ ϕ ::= C(t) | r(t1 , t2 ) Ψ ::= ϕ | Ψ1 ∧ Ψ2 | #− Ψ | #Ψ | Ψ1 S Ψ2 | Ψ1 U Ψ2 and C is a concept description, r is a role name, t, t1 , t2 are terms in Terms(Q). Derived temporal modalities like 3− (sometimes in the past), 2− (always in the past), 3, 2 can be defined in a usual way (see, e.g. [4]). Example 2. A query asking about students who had defended their thesis some time ago and had been ex-matriculated since then is expressed as follows: Q(x) = {x | ∃y.3− Student(x) ∧ exM atriculated(x) S hasDef ended(x, y)} The semantics of the TCQ is defined as follows. Definition 4. A total function π : Terms(Ψ ) → ∆ is a binding for a query Ψ in an interpretation I, if π(a) = a for all individuals a ∈ dom(π), and the validity I, π |= Φ for atemporal CQ ϕ is defined inductively: I, π |= C(t) iff I |= C(π(t)) I, π |= r(t1 , t2 ) iff I |= r(π(t1 ), π(t2 )) I, π |= ϕ1 ∧ ϕ2 iff I, π |= ϕ1 and I, π |= ϕ2 I, π |= ∃yϕ iff ∃e ∈ ∆ : π 0 = π[y/e] and I, π 0 |= ϕ where the notation π[y/e] represents a binding π extended with π(y) = e if y is not in the domain of π, otherwise the original value for y is replaced by e. The validity for a TCQ Ψ and a KB K = hT , (Ai )0≤i≤n i is extended as follows: K, i, π |= ϕ iff ∀I |=T Ai .I, π |= ϕ K, i, π |= Ψ1 ∧ Ψ2 iff K, i, π |= Ψ1 and K, i, π |= Ψ2 K, i, π |= #Ψ iff i < n and K, i + 1, π |= Ψ K, i, π |= #− Ψ iff i > 0 and K, i − 1, π |= Ψ K, i, π |= Ψ1 U Ψ2 iff ∃k, i ≤ k ≤ n : K, k, π |= Ψ2 and ∀j, i ≤ j < k : K, j, π |= Ψ1 K, i, π |= Ψ1 S Ψ2 iff ∃k, 0 ≤ k ≤ i : K, k, π |= Ψ2 and ∀j, k < j ≤ i : K, j, π |= Ψ1 Answering Conjunctive Queries over a Temporally-Ordered ... 83 For a binding π, if, for every i, ∀I |=T Ai .I |= K, this implies I |= Ψ . If such evaluation exists, we write K |= Ψ and we say π is a match for Ψ in K. For a tuple of individuals c1 , . . . , cn mapped to a tuple of answer variables x1 , . . . , xn we say c1 , . . . , cn is a certain answer for Ψ in K, iff K |= Ψ [x1 , . . . , xn /c1 , . . . , cn ]. We denote a set of certain answers for Ψ as Ans(Ψ ). Definition 5. A union of temporal conjunctive queries (UTCQ) Q(x) is a disjunction of temporal conjunctive queries (see Definition 3): Q(x) = {x | tconj1 (x, c) ∨ . . . ∨ tconjn (x, c)} 4 Answering a Union of Temporal CQs Over a Sequence of ABoxes 4.1 Algorithm Answering a Union of Temporal CQs The idea of answering a UTCQ against a set of ABoxes is to use temporal operators as the means of detection of time points at which atemporal CQs should be evaluated. Due to the recursive nature of such temporal operators as S , U we have to store all the ABoxes and the values of particular CQs depending on the operator. Intuitively, given Ψ = #φ at a time point i, φ is evaluated at the time i + 1, and so on. To be able to combine certain answers obtained from different CQs of one TCQ, let’s take a closer look at the nature of certain answers. A certain answer to a CQ φ is a binding π of each xi ∈ x (distinguished variables) to some individual name that appeared in the KB K, such that in all models of K, K |= φ(π(x)). There could be more than one certain answer for a CQ φ, so further we shall consider a set of certain answers for a query φ(x). A correspondent set of matches for φ actually produces some k-ary relation, where k is the arity of a CQ φ. A certain answer to a UCQ Φ is a combination of answers of CQs in Φ, i.e. c1 ∪. . .∪ cn where n is a number of CQs in Φ. For such a combination there are two possible situations: (i) disjuncts φj1 , φj2 in UCQ Φ use pairwise disjoint sets of distinguished variables (i.e. there are no common distinguished variables in two arbitrary disjuncts of Φ); (ii) some disjuncts can share (some) distinguished variables of each other. To deal with sets of certain answers (that are actually relations) we adopt two operators of relational algebra, namely, × - a cross-product, and ./ - a natural join. Cross-product operator × [5] is used for the case (i). Definition 6. Given two bindings π1 : (x1 , . . . , xn ) → ∆, π2 : (y1 , . . . , ym ) → ∆, their cross-product, π1 × π2 is a binding π : X → ∆ where x, y are free variables that do not have any variables in common, and X = (x1 , . . . , xn , y1 , . . . , ym ). Join operator ./ [5] is used for the case (ii) to join two bindings w.r.t. common variables in both bindings are mapped to same constant. Definition 7. Given two bindings π1 : (x1 , . . . , xn , z) → ∆, π2 : (y1 , . . . , ym , z) → ∆, their join, π1 ./ π2 is a binding π : X → ∆ where x, y, z are free variables and X = (x1 , . . . , xn , y1 , . . . , ym , z), iff every common variable z must be mapped to same constant c ∈ ∆. 84 N. G. Keberle A correspondent binding for Φ will be: for (i) π = πφ1 × . . . × πφn , and for (ii) π = πφ1 ./ . . . ./ πφn The following theorems show applications of × and ./ for bindings. Theorem 1. Given a formula Φ = φ1 ∧ φ2 , where φ1 , φ2 are CQ formulas, a binding π = π1 ./ π2 is a match for Φ iff bindings π1 , π2 are matches for φ1 , φ2 . Proof. It is true based on the definition of the join operator. Theorem 2. Given a formula Φ = φ1 ∨ φ2 , where φ1 , φ2 are CQ formulas, a binding π = π1 × π2 is a match for Φ iff the binding π1 is a match for φ1 or the binding π2 is a match for φ2 . Proof. The ⇒ direction is trivial. For ⇐ direction, assume π1 : (x1 , . . . , xn , z) 7→ ∆, π2 : (y1 , . . . , ym , z) 7→ ∆, and they are matches for φ1 and φ2 . From the nature of disjuntion, we know that formula Φ is satisfiable if either φ1 or φ2 is satisfiable. That means if there is a match for either φ1 or φ2 . If z appears in both of the CQs, renaming z in one of the CQs does not change the validity. Therefore, we have that π : (x1 , . . . , xn , z, y1 , . . . , ym , z 0 ) 7→ ∆ which is obtained from π1 × π2 is indeed a match for Φ. Now, consider a structure of a certain answer to a union of temporal CQs (UTCQ). It is a combination of answers to a (set of) TCQ obtained at proper time points, referred by temporal operators used in a UTCQ. One more thing to be explicitly addressed is that known algorithms for conjunctive query answering, such as [6], [7], are focused on query entailment, that is, a Boolean conjunctuve query answering. This means that the task of answering an atemporal CQ requires a preprocessing step, and considers a Boolean conjunctive query answering algorithm as a black box. Namely, at the preprocessing step a candidate match (a tuple of variables, substituted via some binding π with a tuple of individuals c) is submitted to a Boolean conjunctive query answering engine, and that engine decides if such a candidate match is a certain answer. Now, present the algorithm informally. Eliminate temporal operators in a UTCQ The important step in our algorithm is to get a normal form where the temporal operators are used to decide at which time point should each CQ be evaluated. This is done by iterative applecation of the expansion rules Table 1. For every # and #− operators, we just shift one point forward and backward. By doing these, we obtain a query that is in normal form whose atoms are UCQs, except some recursion atom which is a TCQ. Replace the boolean operators with relational operators Every conjunction is replaced with join and every disjunction - with cross-product. Retrieve an answer Use an arbitrary query answering algorithm [6–9] as a black-box approach to compute a set of answers for a given UCQ. If the original UTCQ con- tains U , S , 2, 2− , 3, 3− , the normal form of the transformed query might contain a recursion. In such case, if the time point i < 0 or i > n, then return ∅, else evaluate CQs with leading # or #− for U , S and for derived modalities (if any). Answering Conjunctive Queries over a Temporally-Ordered ... 85 Algorithm 1 Decide Q Input: K = {T , (Ai )0≤i≤n } : knowledge base consists of a TBox and a sequence of ABoxes at a time point i, 0 ≤ i ≤ n Q : a UTCQ Output: Ans(Q, i) - a set of certain answers to Q at time point i Ans(Q, i) = ∅ repeat Ans0 = Ans(Q, i) if Q = T CQ1 ∨ T CQ2 then Ans(Q, i) = Ans(T CQ1 , i) × Ans(T CQ2 , i) end if if Q = T CQ1 ∧ T CQ2 then Ans(Q, i) = Ans(T CQ1 , i) ./ Ans(T CQ2 , i) end if if Q = #− T CQ then if i=1 then Ans(Q, i) = ∅ else Ans(Q, i) = Ans(T CQ, i − 1) end if end if if Q = #T CQ then if i=n then Ans(Q, i) = ∅ else Ans(Q, i) = Ans(T CQ, i + 1) end if end if if Q = T CQ1 U T CQ2 then if i=n then Ans(Q, i) = Ans(T CQ2 , i) else Ans(Q, i) = Ans(T CQ2 , i) × (Ans(T CQ1 , i) ./ Ans(Q, i + 1)) end if end if if Q = T CQ1 S T CQ2 then if i=1 then Ans(Q, i) = Ans(T CQ2 , i) else Ans(Q, i) = Ans(T CQ2 , i) × (Ans(T CQ1 , i) ./ Ans(Q, i − 1)) end if end if until Ans0 = Ans(Q, i) return Ans(Q, i) 86 N. G. Keberle Table 1. Equivalence rules of LTL for future operators. Taken from [4] idempotent rule 2Ψ ≡ 22Ψ 3Ψ ≡ 33Ψ Ψ1 U (Ψ1 U Ψ2 ) ≡ Ψ1 U Ψ2 (Ψ1 U Ψ2 ) U Ψ2 ≡ Ψ1 U Ψ2 commutativity rule 2 # Ψ ≡ #2Ψ 3 # Ψ ≡ #3Ψ #(Ψ1 U Ψ2 ) ≡ (#Ψ1 U # Ψ2 ) distributivity rule 2(Ψ1 ∧ Ψ2 ) ≡ (2Ψ1 ∧ 2Ψ2 ) 3(Ψ1 ∨ Ψ2 ) ≡ (3Ψ1 ∨ 3Ψ2 ) #(Ψ1 ∧ Ψ2 ) ≡ (#Ψ1 ∧ #Ψ2 ) #(Ψ1 ∨ Ψ2 ) ≡ (#Ψ1 ∨ #Ψ2 ) ((Ψ1 ∧ Ψ2 ) U Ψ3 ) ≡ ((Ψ1 U Ψ3 ) ∧ (Ψ2 U Ψ3 )) (Ψ1 U (Ψ2 ∨ Ψ3 )) ≡ ((Ψ1 U Ψ2 ) ∨ (Ψ1 U Ψ3 )) temporal recursion rule 2Ψ ≡ Ψ ∧ #2Ψ 3Ψ ≡ Ψ ∨ #3Ψ Ψ1 U Ψ2 ≡ Ψ2 ∨ (Ψ1 ∧ #(Ψ1 U Ψ2 )) absorption rule 323Ψ ≡ 23Ψ 232Ψ ≡ 32Ψ In Table 1, presented are some equivalence rules in LTL, used in Algorithm 1. For the illustration of Algorithm 1 consider some examples, assuming that Algo- rithm 1 returns a set Ans of answers to Ψ at the time point i. Example 3. Given a TCQ query Ψ = #− (Φ1 U Φ2 ) at a point i. Ans(Ψ, i) = Ans #− (Φ1 U Φ2 ), i  ∗\move back one pointby #− = Ans Φ1 U Φ2 , i − 1 ∗\expansion rule for U  = Ans Φ2 ∨ (Φ1 ∧ #Ψ ), i − 1 ∗\transforming ∨  = Ans Φ2 , i − 1 × Ans Φ1 ∧ #Ψ, i − 1 ∗\transforming ∧     = Ans Φ2 , i − 1 × Ans Φ1 , i − 1 ./ Ans # Ψ, i − 1 ∗\move forward one point by #     = Ans Φ2 , i − 1 × Ans Φ1 , i − 1 ./ Ans Ψ, i   If i = 0 in Ans Φ2 , i − 1 and Ans Φ1 , i − 1 , then the evaluation of Ψ is the empty set. A more complex example is given below. Answering Conjunctive Queries over a Temporally-Ordered ... 87 Example 4. Given a TCQ query Ψ = 3− (Φ1 U Φ2 ) at a point i. Ans(Ψ, i) = Ans 3− (Φ1 U Φ2 ), i  ∗\expansion rule for 3− = Ans (Φ1 U Φ2 ) ∨ #− Ψ, i  ∗\transforming ∨  = Ans Φ1 U Φ2 , i × Ans #− Ψ, i  ∗\move back one point  by #−  = Ans Φ1 U Φ2 , i × Ans Ψ, i − 1 ∗\We substitute Φ1 U Φ2 with Ψ 0 Expansion rule for U   = Ans Φ2 ∨ (Φ1 ∧ #Ψ 0 , i × Ans Ψ, i − 1  ∗\transforming  ∨ = Ans Φ2 , i × Ans Φ1 ∧ #Ψ 0 , i × Ans Ψ, i − 1    ∗\transforming  ∧ =  Ans Φ 2 , i ×  Ans Φ1 , i ./ Ans # Ψ 0 , i × Ans Ψ, i − 1   ∗\move forward one point by #    = Ans Φ2 , i × Ans Φ1 , i ./ Ans Ψ 0 , i + 1 × Ans Ψ, i − 1   If i = n in Ans Ψ 0 , i + 1 , then Ans Ψ 0 , i + 1 is evaluated to the empty set.   There is one thing we have to ensure that in the intersection of two sets of answers for conjunction of CQs a certain answer is obtained, i.e. there is a common answer for both CQs, otherwise an empty set. One way to do this is to retrieve all answers for each CQ and then to intersect them to get some common answers. Another way is first to retrieve an answer of a UCQ and then to decide if this answer is also the answer for the other CQs in the conjunction, otherwise keep retrieving and deciding until there is no more answer obtained. The former way is preferred since it offers more practical solution. It means that we can deal with it using relational algebra operators or database language operators. 4.2 Termination, Soundness, Completeness of the Algorithm Definition 8. (UTCQ closure). Given a temporal union of conjunctive queries Q, its closure set, Cl(Q) is a set of query atoms closed under the following rules if q ∈ Q then q ∈ Cl(Q) if #− q ∈ Q then q ∈ Cl(Q) if #q ∈ Q then q ∈ Cl(Q) if q1 ∧ q2 then q1 , q2 ∈ Cl(Q) if q1 ∨ q2 then q1 , q2 ∈ Cl(Q) if q1 U q2 then q1 , q2 , #(q1 U q2 ) ∈ Cl(Q) if q1 S q2 then q1 , q2 , #− (q1 S q2 ) ∈ Cl(Q) Since a closure set for a UTCQ is finite, Algorithm 1 terminates after a finite number of steps. 88 N. G. Keberle Theorem 3. (Local) termination. Given a UTCQ Q and a knowledge base K = {T , (Ai )0≤i≤n }. Algorithm 1 always terminates. Proof. We can show the local termination inductively. Base case. Any query is also cointained in the closure set of itself. Inductive case. (C(a), r(a1 , a2 )) If we have a query Q which is atomic, then the closure set contains C(a) or r(a1 , a2 ). (#− T CQ) For such query Cl(Q) = {T CQ, #− T CQ}, i.e. evaluated are two el- ements, and in case of i = 0 the value of #− T CQ is known to be ∅, so Algorithm 1 stops after two evaluations. (T CQ1 U T CQ2 ) For such query Cl(Q) = {T CQ2 , T CQ1 , T CQ1 U T CQ2 , # (T CQ1 U T CQ2 )} (T CQ1 S T CQ2 ) For such query Cl(Q) = {T CQ2 , T CQ1 , T CQ1 S T CQ2 , # (T CQ1 S T CQ2 )} Theorem 4. Soundness. If for UTCQ Q its answer set Ans(Q(x), i), obtained with Al- gorithm 1, is not empty, then Q has at least those certain answers that are in Ans(Q, i). Proof. We prove by induction. We start with evaluating non-temporal query, i.e. a query containing no temporal operator. Base case If we have an atomic query in the form of C(a), then using any ap- proach of CQ answering we obtain all the answers for the query Q entailment over K = {T , (Ai )0≤i≤n }. If K |= C(a) and a ∈ Ans(Q(x), i), the function returns a and this value is stored in Ans(Q(x), i). By Definition 4, this result tells us that the individual a is a certain answer to the query C(x) w.r.t. the match π(x) = a. The same result is obtained if we have atomic query in the form of r(a, b). Inductive case can be obtained by Definition 4. Theorem 5. Completeness. If a UTCQ Q has a certain answer ans, then Algorithm 1 shows that this answer is in Ans(Q, i). Proof. By contradiction. Assume that (i) Q(x) has a certain answer ans w.r.t π, (ii) Ans(Q, i) - is a set of certain answers obtained by Algorithm 1, and (iii) ans 6∈ Ans(Q, i). By (i), we know that K |= Q(ans) and that for all time points 0 ≤ i ≤ n in all models I, such that I |= K, I |= Q(ans). By (ii), for Algorithm 1 to return Ans(Q, i) such that ans 6∈ Ans(Q, i) there are several reasons for it. Q is atomic. If Q is atomic, i.e. in the form C(x) or r(x, y), then we know that Ans(Q, i) does not contain ans. This means that there is a model I of a knowledge base K which does not entail Q(ans). But this is a contradiction to our assumption (i). (T CQ1 ∧ T CQ2 ). If Ans(Q, i) does not contain ans, according to Algorithm 1 it means that ans 6∈ Ans(T CQ1 , i) ./ Ans(T CQ2 , i). This, in turn, leads to the existence of a model I of a knowledge base K such that I |= T CQ1 (ans) and I 2 T CQ2 (ans) or vice versa, that contradicts to (i). (T CQ1 ∨ T CQ2 ). If Ans(Q, i) does not contain ans, according to Algorithm 1 it means that ans 6∈ Ans(T CQ1 , i) × Ans(T CQ2 , i). This, in turn, leads to the ex- istence of a model I of a knowledge base K such that either I 2 T CQ1 (ans) or I 2 T CQ2 (ans), that contradicts to (i). Answering Conjunctive Queries over a Temporally-Ordered ... 89 (#− T CQ). If Ans(Q, i) does not contain ans, according to Algorithm 1 it means that ans 6∈ Ans(Q, i − 1). This, in turn, leads to the existence of a model I of a knowledge base K such that I, i − 1 2 Q(ans), that contradicts to (i). (T CQ1 U T CQ2 ). If Ans(Q, i) does not contain ans, according to Algorithm 1 it means that ans 6∈ Ans(T CQ2 , i) × (Ans(T CQ1 , i) ./ Ans(Q, i + 1). This, in turn, leads to the existence of a model I of a knowledge base K such that either I, i 2 T CQ2 (ans) or I, i 2 T CQ1 (ans) and I, i + 1 2 Q, that contradicts to (i). (T CQ1 S T CQ2 ). If Ans(Q, i) does not contain ans, according to Algorithm 1 it means that ans 6∈ Ans(T CQ2 , i) × (Ans(T CQ1 , i) ./ Ans(Q, i − 1). This, in turn, leads to the existence of a model I of a knowledge base K such that either I, i 2 T CQ2 (ans) or I, i 2 T CQ1 (ans) and I, i − 1 2 Q, that contradicts to (i). The proof for the temporal operator # acting in the direction of future can be com- pleted in the same manner. 5 Related Work and Conclusions Transition graphs for a temporal query language answering over a finite set of versions of a database were investigated in [10]. The expressivity of a temporal query language presented is however restricted either to past [11], or to future [10], [12] direction of time. Known are several algorithms for answering unions of conjunctive queries over knowledge bases with static TBox and ABox, for example works of Ortiz [6], Glimm [7], Tessaris [9], Motik [8] should be mentioned. Any of those algorithms could serve as a basis for finding answers to atemporal CQs at particular time points, whereas possible extensions of those algorithms for the application to a sequence of ABoxes is an open question. A language of temporal conjunctive queries with negation, together with the computational and combined computational complexity is intriduced in [13]. Summing up, obtaining benefits from keeping a large evolving ABox of a knowledge base in a database and applying TBox of that knowledge base to obtain missing as- sertional axioms is one of the ways of dealing with complex evolving domains. It is interesting, due to high computational complexity of temporal conjunctive query an- swering in general, to find a balance between the expressivity of a query language and its practical applicability. Acknowledgements The presented results were obtained during the research visit of the author to the Chair of Automata Theory at Dresden University of Technology. The author is grateful to the group of Prof. Franz Baader, and in particular, Eldora, Marcel Lippmann and Anni-Yasmin Turhan for the fruitful discussions and ideas at the stage of early drafts of the paper. References 1. Poggi, A., Lembo, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Rosati R. Linking Data to Ontologies. J. on Data Semantics, X, 133–173 (2008) 90 N. G. Keberle 2. Baader, F., Bauer, A., Baumgartner, P., Cregan,A., Gabaldon,A., Ji, K., Lee,K., Rajarat- nam,D., Schwitter, R. A novel architecture for situation awareness systems. In: Giese, M. and Waaler, A. (eds.) Proc. 18th International Conference on Automated Reasoning with An- alytic Tableaux and Related Methods (Tableaux 2009). LNCS, vol. 5607, pp. 77–92. Springer, Berlin/Heidelberg (2009) 3. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.). The De- scription Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press (2003) 4. Baier, C., Katoen, J.-P. Principles of Model Checking. The MIT Press, Cambridge, Mas- sachusetts, USA (2008) 5. Abiteboul, S., Hull, R., Vianu, V. Foundations of Databases. Addison-Wesley (1995) 6. Ortiz de la Fuente, M.M. Query Answering in Expressive Description Logics Techniques and Complexity Results. PhD Thesis. Technischen Universitt Wien, Fakultt fr Informatik (2010) 7. Glimm, B. Querying Description Logic Knowledge Bases. PhD Thesis. The University of Manchester (2007) 8. Motik, B. Reasoning in Description Logics using Resolution and Deductive Databases. Uni- vesitt Karlsruhe (2006) 9. Tessaris, S. Questions and answers: reasoning and querying in Description Logic. The Uni- versity of Manchester (2001) 10. Lipeck, U.W. Transformation of Dynamic Integrity Constraints into Transaction Specifica- tions. Theor. Comput. Sci., 76(1), pp. 115–143 (1990) 11. Schwiderski, S., Hartmann, T., Saake, G. Monitoring Temporal Preconditions in a Behaviour Oriented Object Model. Data Knowl. Eng., 14(2), pp. 143–186 (1994) 12. Lipeck, U.W., Feng, D. Construction of Deterministic Transition Graphs from Dynamic In- tegrity Constraints. LNCS, vol. 344, pp.166–179. Springer Verlag (1989) 13. Baader F., Borgwardt, S., Lippmann, M. On the Complexity of Temporal Query Answering. Technical report LTCS-Report 13-01. Available at http://lat.inf.tu- dresden.de/research/reports/2013/BaBoLi-LTCS-13-01.pdf (2013)