Deciding Monodic Fragments by Temporal Resolution

U Hustadt, B Konev, R A Schmidt

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


    In this paper we study the decidability of various fragments of monodic first-order temporal logic by temporal resolution. We focus on two resolution calculi, namely, monodic temporal resolution and fine-grained temporal resolution. For the first, we state a very general decidability result, which is independent of the particular decision procedure used to decide the first-order part of the logic. For the second, we introduce refinements using orderings and selection functions. This allows us to transfer existing results on decidability by resolution for first-order fragments to monodic first-order temporal logic and obtain new decision procedures. The latter is of immediate practical value, due to the availability of TeMP, an implementation of fine-grained temporal resolution.
    Original languageEnglish
    Title of host publicationProceedings of the 20th International Conference on Automated Deduction (CADE-20)
    EditorsR Nieuwenhuis
    PublisherSpringer Nature
    Number of pages15
    Publication statusPublished - 2005
    EventProceedings of the 20th International Conference on Automated Deduction (CADE-20) -
    Duration: 1 Jan 1824 → …

    Publication series

    NameLecture Notes in Artificial Intelligence
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceProceedings of the 20th International Conference on Automated Deduction (CADE-20)
    Period1/01/24 → …


    Dive into the research topics of 'Deciding Monodic Fragments by Temporal Resolution'. Together they form a unique fingerprint.

    Cite this