Theorem of three circles in coq

1Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

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, 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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free