Abstract
We study the spatiotemporal logic that results by combining the propositional temporal logic (PTL) with a qualitative spatial constraint language, namely, the L1 logic, and present a first semantic tableau method that given a L1 formula φ systematically searches for a model for φ. 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 L1, 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 L1.
Cite
CITATION STYLE
Sioutis, M., Condotta, J. F., Salhi, Y., & Mazure, B. (2015). Generalized qualitative spatio-temporal reasoning: Complexity and tableau method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9323, pp. 54–69). Springer Verlag. https://doi.org/10.1007/978-3-319-24312-2_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
