Projects per year
Abstract / Description of output
Methods for deciding quantifierfree nonlinear arithmetical conjectures over ℜ are crucial in the formal verification of many realworld systems and in formalised mathematics. While nonlinear (rational function) arithmetic over ℜ is decidable, it is fundamentally infeasible: any general decision method for this problem is worstcase 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 highdimensional 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 sweetspots. We discuss highlevel mathematical and design aspects of RAHD and illustrate its use on a number of examples.
Original language  English 

Title of host publication  Intelligent Computer Mathematics 
Subtitle of host publication  16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 612, 2009. Proceedings 
Editors  Jacques Carette, Lucas Dixon, Claudio Coen, Stephen Watt 
Publisher  SpringerVerlag GmbH 
Pages  122137 
Number of pages  16 
ISBN (Print)  9783642026133 
DOIs  
Publication status  Published  2009 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer Berlin / Heidelberg 
Volume  5625 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Fingerprint
Dive into the research topics of 'Combined Decision Techniques for the Existential Theory of the Reals'. Together they form a unique fingerprint.Projects
 1 Finished

Integration and Interaction of multiple mathematical reasoning processes
Bundy, A., Colton, S., Aspinall, D., Dennis, L., Fleuriot, J., Georgieva, L., Ireland, A., Jackson, P. & Smaill, A.
1/04/07 → 31/03/11
Project: Research