RSolver User Manual

Stefan Ratschan

November 20, 2013

Contents

1 Introduction
2 Running a First Example
3 The Input
4 Produced Output
5 Running RSolver
6 Relaxation Algorithm
7 Program Termination
8 The Algorithm
9 The Implementation
10 Known Bugs

Bibliography

[1]   B. F. Caviness and J. R. Johnson, editors. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Wien, 1998.

[2]   G. E. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Second GI Conf. Automata Theory and Formal Languages, volume 33 of LNCS, pages 134–183. Springer Verlag, 1975. Also in [1].

[3]   G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12:299–328, 1991. Also in [1].

[4]   P. Dorato, W. Yang, and C. Abdallah. Robust multi-objective feedback design by quantifier elimination. Journal of Symbolic Computation, 24:153–159, 1997.

[5]   H.-D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical Logic. Springer Verlag, 1984.

[6]   T. J. Hickey. smathlib. http://interval.sourceforge.net/interval/prolog/clip/clip/smath/README.html.

[7]   T. J. Hickey. Metalevel interval arithmetic and verifiable constraint solving. Journal of Functional and Logic Programming, 2001(7), October 2001.

[8]   L. Jaulin, M. Kieffer, O. Didrit, and É. Walter. Applied Interval Analysis, with Examples in Parameter and State Estimation, Robust Control and Robotics. Springer, Berlin, 2001.

[9]   R. B. Kearfott. Interval computations: Introduction, uses, and resources. Euromath Bulletin, 2(1):95–112, 1996.

[10]   R. E. Moore. Interval Analysis. Prentice Hall, Englewood Cliffs, NJ, 1966.

[11]   A. Neumaier. Interval Methods for Systems of Equations. Cambridge Univ. Press, Cambridge, 1990.

[12]   S. Ratschan. Continuous first-order constraint satisfaction. In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors, Artificial Intelligence, Automated Reasoning, and Symbolic Computation, number 2385 in LNCS, pages 181–195. Springer, 2002.

[13]   S. Ratschan. Quantified constraints under perturbations. Journal of Symbolic Computation, 33(4):493–505, 2002.

[14]   S. Ratschan. Search heuristics for box decomposition methods. Journal of Global Optimization, 24(1):51–60, 2002.

[15]   S. Ratschan. Efficient solving of quantified inequality constraints over the real numbers. ACM Transactions on Computational Logic, 7(4):723–748, 2006.

[16]   S. Ratschan and Z. She. Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM Journal on Control and Optimization, 48(7):4377–4394, 2010.

[17]   A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley, 1951. Also in [1].

[18]   P. Van Hentenryck, D. McAllester, and D. Kapur. Solving polynomial systems using a branch and prune approach. SIAM Journal on Numerical Analysis, 34(2):797–827, 1997.