Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Topological Logics with Connectedness over Euclidean Spaces

Roman Kontchakov, Yavor Nenov, Ian Pratt-Hartmann, Michael Zakharyaschev

TL;DR

This work characterizes the computational landscape of topological logics with connectedness over Euclidean spaces, contrasting regular closed sets with polyhedral regions. By constructing formulas that force infinitely many components and reducing the Post correspondence problem, it proves undecidability for Bc, Cc and their variants in polyhedral and planar contexts, while pinpointing exact complexities for Bc^∘: NP-complete over regular closed sets in dimensions at least 3 and ExpTime-complete over polyhedra. The results illuminate a sharp complexity jump between Euclidean spaces and more general topological spaces, and reveal a precise boundary in 3D versus higher dimensions for these qualitative spatial logics. Overall, the paper significantly advances understanding of how dimensionality and region tameness affect decidability and complexity in qualitative spatial reasoning frameworks.

Abstract

We consider the quantifier-free languages, Bc and Bc0, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of n-dimensional Euclidean space (n greater than 1) and, additionally, over the regular closed polyhedral sets of n-dimensional Euclidean space. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric "Qualitative Spatial Reasoning." We prove that the satisfiability problem for Bc is undecidable over the regular closed polyhedra in all dimensions greater than 1, and that the satisfiability problem for both languages is undecidable over both the regular closed sets and the regular closed polyhedra in the Euclidean plane. However, we also prove that the satisfiability problem for Bc0 is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed polyhedra is ExpTime-complete. Our results show, in particular, that spatial reasoning over Euclidean spaces is much harder than reasoning over arbitrary topological spaces.

Topological Logics with Connectedness over Euclidean Spaces

TL;DR

This work characterizes the computational landscape of topological logics with connectedness over Euclidean spaces, contrasting regular closed sets with polyhedral regions. By constructing formulas that force infinitely many components and reducing the Post correspondence problem, it proves undecidability for Bc, Cc and their variants in polyhedral and planar contexts, while pinpointing exact complexities for Bc^∘: NP-complete over regular closed sets in dimensions at least 3 and ExpTime-complete over polyhedra. The results illuminate a sharp complexity jump between Euclidean spaces and more general topological spaces, and reveal a precise boundary in 3D versus higher dimensions for these qualitative spatial logics. Overall, the paper significantly advances understanding of how dimensionality and region tameness affect decidability and complexity in qualitative spatial reasoning frameworks.

Abstract

We consider the quantifier-free languages, Bc and Bc0, obtained by augmenting the signature of Boolean algebras with a unary predicate representing, respectively, the property of being connected, and the property of having a connected interior. These languages are interpreted over the regular closed sets of n-dimensional Euclidean space (n greater than 1) and, additionally, over the regular closed polyhedral sets of n-dimensional Euclidean space. The resulting logics are examples of formalisms that have recently been proposed in the Artificial Intelligence literature under the rubric "Qualitative Spatial Reasoning." We prove that the satisfiability problem for Bc is undecidable over the regular closed polyhedra in all dimensions greater than 1, and that the satisfiability problem for both languages is undecidable over both the regular closed sets and the regular closed polyhedra in the Euclidean plane. However, we also prove that the satisfiability problem for Bc0 is NP-complete over the regular closed sets in all dimensions greater than 2, while the corresponding problem for the regular closed polyhedra is ExpTime-complete. Our results show, in particular, that spatial reasoning over Euclidean spaces is much harder than reasoning over arbitrary topological spaces.

Paper Structure

This paper contains 17 sections, 25 theorems, 86 equations, 36 figures.

Table of Contents

  1. Introduction
  2. Spatial logic
  3. Algebraic and modal logic
  4. Spatial logics with connectedness
  5. Plan of the paper and summary of results
  6. Preliminaries
  7. Basic topological notions
  8. Frames
  9. Topological logics
  10. Graphs
  11. Post correspondence problem
  12. Forcing infinitely many components in locally connected unicoherent spaces.
  13. Undecidability: the polyhedral case
  14. Undecidability: the plane case
  15. Forcing infinitely many components with $\mathcal{B}{c}^\circ$
  16. ...and 2 more sections

Key Result

Lemma 1

Let $X$ be a regular closed subset of a topological space $T$ and $S$ a component of $-X$. If $-X$ has finitely many components, then $\delta S \subseteq X$. Alternatively, if $T$ is locally connected, then $\delta S \subseteq X$.

Figures (36)

  • Figure 1: $\mathcal{RCC}8$-relations over discs in $\mathbb{R}^2$.
  • Figure 2: Three regions in ${\sf RC}(\mathbb{R}^2)$ satisfying \ref{['eq:wiggly']}.
  • Figure 3: Regions satisfying $\varphi_\infty$.
  • Figure 4: Sequences $X_0,X_1,\dots$ of components $X_i$ of $r_{{\lfloor i\rfloor_{}}}$ and $V_0,V_1,\dots$ of open sets $V_i$ connecting $X_i$ to $X_{i+1}$ with the 'holes' $S_{i+1}$ and $R_{i+1}$ of $X_{i+1}$ containing $X_{i}$ and $X_{i+2}$, respectively.
  • Figure 5: Region $s$ lying inside $\sum_{j = 0}^3 r_j'$ and connecting the components of each $r_i'$ .
  • ...and 31 more figures

Theorems & Definitions (44)

  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • Lemma 4
  • proof
  • Theorem 5
  • proof
  • Corollary 6
  • ...and 34 more