I-RiSC: an SMT-compliant solver for the existential fragment of real algebra. This paper connects research in computer science in the field of SAT-modulo-theories (SMT) solving and research in mathematics on decision procedures for real algebra. We consider a real algebraic decision procedure computing all realizable sign conditions of a set of polynomials. We modify this procedure so that it satisfies certain requirements needed for the embedding into an SMT-solver.
Keywords for this software
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.
- Loup, Ulrich; Ábrahám, Erika: I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (2011)