Certified exact transcendental real number computation in Coq

Files in This Item:

File	Description	Size	Format
		200.01 kB	Adobe PDF	View/Open

Title:	Certified exact transcendental real number computation in Coq
Author(s):	O'Connor, Russell (275907317)
Publication year:	2008
Document type:	Article in monograph or in proceedings
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
ISBN:	9783540710677 3540710655 9783540710653
Start page:	p. 246
End page:	p. 261
Series:	Lecture Notes in Computer Science ; 5170. SL 1, Theoretical Computer Science and General Issues
Publisher:	New York : Springer
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.
Organization:	Institute for Computing and Information Sciences
Appears in Collections:	Electronic documents Radboud University

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