Implementing Field Extensions of the Form Q[sqrt(b)]

René Thiemann

6 February 2014


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)

Change history

[2014-07-11] Moved NthRoot_Impl to Sqrt-Babylonian.

Depends On

Used by


Related Entries