Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method

We study the spatiotemporal logic that results by combining the propositional temporal logic (PTL) with a qualitative spatial constraint language, namely, the L-1 logic, and present a first semantic tableau method that given a L-1 formula phi systematically searches for a model for phi. Our approach builds on Wolper's tableau method for PTL, while the ideas provided can be carried to other tableau methods for PTL as well. Further, we investigate the implication of the constraint properties of compactness and patchwork in spatiotemporal reasoning. We use these properties to strengthen results regarding the complexity of the satisfiability problem in L-1, by replacing the stricter global consistency property used in literature and generalizing to more qualitative spatial constraint languages. Finally, the obtained strengthened results allow us to prove the correctness of our tableau method for L-1.