TY - GEN

T1 - Automated complexity proofs for qualitative spatial and temporal calculi

AU - Renz, Jochen

AU - Li, Jason Jingshi

PY - 2008

Y1 - 2008

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=77958595034&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9781577353843

T3 - Proceedings of the International Conference on Knowledge Representation and Reasoning

SP - 715

EP - 723

BT - Principles of Knowledge Representation and Reasoning

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 11th International Conference on Principles of Knowledge Representation and Reasoning, KR 2008

Y2 - 16 September 2008 through 19 September 2008

ER -