Email Gateway (Aug 19 2022 at 13:48): Email Gateway (Aug 19 2022 at 13:48):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
Email Gateway (Aug 19 2022 at 13:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Cool!
Florian
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC