Machine-Checking the Timed Interval Calculus
Jeremy E. Dawson3 
and Rajeev Goré3
| (3) |
Department of Computer Science and Automated Reasoning Group, Australian National University, 0200 Canberra, ACT, Australia |
Abstract
We describe how we used the interactive theorem prover Isabelle to formalise and check the laws of the Timed Interval Calculus
(TIC). We also describe some important corrections to, clarifications of, and flaws in these laws, found as a result of our
work.
Keywords Reasoning about time - automated reasoning - theorem proving
Supported by an Australian Research Council Large Grant
Supported by an Australian Research Council QEII Fellowship
References secured to subscribers.