Skolemization（斯科勒姆化）：在一阶逻辑中，为了消去存在量词（∃），用斯科勒姆常量或斯科勒姆函数（Skolem constants/functions）替代相应变量，把公式改写成等可满足（equisatisfiable）的形式，常用于自动定理证明与规范形转换（如前束范式、合取范式）。
/ˌskoʊləmɪˈzeɪʃən/
Skolemization removes existential quantifiers by introducing new function symbols.
斯科勒姆化通过引入新的函数符号来消去存在量词。
After skolemization, the formula becomes easier to convert into conjunctive normal form for resolution.
经过斯科勒姆化后，该公式更容易转换为用于归结法的合取范式。
该词源自挪威数学家与逻辑学家 Thoralf Skolem（托拉尔夫·斯科勒姆） 的姓氏，加上英语构词后缀 -ization（表示“使……化/……过程”），意为“进行斯科勒姆式的改写过程”。该方法与20世纪数理逻辑的发展、模型论与证明论的形式化技术密切相关。
Select Language