Truth & Proof

Abstract

This chapter augments the dynamic axioms for dynamical systems from the previous chapter with the full mathematical rigor of a proof system. This proof system enables rigorous, systematic proofs for cyber-physical systems by providing systematic structuring mechanisms for their correctness arguments. The most important goals of such a proof system are that it guarantees to cover all cases of a correctness argument, so all possible behavior of a CPS, and that it provides guidance on which proof rules to apply. Its most important feature is the ability to use the dynamic axioms for dynamical systems that we already identified for rigorous reasoning about hybrid programs. A high-level interface of proofs with reasoning for real arithmetic as well as techniques for logically simplifying real-arithmetic questions are discussed as well.