Satisfiability of Non-linear (Ir)rational Arithmetic

DOI10.1007/978-3-642-17511-4_27zbMATH Open1310.68126OpenAlexW1552495765MaRDI QIDQ3066114FDOQ3066114

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

term rewritingSMT solvingnonlinear arithmeticterminationmatrix interpretations

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Cited In (14)

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

Uses Software

• MiniSat

This page was built for publication: Satisfiability of Non-linear (Ir)rational Arithmetic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3066114)