Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
From MaRDI portal
Publication:287269
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
polynomial inequalitiesautomated theorem provingSturm's theoremdecision procedureinteractive theorem provingnonlinear arithmeticprototype verification system (PVS)Tarski's theorem
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
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
