Abstract: |
We apply data refinement to implement the real numbers, where we support all
numbers in the field extension Q[sqrt(b)], i.e., all numbers of the form p +
q * sqrt(b) for rational numbers p and q and some fixed natural number b. To
this end, we also developed algorithms to precisely compute roots of a
rational number, and to perform a factorization of natural numbers which
eliminates duplicate prime factors.
Our results have been used to certify termination proofs which involve
polynomial interpretations over the reals.
|
BibTeX: |
@article{Real_Impl-AFP,
author = {René Thiemann},
title = {Implementing field extensions of the form Q[sqrt(b)]},
journal = {Archive of Formal Proofs},
month = feb,
year = 2014,
note = {\url{http://isa-afp.org/entries/Real_Impl.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|