Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems

DOI10.1007/s10817-015-9320-xzbMath1356.68196OpenAlexW1978149312MaRDI QIDQ287269

Anthony Narkawicz, Aaron Dutle, César A. Muñoz

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9320-x

zbMATH Keywords

polynomial inequalitiesautomated theorem provingSturm's theoremdecision procedureinteractive theorem provingnonlinear arithmeticprototype verification system (PVS)Tarski's theorem

Mathematics Subject Classification ID

Related Items (6)

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL ⋮ The natural algorithmic approach of mixed trigonometric-polynomial problems ⋮ Evaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOL ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

• Coq
• MetiTarski
• PVS
• RealPaver
• Gappa
• dReal
• PVSio

Cites Work

• Unnamed Item
• Unnamed Item
• MetiTarski: An automatic theorem prover for real-valued special functions
• Subresultants revisited.
• Application of Bernstein expansion to the solution of control problems
• Formalization of Bernstein polynomials and applications to global optimization
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
• A Refinement-Based Approach to Computational Algebra in Coq
• Point-Free, Set-Free Concrete Linear Algebra
• On the Generation of Positivstellensatz Witnesses in Degenerate Cases
• Implementing the cylindrical algebraic decomposition within the Coq system
• Formalization and Execution of Linear Algebra: From Theorems to Algorithms
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Proving Bounds on Real-Valued Functions with Computations
• Algorithm 852
• Combined Decision Techniques for the Existential Theory of the Reals
• The Fundamental Theorem of Algebra Made Effective: An Elementary Real-algebraic Proof via Sturm Chains
• Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
• dReal: An SMT Solver for Nonlinear Theories over the Reals
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Certifying the Floating-Point Implementation of an Elementary Function Using Gappa
• Automated Deduction – CADE-20
• Algorithms in real algebraic geometry

This page was built for publication: Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems