Keywords

1 Introduction. Main Definitions

In 1983, J.A. Allen has published the seminal paper “Maintaining knowledge about temporal intervals”, where he has proposed a simple temporal logic formalism [1]. Allen studied qualitative constraints with temporal intervals linked by means of elementary relations (like “before”, “after”, “during”, “overlaps” and so on). His work was followed by a study of metric constraints for temporal intervals. Allen’s interval logic and its extensions were applied to various problems of intelligent information systems designing (knowledge representation, common sense reasoning, natural language understanding, actions planning, ontology modeling et al.).

An ontology for a dynamic problem domain contains temporal dependencies between concepts [3, 5, 8]. For example, suppose that a given ontology contains the concept Agent with the attribute Action. Let a be one of the values of the attribute. Then the expression \( Agent.Action = a \) denotes the event “the agent carries out the action a”. We assume that the event takes place within a certain temporal interval A = [A −, A +], where A − and A + are time points which mark the beginning and end of the interval. We also assume that A −, A + are integers and A − < A + (so, we consider only non-degenerated intervals).

Thus, with every ontology for dynamic problem domain it is associated the interval ontology whose concepts are temporal intervals and temporal relations.

In Allen’s interval logic (let us denote it by LA), there are 7 basic relations between intervals: e (equals), b (before), m (meets), o (overlaps), f (finishes), s (starts), d (during) (see Table 1.) The inverted relations are marked by asterisks: b* (after), m* (met-by), o* (overlapped-by), f* (finished-by), s* (started-by), d* (contains). (So, \( A\,{\upalpha} * B \Leftrightarrow B\,\upalpha\,A, \) where α is basic relation and A, B are temporal intervals.)

Table 1 Basic relations of Allen’s interval logic
Full size table

A sentence (formula) of LA is an expression of the form A ω B where ω is any subset of the set Ω = {e, b, m, o, f, s, d, b*, m*, o*, f*, s*, d*} and A, B are interval names. If ω = {α}, then we have a primitive sentence, and instead of A{α}B we write A α B. If ω = {α1, α2,…, αk} then we write A α1α2…αk B instead of A{α1, α2,…, αk}B. The formula A ω B is interpreted as disjunction of the primitive formulas: \( A\,\upomega\,B \Leftrightarrow {\text{V}}\{ A\,\upalpha\,B|\upalpha \in\upomega\} \).

As every logic, LA induces the relation “|=” of logical consequence. Let O be an interval ontology written in LA and σ be a LA sentence. Then O | = σ if and only if there is no interpretation such that all sentences of O are true but σ is false.

Boolean extension LA+ of Allen’s interval logic LA consists of formulas which are Boolean combinations of LA formulas, i.e. LA+ has the following syntax: (a) propositional variables are LA+ sentences; (b) LA sentences belong to LA+; (c) ~ φ, (φ ∧ ψ), (φ ∨ ψ) are LA+ sentences if φ and ψ are LA+ sentences. We also introduce φ → ψ as an abbreviation of ~ φ ∨ ψ. Semantics of LA+ formulas is defined as usual.

Take, for example, the primitive LA sentence A o B. The sentence is characterized by the inequalities A − < B −, B − < A +, A +< B + or by the inequalities B − – A − > 0, A +– B − > 0, B +– A + > 0. Suppose, B − – A − = 3, A +– B − ≥ 1. Then we have metric information which constrains interpretation of the sentence A o B, and we write the sentence A o(B −– A − = 3; A +– B − ≥ 1) B. The sentences of this type make up the language μLA of the Boolean extension interval Allen’s logic with metrical information. The language μLA has the following syntax:

  1. (a)

    primitive constraints in the ontology O with intervals A 1, A 2,…, A n have the forms X – Y = r, X – Y > r, X – Y ≥ r, X – Y < r, X – Y ≤ r, X – Y < s, where X, Y \( \in\){A −1 , A +1 , A −2 , A +2 , …, A − n , A + n } and r is an integer;

  2. (b)

    an arbitrary constraint λ is a conjunction of primitive constraints, i.e. λ has the form θ1; θ2;…; θ m where θ i are primitive constraints, and semicolon denotes conjunction;

  3. (c)

    a μLA sentence has the form A δ1δ2…δ m B, where every δ i \( \in\) Ω or δ i  = α(λ), α \( \in\) Ω and λ is a constraint such that only members of {A −, A +, B −, B +} can occur in λ.

