A sequent calculus for signed interval logic

Thomas Marthedal Rasmussen

    Research output: Book/ReportReportResearchpeer-review

    304 Downloads (Pure)

    Abstract

    We propose and discuss a complete sequent calculus formulation for Signed Interval Logic (SIL) with the chief purpose of improving proof support for SIL in practice. The main theoretical result is a simple characterization of the limit between decidability and undecidability of quantifier-free SIL. We present a mechanization of SIL in the generic proof assistant Isabelle and consider techniques for automated reasoning. Many of the results and ideas of this report are also applicable to traditional (non-signed) interval logic and, hence, to Duration Calculus.
    Original languageEnglish
    Publication statusPublished - 2001

    Cite this