Implementing the cylindrical algebraic decomposition within the Coq system
From MaRDI portal
Publication:3431546
DOI10.1017/S096012950600586XzbMath1121.03023MaRDI QIDQ3431546
Publication date: 12 April 2007
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ Proving Bounds on Real-Valued Functions with Computations ⋮ On the Generation of Positivstellensatz Witnesses in Degenerate Cases ⋮ A formal study of Bernstein coefficients and polynomials ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Formalization of Bernstein polynomials and applications to global optimization ⋮ Theorem of three circles in Coq
Uses Software
This page was built for publication: Implementing the cylindrical algebraic decomposition within the Coq system
