Dual Tableaux for Interval Temporal Logics

Abstract

The representation of time by means of intervals rather than points was initiated in philosophical logic, see e.g., [Hum79, Röp80, Bur82, vB83]. In computer science the interval structure of time was adopted by James Allen [All83] for use in solving some artificial intelligence problems such as planning and by Ben Moszkowski [Mos83] for reasoning about periods of time found in a formal description of hardware and software systems. Since then interval temporal logics have been extensively studied both in logic and computer science, and they are successfully applied to the specification and verification of properties of real time systems.

1 Introduction

The representation of time by means of intervals rather than points was initiated in philosophical logic, see e.g., [Hum79, Röp80, Bur82, vB83]. In computer science the interval structure of time was adopted by James Allen [All83] for use in solving some artificial intelligence problems such as planning and by Ben Moszkowski [Mos83] for reasoning about periods of time found in a formal description of hardware and software systems. Since then interval temporal logics have been extensively studied both in logic and computer science, and they are successfully applied to the specification and verification of properties of real time systems.

A calculus of time intervals in a linearly ordered time structure was introduced by Allen in [All83]. In [LM87] (see also [LM94]), this calculus was presented and studied as a relation algebra, called an interval algebra. In the literature various propositional and first-order interval temporal logics have been proposed; a comprehensive survey can be found in [GMS04]. The most popular propositional logics are Halpern and Shoham’s HS [HS91, Ven90], Venema’s CDT logic [GMS03a, GMSS06, Ven91], Moszkowski’s Propositional Interval Temporal Logic PITL (see [Mos83]), and Goranko, Montanari, and Sciavicco’s Propositional Neighborhood Logic PNL [BM05, BMS07, GMS03b].

Propositional interval temporal logics are very expressive. It is known that both HS and CDT are strictly more expressive than every point-based temporal logic on linear orders: they enable us to express properties of pairs of time points rather than single time points. In a linearly ordered set 13 different binary relations between intervals are possible (see [All83]): equals (1′), ends (E), during (D), begins (B), overlaps (O), meets (M), precedes (P) together with their converses (see Table 17.1). Propositional interval temporal logics are usually characterized by modalities of the form ⟨R⟩ and ⟨R ^{− 1}⟩, where R is any of these relations.

Table 17.1 Allen’s interval relations

In this chapter we present relational dual tableaux for several interval temporal logics: for the Halpern–Shoham logic, for some of its axiomatic and signature extensions, and also for its proper fragment without the converses of the interval relations. The extensions are chosen so that they reflect some characteristics of intervals or properties of the ordering of time points. The content of this chapter is based on [BGPO06].

2 Halpern–Shoham Logic

Halpern–Shoham logic, HS,is a propositional interval logic characterized by four temporal modalities that correspond to Allen’s relations begins and ends, and their converses [HS91, Ven90]. These four modalities suffice to define all unary modalities corresponding to Allen’s relations. Hence, the logic HS is the most expressive interval temporal logic. It is undecidable as shown in [HS91]. HS-language is a modal language with four basic modal operations ⟨B⟩, ⟨E⟩, ⟨B ^{− 1}⟩, and ⟨E ^{− 1}⟩. The other propositional operations, such as ∧ , → , and the propositional constants ⊤ (true) and $\perp$ (false), as well as the necessity modalities [B], [E], [B ^{− 1}], and [E ^{− 1}] are defined as in Sect. 7.3.

Given a strict linear ordering (D, < ), a non-strict interval on D is a pair [c, d] such that c ≤ d. We denote the set of all non-strict intervals on D by $\mathbb{I}{(D)}^{+}$. An HS-model is a structure ${\mathcal{M}}^{+} = (D, \mathbb{I}{(D)}^{+},<,m)$, where (D, < ) is a strict linear ordering and m is a meaning function assigning a set of intervals to every propositional variable $p \in \mathbb{V}$, with the intuition that p is true in these intervals. The semantics of HS is defined in terms of the satisfaction relation ⊧ as follows. Let ${\mathcal{M}}^{+} = (D, \mathbb{I}{(D)}^{+},<,m)$ be an HS-model and let $[c,d] \in \mathbb{I}{(D)}^{+}$:

• ${\mathcal{M}}^{+},[c,d]\models p$ iff [c, d] ∈ m(p), for every propositional variable $p \in \mathbb{V}$;

• ${\mathcal{M}}^{+},[c,d]\models \neg \varphi$ iff ${\mathcal{M}}^{+},[c,d]\nvDash \varphi$;

• ${\mathcal{M}}^{+},[c,d]\models \varphi \vee \psi$ iff ${\mathcal{M}}^{+},[c,d]\models \varphi$ or ${\mathcal{M}}^{+},[c,d]\models \psi$;

• ${\mathcal{M}}^{+},[c,d]\models \langle B\rangle \varphi$ iff ∃c′ ∈ D such that c′ < d and ${\mathcal{M}}^{+},[c,c^{\prime}]\models \varphi$;

• ${\mathcal{M}}^{+},[c,d]\models \langle E\rangle \varphi$ iff ∃c′ ∈ D such that c < c′ and ${\mathcal{M}}^{+},[c^{\prime},d]\models \varphi$;

• ${\mathcal{M}}^{+},[c,d]\models \langle {B}^{-1}\rangle \varphi$ iff ∃c′ ∈ D such that d < c′ and ${\mathcal{M}}^{+},[c,c^{\prime}]\models \varphi$;

• ${\mathcal{M}}^{+},[c,d]\models \langle {E}^{-1}\rangle \varphi$ iff ∃c′ ∈ D such that c′ < c and ${\mathcal{M}}^{+},[c^{\prime},d]\models \varphi$.

The notions of the truth and HS-validity are defined as usual.

