|
2.2.3 G是不可满足的当且仅当S是不可满足的
公式G与其子句集S并不等值，但它们在不可满足的意义下是一致的。从而要证明
∧
∧
→B只需证明G＝∧∧∧～B的子句集S是不可满足的，这正是引入子句集的目的。我们将这个要结果叙述成定理。 |
定理 |
| 若G是给定的公式，而相应的子句集为S，则G是不可满足的当且仅当S是不可满足的。 | |
| 先作点讨论再作证明。给了公式G，可令 G＝(   )…(  )…(  )
M(,…,)这里G已为前束形，M( ,…,)已为合取范式形式。因为将G化成前束形，M(,…,)化成合取范式形式是容易实现的等值演算。又设( )是第一个出现的存在量词，为化成
SKOLEM 形需先消去这个()，并引入SKOLEM函数得 G1＝(  )…( )(  )…()M（,…,,f(,…,),,…,）而 G＝( )…()( xr)()…()M(,…,,…,)只须证明G不可满足  G1不可满足便可得定理。因为同理可将G1中的第一个出现的存在量词消去并引入 SKOLEM 函数得公式G2，依G不可满足 G1不可满足的证明方法便有 G1不可满足 G2不可满足重复这个过程直到 Gm 为 G 的 SKOLEM 标准形为止（Gm中不再有存在量词），而有 Gm-1不可满足
Gm 不可满足回顾S只不过是 Gm 的种集合的表示形式，自然有 Gm 不可满足 S不可满足 现在证明 G不可满足 G1不可满足先证明  知 G 是不可满足的，而假设 G1 是可满足。于是便有某个解释IG1使G1|IG1＝T。即对任意的 ,…,在IG1的设定下有()…()M(,…,,f(,…,),,…,)为真。也就是对任意的,…,都有一个f(,…,)使()…()M(,…,,f(,…,),,…,)为真。这便是IG1下( )…()()()…()M( ,…,,…,)为真，也即 G|IG1＝T。 但这与假设G是不可满足的相矛盾，从而G不可满足必有G1不可满足。 再证明  知G1是不可满足的，而假设G是可满足的。于是便有某个解释IG使G|IG＝T。即对任意的 ,…,在IG的设定下都可找到一个使( )
…()
M(,…,,…,)为真。对G1来说不管怎样设定函数f( ,…,)都可构成IG1令数f(,…,)的值就取找到的这个。这样由IG再考虑到f(,…,)=的设定便构成公式G1的一个解释IG1，且在IG1下对任意的
,…,
都有 ( )…()M(,…,,f(,…,),,…,)为真。这便是G|IG1＝T，但这与假设G1是不可满足相矛盾，从而G1不可满足必有G不可满足。 定理得证。 |
|
 |
例1: |
| G=(x)P(x)的SKOLEM
标准形与G并不是等值的。 考虑论域为D＝{1,2}，这时 G＝( x)P(x)=P(1)∨P(2)取IG： P(1)＝F P(2)＝T 有 G|IG＝T 而G的 SKOLEM 标准形 G1＝P(a) 若取a 为1这时G1＝F，与G不等值。 直观地说，G1是G的一个具体的例化，考虑到存在量词有"或"的含义，自然不能保证G真必有G1真。( x)P(x)为真，只要在论域D中找到一个个体x0使P(x0)为真。而G1＝P(a)是从论域中选定一个个体a,这样不能保证P(a)为真。 |
|
|
例2: |
| G＝(x)(y)P(x,y) G1＝( x)P(x,f(x))考虑G与G1的逻辑关系。仍在论域D＝{1,2}上讨论。便有 G＝(P(1,1)∨P(1,2))∧(P(2,1)∨P(2,2)) 取IG: P(1,1)=T,P(1,2)=F ,P(2,1)=F ,P(2,2)=T 有 G|IG ＝T G1＝P(1,f(1))∧P(2,f(2)) 显然IG下不能决定G1的真值，因为尚需对 SKOLEM 函数f(1),f(2)做设定。或说IG不是公式G1的解释。若设定f(1)=2,f(2)=2方构成G1的一个解释 IG1= IG∪{f(1)=2 ,f(2)=2} 然而 G1|IG1=F。同例1一样，G1只是G的一个示例，不能保证G真G1必真。 然而反过来却有 G1|IG1=T G|IG=T也即 G1
G 一般情形下有 S
G总之，S与G并不等值，但在不可满足的意义下是一致的。而且G是S的逻辑推论，反过来不成立。 |
2.2.4 G＝G1∧…∧Gn的子句形
设Si是Gi i=1…n的子句形，不难看出，公式G的子句形SG不是S1∪…∪Sn ，而且SG常较S1∪…∪Sn 来得复杂得多。令人满意的是S1∪…∪Sn 与SG在不可满足的意义上说是一致的，也就是说SG不可满足
S1∪…∪Sn 不可满足这样对SG的讨论，可以较为简单的S1∪…∪Sn 来代替，为方便也称S1∪…∪Sn 为G的子句形。下面这些例子所建立的子句集，都是S1∪…∪Sn 。