Interval logic. Proof theory and theorem proving

摘要

Real-time systems are computer systems which have to meet real-time 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 real-time 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 case-studies of real-time 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 case-studies 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 case-studies.