A Decidable Logic for Time Intervals: Propositional Neighborhood Logic

Contents

Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of artificial intelligence and computer science. Unfortunately, most time interval logics proposed in the literature are (highly) undecidable. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power. In this paper, we focus our attention on the propositional fragment of Neighborhood Logic (PNL for short). We show that PNL is expressive enough to capture meaningful timing properties and that it is decidable. Decidability is proved by developing an original tableau decision method for PNL. We conclude the paper by pointing out interesting relationships between PNL and compass logics for spatial reasoning.