Logics for Qualitative Reasoning   Logics for space   Spatial Propositional Neighborhood Logic (SpPNL)

Spatial Propositional Neighborhood Logic (SpPNL)   (written by Przemysław Wałęga)

Formalism description:

Formulas $\varphi$ of compass logic are generated by the following abstract syntax: $$ \varphi ::= p \mid \neg \varphi \mid \varphi \lor \varphi \mid \langle \text{E} \rangle \varphi \mid \langle \text{W} \rangle \varphi \mid \langle \text{N} \rangle \varphi \mid \langle \text{S} \rangle \varphi ,$$ where $p$ denotes a propositional letter.

Kripke-style semantics:

An SpPNL model is a tuple of the form $\mathfrak{M} = (\mathbb{F},\mathbb{O}(\mathbb{F}) , V)$, where $\mathbb{F} = (\mathbb{H} \times \mathbb{V})$ is a spatial structure composed of two linear orders, namely $\mathbb{H} = ( H, < )$ and $ \mathbb{V} = ( V, < )$, $\mathbb{O}(\mathbb{F})$ is a set of all objects (rectangles) in $\mathbb{F}$, i.e., $\mathbb{O}(\mathbb{F}) = \{ \langle (h, v) , (h' , v' ) \rangle \mid h < h', v < v', h, h' \in \mathbb{H}, \text{ and } v, v' \in \mathbb{V} \}$, and $V : \mathbb{O}(\mathbb{F}) \to 2^{Var}$ is a valuation assigning a set of propositions variables to each object (rectangle).

The satisfaction relation for a model $\mathfrak{M}$ and an object $\langle (h, v) , (h' , v' ) \rangle$ is defined as follows:

\[ \begin{array}{lll} \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models p & \text{iff} & p \in V\big(\langle (h, v) , (h' , v' ) \rangle\big) \text{ for any } p\in Var; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \neg \varphi & \text{iff} & \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \not\models \varphi; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \varphi \lor \psi & \text{iff} & \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \varphi \\ & & \text{or } \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \psi; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \langle \text{E} \rangle \varphi & \text{iff} & \text{there is } h'' \in H \text{ such that } h' < h'',\\ & & \text{and } \mathfrak{M}, \langle (h', v) , (h'' , v' ) \rangle \models \varphi; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \langle \text{W} \rangle \varphi & \text{iff} & \text{there is } h'' \in H \text{ such that } h'' < h, \\ & & \text{and } \mathfrak{M}, \langle (h'', v) , (h , v' ) \rangle \models \varphi; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \langle \text{N} \rangle \varphi & \text{iff} & \text{there is } v'' \in V \text{ such that } v' < v'', \\ & & \text{and } \mathfrak{M}, \langle (h, v') , (h' , v'' ) \rangle \models \varphi; \\ \mathfrak{M}, \langle (h, v) , (h' , v' ) \rangle \models \langle \text{S} \rangle \varphi & \text{iff} & \text{there is } v'' \in V \text{ such that } v'' < v,\\ & & \text{and } \mathfrak{M}, \langle (h, v'') , (h' , v) \rangle \models \varphi. \\ \end{array} \] Application fields:

Spatial reasoning, interval temporal reasoning.

Comments and references:

SpPNL is introduced in (Morales et al. 2007). In the logic it is possible to express 25 out of 169 basic rectangle algebra relations, and 2 out of 8 region connection calculus relations. The satisfiability problem in SpPNL is shown to be undecidable (by reduction from the satisfability problem in compass logic which is known to be undecidable). A decidable version of SpPNL, the so-called weak spatial propositional neighborhood logic (WSpPNL), is introduced in (Bresolin et al. 2007).