Search Results

Compass Logic is arguably the most intuitive modal spatial logic designed for a point-based ontology, featuring exactly one unary modal operator for each cardinal direction, and interpreted over bi-dimensional structures; it can also be seen as a very natural bi-temporal logic, allowing independent reasoning in terms of future and past in two orthogonal temporal dimensions. As such, Compass Logic finds applications in several areas of modern artificial intelligence, from spatial reasoning to temporal databases. Its introduction is due to Marx and Reynolds in 1999 (inspired by previous work of Venema, 1990), when the authors proved that its satisfiability problem is undecidable regardless of the properties of the underlying structure. More recently, the idea of exploring sub-propositional fragments of unary modal logic emerged, and was applied to point-based and interval-based temporal logic. In the same spirit, in this paper we explore sub-propositional fragments of Compass Logic in the finite/discrete case, and we prove that while its satisfiability problem remains undecidable in very weak conditions, such as for the core fragment, characterized by having only formulas that are conjunctions of binary Horn clauses, it becomes surprisingly decidable for the same core fragment devoid of existential quantifiers.