Fulltext present in this item

Thumbnail
Fulltext: certextrr.pdf
Format: PDF
Title: Certified exact transcendental real number computation in Coq
Author(s): O'Connor, Russell
Publication year: 2008
In: 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, pp. 246-261
Publisher: New York : Springer
ISBN: 9783540710677
9783540710653
Publication type: Article in monograph or in proceedings

Please use this identifier to cite or link to this item : https://hdl.handle.net/2066/32281   https://hdl.handle.net/2066/32281

Display more details
Organization: Institute for Computing and Information Sciences
Book title: 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
Page start: p. 246
Page end: p. 261
Abstract:
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.
Languages used: en_US

This item appears in the following Collection(s)

Browse

Statistics