diamond1   Logics for Qualitative Reasoning   Logics for time   Halpern-Shoham Logic

Halpern-Shoham Logic   (written by Przemysław Wałęga)

Formalism description:

Formulas $\varphi$ of Halpern-Shoham logic are generated by the following abstract syntax: $$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid \langle \text{B} \rangle \varphi \mid \langle \text{E} \rangle \varphi \mid \langle \overline{\text{B}} \rangle \varphi \mid \langle \overline{\text{E}} \rangle \varphi , $$ where $p$ denotes a propositional letter.

Kripke-style semantics:

A Halpern-Shoham model is of the form $\mathfrak{M} = ( \mathbb{D}, V )$, where $\mathbb{D}=( D , <)$ is a strict linear ordering on a set $D$ of time points, $I(\mathbb{D})^+$ is a set of all non-strict intervals over $\mathbb{D}$, i.e., $I(\mathbb{D})^+=\{ [d_0 , d_1] \mid d_0, d_1 \in D \text{ and } d_0 \leq d_1 \}$, and $V : I(\mathbb{D})^+ \to 2^{Var}$ is a valuation assigning a set of propositions variables to each interval.

The satisfaction relation for a model $\mathfrak{M}$ and an interval $[d_0, d_1]$ is defined as follows:

\[ \begin{array}{lll} \mathfrak{M}, [d_0 , d_1]\models p & \text{iff} & p \in V([d_0,d_1]) \text{ for } p\in Var; \\ \mathfrak{M}, [d_0 , d_1]\models \neg \varphi & \text{iff} & \mathfrak{M}, [d_0 , d_1] \not\models \varphi; \\ \mathfrak{M}, [d_0 , d_1]\models \varphi \lor \psi & \text{iff} & \mathfrak{M}, [d_0 , d_1]\models \varphi \text{ or } \mathfrak{M}, [d_0 , d_1]\models \psi; \\ ; \mathfrak{M}, [d_0 , d_1]\models \langle \text{B} \rangle \varphi & \text{iff} & \text{there is } d_2 \text{ such that } d_2 < d_1 \text{ and } \mathfrak{M}, [d_0 , d_2]\models \varphi; \\ \mathfrak{M}, [d_0 , d_1]\models \langle \text{E} \rangle \varphi & \text{iff} & \text{there is } d_2 \text{ such that } d_0 < d_2 \text{ and } \mathfrak{M}, [d_2 , d_1]\models \varphi; \\ \mathfrak{M}, [d_0 , d_1]\models \langle \overline{\text{B}} \rangle \varphi & \text{iff} & \text{there is } d_2 \text{ such that } d_1 < d_2 \text{ and } \mathfrak{M}, [d_0 , d_2]\models \varphi; \\ \mathfrak{M}, [d_0 , d_1]\models \langle \overline{\text{E}} \rangle \varphi & \text{iff} & \text{there is } d_2 \text{ such that } d_2 < d_0 \text{ and } \mathfrak{M}, [d_2 , d_1]\models \varphi. \\ \end{array} \] Application fields:

Spatial reasoning, interval temporal reasoning.

Comments and references:

Halpern-Shoham logic is introduced in (Halpern & Shoham 1991). It is expressive enough to describe all relations of Allen's interval algebra. Moreover, the logic is strictly more expressive than any point-based temporal logic in a sense that Halpern-Shoham logic distinguishes more temporal frames than any point-based logic (Venema 1990).

Decidability of the satisfiability problem in Halpern-Shoham logic depends on the class of underlying temporal structures. In particular, the problem is undecidable in any class of linear orders that contains at least one linear order with an infinite ascending sequence (e.g., $\mathbb{Z}$, $\mathbb{Q}$, and $\mathbb{R}$) (Halpern & Shoham 1991). A number of restrictions of the logic have been introduced in order to obtain decidable logics (see, e.g., (Goranko et al. 2004), (Della et al. 2013), and (Montanari 2010)).


  1. Goranko, V., & Montanari, A., & Sciavicco, G. (2004). A Road Map of Interval Temporal Logics and Duration Calculi. Journal of Applied Non-Classical Logics, 14(1-2), 9--54, 2004.
  2. Della Monica D., & Goranko, V., & Montanari, A., & Sciavicco, G. (2013). Interval Temporal Logics: A Journey. Bulletin of EATCS, 3(105).
  3. Halpern, J., Y., & Shoham, Y. (1991). A Propositional Modal Logic of Time Intervals. Journal of the ACM (JACM), 38(4), 935--962.
  4. Montanari, A., & Puppis, G., & Sala, P. (2010). Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals. Automata, Languages and Programming, 345--356, Springer. .
  5. Venema, Y. (1990). Expressiveness and Completeness of an Interval Tense Logic. Notre Dame Journal of Formal Logic, 31(4), 529--547, University of Notre Dame.