2026-10-10T21:17:36Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:27698 2026-10-10T19:48:19Z ddc:004 open_access

Core Fragments of Compass Logic Casavecchia, Pietro Sciavicco, Guido Serrentino, Leonardo spatial logic bi-temporal logic Horn fragment core fragment undecidability decidability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pietro Casavecchia and Guido Sciavicco and Leonardo Serrentino 2026 Is Part Of OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.TIME.2026.2 urn:nbn:de:0030-drops-276985 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.2 eng https://creativecommons.org/licenses/by/4.0/legalcode