Edinburgh Research Explorer

Combined Decision Techniques for the Existential Theory of the Reals

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://www.springerlink.com/content/21361010254m3m14
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
Pages122-137
Number of pages16
ISBN (Print)978-3-642-02613-3
DOIs
Publication statusPublished - 2009

Publication series

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

Abstract

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.

Download statistics

No data available

ID: 1133618