DROPS

Document

DOI: 10.4230/OASIcs.TIME.2026.2

Core Fragments of Compass Logic

Authors: Pietro Casavecchia, Guido Sciavicco, and Leonardo Serrentino

Published in: OASIcs, Volume 146, 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)

Abstract

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.

Cite as

Pietro Casavecchia, Guido Sciavicco, and Leonardo Serrentino. Core Fragments of Compass Logic. In 33rd International Symposium on Temporal Representation and Reasoning (TIME 2026). Open Access Series in Informatics (OASIcs), Volume 146, pp. 2:1-2:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{casavecchia_et_al:OASIcs.TIME.2026.2,
  author =	{Casavecchia, Pietro and Sciavicco, Guido and Serrentino, Leonardo},
  title =	{{Core Fragments of Compass Logic}},
  booktitle =	{33rd International Symposium on Temporal Representation and Reasoning (TIME 2026)},
  pages =	{2:1--2:16},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-448-2},
  ISSN =	{2190-6807},
  year =	{2026},
  volume =	{146},
  editor =	{Orlandini, AndreA and Pinchinat, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.TIME.2026.2},
  URN =		{urn:nbn:de:0030-drops-276985},
  doi =		{10.4230/OASIcs.TIME.2026.2},
  annote =	{Keywords: spatial logic, bi-temporal logic, Horn fragment, core fragment, undecidability, decidability}
}

Document

DOI: 10.4230/LIPIcs.TIME.2025.4

Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic

Authors: Pietro Bellodi, Pietro Casavecchia, Alberto Paparella, Guido Sciavicco, and Ionel Eduard Stan

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract

The logical reasoning skills of Large Language Models (LLMs) is poorly understood and often overstated. Current evaluation suites rely on algebraic or commonsense puzzles that mix reasoning with symbolic manipulation and/or provide static datasets that quickly saturate or leak into pretraining corpora. In purely logical terms, the most relevant reasoning skill is the meta-mathematical task of valid formula recognition, which is at the foundation of higher-level reasoning tasks (including deduction and minimization of assertions, to name just a few). In the current landscape of LLMs benchmarking, puzzles are most often stated in propositional or first-order logic, with a few exceptions for point-based temporal logic, such as LTL; yet, in the real world, event-based temporal statements are prevalent, and they are more naturally expressed in interval-based temporal logic. Interval temporal logic offers a much richer (w.r.t. point-based temporal logic, for example) variety of problems, and not only do different languages present different expressive powers, but also the computational complexity of the validity problem can vary widely. In this paper, we tackle the problem of assessing the ability of LLMs to reason about interval-based statements in the form of validity recognition. We explore whether their accuracy is sensible to the underlying language, the computational complexity of the associated validity problem, and the intrinsic hardness of the problem in terms of formula length and modal depth of the problem. We benchmark several frontier LLMs (Gemma 3 27b It, Llama 4 Maverick, DeepSeek Chat V3 release 0324, Qwen 3 32b, and Qwen 3 235b) and show that, despite apparently impressive performance on algebraic or commonsense benchmarks, they falter on logically rigorous tasks.

Cite as

Pietro Bellodi, Pietro Casavecchia, Alberto Paparella, Guido Sciavicco, and Ionel Eduard Stan. Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 4:1-4:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bellodi_et_al:LIPIcs.TIME.2025.4,
  author =	{Bellodi, Pietro and Casavecchia, Pietro and Paparella, Alberto and Sciavicco, Guido and Stan, Ionel Eduard},
  title =	{{Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{4:1--4:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.4},
  URN =		{urn:nbn:de:0030-drops-244504},
  doi =		{10.4230/LIPIcs.TIME.2025.4},
  annote =	{Keywords: Large Language Models, Benchmarking, Interval Temporal Logic}
}

Search Results

Documents authored by Casavecchia, Pietro

Core Fragments of Compass Logic

Abstract

Cite as

Assessing the (In)Ability of LLMs to Reason in Interval Temporal Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message