We extend the language μLA to the language of the extended Allen’s interval logic μLA+ in the same way as we have extended LA to LA+. The language μLA+ has the following syntax: (a) propositional variables are μLA+ sentences; (b) constraints are μLA+ sentences; (c) μLA sentences are μLA+ sentences; (d) ~ φ, (φ ∧ ψ), (φ ∨ ψ) are μLA+ sentences if φ and ψ are μLA+ sentences.

Example 1

Suppose, there is an agent which can carry out the actions a, b and c. Each action requires some time; therefore, temporal intervals A, B, C are associated with the actions a, b, c. Moreover, suppose that there are conditions p and q such that:

  1. (1)

    If p is true then there is no time point at which both actions a and b are carried out;

  2. (2)

    If q is true then the action b is carried out only when the action c is carried out.

    Consider the question:

  3. (3)

    What Allen’s relations are impossible between the A and C if both conditions p and q take place?

It is clear that the assertions (1) and (2) can be represented in LA+ by the formulas p → A bb* B and q → B edfs C. Also, we may write the question (3) as the query ?x – p ∧ q → ~ A x C to the ontology O = {p → A bb* B, q → B edfs C}. The answer to the query consists of those relations x \( \in\) Ω that the logical consequence O | = p ∧ q → ~ C x A holds. Later, in Example 3, we will find that the answer consists of the relations d*, e, f* and s.

Consider the following two assertions about the actions a, b, c, and the query:

  1. (4)

    If p is true then the action a is carried out before b with time distance ≥ 2;

  2. (5)

    If p is true then the action b is carried out before c with time distance ≥ 3;

  3. (6)

    Suppose if p /\ q holds. Find the greatest x such that distance between intervals A and C is not less than x.

These assertions are written in μLA+ as p → A b(B − – A + ≥ 2) B, q → B b(C −– A + ≥ 3) C.

The query can be written as ? max x – p /\ q → A b(C − – A + ≥ x) C. (End of Example 1.)

In this paper, we give the deduction method based on analytical tableaux for the extended Allen’s interval logics LA+ and μLA+. We show how to apply this method for query answering over ontologies written in LA+ and μLA+.

2 Inference Rules and Deduction in the Logics LA+ and μLA+

In Tables 2, 3 and 4, there are the inference rules for the logics LA+ and μLA+. Consider an example of deduction by means of these rules.

Table 2 Inference rules for propositional connectives
Full size table
Table 3 Inference rules for the Allen’s connectives
Full size table
Table 4 Inference rules for constraints
Full size table

Example 2

Take the ontology O = {p → A b(B −– A + ≥ 2) B, q → B b(C − – A + ≥ 3) C} and the formula – p ∧ q → A b(C −– A + ≥ 3) C. To prove that O | = – p ∧ q → A b(C − – A + ≥ 3) C, we construct the deduction tree by applying the inference rules to the following set of formulas with signs “+” and “–”: {+ p → A b(B −– A + ≥ 2) B, + q → B b(C −– A + ≥ 3) C} (see Fig. 1).

Fig. 1
figure 1

Deduction tree for Example 2

Full size image

