This paper presents a new method for quantifier elimination in the elementary theory of real closed fields, developed by George E. Collins in 1973. Tarski's original method, though theoretically sound, was computationally impractical for non-trivial problems. Collins' new method is significantly more efficient, with a computing time dominated by a polynomial function in terms of the number of variables, polynomials, their degrees, coefficients, and atomic formulas. In contrast, Tarski's and Seidenberg's methods have exponential time complexity in terms of these parameters. Boege's improvement of Tarski's method eliminates the exponential dependency on the number of polynomials but retains the exponential dependency on the degree of the polynomials.
Fischer and Rabin showed that any decision method for the first-order theory of the real numbers has a maximum computing time that grows at least exponentially with the input length. Collins' method has a computing time dominated by $ 2^{2^{kN}} $, where $ k \leq 8 $, suggesting it is among the most efficient known methods. Although a decision method with a doubly exponential bound was found by Monk and Solovay, Collins' method is more efficient and has a clearer theoretical foundation.
The method relies on cylindrical algebraic decomposition (CAD), which decomposes real space into cells where the sign of each polynomial in a given set remains constant. This decomposition is invariant under the polynomials and is constructed recursively, allowing for the efficient handling of quantifiers. The method is particularly effective for prenex formulas, where the quantifiers are all at the beginning. The CAD approach enables the determination of the truth of the unquantified part of the formula within each cell, facilitating the elimination of quantifiers. The method's efficiency and practical applicability make it a significant advancement in the field of real closed field theory.This paper presents a new method for quantifier elimination in the elementary theory of real closed fields, developed by George E. Collins in 1973. Tarski's original method, though theoretically sound, was computationally impractical for non-trivial problems. Collins' new method is significantly more efficient, with a computing time dominated by a polynomial function in terms of the number of variables, polynomials, their degrees, coefficients, and atomic formulas. In contrast, Tarski's and Seidenberg's methods have exponential time complexity in terms of these parameters. Boege's improvement of Tarski's method eliminates the exponential dependency on the number of polynomials but retains the exponential dependency on the degree of the polynomials.
Fischer and Rabin showed that any decision method for the first-order theory of the real numbers has a maximum computing time that grows at least exponentially with the input length. Collins' method has a computing time dominated by $ 2^{2^{kN}} $, where $ k \leq 8 $, suggesting it is among the most efficient known methods. Although a decision method with a doubly exponential bound was found by Monk and Solovay, Collins' method is more efficient and has a clearer theoretical foundation.
The method relies on cylindrical algebraic decomposition (CAD), which decomposes real space into cells where the sign of each polynomial in a given set remains constant. This decomposition is invariant under the polynomials and is constructed recursively, allowing for the efficient handling of quantifiers. The method is particularly effective for prenex formulas, where the quantifiers are all at the beginning. The CAD approach enables the determination of the truth of the unquantified part of the formula within each cell, facilitating the elimination of quantifiers. The method's efficiency and practical applicability make it a significant advancement in the field of real closed field theory.