POLYNOMIAL-TIME ALGORITHMS FOR SENTENCES OVER NUMBER-FIELDS

We call φ{symbol} a ∀∃ sentence if and only if ρ is logically equivalent to a sentence of the form ∀x∃yψ(x, y), where ψ(x, y) is a quantifier free formula constructed with logical and arithmetical symbols. Now let φ{symbol} be a ∀∃ sentence in conjunctive or disjunctive normal form. We show that given an arbitrary algebraic number field K there is a polynomial time algorithm to decide whether φ{symbol} is true in K or not. We also show that ther are polynomial time algorithms to decide whether or not φ{symbol} is true in every algebraic number field or every radical extension field of Q. © 1992.