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



> 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
Description: OpenPGP digital signature



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