Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

DOI10.2168/LMCS-8(1:2)2012zbMath1241.68096arXiv1201.3731OpenAlexW2022441937MaRDI QIDQ2881068

Cyril Cohen, Assia Mahboubi

Publication date: 3 April 2012

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

quantifier eliminationformal proofsreal algebraic geometryreal closed fields\texttt{Coq}small scale reflection

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Real algebraic and real-analytic geometry (14P99) Ordered fields (12J15) Quantifier elimination, model completeness, and related topics (03C10)

Related Items (16)

Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Validating Mathematical Structures ⋮ Recent Advances in Real Geometric Reasoning ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Unnamed Item ⋮ Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Elementary recursive quantifier elimination based on Thom encoding and sign determination ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Algebraic Numbers in Isabelle/HOL ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ Formalization of Bernstein polynomials and applications to global optimization ⋮ Theorem of three circles in Coq

Uses Software

• Coq
• QEPCAD
• Coq/SSReflect
• CoqMT

This page was built for publication: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination