Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. (English) Zbl 1241.68096

Cohen, Cyril; Mahboubi, Assia

Log. Methods Comput. Sci. 8, No. 1, Paper No. 2, 40 p. (2012).

Summary: 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 nonlinear 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.

MSC:

68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
03C10	Quantifier elimination, model completeness, and related topics
12J15	Ordered fields
14P99	Real algebraic and real-analytic geometry
68W30	Symbolic computation and algebraic computation

Keywords:

formal proofs; Coq; quantifier elimination; small scale reflection; real algebraic geometry; real closed fields

Software:

CoqMT; QEPCAD; Coq/SSReflect; Coq