Interval logic. Proof theory and theorem proving  Thomas Marthedal Rasmussen
 Abstract  Realtime systems are computer systems which have to meet realtime constraints. To increase the confidence in such systems, formal methods and formal verification are utilized. The class of logics known as interval logics can be used for expressing properties and requirements of realtime systems. By theorem proving we understand the activity of
proving theorems of a logic with the assistance of a computer.
The goal of this thesis is to improve theorem proving support for interval logics such that larger and more realistic casestudies of realtime systems can be conducted using these formalisms. For achieving this goal we (1) investigate the foundations necessary for providing a useful theorem proving system for interval logics, and (2) actually provide such a system as well as conduct experiments with it.
We introduce an interval logic, Signed Interval Logic (SIL), which includes the notion of a direction of an interval, and present a sound and complete Hilbert proof system for it. Because of its generality, SIL can conveniently act as a general formalism in which other interval logics can be encoded.
We develop proof theory for SIL including both a sequent calculus system and a labelled natural deduction system. We conduct theoretical investigations of the systems with respect to subformula properties, proof search, etc.
The generic theorem proving system Isabelle is used as a framework for encoding both proof theoretical systems. We consider a number of examples/small casestudies and discuss strengths and weaknesses of the encodings.
From both a theoretical and a practical viewpoint, the labelled natural deduction system is the clear winner. We discuss how to scale the approach to larger casestudies.  Keywords  realtime systems, interval logic, Duration Calculus, proof theory,
automated reasoning, theorem proving, Isabelle  Type  Ph.D. thesis [Academic thesis]  Year  2002  Publisher  Informatics and Mathematical Modelling, Technical University of Denmark, DTU  Address  Richard Petersens Plads, Building 321, DK2800 Kgs. Lyngby  Series  IMMPHD200297  Electronic version(s)  [pdf]  BibTeX data  [bibtex]  IMM Group(s)  Computer Science & Engineering 
Back :: IMM Publications
