I-RiSC

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

Anything in here will be replaced on browsers that support the canvas element


References in zbMATH (referenced in 1 article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Loup, Ulrich; Ábrahám, Erika: I-RiSC: an SMT-compliant solver for the existential fragment of real algebra (2011)