Note that $\mathbb{I}{(D)}^{+}$ includes also intervals of the form [c, c]. They are called point intervals. Since point intervals have no intervals that begin and/or end them, they can be distinguished by the formulas [B] ⊥ and [E] ⊥ . Namely, [B] ⊥ is satisfied in a model ${\mathcal{M}}^{+}$ by [c, d] iff d is the beginning of this interval. Similarly, [E] ⊥ is satisfied in a model ${\mathcal{M}}^{+}$ by [c, d] iff c is the end point of this interval. This allows us to define two derived operations, [BP] and [EP], that express properties holding on the begin point and on the end point of the current interval, respectively:

$$\begin{array}{rcl} [BP]\varphi &{ \mathrm{df} \atop =} & ([B]\perp \wedge \varphi ) \vee \langle B\rangle ([B]\perp \wedge \varphi ); \\ {[EP]}\varphi &{ \mathrm{df} \atop =} & ([E]\perp \wedge \varphi ) \vee \langle E\rangle ([E]\perp \wedge \varphi ).\end{array}$$

In the presence of point intervals, the modalities corresponding to the other Allen’s relations are definable in logic HS:

$$\begin{array}{lp{1cm}l} \langle D\rangle \varphi { \mathrm{df} \atop =} \langle B\rangle \langle E\rangle \varphi ; & &\langle {D}^{-1}\rangle \varphi { \mathrm{df} \atop =} \langle {B}^{-1}\rangle \langle {E}^{-1}\rangle \varphi ; \\ \langle O\rangle \varphi { \mathrm{df} \atop =} \langle B\rangle \langle {E}^{-1}\rangle \varphi ; & &\langle {O}^{-1}\rangle \varphi { \mathrm{df} \atop =} \langle {B}^{-1}\rangle \langle E\rangle \varphi ; \\ \langle M\rangle \varphi { \mathrm{df} \atop =} [BP]\langle {E}^{-1}\rangle \varphi ;& &\langle {M}^{-1}\rangle \varphi { \mathrm{df} \atop =} [EP]\langle {B}^{-1}\rangle \varphi ; \\ \langle P\rangle \varphi { \mathrm{df} \atop =} \langle M\rangle \langle M\rangle \varphi ; & &\langle {P}^{-1}\rangle \varphi { \mathrm{df} \atop =} \langle {M}^{-1}\rangle \langle {M}^{-1}\rangle \varphi \end{array}$$

3 Relational Logic for Halpern–Shoham Logic

In this section we define a relational logic RL _HS associated with logic HS. The vocabulary of the language of the logic RL _HS consists of the pairwise disjoint sets listed below:

• $\mathbb{I}\mathbb{V} =\{ i,j,k,\ldots \,\}$ – a countable infinite set of interval variables;

• $\mathbb{P}\mathbb{V}\,=\,\{{i}_{1},{i}_{2} : i\,\in \,\mathbb{I}\mathbb{V}\}$ – a countable infinite set of point variables; since intervals are meant to be certain pairs of points, to every interval variable i we associate two point variables denoted i ₁ and i ₂, with the intuition that i = [i ₁, i ₂];

• $\mathbb{I}\mathbb{R}\mathbb{V}$ – a countable infinite set of interval relational variables;

• $\mathbb{P}\mathbb{R}\mathbb{C} =\{ 1^{\prime},<\}$ – the set of point relational constants;

• $\mathbb{I}\mathbb{R}\mathbb{C} =\{ 1,B,E\}$ – the set of interval relational constants;

• $\{-,\cup ,\cap ,\,;\,{,}^{-1}\}$ – the set of relational operations.

The constant < is intended to represent an ordering on the set of time points. The set of point relational terms, $\mathbb{P}\mathbb{R}\mathbb{T}$, is the smallest set of expressions that includes $\mathbb{P}\mathbb{R}\mathbb{C}$ and is closed with respect to the relational operations. The set of interval relational terms, $\mathbb{I}\mathbb{R}\mathbb{T}$, is the smallest set of expressions that includes $\mathbb{I}\mathbb{R}\mathbb{A} = \mathbb{I}\mathbb{R}\mathbb{V} \cup \mathbb{I}\mathbb{R}\mathbb{C}$ and is closed with respect to the relational operations. The set of point relational formulas consists of expressions of the form xRy, where $x,y\,\in \,\mathbb{P}\mathbb{V}$ and $R\,\in \,\mathbb{P}\mathbb{R}\mathbb{T}$. The set of interval relational formulas consists of expressions of the form iRj, where $i,j \in \mathbb{I}\mathbb{V}$ and $R \in \mathbb{I}\mathbb{R}\mathbb{T}$. RL _HS -formulas are point formulas or interval formulas. R is said to be an atomic relational term whenever $R \in \mathbb{P}\mathbb{R}\mathbb{C} \cup \mathbb{I}\mathbb{R}\mathbb{A}$. A formula xRy is said to be atomic whenever R is an atomic relational term.

An RL _HS -model is a structure $\mathcal{M} = (U, \mathbb{I}{(U)}^{+},<,B,E,m)$, where U and $\mathbb{I}{(U)}^{+}$ are non-empty sets and $m: \mathbb{P}\mathbb{R}\mathbb{T} \cup \mathbb{I}\mathbb{R}\mathbb{T} \rightarrow \mathcal{P}(U \times U) \cup \mathcal{P}(\mathbb{I}{(U)}^{+} \times \mathbb{I}{(U)}^{+})$ is a meaning function which assigns binary relations on U ×U to point relational terms and binary relations on $\mathbb{I}{(U)}^{+} \times \mathbb{I}({U}^{+})$ to interval relational terms as follows:

• m(1′) is the relation on U defined as in RL(1, 1′)-models;

