Combined Decision Techniques for the Existential Theory of the Reals
From MaRDI portal
Publication:3637273
DOI10.1007/978-3-642-02614-0_14zbMath1247.03018OpenAlexW1490012302MaRDI QIDQ3637273
Paul B. Jackson, Grant Olney Passmore
Publication date: 9 July 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02614-0_14
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ raSAT: an SMT solver for polynomial constraints ⋮ The Strategy Challenge in SMT Solving ⋮ raSAT: An SMT Solver for Polynomial Constraints ⋮ Virtual Substitution for SMT-Solving ⋮ Formalization of Bernstein polynomials and applications to global optimization
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Quantifier elimination for real algebra -- the quadratic case and beyond
- Solving systems of polynomial inequalities in subexponential time
- Real quantifier elimination is doubly exponential
- An algorithm for the computation of the radical of an ideal
- Solving Polynomial Strict Inequalities Using Cylindrical Algebraic Decomposition
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Efficient projection orders for CAD
- QEPCAD B
- Computer Science Logic
- Automated Deduction – CADE-20
- Theorem Proving in Higher Order Logics
- Decision procedures for real and p‐adic fields
- A Computing Procedure for Quantification Theory
This page was built for publication: Combined Decision Techniques for the Existential Theory of the Reals
