On the Generation of Positivstellensatz Witnesses in Degenerate Cases

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

Mathematics Subject Classification ID

Fields related with sums of squares (formally real fields, Pythagorean fields, etc.) (12D15) Quantifier elimination, model completeness, and related topics (03C10)

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

• Coq
• RAGlib
• DSDP5

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