@TECHREPORT\{IMM2001-0836,
    author       = "T. M. Rasmussen",
    title        = "A sequent calculus for signed interval logic",
    year         = "2001",
    number       = "",
    series       = "IMM-TR-2001-6",
    institution  = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/836-full.html",
    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."
}