zbMATH — the first resource for mathematics

Using theory interpretation to mechanise the reals in a theorem prover. (English) Zbl 0970.68146
Fidge, Colin (ed.), Computing: The Australasian Theory Symposium, CATS 2001. Proceedings of the 7th symposium, Bond Univ., Gold Coast, Australia, January 29-30, 2001. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 42, 16 p., electronic only (2001).
Summary: 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.
For the entire collection see [Zbl 0957.00045].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
theorem power
Ergo 6; Qu-Prolog
Full Text: Link