On Decidability and Expressiveness of Propositional Neighborhood Logics

Interval-based temporal logics are an important research area in computer science and artificial intelligence. In this paper we investigate decidability and expressiveness issues for Propositional Neighborhood Logics (PNLs). We begin by comparing the expressiveness of the different PNLs. Then, we focus on the most expressive one, namely, PNLπ+, and we show that it is decidable over various classes of linear orders by reducing its satisfiability problem to that of the two-variable fragment of first-order logic with binary relations over linearly ordered domains, due to Otto. Next, we prove that PNLπ+ is expressively complete with respect to such a fragment. We conclude the paper by comparing PNLπ+ expressiveness with that of other interval-based temporal logics. © Springer-Verlag Berlin Heidelberg 2007.