Certified exact transcendental real number computation in Coq
New York : Springer
InOtmane Ait Mohamed, César Muñoz, Sofiène Tahar (ed.) Theorem proving in higher order logic : 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008 : proceedings, pp. 246-261
Article in monograph or in proceedings
Display more detailsDisplay less details
Institute for Computing and Information Sciences
Otmane Ait Mohamed, César Muñoz, Sofiène Tahar (ed.) Theorem proving in higher order logic : 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008 : proceedings
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete metric spaces in the Coq proof assistant and used this library to build a constructive real number implementation including elementary real number functions and proofs of correctness. Using this library, I have created a tactic that automatically proves strict inequalities over closed elementary real number expressions by computation.
Upload full text
Use your RU credentials (u/z-number and password) tolog in with SURFconextto upload a file for processing by the repository team.