Using Theory Interpretation to Mechanise the Reals in a Theorem Prover
Jamie Barry Nathan. Shield, Ian J. Hayes, D. A. Carrington · Electronic Notes in Theoretical Computer Science · 2001
The mechanisation of the real numbers within theorem provers is of practical benefit for the verification of real-time systems. The real numbers provide a foundation within the theorem prover for classical mathematical analysis such as differentiation and integration. The approach we have taken makes extensive use of the theory interpretation facilities of the interactive theorem prover Ergo to maximise theory reuse and hence minimise theorem redundancy. The theory developed is compared with Harrison's HOL version.