Theorem of three circles in Coq

DOI10.1007/s10817-013-9299-0zbMath1314.68289arXiv1306.0783OpenAlexW3102933860MaRDI QIDQ2351412

Julianna Zsidó

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1306.0783

zbMATH Keywords

Coqformalisationreal root isolationBernstein coefficientsthree circlesnormal polynomial

Mathematics Subject Classification ID

Uses Software

• Coq
• Coq/SSReflect
• Flyspeck
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A revision of the proof of the Kepler conjecture
• Formalization of Bernstein polynomials and applications to global optimization
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• Isolating real roots of real polynomials
• A Refinement-Based Approach to Computational Algebra in Coq
• A formal study of Bernstein coefficients and polynomials
• Implementing the cylindrical algebraic decomposition within the Coq system
• When Newton meets Descartes
• Efficient real root approximation
• Algorithms in real algebraic geometry

This page was built for publication: Theorem of three circles in Coq