微信搜索“高速商务通”，马上办理ETC
∀
根据第34
页的定义3.4 ，当且仅当对于变量 x的所有解释都为真时，公式 xp（x）才为真。取而代之的是量词的，人们可以写 P（A 1）∧…∧ P（AN）对于所有常量一个1 …的在 ķ
。对于∃xp（x），可以写 p（a 1）∨・・・∨p（an）。由此得出de
Morgan定律
∀ Xφ＆equiv;¬∃ X ¬ φ。
通过这种等价，通用和存在量词可以相互替代。
例3.4 “每个人都想被爱”的命题等同于“没有人不想被爱” 的命题。
§ 齐∈{∀，∃} 为我= 1，…，N 。
§ φ = Q 1 x 1 … Qnxnψ 。
量词是谓词逻辑表达能力的重要组成部分。但是，它们对AI的自动推理具有破坏性，因为它们使得公式的结构更加复杂，并且在证明的每个步骤中增加了适用的推理规则的数量。因此，我们的下一个目标是为每个谓词逻辑公式找到标准化正规形式的等效公式，并尽可能少量化。作为第一步，我们将通用量词引入公式的开头并进行定义
定义3.6谓词逻辑公式φ如果保持不变，则为prenex normal格式
§ ψ 是无量词的公式。
如果量化变量超出其量化范围，则建议小心，例如x in
∀xp （x） ⇒∃xq （x）。
这里必须重命名两个变量之一，并在其中
∀ XP（x）的 ⇒∃ YQ（y）的
量词可以很容易地被带到前面，我们得到等价公式作为输出
∀ X ∃ YP（x）的 ⇒ Q（y）的。
但是，如果我们希望正确地将量词放在前面
（∀ XP（X））⇒∃ YQ（Y）（3.4）我们首先写式中的等价形式
¬ （ ∀
XP（X）） ∨∃ YQ（Y）。
第一个通用量词现在变成了
（∃ X ¬ P（X））∨∃ YQ（y）的
现在这两个量词最终可以被提前
∃ X ∃ Ý ¬ P（X） ∨ Q（y）时，
这相当于
∃ X ∃ YP（x）的 ⇒ Q（y）的。
然后我们看到在（ 3.4 ）中我们不能简单地将两个量词拉到前面。相反，我们必须首先消除影响，以便对量化器没有任何否定。一般认为，如果否定仅直接存在于原子子公式中，我们可能只会拉出量词。
∈
实施例3.5 如分析中所熟知的，系列（a）n N 与极限 a的收敛定义为
∀ ε> 0 ∃ Ñ 0 ∈ Ñ ∀ N>Ñ 0 | an – a | <ε。
使用函数 abs（x）为| x | ， A（N）为一个，减去（X，Y）为 X – ÿ 和predi-凯茨 EL（X，Y）为 X ∈ Ý ， GR（X，Y）为 X> Y ，式中读取
∀ ε（GR（ε， 0） ⇒∃ Ñ 0（EL（N 0， Ñ） ⇒∀ N（GR（N，N- 0） ⇒ GR（ε，ABS（减去（A（N），一）））
）））。
（3.5）
∃∀
这显然不是正常形式。由于内部量化器n 0和n的变量不会出现在各自量词的左侧，因此不必重命名变量。接下来我们消除影响并获得
＆ForAll; ε（¬ GR（ε，0）∨∃ Ñ 0（¬ EL（N 0，Ñ）∨∀ N（¬ GR（N，N- 0）∨ GR（ε，ABS（减去（A（N），一））））））。
因为每个否定都在一个原子公式的前面，我们将量词推进，消除多余的括号，并用
∀ ε ∃ Ñ 0 ∀ N（¬ GR（ε，0）∨¬ EL（N 0，Ñ）∨¬ GR（N，N- 0）∨ GR（ε，ABS（减去（A（N），a））的））
它成为联合正常形式的量化条款。
转换后的公式等同于输出公式。事实上，这种转变始终是可能的
定理3.2 每个谓词逻辑公式都可以转换为prenex normal形式的等价公式。
∧¬
此外，我们可以消除所有存在量词。然而，由所谓的Skolemization产生的公式不再等同于输出公式。然而，它的可满足性保持不变。在许多情况下，特别是当想要显示KB Q的不可满足性时，这就足够了。prenex normal form中的以下公式现在将被简化：
∀ X 1 ∀ X 2 ∃ ý 1 ∀ X 3 ∃ Ý 2 P（F（X 1）中，x 2，Y 1）∨ Q（Ý 1，X 3，Y 2）。
因为变量y 1显然取决于x 1和x 2，所以y 1的每次出现都被Skolem函数g（x 1 ，x 2 ）代替。重要的是g是一个尚未出现在公式中的新函数符号。我们获得
∀ X 1个∀ X 2 ∀ X 3 ∃ Ý 2 P（F（X 1）中，x 2，G（X 1，X 2））∨ Q（克（X 1，X 2）中，x 3，Y 2）
并且通过h（x 1 ，x 2 ，x 3 ）类似地替换y 2 ，这导致
∀ X 1个∀ X 2 ∀ X 3 P（F（X 1）中，x 2，G（X 1，X 2））∨ Q（克（X 1，X 2）中，x 3，H（X 1，X 2，x 3））。
因为现在所有变量都是普遍量化的，所以可以省略通用量词，从而产生
p（f（x 1），x 2，g（x 1，x 2））∨q（g（x 1，x 2），x 3，h（x 1，x 2，x 3））。
N ORMAL F ORM T RANSFORMATION（公式）：
4.
转换为prenex普通形式：
转换为联合正规形式（定理2.1）：消除等价。
消除影响。
反复应用德摩根定律和分配律。
5.
Skolemization
：
用新的Skolem函数替换存在量化的变量。
删除生成的通用量词。
图3.2 谓词逻辑公式转换为正规形式
现在我们可以通过引入Skolem函数n 0 （ε）来消除第 39 页的（ 3.5 ）中的存在量词（从而也消除通用量词）。因此，第 39 页的（ 3.5 ）的scolemized
prenex和conjunctive normal格式读取
¬克（ε，0）∨¬ EL（N 0（ε），Ñ）∨¬ GR（N，N- 0（ε））∨ GR（ε，ABS（减去（A（N），A）））。
通过删除变量n 0，Skolem函数可以接收名称n 0。
∃
∀∀[]
∀∀∃
当以正常形式对公式进行分析时，所有存在量词都从外向内消除，其中x 1 … xnyφ形式的公式被x 1 …xnφy/ f（x 1 ， …，xn），其中f可能不出现在φ中。如果存在量词位于远处外部，例如yp（y），那么y必须被常量（即零位函数符号）替换。
以连接法线形式转换公式的过程在图 3.2中表示的伪码中进行了总结。Skolemization在文字数量上具有多项式运行时间。当转换为正规形式时，正常形式的文字数量可以指数增长，这可能导致指数计算时间和指数内存使用。其原因是分配法的重复适用。由大量条款产生的实际问题是搜索空间的组合爆炸，用于后续分辨率证明。然而，有一种优化的变换算法，它只产生多个文字[Ede91]。
