Assia Mahboubi ; Cyril Cohen - Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

lmcs:844 - Logical Methods in Computer Science, February 16, 2012, Volume 8, Issue 1 -
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

Authors: Assia Mahboubi ; Cyril Cohen

    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.

    Volume: Volume 8, Issue 1
    Published on: February 16, 2012
    Accepted on: June 25, 2015
    Submitted on: May 16, 2011
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Fundings :
      Source : OpenAIRE Research Graph
    • Formalisation of Mathematics; Funder: European Commission; Code: 243847

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2102.03003
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.itp.2021.14
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2102.03003
    • 10.4230/lipics.itp.2021.14
    • 10.48550/arxiv.2102.03003
    • 2102.03003
    A Verified Decision Procedure for Univariate Real Arithmetic with the BKR Algorithm
    Cordwell, Katherine ; Tan, Yong Kiam ; Platzer, André ;

    13 Documents citing this article


    Consultation statistics

    This page has been seen 471 times.
    This article's PDF has been downloaded 416 times.