- Abstract:
-
Methods for deciding quantifier-free non-linear arithmetical conjectures over \mathbb{R} are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over \mathbb{R} is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have ``sweet spots'' -- e.g., types of problems for which they perform much better than they do in general. Such ``sweet spots'' can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation. RAHD (``Real Algebra in High Dimensions'') is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective ``sweet-spots.'' We discuss high-level mathematical and design aspects of RAHD and illustrate its use on a number of examples.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-1330,
- author = {
Grant Passmore
and Paul Jackson
},
- title = {Combined Decision Techniques for the Existential Theory of the Reals},
- book title = {Calculemus/MKM 2009},
- publisher = {Springer-Verlag},
- year = 2009,
- month = {Jul},
- volume = {5625},
- pages = {122-137},
- url = {http://homepages.inf.ed.ac.uk/s0793114/passmore-jackson-calculemus09.pdf},
- }
|
