量词消去原则：
1) 消去存在量词"
"，即，将该量词约束的变量用任意常量（a,
b等）、或全称变量的函数(f(x), g(y)等)代替。如果存在量词左边没有任何全称量词，则只将其改写成为常量；如果是左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数。
2) 略去全程量词"
"，简单地省略掉该量词。Skolem 定理：
谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。
注意：公式G的SKOLEM标准形同G并不等值。
| 消去量词 量词消去原则： 1) 消去存在量词" "，即，将该量词约束的变量用任意常量（a,
b等）、或全称变量的函数(f(x), g(y)等)代替。如果存在量词左边没有任何全称量词，则只将其改写成为常量；如果是左边有全程量词的存在量词，消去时该变量改写成为全程量词的函数。
2) 略去全程量词" "，简单地省略掉该量词。Skolem 定理： 谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。 注意：公式G的SKOLEM标准形同G并不等值。 |