Automated Complexity Proofs for Qualitative Spatial and Temporal Calculi

Jochen Renz, Jason Jingshi Li

Identifying complexity results for qualitative spatial or temporal calculi has been an important research topic in the past 15 years. Most interesting calculi have been shown to be at least NP-complete, but if tractable fragments of the calculi can be found then efficient reasoning with these calculi is possible. In order to get the most efficient reasoning algorithms, we are interested in identifying maximal tractable fragments of a calculus (tractable fragments such that any extension of the fragment leads to NP-hardness). All required complexity proofs are usually made manually, sometimes using computer assisted enumerations. In a recent paper by Renz (2007), a procedure was presented that automatically identifies tractable fragments of a calculus. In this paper we present an efficient procedure for automatically generating NP-hardness proofs. In order to prove correctness of our procedure, we develop a novel proof method that can be checked automatically and that can be applied to arbitrary spatial and temporal calculi. Up to now, this was believed to be impossible. By combining the two procedures, it is now possible to identify maximal tractable fragments of qualitative spatial and temporal calculi fully automatically.

Subjects: 3.2 Geometric Or Spatial Reasoning; 3.6 Temporal Reasoning

Submitted: Jun 17, 2008


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.