Satisfiability of Non-linear (Ir)rational Arithmetic

DOI10.1007/978-3-642-17511-4_27zbMath1310.68126OpenAlexW1552495765MaRDI QIDQ3066114

Aart Middeldorp, Harald Zankl

Publication date: 7 January 2011

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.631.2520

zbMATH Keywords

terminationterm rewritingSMT solvingnonlinear arithmeticmatrix interpretations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Optimization modulo non-linear arithmetic via incremental linearization, SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving, Uncurrying for termination and complexity, raSAT: an SMT solver for polynomial constraints, Decreasing diagrams and relative termination, SAT modulo linear arithmetic for solving polynomial constraints, Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations, Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems, I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra, The Strategy Challenge in SMT Solving, $$\mathsf {SC}^\mathsf{2} $$ : Satisfiability Checking Meets Symbolic Computation, raSAT: An SMT Solver for Polynomial Constraints

Uses Software

• MiniSat