A sequent calculus for signed interval logic |
Thomas Marthedal Rasmussen
|
| 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. |
| Type | Technical report |
| Year | 2001 |
| Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU |
| Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby |
| Series | IMM-TR-2001-6 |
| Electronic version(s) | [pdf] |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |