Quantifier Elimination

释义 / Definition

量词消去：在一阶逻辑或相关形式系统中，把含有“∀（对所有）/∃（存在）”等量词的公式，通过等价变形改写为不含量词（或量词更少、结构更简单）的公式的方法。常用于证明某些理论的可判定性、分析可定义集合、以及自动推理与符号计算中。（在不同理论里是否能做到“完全消去”取决于该理论的性质。）

例句 / Examples

Quantifier elimination makes some logical statements easier to analyze.
量词消去会让一些逻辑陈述更容易分析。

Using quantifier elimination for real closed fields, we can transform a complex first-order formula into an equivalent quantifier-free condition.
在实闭域上使用量词消去，我们可以把复杂的一阶公式转化为等价的无量词条件。

发音 / Pronunciation (IPA)

/ˈkwɑːntɪfaɪər ɪˌlɪmɪˈneɪʃən/

词源 / Etymology

quantifier 来自拉丁语 quantus（“多少”），在逻辑中指“量化范围”的符号，如 ∀、∃；elimination 源自拉丁语 eliminare（“移除、排除”）。合起来表示“把公式中的量词移除（在等价意义下消去）”。

相关词 / Related Words

• Quantifier
• Eliminate
• First-Order Logic
• Model Theory
• Decidability
• Real Closed Field
• Presburger Arithmetic
• O-Minimality
• Cylindrical Algebraic Decomposition

文学与著作举例 / Notable Works

• Alfred Tarski, A Decision Method for Elementary Algebra and Geometry（提出并推动了与实闭域相关的量词消去思想）
• Wilfrid Hodges, Model Theory（模型论教材中系统讨论量词消去）
• David Marker, Model Theory: An Introduction（含量词消去与相关应用）
• Lou van den Dries, Tame Topology and O-minimal Structures（在 o-极小结构中大量使用量词消去/等价表述思想）
• George E. Collins 等关于 Cylindrical Algebraic Decomposition 的论文与综述（代数几何/计算代数中实现量词消去的经典方法之一）