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

Leonardo Mendonça de Moura; Grant Olney Passmore

doi:10.1007/978-3-642-38574-2_12

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 proceeding › Conference contribution

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.

Original language	English
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
Publisher	Springer
Pages	178-192
Number of pages	15
Volume	7898
ISBN (Electronic)	978-3-642-38574-2
ISBN (Print)	978-3-642-38573-5
DOIs	https://doi.org/10.1007/978-3-642-38574-2_12
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Keywords / Materials (for Non-textual outputs)

dblp

Access to Document

10.1007/978-3-642-38574-2_12

Moura and Passmore 2013 Computation in real closed infinitesimalAccepted author manuscript, 340 KB

http://dblp.uni-trier.de/db/conf/cade/cade2013.html#MouraP13

Automatic proof procedures for polynomials and special functions
Jackson, P. (Principal Investigator)
EPSRC
1/11/10 → 28/02/15
Project: Research

Cite this

de Moura, L. M., & Passmore, G. O. (2013). Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In M. P. Bonacina (Ed.), Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings (Vol. 7898, pp. 178-192). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/978-3-642-38574-2_12

de Moura, Leonardo Mendonça ; Passmore, Grant Olney. / Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. editor / Maria Paola Bonacina. Vol. 7898 Springer, 2013. pp. 178-192 (Lecture Notes in Computer Science).

@inproceedings{6875c2b6d53a4ec7b353550d902756d0,

title = "Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals.",

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{\textquoteright}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.",

keywords = "dblp",

author = "\{de Moura\}, \{Leonardo Mendon{\c c}a\} and Passmore, \{Grant Olney\}",

year = "2013",

doi = "10.1007/978-3-642-38574-2\_12",

language = "English",

isbn = "978-3-642-38573-5",

volume = "7898",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "178--192",

editor = "Bonacina, \{Maria Paola\}",

booktitle = "Automated Deduction – CADE-24",

address = "United Kingdom",

}

de Moura, LM & Passmore, GO 2013, Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. in MP Bonacina (ed.), Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. vol. 7898, Lecture Notes in Computer Science, Springer, pp. 178-192. https://doi.org/10.1007/978-3-642-38574-2_12

Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. / de Moura, Leonardo Mendonça; Passmore, Grant Olney.
Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. ed. / Maria Paola Bonacina. Vol. 7898 Springer, 2013. p. 178-192 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - de Moura, Leonardo Mendonça

AU - Passmore, Grant Olney

PY - 2013

Y1 - 2013

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

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

KW - dblp

U2 - 10.1007/978-3-642-38574-2_12

DO - 10.1007/978-3-642-38574-2_12

M3 - Conference contribution

SN - 978-3-642-38573-5

VL - 7898

T3 - Lecture Notes in Computer Science

SP - 178

EP - 192

BT - Automated Deduction – CADE-24

A2 - Bonacina, Maria Paola

PB - Springer

ER -

de Moura LM, Passmore GO. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In Bonacina MP, editor, Automated Deduction – CADE-24: 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings. Vol. 7898. Springer. 2013. p. 178-192. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-38574-2_12

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

Abstract

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Automatic proof procedures for polynomials and special functions

Cite this