Projects per year
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.
Original language  English 

Publication status  Published  Aug 2002 

Keywords
 theorem proving
 Duration Calculus
 automated reasoning
 Isabelle
 realtime systems
 proof theory
 interval logic
Fingerprint Dive into the research topics of 'Interval logic. Proof theory and theorem proving'. Together they form a unique fingerprint.
Projects
 1 Finished

Formelle notationer til specifikation og verification af indlejrede, tidstro systemer
Rasmussen, T. M., Hansen, M. R., Rischel, H., Løvengreen, H. H., Guldstrand Larsen, K. & Nipkow, T.
01/02/1999 → 23/08/2002
Project: PhD