Deciding polynomial-transcendental problems

Reviewer: James Harold Davenport

The theory of quantifier elimination over real closed fields goes back to Tarski [1], though practical methods had to wait for Collins in 1975 [2]. Given a formula Q 1 x 1, ..., Q k x k φ( x 1, ..., x n ) (where each Q i is either ∃ or is ∀, and φ is a Boolean combination of equalities and inequalities between polynomials), an equivalent formula ψ( x k +1, ..., x n ) is produced. In particular, if k = n , we get either "true" or "false." Expressions like √ x 2 - 1 can be handled by writing them as y and adding ∧ y 2 = x 2-1, for example. How can we add transcendental functions__?__ The authors first consider problems of the form Q 1 x 1 φ( x 1, trans( x 1)), where trans is a strongly transcendental function with a suitably neat algebraic relationship between trans and trans'. Log, exp, and arctan all satisfy these requirements. Here, they produce an unconditional algorithm for reducing this to "true" or "false." Here, "unconditional" means not relying on Schanuel's conjecture [3] or equivalent hard problems in number theory, and it is this unconditionality that is the most surprising part of the work. This will, for example, decide ∀ x 1(exp( x 1))(1- x 1) ? 1 x 1 ≥ 1, and will in fact do so in less than one second. The authors then take problems of the form Q 1 x 1 Q 2 x 2 ... Q n x n φ( x 1,trans( x 1), x 2, ..., x n ), apply the Collins-style quantifier elimination to Q 2, x 2, ... Q n x n φ( x 1, y , x 2 ... x n ) to get φ( x 1, y ), and apply their previous method to Q 1 x φ( x , trans( x )). Again, the process is unconditional. They also show how various other problems, such as ∀ x x >⇒ cosh( x )> x 3-4 x , can be transformed into this form and decided (in 17 seconds). While this is a significant step forward, we should note that we are limited to one occurrence of "trans," and this has to be the first quantifier. Also, this is purely a decision procedure, and will not do more general quantifier elimination. Online Computing Reviews Service