On the Generation of Positivstellensatz Witnesses in Degenerate Cases
From MaRDI portal
Publication:3088010
DOI10.1007/978-3-642-22863-6_19zbMath1342.68296arXiv1105.4421OpenAlexW1501825542MaRDI QIDQ3088010
Pierre Corbineau, David Monniaux
Publication date: 17 August 2011
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1105.4421
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (11)
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ A heuristic method for certifying isolated zeros of polynomial systems ⋮ Certifying solutions to overdetermined and singular polynomial systems over \(\mathbb{Q}\) ⋮ Solving generic nonarchimedean semidefinite programs using stochastic game algorithms ⋮ Using Intersection of Unions to Minimize Multi-directional Linearization Error in Reachability Analysis ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Bounding averages rigorously using semidefinite programming: mean moments of the Lorenz system ⋮ Validating numerical semidefinite programming solvers for polynomial invariants ⋮ GpoSolver: a Matlab/C++ toolbox for global polynomial optimization ⋮ Formal Proofs for Nonlinear Optimization ⋮ Formalization of Bernstein polynomials and applications to global optimization
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients
- On the complexity of Schmüdgen's Positivstellensatz
- Extremal psd forms with few terms
- Products of positive forms, linear matrix inequalities, and Hilbert 17th problem for ternary forms
- Computing sum of squares decompositions with rational coefficients
- Anneaux preordonnes
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- A Nullstellensatz and a Positivstellensatz in semialgebraic geometry
- A new decision method for elementary algebra
- Implementing the cylindrical algebraic decomposition within the Coq system
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Algorithm 875
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
- On the combinatorial and algebraic complexity of quantifier elimination
- Semidefinite Programming
- Signature of symmetric rational matrices and the unitary dual of lie groups
- Computer Science Logic
- Dynamical method in algebra: Effective Nullstellensätze
This page was built for publication: On the Generation of Positivstellensatz Witnesses in Degenerate Cases
