定义2对一个谓词公式G,通过以下步骤所得的 子句集合S,称为G的子句集 1)消去蕴含词→和等值词 (2)缩小否定词一的作用范围,直到其仅作用于原子公式。 (3)适当改名,使量词间不含同名指导变元和约束变元。 (4)消去存在量词。 (5)消去所有全称量词。 (6)化公式为合取范式。 (7)适当改名,使子句间无同名变元。 (8)消去合取词∧,以子句为元素组成集合S
定义2 对一个谓词公式G，通过以下步骤所得的 子句集合S，称为G的子句集。 (1)消去蕴含词→和等值词←→ 。 (2)缩小否定词﹁的作用范围，直到其仅作用于原子公式。 (3)适当改名，使量词间不含同名指导变元和约束变元。 (4)消去存在量词。 (5)消去所有全称量词。 (6)化公式为合取范式。 (7)适当改名，使子句间无同名变元。 (8)消去合取词∧，以子句为元素组成集合S
定理1谓词公式G不可满足当且仅当其子句集 S不可满足。 定义3子句集S是不可满足的,当且仅当其全 部子句的合取式是不可满足的
定理1 谓词公式G不可满足当且仅当其子句集 S不可满足。 定义3 子句集S是不可满足的，当且仅当其全 部子句的合取式是不可满足的
5.2.2命题逻辑中的归结原理 定义设C1,C2是命题逻辑中的两个子句,C1 中有文字L1,C2中有文字L2,且L1与L2互补,从 C1,C2中分别删除L1,L2,再将剩余部分析取起来, 记构成的新子句为C12,则称C12为C1,C2的归结 式(或消解式),C1,C2称为其归结式的亲本子句 L1,L2称为消解基 例59设C1=- PVOVR,C2=-QVS,则 C1,C2的归结式为 PVRVS
5.2.2 命题逻辑中的归结原理 定义 设C1,C2是命题逻辑中的两个子句，C1 中有文字L1，C2中有文字L2，且L1与L2互补，从 C1,C2中分别删除L1,L2，再将剩余部分析取起来， 记构成的新子句为C12，则称C12为C1,C2的归结 式(或消解式)，C1,C2称为其归结式的亲本子句， L1,L2称为消解基。 例5.9 设C1= ﹁ P∨Q∨R, C2= ﹁ Q∨S, 则 C1,C2的归结式为 ﹁ P∨R∨S
定理2归结式是其亲本子句的逻辑结果。 由定理2即得推理规则: C1∧C2冰=>(C1-{L1})U(C2-{L2)) 其中C1,C2是两个子句,L1,L2分别是C1C2中的文字, 且L1,L2互补。 此规则就是命题逻辑中的归结原理
定理2 归结式是其亲本子句的逻辑结果。 由定理2即得推理规则： C1∧C2＝＞ (C1-｛L1｝)∪(C2-｛L2｝) 其中C1,C2是两个子句，L1,L2分别是C1,C2中的文字， 且L1,L2互补。 此规则就是命题逻辑中的归结原理。
例3.10用归结原理验证分离规则和拒取式 A∧(A→B)=>B (A→→B)∧一B=>-A 解 A∧(A→B)=A∧(_AVB)=>B (A→B)∧B=(-AVB)∧(B)=>-A
例3.10 用归结原理验证分离规则和拒取式 A∧(A→B) ＝＞ B (A→B)∧﹁ B ＝＞﹁ A 解 A∧(A→B) ＝ A∧(﹁ A∨B) ＝＞ B (A→B)∧﹁ B ＝ (﹁ A∨B)∧(﹁ B) ＝＞ ﹁ A