Paper Info
Title
Certified Exact Transcendental Real Number Computation in Coq
Abstract
Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exactreal 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.
Year
DOI
Venue
2008
10.1007/978-3-540-71067-7_21
TPHOLs '08 Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics
Keywords
DocType
Volume
theorem proving,elementary real number function,constructive real number implementation,number computation,real number expression,certified exact transcendental real,strict inequality,closed elementary real number,coq proof assistant,exactreal number computation,complete metric space,proof assistant,numerical analysis
Conference
abs/0805.2438
ISSN
Citations 
PageRank 
Ait Mohamed, C. Munoz, and S. Tahar (Eds.): TPHOLs 2008, LNCS 5170, pp. 246-261, 2008
24
1.41
References 
Authors
12
1
Name
Order
Citations
PageRank
Russell O'Connor115411.75