Combined Decision Techniques for the Existential Theory of the Reals

Methods for deciding quantifier-free non-linear arithmetical conjectures over R are crucial in the formal verification of many realworld systems and in formalised mathematics. While non-linear (rational function) arithmetic over 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...

• Type: Conference
• Year: 2009
• Where: MKM
• Authors: Grant Olney Passmore, Paul B. Jackson
• Keywords: Algebraic Decision Methods, Decision Methods, Information Management, MKM 2009, Real Algebraic Decision