Certified Exact Transcendental Real Number Computation in Coq

Details Certified Exact Transcendental Real Number Computation in Coq Certified Exact Transcendental Real Number Computation in Coq

2008-05-16

arxiv.org/abs/0805.2438v1

Ait Mohamed, C. Munoz, and S. Tahar (Eds.): TPHOLs 2008, LNCS 5170, pp. 246-261, 2008

Computer Science

Logic in Computer Science

This paper is to be part of the proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TP

Scientific paper

10.1007/978-3-540-71067-7_21

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.

Affiliated with

Also associated with

No associations

Rating

Certified Exact Transcendental Real Number Computation in Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Certified Exact Transcendental Real Number Computation in Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Certified Exact Transcendental Real Number Computation in Coq will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-272354