Abstract: Since Tarski's work in the 1930s, it has been known that the first-order theory of real-closed fields (with addition and multiplication) admits quantifier elimination and is decidable. Although practical implementations of algorithms for this problem can be useful, their worst-case efficiency is discouraging. Moreover, many of the best algorithms, e.g. Collin's CAD (Cylindrical Algebraic Decomposition) are quite complicated, making it difficult to certify results rigorously.

However, if we restrict ourselves to proving entirely universally quantified formulas, which still takes in a lot of important practical problems, quite different approaches become possible. Since every ordered field can be embedded in a real closed field, it follows that any valid universal formula can be proved just from the ordered field axioms, without using special properties of real-closed fields. There are important sharper results along these lines, e.g. various forms of real "Positivstellensatz". In almost all such results, a key role is played by sums of squares of polynomials, and in order to base a practical algorithm on this observation, one needs to be able to find decompositions of certain polynomials into sums of squares.

This approach has many attractions, including the existence of very short and simple "proofs". In the simplest case, if we can obtain a sum-of-squares decomposition for a polynomial, we know it is nonnegative. A slightly richer example with an equational hypothesis is proving that a quadratic equation with a real root must have a nonnegative discriminant:

forall a b c x. a * x^2 + b * x + c = 0 ==> b^2 - 4 * a * c >= 0

An almost trivial proof can be obtained from the following algebraic identity expressing the discriminant as a sum of squares plus a multiple of the input equation:

b^2 - 4 * a * c = (2 * a * x + b)^2 - 4 * a * (a * x^2 + b * x + c)

How does one find decompositions of polynomials into sums of squares? The best method known, pioneered by Parrilo, uses an optimization technique known as semidefinite programming, a generalization of linear programming. We will give an overview of this method and show how effective it is in practice, as well as describing an attractive alternative for the univariate case.

John Harrison has worked in formal verification and automated theorem proving since 1990, when he joined Mike Gordon's "Hardware Verification Group" (HVG) at the University of Cambridge Computer Laboratory. As well as working on the development of the HOL theorem prover, he developed a particular interest in the formalization of real analysis and its application to formal verification of floating-point hardware. His PhD in this area, "Theorem Proving with the Real Numbers", written under Mike Gordon's supervision, won a UK Distinguished Dissertation award and was published as a book. He also redesigned HOL from scratch, resulting in an alternative version called HOL Light. After completing his PhD research in 1995, John Harrison spent a very enjoyable year at Abo Akademi University and Turku Centre for Computer Science (TUCS) in Turku, Finland, where he was a member of Ralph Back's Programming Methods Research Group. Among other activities, he championed the "declarative" proofs of the Mizar system and showed how these could be integrated into other theorem-provers, work subsequently taken up in DECLARE, Isar and other systems. John Harrison then returned to Cambridge and worked on a formal model of floating-point arithmetic and its application to the verification of some realistic algorithms for transcendental functions. This work attracted the attention of Intel, and in 1998 John Harrison joined the company as a Senior Software Engineer specializing in the design and formal verification of mathematical algorithms. He has formally verified and in many cases designed or redesigned numerous algorithms for mathematical functions including division, square root and transcendental functions. In his limited spare time over the past 10 years, John Harrison has been working on a book giving a comprehensive introduction to automated theorem proving. Appointments: dcm@cs.cmu.edu