第二章 归结推理方法

　　2.2 子句形

　　设有由一阶谓词逻辑描述的公式,,和B，证明在∧∧∧成产的条件下有B成立。仍然采用反演法来证明
　　　∧∧∧～B　
　　是不可满足的。和命题逻辑不同，首先遇到了量词问题，为此要将∧∧∧～B化成SKOLEM标准形，进而建立子句集，方可使用 Herbrand 定理和归结原理来证明∧∧∧→B成立。

　　2.2.1 SKOLEM 标准形
　　对给定的一阶谓词逻辑公式
　　　G＝∧∧～B
　　首先化成与其等值的前束范式
　　(Q1x1)…(Qn xn)M(x1,…,xn)
　　其中Qi(i=1,…,n)是存在量词或全称量词，而母式M(x1,…,xn)中不再含有量词。
　　进而可将M(x1,…,xn)化成等值的合取范式。
　　最后将所有存在量词消去，便得公式G的SKOLEM标准形了。消存在量词的过程如下：
　　设　(Qr xr) 1≤ r ≤n是第一个出现于
　　　　(Q1x1)… (Qrxr) …(Qnxn) M(x1,…,xn)
　　中的存在量词，即Q1,…,Qr-1　均为全称量词。
　　若r＝1，则将M(x1,…,xn)中的所有变量x1均以某个常量C代之，但要求C不同于已出现在M(x1,…,xn)中的任一常量。然后便可消去这个存在量词(Q1x1)即($x1)。
　　若1≤ r ≤n，(QrXr)的左边有全称量词　
　　　　(Qs1xs1), … ,(Qsmxsm)
　　而1≤s1<s2<…<sm<r 则将M(x1,…,xr,…xn)中的所有变量xr均以变量xs1,… ,xsm的某个函数如f(xs1, …,xsm)代之，但要求f不同于已出现在M(x1,┅xn)中的任一函数，而对f的具体形式没有要求。然后消去这个存在量词(QrXr)。
　　反复使用这种方法于(Q1x1)…(Qnxn) M(x1,…,xn)，便可消去其中所有的存在量词，所得之公式称作公式G的 SKOLEM 标准形。
例题 例1:
  　G＝(x)(y)(z)((～P(x,y)∧Q(x ,z))∨R(x,y,z)),G已是前束形了，需将M(x ,y ,z)化成合取范式。
　M(x,y,z)=(～P(x,y)∧Q(x,z))∨R(x,y,z)=(～P(x ,y)∨R(x ,y ,z))∧(Q(x ,y)∨R(x ,y ,z))
　于是　G＝(x)(y)(z)((～P(x,y)∧R(x,y,z))∧(Q(x,z)∨R(x,y,z)))
先消去(y)，因其左边只有全称量词(x)，于是引入f(x)代入M(x ,y ,z)中的所有变量y。再消去(z)，它左边也只有(x)，也引入一个不同于f(x)的g(x)代入M(x ,y ,z)中的所有变量z。最后得　
　　(x)((～P(x,f(x))∨R(x ,f(x),g(x))∧(Q,x,g(x))∨R(x,f(x),g(x)))
　便是G的 SKOLEM 标准形，其中f(x),g(x)称作 SKOLEM 函数。
例题 例2:
  　 G＝(x)(y)(z)(u)(P(x ,y ,z ,u))
　G已是前束形，M(x ,y ,z ,u)=P(x ,y ,z ,u)也已是合取范式。
　先消去(x)，因其左边没有全称量词，于是引入常量c代入P(x ,y ,z ,u)中的所有变量x。再消去(u)，它左边有全称量词(y)(z)，于是需引入一个二元函数f(y,z)代入P(x,y,z,u)中的变量u得G的 SKOLEM 标准形
　　(y)(z)P(c ,y ,z ,f(y ,z))