Cone Logic   (written by Przemysław Wałęga)

Formalism description:

Formulas $\varphi$ of cone logic are generated by the following abstract syntax:

$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid$ $\varphi \mid$  $\varphi \mid$ $\varphi \mid $  $\varphi \mid$  ⁺$\varphi \mid$  ⁺$\varphi \mid$  ⁺$\varphi \mid $  ⁺$\varphi ,$

where $p$ denotes a propositional letter.

Formulas of cone logic are evaluated over regions of the form $\mathbb{P} = ( \mathsf{P} , \sigma)$ where $\mathsf{P} \subseteq \mathbb{Q} \times \mathbb{Q}$ and $\sigma: \mathsf{P} \to 2^{Var}$ assigns a subset of a set of all propositional variables $Var$ to each point from $\mathsf{P}$.

The satisfaction relation $\models$ for a region $\mathbb{P}$ and a point $(x,y) \in \mathsf{P}$ is defined as follows:

$\mathbb{P}, (x,y) \models p$	iff	$p \in \sigma \big( (x,y) \big); $
$\mathbb{P}, (x,y) \models \neg \varphi$	iff	$\mathbb{P}, (x,y) \not\models \varphi; $
$\mathbb{P}, (x,y) \models \varphi \lor \psi $	iff	$\mathbb{P}, (x,y) \models \varphi \text{ or } \mathbb{P}, (x,y) \models \psi; $
$\mathbb{P}, (x,y) \models $ $\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' < x, y' < y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $ $\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' > x, y' < y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $ $\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' < x, y' > y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $ $\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' > x, y' > y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $  +$\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' ≤ x, y' ≤ y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $  +$\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' ≥ x, y' ≤ y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $  +$\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' ≤ x, y' ≥ y, \text{and } \mathbb{P}, (x',y') \models \varphi;$
$\mathbb{P}, (x,y) \models $  +$\varphi $	iff	$\text{there is } (x',y') \in \mathsf{P} \text{ such that } x' ≥ x, y' ≥ y, \text{and } \mathbb{P}, (x',y') \models \varphi;$

Spatial reasoning, interval temporal reasoning.

Cone logic is introduced in (Montanari et al. 2009). It is proved to be decidable, and in particular PSpace-complete. Moreover, it is expressive enough to subsume meaningful interval temporal logics.