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.
|Publication status||Published - 2001|