[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
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.
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