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

René Thiemann 📧

February 6, 2014

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.

GNU Lesser General Public License (LGPL)

Change history

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

Topics

Theories of Real_Impl