Presburger Modal Logic Is PSPACE-Complete

We introduce a Presburger modal logic PML with regularity constraints and full Presburger constraints on the number of children that generalize graded modalities, also known as number restrictions in description logics. We show that PML satisfiability is only pspacecomplete by designing a Ladner-like algorithm. This extends a wellknown and non-trivial pspace upper bound for graded modal logic. Furthermore, we provide a detailed comparison with logics that contain Presburger constraints and that are dedicated to query XML documents. As an application, we show that satisfiability for Sheaves Logic SL is pspace-complete, improving significantly its best known upper bound.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Stéphane Demri, Denis Lugiez
• Keywords: CADE 2006, Logical Reasoning, Modal Logic, Modal Logic Pml, Presburger Constraints