Constructing the deduction tree starts with the initial branch containing the formulas +p → A b(B − – A + ≥ 2) B, +q → B b(C −– B + ≥ 3) C, – p ∧ q → A b(C − – A + ≥ 3) C. At the first step we have applied the rule from Table 2 in the second row and fourth column (denote it T2.24) to the formula – p ∧ q → A b(C − – A + ≥ 3) C and have put the label “[7]” on the right of the formula. As a result of the application of the rule T2.24, two formulas + p ∧ q and – A b(C − – A + ≥ 3) C have been added in sequence to the initial branch, and the label “1:” has been put on the left of these formulas. At the step 7, the rule T2.23 has been applied to +q → B b(C −– B + ≥ 3) C. As a result, the “fork” with formulas – q and +B b(C − – B + ≥ 3) C has been added to the current branch. The tree has four branches. The first (left) branch is closed, i.e. it is inconsistent since it contains the contrary pair +p and – p. The second branch also closed since it contains the contrary pair +q and – q. Let us write out of the third and fourth branches all inequalities (without signs), and add the valid inequalities A + – A − ≥ 1, B + – B − ≥ 1, C +– C − ≥ 1:

$$ \begin{aligned} & {\text{S}}_{ 1} = \{ B^{-} {-}A^{ + } \ge 2,\,C^{-} {-}B^{ + } \ge 3,\,A^{ + } {-}C^{-} \ge 0,\,A^{ + } {-}A^{-} \ge 1,\,B^{ + } {-}B^{-} \ge 1,\,C^{ + } {-}C^{-} \ge 1\} , \\ & {\text{S}}_{ 2} = \{ B^{-} {-}A^{ + } \ge 2,\,C^{-} {-}B^{ + } \ge 3,\,A^{ + } {-}C^{-} \ge {-} 3,\,A^{ + } {-}A^{-} \ge 1,\,B^{ + } {-}B^{-} \ge 1,\,C^{ + } {-}C^{-} \ge 1\} . \\ \end{aligned} $$

The sets S 1 and S 2 are inconsistent. Indeed, S1 includes the inequalities B − – A +≥ 2, B +– B − ≥ 1, C + – B +≥ 3, A + – C − ≥ 1. Adding up these inequalities (B − – A +) + (B +– B −) + (C +– B +) + (A +– C −), we obtain 0 ≥ 2 + 1+3 + 0 = 6 (contradiction). Similarly, S2 is inconsistent, since it includes the inequalities B − – A +≥ 2, B + – B − ≥ 1, C +– B +≥ 3, A + – C − ≥ –3, and adding up them we obtain 0 ≥ 2 + 1+3 + (– 3) = 3 (contradiction). Hence, the deduction tree is closed, and this means inconsistency of the ontology O. (End of Example 2.)

Let S be any set of inequalities of the forms X – Y  ≥ r, where X, Y are integer variables and r is an integer. We associate with S the following labeled directed graph Г(S). Its vertices are integer variables and its labeled arcs are triples (X, Y, r) with the condition that the inequality X – Y  ≥ r enters the set S.

Figure 2 shows the graphs Г(S1) and Г(S2) for the above sets S1 and S2. (Here we did not draw the labels “1”.) We see that the graphs contain the cycle A +, B −, B +, C +, D −, A +. Length of this cycle in Г(S1) is 6, and in Г(S2) is 3.

Fig. 2
figure 2

Graphs for systems of inequalities

Full size image

In general, for arbitrary set S of inequalities the following assertion is true: S is inconsistent if and only if Г(S) has a positive cycle. There is a computationally effective algorithm for detecting positive cycles in labeled graphs. This algorithm can be used to prove the closing of deduction trees.

3 Query Answering Over Ontologies in LA+ and μLA+

Let O be an ontology in LA+. A query to O has the form

?(x 1, x 2,…, x n ) – κ[x 1, x 2,…, x n ],

where κ[x 1, x 2,…, x n ] is a LA+ formula that contains primitive sentences of the form A x i B. The answer to this query is the tuple (α1, α2,…, α n ) (where α n \( \in\) Ω) such that the formula, which is the result of replacing x i with α i , is logical consequence of the ontology: O |= κ[α1, α2,…, α n ].

Example 3

Take the ontology O = {p → A bb* B, q → B edfs C} and the query ?x – p ∧ q → ~ A x C. In Fig. 3, the deduction tree for the set {+ p → A bb* B, +q → B edfs C} of formulas (with signs “+” and “ –”) is shown. Here at step 6 we have applied the second inference rule from Table 3 to formulas A bb* B and B edfs C. As result, we have get +A bb*dmm*o*s B since (see Table 5)

