# [isabelle] AFP: Implementing field extensions of the form Q[sqrt(b)]

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] AFP: Implementing field extensions of the form Q[sqrt(b)]
*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>
*Date*: Tue, 11 Feb 2014 00:02:17 +0000
*Accept-language*: en-AU, en-US
*Thread-index*: AQHPJryG2BKLVZPVn0WWOshAeoDbFQ==
*Thread-topic*: Implementing field extensions of the form Q[sqrt(b)]

An new AFP entry is available:
Implementing field extensions of the form Q[sqrt(b)]
by René Thiemann
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.
[http://afp.sourceforge.net/entries/Real_Impl.shtml]
Cheers,
Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*