第四章归结法原理.ppt

《第四章归结法原理.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第四章归结法原理张玉平第二章归结法原理命题逻辑的归结法前束范式与斯科伦范式谓词逻辑的归结法命题逻辑的归结法子句归结子句反驳子句定义：文字的有穷集合称为子句。不包含任何文字的子句称为空子句，记为□。如果真值赋值v满足子句集S中的每个子句，则称v满足S。如果至少有一个真值赋值满足子句集S，则称S是可满足的，否则称S是不可满足的。归结子句设L1,L2是相反文字，并且分别在子句C1和C2中出现，称子句(C1-{L1})(C2-{L2})为C1和C2的归结子句。反驳如果子句C1,…,Cn序列满足以下条件，

2、则称该子句序列为子句集合S的一个反驳。(1)对每个i≤n，Ci∈S或者存在j,k

3、A1∨…∨An为简单析取式。若B1,…,Bn是简单析取式，则称B1∧…∧Bn为合取范式。斯科伦范式母式是合取范式的无前束范式称为斯科伦范式。谓词逻辑的归结法相反文字基子句子句集的满足性赫布兰德解释归结推演相反文字如果一个文字恰为另一个文字的否定，则称它们为相反的文字。文字的有穷集合称为子句。不包含任何文字的子句称为空子句，记为□。基子句不出现变元的文字称为基文字，基文字的有穷集合称为基子句。子句集合的满足性若解释I满足子句集合S中的每个子句，则称I满足S，记为I

4、=S。如果至少有一个解释满足子句

5、集合S，则称是S可满足的，否则称S是不可满足的。每个子句集对应一个没有自由变元的斯科伦范式，解释满足子句集当且仅当它满足对应的斯科伦范式。赫布兰德解释满足以下条件的解释称为赫布兰德解释：(1)I的论域是全体基项组成的集合。(2)对每个常元a，aI=a。(3)对每个元函数符号f，fI(t1,…tn)=f(t1,…,tn)归结推演设S是子句集合。如果非空子句序列C1,…,Cn中的每个子句Ci满足以下条件之一，则称该子句序列为S的一个归结推演。(1)Ci在S中；(2)存在j,k

6、的归结子句。如果S的归结推演C1,…,Cn的最后一个子句Cn是空子句□，则称C1,…,Cn为S的一个反驳。