Implementing field extensions of the form Q[sqrt(b)]

René Thiemann 🌐

February 6, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


GNU Lesser General Public License (LGPL)


July 11, 2014
Moved NthRoot_Impl to Sqrt-Babylonian.


Session Real_Impl