Computing with Classical Real Numbers

Details Computing with Classical Real Numbers Computing with Classical Real Numbers

2008-09-09

arxiv.org/abs/0809.1644v1

Journal of Formalized Reasoning, 2(1):27-39, 2009

Computer Science

Logic in Computer Science

Scientific paper

There are two incompatible Coq libraries that have a theory of the real numbers; the Coq standard library gives an axiomatic treatment of classical real numbers, while the CoRN library from Nijmegen defines constructively valid real numbers. Unfortunately, this means results about one structure cannot easily be used in the other structure. We present a way interfacing these two libraries by showing that their real number structures are isomorphic assuming the classical axioms already present in the standard library reals. This allows us to use O'Connor's decision procedure for solving ground inequalities present in CoRN to solve inequalities about the reals from the Coq standard library, and it allows theorems from the Coq standard library to apply to problem about the CoRN reals.

Affiliated with

Also associated with

No associations

Rating

Computing with Classical Real Numbers 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 Computing with Classical Real Numbers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Computing with Classical Real Numbers will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-211435