SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox

1. Ábrahám, E., et al.: A lazy SMT-solver for a non-linear subset of real algebra. In: Proc. of SMT 2010 (2010)

   Google Scholar 

2. Basu, S., Pollack, R., Roy, M.: Algorithms in Real Algebraic Geometry. Springer (2010)

   Google Scholar 

3. Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

   Google Scholar 

4. Brown, C.W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin 37(4), 97–108 (2003)

   Article  MATH  Google Scholar 

5. Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The OpenSMT Solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 150–153. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

6. Collins, G.E.: Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)

   Google Scholar 

7. Corzilius, F., Ábrahám, E.: Virtual Substitution for SMT-Solving. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 360–371. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

8. http://cs.nyu.edu/acsys/cvc3/

9. de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving, http://research.microsoft.com/en-us/um/people/leonardo/mp-smt-strategy.pdf

10. Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulas over ordered fields. Journal of Symbolic Computation 24, 209–231 (1995)

    Article  MathSciNet  Google Scholar 

11. Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. SIGSAM Bulletin 31(2), 2–9 (1997)

    Article  MathSciNet  Google Scholar 

12. Fränzle, M., et al.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1(3-4), 209–236 (2007)

    Google Scholar 

13. Heintz, J., Roy, M.F., Solernó, P.: On the theoretical and practical complexity of the existential theory of the reals. The Computer Journal 36(5), 427–431 (1993)

    Article  MathSciNet  MATH  Google Scholar 

14. Loup, U., Ábrahám, E.: GiNaCRA: A C++ Library for Real Algebraic Computations. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 512–517. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

15. Passmore, G.O., Jackson, P.B.: Combined Decision Techniques for the Existential Theory of the Reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 122–137. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

16. Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1948)

    Google Scholar 

17. Weispfenning, V.: A new approach to quantifier elimination for real algebra. In: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation, pp. 376–392. Springer (1998)

    Google Scholar 

18. Weispfenning, V.: The complexity of linear problems in fields. Journal of Symbolic Computation 5(1-2), 3–27 (1988)

    Article  MathSciNet  MATH  Google Scholar 

19. Weispfenning, V.: Quantifier elimination for real algebra – The quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing 8(2), 85–101 (1997)

    Article  MathSciNet  MATH  Google Scholar 

20. http://research.microsoft.com/en-us/um/redmond/projects/z3/

Download references