Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.

Leonardo Mendonça de Moura, Grant Olney Passmore

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationAutomated Deduction – CADE-24
Subtitle of host publication24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings
EditorsMaria Paola Bonacina
PublisherSpringer Japan
Number of pages15
ISBN (Electronic)978-3-642-38574-2
ISBN (Print)978-3-642-38573-5
Publication statusPublished - 2013

Publication series

NameLecture Notes in Computer Science


  • dblp


Dive into the research topics of 'Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.'. Together they form a unique fingerprint.

Cite this