*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] AFP: Implementing field extensions of the form Q[sqrt(b)]*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 12 Feb 2014 19:39:04 +0100*In-reply-to*: <72083C9E-0578-42D7-A145-04A92EFE2B5B@nicta.com.au>*Organization*: TU Munich*References*: <72083C9E-0578-42D7-A145-04A92EFE2B5B@nicta.com.au>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

> 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] Cool! Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] AFP: Implementing field extensions of the form Q[sqrt(b)]***From:*Gerwin Klein

- Previous by Date: [isabelle] Prelim lifting & coercion done: Want a type of non-negatives for a field, to work like nat/int
- Next by Date: Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Previous by Thread: [isabelle] AFP: Implementing field extensions of the form Q[sqrt(b)]
- Next by Thread: [isabelle] ACL2'14: Call for papers
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list