Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Combined Decision Techniques for the Existential Theory of the Reals
Authors: Grant Passmore ; Paul Jackson
Date:Jul 2009
Publication Title:Calculemus/MKM 2009
Publication Type:Conference Paper Publication Status:Published
Volume No:5625 Page Nos:122-137
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
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 = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh