主题
Search

塔斯基定理

塔斯基定理指出，实数的一阶理论在包含 +, *, =, 和 > 运算时允许量词消去。 算法量词消去意味着可判定性，前提是仅包含常量的语句的真值可以被计算出来。 然而，反之则不然。 例如，实数的一阶理论在包含 +, *, 和 = 运算时是可判定的，但不允许量词消去。

塔斯基定理意味着，实代数方程和不等式的量化系统的解集是一个半代数集 (Tarski 1951, Strzebonski 2000)。

尽管塔斯基证明了量词消去是可能的，但他的方法完全不切实际 (Davenport and Heintz 1988)。 一种更有效的实现量词消去的程序称为柱形代数分解。 它由 Collins (1975) 开发，并实现为CylindricalDecomposition[ineqs, vars].

参见

柱形代数分解, 可判定的, 量化系统, 量词, 量词消去, 半代数集

本条目部分内容由 Adam Strzebonski 贡献

使用 Wolfram|Alpha 探索

参考文献

Collins, G. E. "通过柱形代数分解对实闭域进行量词消去。" In Proc. 2nd GI Conf. Automata Theory and Formal Languages. New York: Springer-Verlag, pp. 134-183, 1975.Davenport, J. and Heintz, J. "实数量词消去是双指数级的。" J. Symb. Comput. 5, 29-35, 1988.Marker, D. "模型论与求幂。" Not. Amer. Math. Soc. 43, 753-759, 1996.Strzebonski, A. "求解代数不等式。" Mathematica J. 7, 525-541, 2000.Tarski, A. "Sur les ensembles définissables de nombres réels." Fund. Math. 17, 210-239, 1931.Tarski, A. 初等代数和几何的判定方法。 Manuscript. Santa Monica, CA: RAND Corp., 1948. Republished as 初等代数和几何的判定方法，第二版。 Berkeley, CA: University of California Press, 1951.

在 Wolfram|Alpha 中被引用

塔斯基定理

引用为

Strzebonski, Adam 和 Weisstein, Eric W. "塔斯基定理。" 来自 MathWorld——Wolfram Web 资源。 https://mathworld.net.cn/TarskisTheorem.html

主题分类