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