Generalized Qualitative Spatio-Temporal Reasoning: Complexity and Tableau Method

被引:0
作者
Sioutis, Michael [1 ]
Condotta, Jean-Francois [1 ]
Salhi, Yakoub [1 ]
Mazure, Bertrand [1 ]
机构
[1] Univ Lille Nord France, Artois, CNRS, CRIL,UMR 8188, Lens, France
来源
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015) | 2015年 / 9323卷
关键词
LOGICS;
D O I
10.1007/978-3-319-24312-2_5
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:54 / 69
页数:16
相关论文
共 20 条
[1]   MAINTAINING KNOWLEDGE ABOUT TEMPORAL INTERVALS [J].
ALLEN, JF .
COMMUNICATIONS OF THE ACM, 1983, 26 (11) :832-843
[2]  
[Anonymous], 1985, LOGIQUE ANAL
[3]  
Balbiani P, 2002, LECT NOTES ARTIF INT, V2309, P162
[4]   An automata-theoretic approach to constraint LTL [J].
Demri, Stephane ;
D'Souza, Deepak .
INFORMATION AND COMPUTATION, 2007, 205 (03) :380-415
[5]  
Frank A.U., OGAI
[6]  
Gabelaia D., 2003, FLAIRS
[7]   Systematic Semantic Tableaux for PLTL [J].
Gaintzarain, J. ;
Hermo, M. ;
Lucio, P. ;
Navarro, M. .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 206 (59-73) :59-73
[8]  
Guesgen H.W., 1989, Spatial reasoning based on Allen's temporal logic
[9]  
Huang J., 2012, KR
[10]  
Huth M., 2004, LOGIC COMPUTER SCI M