• < =m( < ) is a strict linear ordering on U, that is for all c, d, e ∈ U, the following hold:

  $$\begin{array}{ll} (\mathrm{irref}\ <)\quad &\quad (c,c)\not\in \, <, \\ (\mathrm{tran}\ <)\quad &\quad \mathrm{if}\ (c,d) \in \,<\ \mathrm{and}\ (d,e) \in \,<,\ \mathrm{then}\ (c,e) \in \,<, \\ (\mathrm{con}\ <)\quad &\quad (c,d) \in \,<\ \mathrm{or}\ (d,c) \in \,<\ \mathrm{or}\ (c,d) \in m(1^{\prime});\end{array}$$

• m extends to all the compound relational terms $R \in \mathbb{P}\mathbb{R}\mathbb{T}$ as in RL-models;

• $\mathbb{I}{(U)}^{+} =\{ [c,d] \in U \times U : (c,d) \in \,< \cup \,m(1^{\prime})\}$;

• $m(1) = \mathbb{I}{(U)}^{+} \times \mathbb{I}{(U)}^{+}$;

• $B = m(B) =\{ ([c,d],[c^{\prime},d^{\prime}]) \in m(1) : (c,c^{\prime}) \in m(1^{\prime})$ and (d′, d) ∈ < };

• $E = m(E) =\{ ([c,d],[c^{\prime},d^{\prime}]) \in m(1) : (c,c^{\prime}) \in \,<$ and (d, d′) ∈ m(1′)};

