主題
Search

塔斯基定理

塔斯基定理指出，實數的一階理論在包含 +, *, =, 和 > 運算時允許量詞消去。 演算法量詞消去意味著可判定性，前提是僅包含常量的語句的真值可以被計算出來。 然而，反之則不然。 例如，實數的一階理論在包含 +, *, 和 = 運算時是可判定的，但不允許量詞消去。

塔斯基定理意味著，實代數方程和不等式的量化系統的解集是一個半代數集 (Tarski 1951, Strzebonski 2000)。

儘管塔斯基證明了量詞消去是可能的，但他的方法完全不切實際 (Davenport and Heintz 1988)。 一種更有效的實現量詞消去的程式稱為柱形代數分解。 它由 Collins (1975) 開發，並實現為CylindricalDecomposition[ineqs, vars].

參見

柱形代數分解, 可判定的, 量化系統, 量詞, 量詞消去, 半代數集

本條目部分內容由 Adam Strzebonski 貢獻

使用 探索

參考文獻

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.

在 中被引用

塔斯基定理

引用為

Strzebonski, Adam 和 Weisstein, Eric W. "塔斯基定理。" 來自 —— 資源。 https://mathworld.tw/TarskisTheorem.html

主題分類