A New Approach to Quantifier Elimination for Real Algebra
A New Approach to Quantifier Elimination for Real Algebra
复制标题
DOI：
10.1007/978-3-7091-9459-1_20
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
V. Weispfenning
中科院分区：
文献类型：
--
作者：
V. Weispfenning
真实的数的初等形式理论的量词消去是数学与计算机科学的交叉领域，如数理逻辑、交换代数与代数几何、计算机代数、计算几何和复杂性理论等。最初，量词消除的方法是由Th。Skolem）在数理逻辑中作为一种技术工具，用于解决形式化数学理论的决策问题。对于真实的数的初等形式理论（或者更准确地说，对于真实的闭域的初等形式理论），这样的量词消去过程是由A. Tarski，使用Sturm定理的1830年的扩展来计算给定区间内一元多项式的真实的零点的数量。从那时起，大量的新的决策和量词消除方法，这个理论的变化和优化已出版的目的，既建立理论的复杂性的问题，并找到方法，是实际的重要性（见Arnon 1988 a和讨论和参考资料在Renegar 1992 a，1992 b，1992 c为这些方法的比较）。对于子问题，如消除量词的变量，这是线性或二次限制，专门的方法已经开发出良好的成功（见Weispfenning 1988;卢什和Weispfenning 1993;洪1992 d; Weispfenning 1997）。
Quantifier elimination for the elementary formal theory of real numbers is a fascinating area of research at the intersection of various field of mathematics and computer science, such as mathematical logic, commutative algebra and algebraic geometry, computer algebra, computational geometry and complexity theory. Originally the method of quantifier elimination was invented (among others by Th. Skolem) in mathematical logic as a technical tool for solving the decision problem for a formalized mathematical theory. For the elementary formal theory of real numbers (or more accurately of real closed fields) such a quantifier elimination procedure was established in the 1930s by A. Tarski, using an extension of Sturm’s theorem of the 1830s for counting the number of real zeros of a univariate polynomial in a given interval. Since then an abundance of new decision and quantifier elimination methods for this theory with variations and optimizations has been published with the aim both of establishing the theoretical complexity of the problem and of finding methods that are of practical importance (see Arnon 1988a and the discussion and references in Renegar 1992a, 1992b, 1992c for a comparison of these methods). For sub-problems such as elimination of quantifiers with respect to variables, that are linearly or quadratically restricted, specialized methods have been developed with good success (see Weispfenning 1988; Loos and Weispfenning 1993; Hong 1992d; Weispfenning 1997).