Pages that link to "Item:Q3523169"
From MaRDI portal
The following pages link to Verifying Nonlinear Real Formulas Via Sums of Squares (Q3523169):
Displaying 26 items.
- Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems (Q287269) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Efficient and accurate computation of upper bounds of approximation errors (Q633637) (← links)
- Amortized complexity verified (Q670702) (← links)
- ATLAS: automated amortised complexity analysis of self-adjusting data structures (Q832253) (← links)
- A revision of the proof of the Kepler conjecture (Q977177) (← links)
- Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL (Q1725844) (← links)
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials (Q1733314) (← links)
- Duality of sum of nonnegative circuit polynomials and optimal SONC bounds (Q2156369) (← links)
- Formalization of Bernstein polynomials and applications to global optimization (Q2351165) (← links)
- Computing sum of squares decompositions with rational coefficients (Q2378506) (← links)
- Amortized Complexity Verified (Q2945642) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- On the Generation of Positivstellensatz Witnesses in Degenerate Cases (Q3088010) (← links)
- HOL Light: An Overview (Q3183517) (← links)
- Proving Bounds on Real-Valued Functions with Computations (Q3541683) (← links)
- A Short Presentation of Coq (Q3543643) (← links)
- Combined Decision Techniques for the Existential Theory of the Reals (Q3637273) (← links)
- Sharper and Simpler Nonlinear Interpolants for Program Verification (Q5056007) (← links)
- Real World Verification (Q5191121) (← links)
- DSOS and SDSOS Optimization: More Tractable Alternatives to Sum of Squares and Semidefinite Optimization (Q5382573) (← links)
- Validating numerical semidefinite programming solvers for polynomial invariants (Q5916266) (← links)
- Mathematics and the formal turn (Q6130523) (← links)
- Verified reductions for optimization (Q6536123) (← links)
- Transforming optimization problems into disciplined convex programming form (Q6648168) (← links)