I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra

DOI10.1007/978-3-642-21493-6_15zbMath1339.68242OpenAlexW42497840MaRDI QIDQ3014943

Ulrich Loup, Erika Ábrahám

Publication date: 8 July 2011

Published in: Algebraic Informatics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-21493-6_15

zbMATH Keywords

SMT solvingreal algebraDPLL(T)FO logicI-RiSC

Mathematics Subject Classification ID

Uses Software

• cvc3
• z3
• GiNaCRA
• OpenSMT
• I-RiSC
• ABsolver

Cites Work

• Unnamed Item
• Unnamed Item
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Solving SAT and SAT Modulo Theories
• Algorithms in real algebraic geometry

This page was built for publication: I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra