Automated Proof Support for Interval Logics

Thomas Marthedal Rasmussen

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    We outline the background and motivation for the use of interval logics and consider some initial attempts toward proof support and automation. The main focus, though, is on recent work on these subjects. We compare different proof theoretical formalisms, in particular a "classical" versus a "labelled" one. We discuss encodings of these in the generic proof assistant Isabelle and consider some examples which show that in some cases the labelled formalism gives an order of magnitude improvement in proof length compared to a classical approach.
    Original languageEnglish
    Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
    Volume2250
    PublisherSpringer Verlag
    Publication date2001
    Pages320-329
    ISBN (Print)978-354042957-9
    DOIs
    Publication statusPublished - 2001
    Event8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Havana, Cuba
    Duration: 3 Dec 20017 Dec 2001
    Conference number: 8

    Conference

    Conference8th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
    Number8
    Country/TerritoryCuba
    CityHavana
    Period03/12/200107/12/2001

    Fingerprint

    Dive into the research topics of 'Automated Proof Support for Interval Logics'. Together they form a unique fingerprint.

    Cite this