Implementing the cylindrical algebraic decomposition within the Coq system
From MaRDI portal
Recommendations
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Proof certificates for algebra and their application to automatic geometry theorem proving
- Quantifier elimination over algebraically closed fields in a proof assistant using a computer algebra system
- Floating-point arithmetic in the Coq system
- Certified Exact Transcendental Real Number Computation in Coq
Cited in
(11)- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL
- Flexible proof production in an industrial-strength SMT solver
- Formalization of Bernstein polynomials and applications to global optimization
- Theorem of three circles in Coq
- Dealing with algebraic expressions over a field in Coq using Maple
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases
- A formal study of Bernstein coefficients and polynomials
- Proving Bounds on Real-Valued Functions with Computations
- Embedding of Systems of Affine Recurrence Equations in Coq
This page was built for publication: Implementing the cylindrical algebraic decomposition within the Coq system
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3431546)
