Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
From MaRDI portal
Publication:5191109
DOI10.1007/978-3-642-02959-2_23zbMath1250.68184OpenAlexW1582592616MaRDI QIDQ5191109
Cristina Borralleras, Rafael Navarro-Marset, Albert Rubio, Salvador Lucas, Enric Rodríguez-Carbonell
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.491.5880
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ SAT modulo linear arithmetic for solving polynomial constraints ⋮ Automatic Proofs of Termination With Elementary Interpretations ⋮ Proving Termination Properties with mu-term ⋮ $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation ⋮ A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic ⋮ Generating invariants for non-linear hybrid systems
Uses Software
Cites Work
- Unnamed Item
- Mechanically proving termination using polynomial interpretations
- Tyrolean termination tool: techniques and features
- Termination of term rewriting using dependency pairs
- Constraint-Based Approach for Analysis of Hybrid Systems
- Maximal Termination
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Polynomials over the reals in proofs of termination : from theory to practice
- Artificial Intelligence and Symbolic Computation
- Logic Programming
- Search Techniques for Rational Polynomial Orders
- Algorithms in real algebraic geometry
This page was built for publication: Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
