Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings
Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings
复制标题
自动演绎 - CADE-24 - 第 24 届国际自动演绎会议，美国纽约州普莱西德湖，2013 年 6 月 9 日至 14 日。会议记录
DOI：
10.1007/978-3-642-38574-2_12
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
De Moura L
中科院分区：
文献类型：
--
作者：
De Moura L
非线性真实的算术（真实的闭域理论，或RCF）的决策过程的最新应用已经提出了不仅需要用多项式，而且需要用超越常数和无穷小量进行推理。在充分的一般性，这种推理的代数设置包括ofreal封闭超越和无穷小扩展的有理数。我们提出了一个库计算这些扩展。这个库包含许多贡献，包括一个新的组合Thom的引理和区间算术表示根，并提供了所有的核心机械需要建立RCF决策过程。我们描述了抽象的代数设置计算等领域的扩展，提出了我们的具体算法和优化，并说明了库上的一系列例子。
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 ofreal 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.