Fig. 3
figure 3

Deduction tree for Example 3

Full size image
Table 5 Inference rules for logic LA
Full size table
$$ \begin{aligned} \varvec{bb}* \circ \varvec{edfs} &=\, \varvec{b} \circ \varvec{e}\,{\text{U}}\,\varvec{b} \circ \varvec{d}\,{\text{U}}\,\varvec{b} \circ \varvec{f}\,{\text{U}}\,\varvec{b} \circ \varvec{s}\,{\text{U}}\,\varvec{b}* \circ \varvec{e}\,{\text{U}}\,\varvec{b}* \circ \varvec{d}\,{\text{U}}\,\varvec{b}* \circ \varvec{f}\,{\text{U}}\,\varvec{b}* \circ \varvec{s} \\ &=\, \varvec{b}\,{\text{U}}\,\varvec{bdmos}\,{\text{U}}\,\varvec{bdmos}\,{\text{U}}\,\varvec{b}\,{\text{U}}\,\varvec{b}*{\text{U}}\,\varvec{b}*\varvec{dfm}*\varvec{o}*{\text{U}}\,\varvec{b}*{\text{U}}\,\varvec{b}*\varvec{dfm}*\varvec{o}* \\ &=\, \varvec{bb}*\varvec{dfmm}*\varvec{oo}*\varvec{s}. \\ \end{aligned} $$

The third branch will be closed if and if the x \( \cap \) bb*dmm*o*s = ∅. Hence, the logical consequence O |= p ∧ q → ~ A x C takes place if and only if x \( \subseteq\) Ω \ bb*dmm*o*s = d*ef*s. Thus, the answer to query ? x – p ∧ q → ~ A x C consists of the relations d*, e, f* and s. (End of Example 3.)

For logic μLA+ we consider queries of the form

? max{x 1, x 2,…, x m }, min{y 1, y 2,…, y n } – κ[x 1, x 2,…, x m , y 1, y 2,…, y n },

where κ[x 1, x 2,…, x m , y 1, y 2,…, y n }is μLA+ formula that contains inequalities with integer variables x i and y j . The answer to that query is the maximal values of x i and minimal values of y i such that κ[x 1, x 2,…, x m , y 1, y 2,…, y n } is logical consequence of the given ontology (Table 6).

Table 6 Fragment of Allen’s multiplication table
Full size table

Consider, by example, how to find answers to these kind of queries.

Example 4

Let us take the ontology O = {p → A b(B − – A + ≥ 2) B, q → B b(C −– A + ≥ 3) C} and the query ? max x – p /\ q → A b(C −– A + ≥ x) C. To prove that O | = p /\ q → A b(C − – A + ≥ x) C, we must construct the deduction tree by applying the inference rules to the following set of formulas with the signs “+” and “–”: {+ p → A b(B − – A + ≥ 2) B, + q → B b(C − – A + ≥ x) C}. This tree is obtained from the tree shown in Fig. 1 by replacing the formulas – A b(C −– A + ≥ 4) C (*) and – C −– A + ≥ 4 (*) with – A b(C − – A + ≥ x) C and – C −– A + ≥ x) (correspondingly), and replacing the formula A +n– C − ≥ – 3 (**) with A +n– C − ≥ 1– x. Figure 2 shows the graph Г(S3) which is constructed for fourth branches of the deduction three. The graph Г(S3) contains the cycle A +, B −, B +, C −, A + of the length 2 + 1 + 3 + 1 – x, and that cycle will be positive if and only if x ≤ 6. Therefore, x = 6 is the answer to that query. (End of Example 4.)

4 Conclusion

We have defined the extended Allen’s interval logic μLA+. The sentences of this logic are Boolean combinations of the sentences of Allen’s interval logic with incorporated inequalities and equalities for ends of temporal intervals. For this logic, we have defined the deduction method based on analytical tableaux [2]. This method was used for query answering over ontologies written in μLA+. Possible practical applications of the results of the paper are in domain of workflows technology [7, 4, 6, 8].