Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
From MaRDI portal
Publication:2881068
DOI10.2168/LMCS-8(1:2)2012zbMath1241.68096arXiv1201.3731OpenAlexW2022441937MaRDI QIDQ2881068
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
quantifier eliminationformal proofsreal algebraic geometryreal closed fields\texttt{Coq}small scale reflection
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
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
This page was built for publication: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
