FORMAL PROOFS IN REAL ALGEBRAIC GEOMETRY: FROM ORDERED FIELDS TO QUANTIFIER ELIMINATION
FORMAL PROOFS IN REAL ALGEBRAIC GEOMETRY: FROM ORDERED FIELDS TO QUANTIFIER ELIMINATION
复制标题
DOI：
10.2168/lmcs-8(1:02)2012
复制
发表时间：
2012-01-01
影响因子：
0.6
通讯作者：
Mahboubi, Assia
中科院分区：
文献类型：
--
作者：
Cohen, Cyril;Mahboubi, Assia
本文描述了 COQ 证明助手中离散实闭域的形式化。这种抽象结构捕获了例如实代数数理论，即具有良好算法特性的实数的可判定子集。实代数数理论和更一般的半代数簇理论是实数分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，我们按照该主题的标准计算机代数文献描述了基于伪余数序列的量词消除的代数证明的形式化。这种形式化涵盖了大部分理论，这些理论是计算机代数实践中实现的高效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。
This paper describes a formalization of discrete real closed fields in the COQ proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number of effective methods in real analysis, including decision procedures for non linear arithmetic or optimization methods for real valued functions. After defining an abstract structure of discrete real closed field and the elementary theory of real roots of polynomials, we describe the formalization of an algebraic proof of quantifier elimination based on pseudo-remainder sequences following the standard computer algebra literature on the topic. This formalization covers a large part of the theory which underlies the efficient algorithms implemented in practice in computer algebra. The success of this work paves the way for formal certification of these efficient methods.