Automated complexity proofs for qualitative spatial and temporal calculi

Jochen Renz*, Jason Jingshi Li

*Corresponding author for this work

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    9 Citations (Scopus)


    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.

    Original languageEnglish
    Title of host publicationPrinciples of Knowledge Representation and Reasoning
    Subtitle of host publicationProceedings of the 11th International Conference, KR 2008
    PublisherInstitute of Electrical and Electronics Engineers Inc.
    Number of pages9
    ISBN (Print)9781577353843
    Publication statusPublished - 2008
    Event11th International Conference on Principles of Knowledge Representation and Reasoning, KR 2008 - Sydney, NSW, Australia
    Duration: 16 Sept 200819 Sept 2008

    Publication series

    NameProceedings of the International Conference on Knowledge Representation and Reasoning
    ISSN (Print)2334-1025
    ISSN (Electronic)2334-1033


    Conference11th International Conference on Principles of Knowledge Representation and Reasoning, KR 2008
    CitySydney, NSW


    Dive into the research topics of 'Automated complexity proofs for qualitative spatial and temporal calculi'. Together they form a unique fingerprint.

    Cite this