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

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.

Domaines: Géométrie algorithmique [cs.CG]; Géométrie algébrique [math.AG]; Logique en informatique [cs.LO]

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