 |
    |
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
Leonardo de Moura1 and Grant Olney Passmore2
1Microsoft Research, Redmond, USA
leonardo@microsoft.com
2LFCS, Edinburgh and Clare Hall, Cambridge, UK
grant.passmore@cl.cam.ac.uk
Abstract. Recent applications of decision procedures for nonlinear real arithmetic (the theory of real closed fields, or RCF) have presented a need for reasoning not only with polynomials but also with transcendental constants and infinitesimals. In full generality, the algebraic setting for this reasoning consists of real closed transcendental and infinitesimal extensions of the rational numbers. We present a library for computing over these extensions. This library contains many contributions, including a novel combination of Thom’s Lemma and interval arithmetic for representing roots, and provides all core machinery required for building RCF decision procedures. We describe the abstract algebraic setting for computing with such field extensions, present our concrete algorithms and optimizations, and illustrate the library on a collection of examples.
LNAI 7898, p. 178 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013