Soeren T. Heilmann, 
Proof Support for Duration Calculus, 
Department of Information Technology, Technical University of Denmark, 
PhD-thesis, 
January 1999.

Abstract

We develop a theorem prover, Isabelle/DC, for the real-time logic
Duration Calculus based on the generic proof tool Isabelle. Our
starting point is a definition of classical Duration Calculus logic in
the Hilbert style. We develop a sequent style version of DC and
document its properties in relation to the Hilbert style version.

With a view towards applications we generalize classical DC and
introduce typed states in the style of Ravn and the extra operators of
Extended DC for expressing properties of continuous states.

PC/DC is an existing theorem prover for DC developed by Skakkebaek
and based on PVS, a proof tool for higher order logic. We have worked
with PC/DC to verify a specification of the Steam Boiler by Rischel et
al.  We document the experiences of this work and conclude that there
is a need for more powerful proof commands than found in PC/DC.
Furthermore our work on supporting and further developing PC/DC has
lead us to look for a alternative platform for a DC theorem prover.

Isabelle is the alternative platform we choose for implementation of
our proof tool. We document the basic logic of Isabelle and the
features it provides for extension. This gives us a basis for
presenting the encoding of the sequent style DC developed previously.

We document our work on providing proof support for DC in the new
tool. This is a collection of derived rules and lemmas which have
proved themselves useful. We also make use of the proof programming
facilities of Isabelle and document tactics and tacticals we have
developed for proof search and high level proof steps.

We revisit the Steam Boiler case study. This time equipped with a
proof tool that we can extend easily to provide proof support suitable
for this example and hopefully also generally. We document the
encoding of the Boiler specification and the tactics we develop.
Having two version of the same proofs done with different tools we
compare them and find that Isabelle/DC provide improved proof support
over PC/DC.