Skip to Main content Skip to Navigation
Journal articles

Theorem of three circles in Coq

Julianna Zsidó 1, *
* Corresponding author
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certain area of the complex plane delimited by straight lines. After applying a transformation involving inversion this area is mapped to an area delimited by circles. We provide a formalisation of this rather geometric proof in Ssreflect, an extension of the proof assistant Coq, providing versatile algebraic tools. They allow us to formalise the proof from an algebraic point of view.
Document type :
Journal articles
Complete list of metadata
Contributor : Julianna Zsido Connect in order to contact the contributor
Submitted on : Monday, September 23, 2013 - 12:58:39 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM

Links full text




Julianna Zsidó. Theorem of three circles in Coq. Journal of Automated Reasoning, Springer Verlag, 2013, ⟨10.1007/s10817-013-9299-0⟩. ⟨hal-00864827⟩



Record views