Implementing the cylindrical algebraic decomposition within the Coq system

DOI10.1017/S096012950600586XzbMath1121.03023MaRDI QIDQ3431546

Assia Mahboubi

Publication date: 12 April 2007

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

automated deductiondecision procedure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)

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

• Coq
• QEPCAD
• REDLOG

This page was built for publication: Implementing the cylindrical algebraic decomposition within the Coq system