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, that supports a variety of algebraic tools. They allow us to formalise the proof from an algebraic point of view. © 2013 Springer Science+Business Media Dordrecht.
CITATION STYLE
Zsidó, J. (2014). Theorem of three circles in coq. Journal of Automated Reasoning, 53(2), 105–127. https://doi.org/10.1007/s10817-013-9299-0
Mendeley helps you to discover research relevant for your work.