﻿ MathJax TeX Test Page 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.

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