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)).