Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Formalization of a sign determination algorithm in real algebraic geometry

Cyril Cohen 1 
1 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : One of the problems in real algebraic geometry is root counting. Given a polynomial, we want to count the number of roots that satisfies constraints expressed as polynomial inequalities, this is done through a process called "sign determination". A naive way is to compute an exponential number of time consuming quantities, called Tarski Queries. In this paper, we formalize the construction of the adapted matrix part of the "better sign determination" algorithm from "Algorithms in Real Algebraic Geometry" (Basu, Pollack, Roy). We prove in Coq that the matrix has the properties expected from the book: small size but still invertible.
Complete list of metadata
Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Tuesday, June 29, 2021 - 4:22:17 PM
Last modification on : Friday, February 4, 2022 - 3:12:33 AM
Long-term archiving on: : Thursday, September 30, 2021 - 7:16:19 PM


Files produced by the author(s)


  • HAL Id : hal-03274013, version 1



Cyril Cohen. Formalization of a sign determination algorithm in real algebraic geometry. 2021. ⟨hal-03274013⟩



Record views


Files downloads