Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition
Tarski in 1948, (Tarski 1951) published a quantifier elimination method for the elementary theory of real closed fields (which he had discovered in 1930). As noted by Tarski, any quantifier elimination method for this theory also provides a decision method, which enables one to decide whether any sentence of the theory is true or false. Since many important and difficult mathematical problems can be expressed in this theory, any computationally feasible quantifier elimination algorithm would be of utmost significance.
KeywordsReal Root Atomic Formula Real Zero Real Polynomial Quantifier Elimination
Unable to display preview. Download preview PDF.