``RAHD: A Feasible Proof Procedure for Real Algebra in High Dimensions.'' by Grant Olney Passmore {g.passmore@ed.ac.uk, http://homepages.inf.ed.ac.uk/s0793114/} Visiting Fellow, SRI International Ph.D. Student, University of Edinburgh October 30th, 2008 Talk given at SRI International, CSL Seminar [Short Abstract] In this talk, I will present the basic ideas underlying RAHD (Real Algebra in High Dimensions), a new decision method I have developed for deciding the satisfiability of boolean combinations of high-dimensional polynomial equations and inequalities over the real numbers. [Long Abstract ~ Adapted from my Ph.D. proposal] The discipline of real algebraic geometry centers around the study of subsets of n-dimensional Euclidean space deļ¬nable by boolean combinations of polynomial equations and inequalities. As such ob jects, known as semialgebraic sets, arise naturally in virtually all mathematical and natural sciences, the development of sophisticated techniques for their analysis is a well-motivated problem. We are interested in the development of feasible (semi-)decision methods for the following question: Question: Given a semialgebraic set S defined as the collection of satisfying real vectors r in R^n with respect to some boolean combination of polynomial equations and inequalities Phi, is S empty? It is known that any full decision method for this problem requires time exponential in the dimension of the formula Phi, and currently available proof procedures for this problem are usually only able to solve problems in very low dimensions. However, if one relaxes the completeness criterion, and instead focuses upon the development of proof procedures for restricted but practically useful fragments of this decision problem, much progress can be made, and many high dimensional problems can be routinely settled. Our work centers around the isolation and implementation of feasible proof procedures for such fragments, and has resulted thus far in the RAHD (Real Algebra in High Dimensions) tool with encouraging prelimary results. We will discuss our decision method, its implementation as both a stand-alone tool and as a new deduction mechanism in the mechanical proof assistant PVS, and sketch our goals for the future.