Combined Decision Techniques for the Existential Theory of the Reals

Grant Passmore, Paul Jackson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

Methods for deciding quantifier-free non-linear arithmetical conjectures over ℜ are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over ℜ 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.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publication16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings
EditorsJacques Carette, Lucas Dixon, Claudio Coen, Stephen Watt
PublisherSpringer-Verlag GmbH
Number of pages16
ISBN (Print)978-3-642-02613-3
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Combined Decision Techniques for the Existential Theory of the Reals'. Together they form a unique fingerprint.

Cite this