Projects per year
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.
|Title of host publication||Automated Deduction – CADE-24|
|Subtitle of host publication||24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings|
|Editors||Maria Paola Bonacina|
|Number of pages||15|
|Publication status||Published - 2013|
|Name||Lecture Notes in Computer Science|
FingerprintDive into the research topics of 'Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.'. Together they form a unique fingerprint.
- 1 Finished
1/11/10 → 28/02/15