• m extends to all the compound interval relational terms $R \in \mathbb{I}\mathbb{R}\mathbb{T}$ in a similar way as in RL-models with the appropriate understanding of relational operations as the operations on $\mathbb{I}{(U)}^{+}$. Accordingly, $m(-R) = (\mathbb{I}{(U)}^{+} \times (\mathbb{I}{(U)}^{+}) \setminus m(R)$.

RL _HS -models such that m(1′) is the identity on U are referred to as standard RL _HS -models. A valuation in an RL _HS -model $\mathcal{M} = (U, \mathbb{I}{(U)}^{+},<,B,E,m)$ is any function $v: \mathbb{P}\mathbb{V} \cup \mathbb{I}\mathbb{V} \rightarrow U \cup \mathbb{I}{(U)}^{+}$ such that:

• If $x \in \mathbb{P}\mathbb{V}$, then v(x) ∈ U;

• If $i \in \mathbb{I}\mathbb{V}$, then $v(i) = [v({i}_{1}),v({i}_{2})] \in \mathbb{I}{(U)}^{+}$.

An RL _HS -formula xRy is said to be satisfied in a model $\mathcal{M}$ by a valuation v, $\mathcal{M},v\models xRy$ for short, whenever (v(x), v(y)) ∈ m(R). A formula is true in $\mathcal{M}$ whenever it is satisfied in $\mathcal{M}$ by every valuation v. A formula is RL _HS -valid whenever it is true in all RL _HS -models.

4 Translation of Halpern–Shoham Logic into a Relational Logic

In this section we define the translation of HS-formulas into relational terms of the logic RL _HS that enables us to represent the validity problem of an HS-formula as the validity problem of the corresponding relational formula. Let τ′ be a one-to-one assignment of interval relational variables to the propositional variables. Then the translation τ that maps HS-formulas to RL _HS -relational terms is defined as follows:

• τ(p) = τ′(p) ; 1, for every propositional variable $p \in \mathbb{V}$;

• $\tau (\neg \varphi ) = -\tau (\varphi )$;

• τ(φ ∨ ψ) = τ(φ) ∪τ(ψ);

• τ(⟨R⟩φ) = R ; τ(φ), for every $R \in \{ B,E,{B}^{-1},{E}^{-1}\}$.

Proposition 17.4.1.

For every HS-model ${\mathcal{M}}^{+}$ and for every HS-formula φ, there exists a standard RL _HS -model $\mathcal{M}$ such that for all interval variables i and j, φ is true in ${\mathcal{M}}^{+}$ iff iτ(φ)j is true in $\mathcal{M}$ .

Proof.

Let φ be an HS-formula and let ${\mathcal{M}}^{+} = (D, \mathbb{I}{(D)}^{+},<,m)$ be an HS-model. Then the corresponding standard RL _HS -model $\mathcal{M} = (U, \mathbb{I}{(U)}^{+},< ^{\prime},B,E,m^{\prime})$ is defined as follows:

• U = D;

• $\mathbb{I}{(U)}^{+} = \mathbb{I}{(D)}^{+}$;

• <′ = < ;

• $m^{\prime}(1) = \mathbb{I}{(U)}^{+} \times \mathbb{I}{(U)}^{+}$ and m′(1′) = Id _U ;

• m′(P) = { ([c, d], [c′, d′]) ∈ m′(1) : [c, d] ∈ m(p)}, for every interval relational variable P such that τ′(p) = P;

• $B =\{ ([c,d],[c^{\prime},d^{\prime}]) \in m^{\prime}(1) : c = c^{\prime}$ and d′ < d};

• E = { ([c, d], [c′, d′]) ∈ m′(1) : c < c′ and d′ = d}.

Given a valuation v in a model ${\mathcal{M}}^{+}$, we show by induction on the complexity of φ that for all interval variables i and j, the following holds:

$${\mathcal{M}}^{+},v(i)\models \varphi \mbox{ iff }\mathcal{M},v\models i\tau (\varphi )j.$$

From that, we can conclude that φ is true in ${\mathcal{M}}^{+}$ iff iτ(φ)j is true in $\mathcal{M}$. By way of example, we prove the required condition for the formulas of the form: $\psi \vee {\vartheta}$, ⟨B⟩ψ, and ⟨E ^{− 1}⟩ψ.

If $\varphi = \psi \vee {\vartheta}$, then ${\mathcal{M}}^{+},v(i)\models \psi \vee {\vartheta}$ iff ${\mathcal{M}}^{+},v(i)\models \psi$ or ${\mathcal{M}}^{+},v(i)\models {\vartheta}$ iff, by the induction hypothesis, $\mathcal{M},v\models i\tau (\psi )j$ or $\mathcal{M},v\models i\tau ({\vartheta})j$ iff $\mathcal{M},v\models i(\tau (\psi ) \cup \tau ({\vartheta}))j$ iff $\mathcal{M},v\models i\tau (\psi \vee {\vartheta})j$.

If φ = ⟨B⟩ψ, then ${\mathcal{M}}^{+},v(i)\models \langle B\rangle \psi$ iff there exists c′ < v(i ₂) such that ${\mathcal{M}}^{+},[v({i}_{1}),c^{\prime}]\models \psi$ iff, by the induction hypothesis and by the definition of $\mathcal{M}$, (v(i), [v(i ₁), c′]) ∈ B and ([v(i ₁), c′], [v(j ₁), v(j ₂)]) ∈ m′(τ(ψ)) iff $\mathcal{M},v\models i(B\,;\,\tau (\psi ))j$ iff $\mathcal{M},v\models i\tau (\langle B\rangle \psi )j$.

Finally, if $\varphi =\langle {E}^{-1}\rangle \psi$, then ${\mathcal{M}}^{+},v(i)\models \langle {E}^{-1}\rangle \psi$ iff there exists c′ < v(i ₁) such that ${\mathcal{M}}^{+},[c^{\prime},v({i}_{2})]\models \psi$ iff, by the induction hypothesis and by the definition of $\mathcal{M}$, (v(i), [c′, v(i ₂)]) ∈ E ^{− 1} and ([c′, v(i ₂)], [v(j ₁), v(j ₂)]) ∈ m′(τ(ψ)) iff $\mathcal{M},v\models i({E}^{-1}\,;\,\tau (\psi ))j$ iff $\mathcal{M},v\models i\tau (\langle {E}^{-1}\rangle \psi )j$.

The following proposition can be proved in a similar way:

Proposition 17.4.2.

For every standard RL _HS -model $\mathcal{M}$ and for every HS-formula φ, there exists an HS-model ${\mathcal{M}}^{+}$ such that for all interval variables i and j, φ is true in ${\mathcal{M}}^{+}$ iff iτ(φ)j is true in $\mathcal{M}$ .

From the above propositions we obtain:

Theorem 17.4.1.

For every HS-formula φ and for all interval variables i and j, the following conditions are equivalent:

• 1. φ is HS-valid;

• 2. iτ(φ)j is true in all standard RL _HS -models.

5 Dual Tableau for Halpern–Shoham Logic

In this section we present a dual tableau for the logic RL _HS and we show how it can be used for verification of validity in HS.

RL _HS -dual tableau contains the decomposition and specific rules of RL(1, 1′)-dual tableau (see Sect. 2.7) adjusted to RL _HS -language. In particular, the rules ( ∪), ( ∩ ), ( − ∪), ( − ∩ ), ( − ), (^{− 1}), $({-}^{-1})$, (; ), and ( − ; ) are assumed both for point relations and for interval relations, i.e., either x, y, z appearing in the rules are point variables and R, S are point relational terms or x, y, z are interval variables and R, S are interval relational terms. The rules (1′1) and (1′2) are assumed for point relational constants, i.e., x and y appearing in the rules are point variables and R is a point relational constant. Furthermore, RL _HS -dual tableau contains the rules of the following forms:

Decomposition Rules from Interval Relations to Point Relations:

For all $i,j,k \in \mathbb{I}\mathbb{V}$ and for every $R \in \mathbb{I}\mathbb{R}\mathbb{A}$,

$$\begin{array}{ll} ({R}_{1})& \frac{iRj} {{i}_{1}1^{\prime}{k}_{1},iRj\ \vert \ {i}_{2}1^{\prime}{k}_{2},iRj\ \vert \ kRj,iRj} \\ ({R}_{2})& \frac{iRj} {{j}_{1}1^{\prime}{k}_{1},iRj\ \vert \ {j}_{2}1^{\prime}{k}_{2},iRj\ \vert \ iRk,iRj}\\ \end{array}$$

For all $i,j \in \mathbb{I}\mathbb{V}$,

$$\begin{array}{ll@{\qquad }ll} (B)& \frac{iBj} {{i}_{1}1^{\prime}{j}_{1},iBj\ \vert \ {j}_{2} < {i}_{2},iBj}\qquad &(-B)& \frac{i-Bj} {{i}_{1}-1^{\prime}{j}_{1},{j}_{2}-<{i}_{2},i-Bj} \\ (E)& \frac{iEj} {{i}_{2}1^{\prime}{j}_{2},iEj\ \vert \ {i}_{1} < {j}_{1},iEj}\qquad &(-E)& \frac{i-Ej} {{i}_{2}-1^{\prime}{j}_{2},{i}_{1}-<{j}_{1},i-Ej}\\ \end{array}$$

Specific Rules:

For all $x,y,z \in \mathbb{P}\mathbb{V}$,

$$\begin{array}{ll} (\mathrm{irref}\ <)& \frac{} {x < x} \\ (\mathrm{tran}\ <) & \frac{x < y} {x < z,x < y\,\vert \,z < y,x < y} \end{array}$$

An RL _HS -axiomatic set is a set including a subset of either of the following forms:

For all $x,y \in \mathbb{P}\mathbb{V}$, $i,j \in \mathbb{I}\mathbb{V}$, $R \in \mathbb{P}\mathbb{R}\mathbb{T}$, and $T \in \mathbb{I}\mathbb{R}\mathbb{T}$,

(Ax1)  {xRy, x − Ry};(Ax1’) {iTj, i − Tj};(Ax2)  {x1′x};(Ax3)  {x < y, x1′y, y < x};(Ax4)  {i1j};(Ax5)  {i ₁ < i ₂, i ₁1′i ₂}.

The axiomatic sets of the form (Ax3) and (Ax5) can be replaced by a rule as discussed in Sect. 25.9.

Observe that any application of the rules of RL _HS -dual tableau, in particular an application of the specific rules listed above, preserves the formulas built with atomic terms or their complements. Thus, the closed branch property holds.

The notion of an RL _HS -set is defined in a similar way as in the relational logics of classical algebras of binary relations (see Sect. 2.4), that is a finite set of RL _HS -formulas is an RL _HS -set whenever the first-order disjunction of its members is valid in every RL _HS -model. Also RL _HS -correctness is defined in a similar way as in Sect. 2.4.

Proposition 17.5.1.

• 1. The RL _HS -rules are RL _HS -correct;

• 2. The RL _HS -axiomatic sets are RL _HS -sets.

Proof.

By way of example, we show that the rules (B) and ( − E) are RL _HS -correct. The proofs of the correctness of the remaining rules are similar. Let X be any finite set of RL _HS -formulas.

(B) It is easy to see that if X ∪{ iBj} is an RL _HS -set, then so are X ∪{ i ₁1′j ₁, iBj} and X ∪{ j ₂ < i ₂, iBj}. Now, assume that X ∪{ i ₁1′j ₁, iBj} and X ∪{ j ₂ < i ₂, iBj} are RL _HS -sets, while X ∪{ iBj} is not an RL _HS -set. Then there exist an RL _HS -model $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that $\mathcal{M},v\nvDash iBj$. However, by the assumption, $\mathcal{M},v\models {i}_{1}1^{\prime}{j}_{1}$ and $\mathcal{M},v\models {j}_{2} < {i}_{2}$, that is (v(i ₁), v(j ₁)) ∈ m(1′), and (v(j ₂), v(i ₂)) ∈ < . By the definition of B, we obtain (v(i), v(j)) ∈ B, thus $\mathcal{M},v\models iBj$, a contradiction.

The proof of correctness of the rule ( − E) is analogous. Namely, if X ∪{ i − Ej}is an RL _HS -set, then so is $X \cup \{ {i}_{2}-1^{\prime}{j}_{2},{i}_{1}-\! <{j}_{1},i-Ej\}$. Now, assume that $X \cup \{ {i}_{2}-1^{\prime}{j}_{2},{i}_{1}-\! <{j}_{1},i-Ej\}$ is an RL _HS -set, while X ∪{ i − Ej} is not an RL _HS -set. Then there exist an RL _HS -model $\mathcal{M}$ and a valuation v in $\mathcal{M}$ such that $\mathcal{M},v\nvDash i-Ej$. However, by the assumption, $\mathcal{M},v\models {i}_{2}-1^{\prime}{j}_{2}$ or $\mathcal{M},v\models {i}_{1}-\! <\,{j}_{1}$, that is (v(i ₂), v(j ₂)) ∉ m(1′) or (v(i ₁), v(j ₁)) ∉ < . By the definition of E, (v(i), v(j)) ∉ E, thus $\mathcal{M},v\models i-Ej$, a contradiction.

The notions of an RL _HS -proof tree, a closed branch of such a tree, a closed RL _HS -proof tree, and RL _HS -provability are defined as in Sect. 2.4.

A branch b of an RL _HS -proof tree is complete whenever it is closed or it satisfies the usual completion conditions determined by the rules ( ∪), ( − ∪), ( ∩ ), ( − ∩ ), ( − ), (^{− 1}), $({-}^{-1})$, (; ), and ( − ; ) listed in Sect. 2.5 adapted both for point relations and for interval relations and, in addition:

For all $x,y \in \mathbb{P}\mathbb{V}$ and $R \in \mathbb{P}\mathbb{R}\mathbb{C}$,

Cpl(1′1) If xRy ∈ b then, for every $z \in \mathbb{P}\mathbb{V}$, xRz ∈ b or y1′z ∈ b, obtained by an application of the rule (1′1);Cpl(1′2) If xRy ∈ b then, for every $z \in \mathbb{P}\mathbb{V}$, z1′x ∈ b or zRy ∈ b, obtained by an application of the rule (1′2);

For all $x,y \in \mathbb{P}\mathbb{V}$,

Cpl(irref < ) x < x ∈ b, obtained by an application of the rule (irref < );Cpl(tran < ) If x < y ∈ b, then for every $z \in \mathbb{P}\mathbb{V}$, x < z ∈ b or z < y ∈ b, obtained by an application of the rule (tran < );

For all $i,j \in \mathbb{I}\mathbb{V}$,

Cpl(R ₁) If iRj ∈ b, then for every $k \in \mathbb{I}\mathbb{V}$ either i ₁1′k ₁ ∈ b, i ₂1′k ₂ ∈ b, or kRj ∈ b, obtained by an application of the rule (R ₁);Cpl(R ₂) If iRj ∈ b, then for every $k \in \mathbb{I}\mathbb{V}$ either j ₁1′k ₁ ∈ b, j ₂1′k ₂ ∈ b, or iRk ∈ b, obtained by an application of the rule (R ₂);Cpl(B) If iBj ∈ b, then either i ₁1′j ₁ ∈ b or j ₂ < i ₂ ∈ b, obtained by an application of the rule (B);Cpl( − B) If i − Bj ∈ b, then ${i}_{1}-1^{\prime}{j}_{1},{j}_{2}- < {i}_{2} \in b$, obtained by an application of the rule ( − B);Cpl(E) If iEj ∈ b, then either i ₂1′j ₂ ∈ b or i ₁ < j ₁ ∈ b, obtained by an application of the rule (E);Cpl( − E) If i − Ej ∈ b, then ${i}_{2}-1^{\prime}{j}_{2},{i}_{1}- < {j}_{1} \in b$, obtained by an application of the rule ( − E).

The notions of a complete RL _HS -proof tree and an open branch of an RL _HS -proof tree are defined as in RL-logic (see Sect. 2.5).

Let b be an open branch of an RL _HS -proof tree. The branch structure ${\mathcal{M}}^{b} = ({U}^{b}, \mathbb{I}{({U}^{b})}^{+},{< }^{b},{B}^{b},{E}^{b},{m}^{b})$ is defined as follows:

• ${U}^{b} = \mathbb{P}\mathbb{V}$;

• m ^b(R) = { (x, y) ∈ U ^b ×U ^b : xRy ∉ b}, for every $R \in \mathbb{P}\mathbb{R}\mathbb{C}$;

• m ^b extends to all the compound relational terms $R \in \mathbb{P}\mathbb{R}\mathbb{T}$ as in RL _HS -models;

• $\mathbb{I}{({U}^{b})}^{+} =\{ [c,d] \in {U}^{b} \times {U}^{b} : (c,d) \in \,{< }^{b} \cup \, {m}^{b}(1^{\prime})\}$;

• ${m}^{b}(R) =\{ (i,j) \in \mathbb{I}{({U}^{b})}^{+} \times \mathbb{I}{({U}^{b})}^{+} : iRj\not\in b\}$, for every $R \in \mathbb{I}\mathbb{R}\mathbb{V}$;

• ${m}^{b}(1) = \mathbb{I}{({U}^{b})}^{+} \times \mathbb{I}{({U}^{b})}^{+}$;

• ${B}^{b} = {m}^{b}(B) =\{ ([c,d],[c^{\prime},d^{\prime}]) \in \mathbb{I}{({U}^{b})}^{+} \times \mathbb{I}{({U}^{b})}^{+} : (c,c^{\prime}) \in {m}^{b}(1^{\prime})$ and (d′, d) ∈ < ^b};

• ${E}^{b}\,=\,{m}^{b}(E)\,=\,\{([c,d],[c^{\prime},d^{\prime}])\,\in \,\mathbb{I}{({U}^{b})}^{+}\,\times \,\mathbb{I}{({U}^{b})}^{+}\,:\,(c,c^{\prime})\,\in \! {< }^{b}$ and (d, d′) ∈ m ^b(1′)};

• m ^b extends to all the compound interval relational terms as in RL _HS -models.

Proposition 17.5.2 (Branch Model Property).

Let b be an open branch of an RL _HS -proof tree. The branch structure ${\mathcal{M}}^{b}$ is an RL _HS -model.

Proof.

We show that < ^b satisfies the conditions (irref < ), (tran < ), and (con < ). All the remaining conditions are satisfied by the definition of the branch structure.

By the completion condition Cpl(irref < ), for every x ∈ U ^b, we have x < x ∈ b, which means that (x, x) ∉ < ^b for every x ∈ U ^b, therefore < ^b is irreflexive. To prove transitivity, assume (x, y) ∈ < ^b and (y, z) ∈ < ^b, that is x < y ∉ b and y < z ∉ b. Suppose (x, z) ∉ < ^b. Then x < z ∈ b. By the completion condition Cpl(tran < ), x < y ∈ b or y < z ∈ b, a contradiction. Therefore < ^b satisfies the condition (tran < ). Since b is open, for all x, y ∈ U ^b, x < y ∉ b or y < x ∉ b or x1′y ∉ b. Otherwise, since the rules preserve formulas built with atomic relational terms or their complements, all of these formulas eventually appear in a node of b and then b would be closed. Thus, (x, y) ∈ < ^b or (y, x) ∈ < ^b or (x, y) ∈ m ^b(1′), therefore < ^b satisfies the condition (con < ).

Given a branch model ${\mathcal{M}}^{b} = ({U}^{b}, \mathbb{I}{({U}^{b})}^{+},{< }^{b},{B}^{b},{E}^{b},{m}^{b})$, let ${v}^{b}: \mathbb{P}\mathbb{V} \cup \mathbb{I}\mathbb{V} \rightarrow {U}^{b} \cup \mathbb{I}{({U}^{b})}^{+}$ be a function such that v ^b(x) = x, for every $x \in \mathbb{P}\mathbb{V}$, and v(i) = [i ₁, i ₂], for every $i \in \mathbb{I}\mathbb{V}$.

Proposition 17.5.3.

Let b be an open branch of an RL _HS -proof tree. Then the function v ^b is a valuation in the branch model ${\mathcal{M}}^{b}$ .

Proof.

By the definition of v ^b, if $x \in \mathbb{P}\mathbb{V}$ then v ^b(x) ∈ U ^b, and if $i \in \mathbb{I}\mathbb{V}$ then v ^b(i) = [v ^b(i ₁), v ^b(i ₂)]. It remains to show that for every $i \in \mathbb{I}\mathbb{V}$, (v ^b(i ₁), v ^b(i ₂)) ∈ < ^b ∪ m ^b(1′). Suppose that there exists $i \in \mathbb{I}\mathbb{V}$ such that (v ^b(i ₁), v ^b(i ₂)) ∉ < ^b ∪ m ^b(1′). Then (v ^b(i ₁), v ^b(i ₂)) ∉ < ^b and (v ^b(i ₁), v ^b(i ₂)) ∉ m ^b(1′). By the definition of m ^b, this implies that i ₁ < i ₂ ∈ b and i ₁1′i ₂ ∈ b. Due to (Ax5), b is closed, a contradiction.

Proposition 17.5.4 (Satisfaction in Branch Model Property).

Let b be an open branch of an RL _HS -proof tree. Then for every RL _HS -formula φ, if ${\mathcal{M}}^{b},{v}^{b}\models \varphi$ , then φ∉b.

Proof.

Let φ be an RL _HS -formula. If φ is a point formula, than the proposition can be proved as in the logic RL(1, 1′) (see Sects. 2.5 and 2.7). Let φ = iRj be an interval formula. The proof is by induction on the complexity of R. If R is an interval relational variable or its complement, the required condition can be proved as in Proposition 2.5.5. Now, we show that the proposition holds for interval relational constants and their complements.

For R = 1, it holds trivially, since every set including i1j is axiomatic.

Let R = B. Assume (i, j) ∈ B ^b, that is (i ₁, j ₁) ∈ m ^b(1′) and (j ₂, i ₂) ∈ < ^b. Then i ₁1′j ₁ ∉ b and j ₂ < i ₂ ∉ b. Suppose iBj ∈ b. By the completion condition Cpl(B), either i ₁1′j ₁ ∈ b or j ₂ < i ₂ ∈ b, a contradiction.

Similarly, for $R = -B$ (resp. E, − E) we use the completion conditions Cpl( − B) (resp. Cpl(E), Cpl( − E)).

Therefore, the proposition holds for all formulas built with an atomic term or its complement. For the formulas built with compound terms it can be proved in a similar way as in RL-logic (see Sect. 2.5).

Following the general method of proving completeness presented in Sect. 2.6, the above propositions imply:

Theorem 17.5.1 (Soundness and Completeness of RL _HS ).

For every RL _HS -formula φ, the following conditions are equivalent:

• 1. φ is RL _HS -valid;

• 2. φ is true in all standard RL _HS -models;

• 3. φ is RL _HS -provable.

Finally, due to the above theorem and Theorem 17.4.1, we get:

Theorem 17.5.2 (Relational Soundness and Completeness of HS).

For every HS-formula φ and for all interval variables i and j, the following conditions are equivalent:

• 1. φ is HS-valid;

• 2. iτ(φ)j is RL _HS -provable.

Example.

Consider the HS-formula:

$$\varphi =\langle B\rangle \langle B\rangle p \rightarrow \langle B\rangle p,$$

which reflects transitivity of relation B. The translation of φ into an RL _HS -term is:

$$\tau (\varphi ) = -(B\,;\,(B\,;\,P)) \cup (B\,;\,P),$$

where for simplicity τ(p) is denoted by P. By Theorem 17.4.1, RL _HS -dual tableau can be used for verification of validity of φ. Figure 17.1 presents an RL _HS -proof of the relational formula iτ(φ)j from which HS-validity of φ follows.

6 Dual Tableaux for Other Interval Temporal Logics

In this section we exploit the modularity of the relational approach, and we show how to extend HS-dual tableau to cope with other interval relations and other meaningful temporal domains.

Fig. 17.1

An RL _HS -proof of the formula ⟨B⟩⟨B⟩p → ⟨B⟩p

Logics Based on Strict Intervals

In the previous sections we considered the non-strict semantics of HS where, given a strict ordering (D, < ), the set of non-strict intervals $\mathbb{I}{(D)}^{+}$ is defined as the set of all [c, d] such that c ≤ d. As a consequence, the set of intervals includes the point intervals of the form [c, c]. In the literature an alternative semantics for interval logics is considered, namely the strict semantics, where the point intervals are excluded. Given a strict ordering (D, < ), a strict interval is a pair [c, d] where c < d. The set of all strict intervals on D is denoted by $\mathbb{I}{(D)}^{-}$. The models based on strict intervals are defined in a way analogous to the non-strict case.

In what follows, we show how to modify the dual tableau for RL _HS in the case of the strict semantics. To this end, we define the relational logic ${\mathsf{RL}}_{\mathsf{HS}}^{-}$ (strict RL _HS ), having the same syntax as non-strict RL _HS , but a different semantics.

An ${\mathsf{RL}}_{\mathsf{HS}}^{-}$-model is a structure ${\mathcal{M}}^{-} = (U, \mathbb{I}{(U)}^{-},<,B,E,m)$, where (U, m) is an RL(1, 1′)-model, < , B, and E are defined as in RL _HS -models, $\mathbb{I}{(U)}^{-} =\{ [c,d] \in U \times U : (c,d) \in \,<\}$ and $m(1) = \mathbb{I}{(U)}^{-}\times \mathbb{I}{(U)}^{-}$. An ${\mathsf{RL}}_{\mathsf{HS}}^{-}$-valuation is any function $v: \mathbb{P}\mathbb{V} \cup \mathbb{I}\mathbb{V} \rightarrow \mathcal{P}(U) \cup \mathcal{P}(\mathbb{I}{(U)}^{-}\times \mathbb{I}{(U)}^{-})$ such that:

• If $x \in \mathbb{P}\mathbb{V}$, then v(x) ∈ U;

• If $i \in \mathbb{I}\mathbb{V}$, then $v(i) = [v({i}_{1}),v({i}_{2})] \in \mathbb{I}{(U)}^{-}$.

The notions of satisfaction and validity of a formula are defined as in logic RL _HS .

A dual tableau for ${\mathsf{RL}}_{\mathsf{HS}}^{-}$ is obtained from the RL _HS -dual tableau by replacing the axiomatic set (Ax5) with:

$$\begin{array}{@{}ll} ({\mathrm{Ax5}}^{-})&\ \,{i}_{1} < {i}_{2},\ \mathrm{for}\ i \in \mathbb{I}\mathbb{V}\end{array}$$

${\mathsf{RL}}_{\mathsf{HS}}^{-}$-dual tableau is sound and complete; it can be proved in a similar way as for RL _HS -dual tableau.

Other Interval Temporal Logics

Now, we show how to modify the relational logic RL _HS and its dual tableau to obtain a relational logic and a corresponding dual tableau for any interval logic based on relations chosen from the 13 Allen’s relations. Let $I \subseteq \{ E,{E}^{-1},D,{D}^{-1},B,{B}^{-1},O,{O}^{-1},M,{M}^{-1},$ P, P ^{− 1}}. A language of a logic L _I is obtained from the HS-language by replacing the set of relational constants $\{B,E,{B}^{-1},{E}^{-1}\}$ with the set I and the set of modal operations with {⟨R⟩ : R ∈ I}. Given an interval logic L _I , the corresponding relational logic ${\mathsf{RL}}_{{\mathsf{L}}_{I}}$ differs from RL _HS only in the choice of the set of interval relational constants, that is $\mathbb{I}\mathbb{R}\mathbb{C} =\{ 1\} \cup I$. Models of ${\mathsf{RL}}_{{\mathsf{L}}_{ I}}$ are defined as those of RL _HS with the assumption that the semantics of the relational constants from I is defined in accordance with the semantics of the chosen primitive interval relations. A validity preserving translation τ of L _I -formulas into ${\mathsf{RL}}_{{\mathsf{L}}_{I}}$-formulas is obtained from the translation presented in Sect. 17.4 by assuming R ∈ I.

A dual tableau for ${\mathsf{RL}}_{{\mathsf{L}}_{I}}$ can be obtained from RL _HS -dual tableau (in the case of the non-strict semantics for intervals) or from ${\mathsf{RL}}_{\mathsf{HS}}^{-}$-dual tableau (in the case of the strict semantics), by replacing the rules (B), (E), ( − B), and ( − E) with the rules appropriate for the choice of basic relations. The rules for the relations D, M, P, and O have the following forms:

For all $i,j \in \mathbb{I}\mathbb{V}$,

$$\begin{array}{ll@{\qquad \quad }ll} (D) & \frac{iDj} {{i}_{1} < {j}_{1},iDj\ \vert \ {j}_{2} < {i}_{2},iDj}\qquad \quad &(-D) & \frac{i-Dj} {{i}_{1}-<{j}_{1},{j}_{2}-<{i}_{2},i-Dj} \\ (M)& \frac{iMj} {{j}_{2}1^{\prime}{i}_{1},iMj} \qquad \quad &(-M)& \frac{i-Mj} {{j}_{2}-1^{\prime}{i}_{1},i-Mj} \\ (P) & \frac{iPj} {{j}_{2} < {i}_{1},iPj} \qquad \quad &(-P) & \frac{i-Pj} {{j}_{2}-<{i}_{1},i-Pj}\\ \end{array}$$

$$\begin{array}{ll} (O) & \frac{iOj} {{j}_{1} < {i}_{1},iOj\ \vert \ {i}_{1} < {j}_{2},iOj\ \vert \ {j}_{2} < {i}_{2},iOj} \\ (-O)& \frac{i-Oj} {{j}_{1}-<{i}_{1},{i}_{1} < {j}_{2},{j}_{2} < {i}_{2},i-Oj} \end{array}$$

The rules presented in Sect. 17.5 allow us to easily adapt RL _HS -dual tableau to any propositional interval temporal logic that is a proper fragment of HS. Here we show two examples of such a modification.

The logic with relations B and B ^{− 1} and the logic with relations E and E ^{− 1} are decidable (see [GMS04]). The logic BE is obtained from HS by deleting the operations ⟨B ^{− 1}⟩ and ⟨E ^{− 1}⟩. It was studied in [Lod00], where its undecidability was proved. Since BE does not have modal operations determined by converses of relations B and E, the relational logic RL _BE appropriate for representation of BE-formulas is the logic RL _HS without the converse operation ^{− 1}. A dual tableau for RL _BE can be obtained from that of RL _HS by deleting the rules (^{− 1}) and (${-}^{-1}$).

Interval logics based on the relation meet, M, and its converse are usually called neighborhood logics. First-order neighborhood logics were first introduced and studied in [CH97]. Their propositional variant, called Propositional Neighborhood Logic, PNL, was proposed and investigated recently in [GMS03b].

In [GMS03b] the authors studied logic PNL both with the non-strict and strict semantics over linear orderings. Let PNL ⁺ and PNL ⁻ be the respective logics. The relati onal logic ${\mathsf{RL}}_{{\mathsf{PNL}}^{+ }}$ is obtained from logic RL _HS by taking the interval relational constant M in place of B and E. A dual tableau for ${\mathsf{RL}}_{{\mathsf{PNL}}^{+ }}$ can be obtained from that of RL _HS by replacing the rules (B), ( − B), (E), and ( − E) with the rules (M) and ( − M). In the case of the strict semantics, the relational logic ${\mathsf{RL}}_{{\mathsf{PNL}}^{- }}$ can be obtained from ${\mathsf{RL}}_{\mathsf{HS}}^{-}$ in the same way.

In all the relational systems RL _L presented above, the strict ordering < is considered to be linear, without any further assumption. We can modify this constraint by requiring that the order of point intervals in the models is, for example, unbounded from below, serial, dense, or discrete. Then, in order to obtain a dual tableau for such a restriction, we replace the rules and axiomatic sets that reflect strict linearity of < by the rules corresponding to the appropriate properties of < assumed in the models, as presented in Sect. 16.3.