国考经典逻辑推理

国考经典逻辑推理第一页，共一百二十七页，编辑于2023年，星期五2023/5/261第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第二页，共一百二十七页，编辑于2023年，星期五2023/5/262基本概念推理什么是推理：依据一定的规则（策略）从已知的事实推出新事实（结论）的过程称为推理。第三页，共一百二十七页，编辑于2023年，星期五2023/5/263基本概念推理推理方式及其分类p.112

演绎推理、归纳推理（完全与否）、默认推理确定推理、不确定推理单调推理、非单调推理启发式推理、非启发式推理

…………第四页，共一百二十七页，编辑于2023年，星期五2023/5/264基本概念推理推理的控制策略，即求解问题的策略。有推理方向、搜索策略、冲突消解策略、求解策略及限制策略等。推理方向正向推理：由原始数据出发寻找可用的知识得出新事实，如此继续直至得到结论。自底向上（bottom-up），事实驱动方式。反向推理：先提出假设，由此出发，进一步寻找支持假设的证据，当所需证据与用户提供原始数据相匹配则成功。自顶向下（top-down），目标驱动方式。第五页，共一百二十七页，编辑于2023年，星期五2023/5/265基本概念正向推理过程规则集中的规则与数据库中的事实进行匹配，得到匹配的规则集合。从匹配的规则集合中选择一条规则作为使用规则。执行使用规则的后件。将该使用规则的后件输入数据库。重复进行，直到达到目标。第六页，共一百二十七页，编辑于2023年，星期五2023/5/266基本概念正向推理算法（产生式系统）断言一个事实使事实与某个规则的前提相匹配完成事实和前提的合一代换把代换应用于规则的结论断言结果，并把它应用于进一步的推理重复1）~5）第七页，共一百二十七页，编辑于2023年，星期五2023/5/267基本概念正向推理算法流程还有适用知识输入信息从KB中选择合适知识新结果存入数据库进行推理无解退出有适用知识DB是否有解输出解结果是新的YYYYNNNN第八页，共一百二十七页，编辑于2023年，星期五2023/5/268基本概念设计一正向推理系统能用数据库（黑板）中的事实去匹配规则的前提，若匹配不成功，能自动地进行下一条规则的匹配，在匹配时，采用什么策略等问题应考虑周到。若某条规则匹配成功了，系统能将此规则的结论部分自动加入数据库。能判断什么时候结束推理。能将匹配成功的规则记录下来。第九页，共一百二十七页，编辑于2023年，星期五2023/5/269基本概念反向推理过程用规则集中的规则后件与目标事实进行匹配，得到匹配的规则集合。从匹配的规则集合中选择一条规则作为使用规则。把执行的使用规则的前件作为下一个循环的目标事实。重复进行，直到达到目标。第十页，共一百二十七页，编辑于2023年，星期五2023/5/2610基本概念反向推理算法（产生式系统）提出获取事实（目标）的请求目标和任何已知的事实都不匹配目标和一条规则的结论匹配进行目标和结论的合一代换将代换应用于规则的前提这个结论成为系统的新目标新目标将执行动作

8)重复1）~7）匹配知识库中的事实匹配规则的结论，以更进一步推理要求用户回答必要的信息失败，原目标也失败第十一页，共一百二十七页，编辑于2023年，星期五2023/5/2611基本概念反向推理算法流程问用户有此证据找一个假设此假设为真结束在事实库有证据还有假设YYYYNNNN找出结论部分含此假设的所有知识此假设为假存入事实库选一条知识让它的条件作为新假设第十二页，共一百二十七页，编辑于2023年，星期五2023/5/2612基本概念设计一反向推理系统能根据用户要求或情况提出假设。能验证此假设是否在数据库中。能从知识库中将结论部分包含此假设的规则都找出来。能将找出来的规则的前提部分取出并作为新假设逐条验证。能判断假设是否是证据节点，若是，能向用户提出相应问题并记录结果。能将匹配成功的规则记录下来。能判断何时应结束推理。第十三页，共一百二十七页，编辑于2023年，星期五2023/5/2613基本概念推理冲突消解策略1规则排序：规则的编排顺序就是规则启用的优先级。专一性排序：若某一规则的条件部分规定的情况比另一条规则的条件部分所规定的情况更专门，则这条规则有较高的优先级。就近排序：把最近使用的规则放在最优先的位置。规模排序：按规则条件部分复杂程度排序，越复杂越优先。第十四页，共一百二十七页，编辑于2023年，星期五2023/5/2614基本概念推理冲突消解策略2数据排序：把规则条件部分的所有条件项按优先级次序组织，可用知识的次序由这些知识所含条件按字典排序方法进行选择。上下文限制：按问题求解状态或新描述的上下文分块组织知识库，在某一求解状态，只能使用相对应组中的知识。数据冗余限制：若知识的操作产生上下文冗余项时，则降低该知识的优先级。第十五页，共一百二十七页，编辑于2023年，星期五2023/5/2615基本概念模式匹配（代换与合一）什么叫模式匹配：是指对两个知识模式（谓词公式、框架片断、语义网络片断等）的比较与耦合，即检查这两个知识模式是否完全一致或近似一致。模式匹配有确定性匹配与不确定性匹配。什么叫合一：一个表达式（公式）的项可以是常量、变量或函数，合一就是寻找项对变量的代换而使得表达式（公式）一致的过程。合一是AI中很重要的过程。第十六页，共一百二十七页，编辑于2023年，星期五2023/5/2616基本概念模式匹配（代换与合一）定义4.1代换：有序对的集合S={t1/x1,t2/x2,…,tn/xn}

表示代换。其中ti/xi表示在公式中用ti代替xi

。例：公式P[x,f(y),B]s1={z/x,w/y}则P[z,f(w),B]s2={A/y}则P[x,f(A),B]s3={g(z)/x}则P[g(z),f(y),B]用代换s作用于公式E所得到的式子记为Es

第十七页，共一百二十七页，编辑于2023年，星期五2023/5/2617基本概念模式匹配（代换与合一）定义4.2代换的复合：设有={t1/x1,t2/x2,…,tn/xn}

和={u1/y1,u2/y2,…,un/yn}是两个代换。则两个代换的复合也是一个代换。={t1/x1,t2/x2,…,tn/xn，u1/y1,u2/y2,…,um/ym}

其中

ti

xi

并且

yi{x1,x2,…,xn}

例：

s1={g(x,y)/z,u/w}s2={A/x,B/y,C/w,D/z,w/u}

则s1s2={g(A,B)/z,A/x,B/y,w/u}性质：满足结合律，而不满足交换律（1）2=（12），而一般1221

第十八页，共一百二十七页，编辑于2023年，星期五2023/5/2618基本概念模式匹配（代换与合一）定义4.3可合一：设有公式集合F={F1,F2,…,Fn},若存在一个代换使得

F1=F2=…=Fn

，则称公式集F是可合一的。称为公式集F的一个合一。例：F={P[x,f(y),B],P[x,f(B),B]}

则s1={A/x,B/y}是公式集F的一个合一

s2={B/y}也是公式集F的一个合一第十九页，共一百二十七页，编辑于2023年，星期五2023/5/2619基本概念模式匹配（代换与合一）定义4.4最一般合一mgu(MostGeneralUnifier)：设是公式集F的一个合一，如果对任一个合一都存在一个代换，使得=则称是一个最一般的合一。可以证明mgu是唯一的。求mgu算法第二十页，共一百二十七页，编辑于2023年，星期五2023/5/2620基本概念求mgu算法（设公式集为F）：令k=0,Fk=F,k=。是一个空代换。若Fk只含一个表达式，则算法停止，k即为所求的mgu。找出Fk的差异集Dk

。若Dk中存在元素xk和tk

，其中xk是变元，tk是项，且xk不在tk中出现，则置：k+1=k{tk/xk},Fk+1=Fk{tk/xk},k=k+1,

然后转2）算法终止，F的mgu不存在第二十一页，共一百二十七页，编辑于2023年，星期五2023/5/2621基本概念求mgu举例：

F={P[f(x),y,g(y)],P[f(x),z,g(x)]}

k=0,F0=F,0=,D0={y,z}1=0{y/z}={y/z}F1=F0{y/z

}={P[f(x),y,g(y)],P[f(x),y,g(x)]}k=1,D1={y,x},2=1{y/x}={y/z,y/x}F2=F1{y/z,y/x

}={P[f(y),y,g(y)],P[f(y),y,g(y)]}F2只含一个表达式，则算法停止，2即为所求的mgu。mgu={y/z,y/x}第二十二页，共一百二十七页，编辑于2023年，星期五2023/5/2622基本概念归结原理由J.A.Robinson由1965年提出。与演绎法完全不同，新的逻辑演算算法。>>>一阶逻辑中，至今为止的最有效的半可判定的算法。即，一阶逻辑中任意恒真公式，使用归结原理，总可以在有限步内给以判定。语义网络、框架表示、产生式规则等等都是以推理方法为前提的。即，有了规则已知条件，顺藤摸瓜找到结果。而归结方法是自动推理、自动推导证明用的。（“数学定理机器证明”）本课程只讨论一阶谓词逻辑描述下的归结推理方法，不涉及高阶谓词逻辑问题。

第二十三页，共一百二十七页，编辑于2023年，星期五2023/5/2623第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第二十四页，共一百二十七页，编辑于2023年，星期五2023/5/2624第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第二十五页，共一百二十七页，编辑于2023年，星期五2023/5/2625命题逻辑的归结法归结反演推理方法基本思想例：

命题：A1、A2、A3

和B求证：A1∧A2∧A3成立，则B成立，即：A1∧A2∧A3→B反证法：证明A1∧A2∧A3∧B是矛盾式（永假式）

归结法是以子句集为背景的第二十六页，共一百二十七页，编辑于2023年，星期五2023/5/2626子句的概念子句与子句集文字：不含任何连接词的谓词公式及其否定。子句(定义4.5)

：任何文字的析取式（谓词的和）。空子句(定义4.6)

：不含任何文字的子句。空子句的不可满足性：由于空子句不含任何文字，它不能被任何解释满足，所以空子句是永假的，不可满足的。子句集：由子句构成的集合。第二十七页，共一百二十七页，编辑于2023年，星期五2023/5/2627子句的概念建立子句集合取范式：命题、命题和的与，如：

P∧

（P∨Q）∧（

P∨Q）子句集S：合取范式形式下的子命题（元素）的集合例：命题公式：P∧（P∨Q）∧（P∨Q）子句集S：S={P,P∨Q,P∨Q}第二十八页，共一百二十七页，编辑于2023年，星期五2023/5/2628子句的概念谓词公式F相对应的子句集S的求取：F→SKOLEM标准形 →消去全称变量 →以“，”取代“∧”，并表示为集合形式。第二十九页，共一百二十七页，编辑于2023年，星期五2023/5/2629命题逻辑的归结法归结过程

将命题写成合取范式求出子句集对子句集使用归结推理规则归结式作为新子句参加归结归结式为空子句□，S是不可满足的（矛盾），原命题成立。

（证明完毕）谓词的归结：除了有量词和函数以外，其余和命题归结过程一样。第三十页，共一百二十七页，编辑于2023年，星期五2023/5/2630第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第三十一页，共一百二十七页，编辑于2023年，星期五2023/5/2631第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第三十二页，共一百二十七页，编辑于2023年，星期五2023/5/2632子句形—谓词公式化为子句集步骤1消去蕴含符号PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}第三十三页，共一百二十七页，编辑于2023年，星期五2023/5/2633子句形—谓词公式化为子句集步骤1消去蕴含符号PQP∨Q例：(x){P(x){(y)[P(y)P(f(x,y))]∧

(y)[Q(x,y)P(y)]}}(x){P(x)

∨{(y)[P(y)

∨P(f(x,y))]∧

(y)[Q(x,y)

∨P(y)]}}第三十四页，共一百二十七页，编辑于2023年，星期五2023/5/2634子句形—谓词公式化为子句集步骤2减少否定符号的辖域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}第三十五页，共一百二十七页，编辑于2023年，星期五2023/5/2635子句形—谓词公式化为子句集步骤2减少否定符号的辖域(P)

P(P∧Q)

P∨Q或(P∨Q)

P∧Q(x)P(x)(x)P(x)或(x)P(x)(x)P(x)

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}第三十六页，共一百二十七页，编辑于2023年，星期五2023/5/2636子句形—谓词公式化为子句集步骤2例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)

[Q(x,y)∨P(y)]}}(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}第三十七页，共一百二十七页，编辑于2023年，星期五2023/5/2637子句形—谓词公式化为子句集步骤3变量标准化，即重新命名变元保证每个量词有其唯一的约束变量。如：(x){P(x)(x)Q(x)}标准化为(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

第三十八页，共一百二十七页，编辑于2023年，星期五2023/5/2638子句形—谓词公式化为子句集步骤3变量标准化，即重新命名变元保证每个量词有其唯一的约束变量。如：(x){P(x)(x)Q(x)}标准化为(x){P(x)(y)Q(y)}

例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(y)[

Q(x,y)∧

P(y)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}第三十九页，共一百二十七页，编辑于2023年，星期五2023/5/2639子句形—谓词公式化为子句集步骤4消去存在量词如：(x)P(x,y)用P(A,y)

替换，A为某一常量。如：(y){(x)P(x,y)}引入Skolem函数g(y)，用(y)

P(g(y),y)

替换例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}第四十页，共一百二十七页，编辑于2023年，星期五2023/5/2640子句形—谓词公式化为子句集步骤4消去存在量词如：(x)P(x,y)用P(A,y)

替换，A为某一常量。如：(y){(x)P(x,y)}引入Skolem函数g(y)，用(y)

P(g(y),y)

替换例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧

(w)[

Q(x,w)∧

P(w)]}}

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十一页，共一百二十七页，编辑于2023年，星期五2023/5/2641子句形—谓词公式化为子句集步骤4消去存在量词

量词消去原则： 消去存在量词“”，略去全称量词“”。

注意：左边有全称量词的存在量词，消去时该变量改写成为全称量词的函数；如没有，改写成为常量。

第四十二页，共一百二十七页，编辑于2023年，星期五2023/5/2642子句形—谓词公式化为子句集步骤5化为前束形如把所有全称量词移到公式的左边，并使得每个量词的辖域包含这个量词后面公式的整个部分，所得公式称为前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十三页，共一百二十七页，编辑于2023年，星期五2023/5/2643子句形—谓词公式化为子句集步骤5化为前束形如把所有全称量词移到公式的左边，并使得每个量词的辖域包含这个量词后面公式的整个部分，所得公式称为前束形。例：

(x){P(x)∨{(y)[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}

(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十四页，共一百二十七页，编辑于2023年，星期五2023/5/2644子句形—谓词公式化为子句集步骤6化前束形为SKOLEM标准形前束范式：把所有的量词都提到前面去，然后消掉所有量词。

定义：说公式A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。SKOLEM标准形==（全称量词串）{母式}

母式：子句的合取式第四十五页，共一百二十七页，编辑于2023年，星期五2023/5/2645子句形—谓词公式化为子句集步骤6化前束形为SKOLEM标准形反复利用分配率，把任一个母式化为合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)∨{

[P(y)∨P(f(x,y))]∧[

Q(x,g(x))∧

P(g(x))]}}第四十六页，共一百二十七页，编辑于2023年，星期五2023/5/2646子句形—谓词公式化为子句集步骤6化前束形为SKOLEM标准形反复利用分配率，把任一个母式化为合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){{P(x)

∨[P(y)∨P(f(x,y))]}∧{P(x)

∨[

Q(x,g(x))∧

P(g(x))]}}第四十七页，共一百二十七页，编辑于2023年，星期五2023/5/2647子句形—谓词公式化为子句集步骤6化前束形为SKOLEM标准形反复利用分配率，把任一个母式化为合取范式。A∨(B∧

C)

(A∨B)∧(A∨C)

例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}第四十八页，共一百二十七页，编辑于2023年，星期五2023/5/2648子句形—谓词公式化为子句集步骤6化前束形为SKOLEM标准形例：(x)(y){P(x)

∨{

[P(y)∨P(f(x,y))]

∧

[

Q(x,g(x))∧

P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧{P(x)

∨[

Q(x,g(x))

∧P(g(x))]}}(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)

∨Q(x,g(x))]∧[P(x)

∨

P(g(x))]}第四十九页，共一百二十七页，编辑于2023年，星期五2023/5/2649子句形—谓词公式化为子句集步骤7消去全称量词例：

(x)(y){[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]}[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))]第五十页，共一百二十七页，编辑于2023年，星期五2023/5/2650子句形—谓词公式化为子句集步骤8对变元更名使得一个变元符号不出现在一个以上的子句中。例：

[P(x)∨P(y)∨P(f(x,y))]∧[P(x)∨Q(x,g(x))]∧[P(x)∨

P(g(x))][P(x)∨P(y)∨P(f(x,y))]∧[P(z)∨Q(z,g(z))]∧[P(w)∨

P(g(w))]第五十一页，共一百二十七页，编辑于2023年，星期五2023/5/2651子句形—谓词公式化为子句集步骤9消去合取符号用子句集代替合取式，即为所求的子句集。例：

[P(x)∨P(y)∨P(f(x,y))]∧[P(z)∨Q(z,g(z))]∧[P(w)∨

P(g(w))]{P(x)∨P(y)∨P(f(x,y))，P(z)∨Q(z,g(z))，P(w)∨

P(g(w))}第五十二页，共一百二十七页，编辑于2023年，星期五2023/5/2652子句形定理： 谓词逻辑的任意公式都可以化为与之等价的前束范式，但其前束范式不唯一。SKOLEM标准形定义： 消去量词后的谓词公式。注意：谓词公式F的SKOLEM标准形同F并不等值。第五十三页，共一百二十七页，编辑于2023年，星期五2023/5/2653子句形F是不可满足的S是不可满足的F与S不等价，但在不可满足的意义下是一致的。

定理： 若F是给定的公式，而S是相应的子句集，则F是不可满足的

S是不可满足的。

注意：F真不一定S真，而S真必有F真。 即：S

F第五十四页，共一百二十七页，编辑于2023年，星期五2023/5/2654子句形把F的不可满足判断S的不可满足引用Herbrand定理，研究S的不可满足性。引用Herbrand定理，以说明归结原理的意义及一个原理形成的根基与背景

第五十五页，共一百二十七页，编辑于2023年，星期五2023/5/2655第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第五十六页，共一百二十七页，编辑于2023年，星期五2023/5/2656第四章经典逻辑推理基本概念命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第五十七页，共一百二十七页，编辑于2023年，星期五2023/5/2657Herbrand定理名词:

公式F永真:对于F的所有解释,F都为真.

公式F永假:没有一个解释使F为真.问题： 要判定一个子句集是不可满足的,就是要判定该子句集中的每一个子句都是不可满足的;要判定一个子句是不可满足的,则需要判定该子句对任何非空个体域的任意解释都是不可满足的.可见,判定子句集的不可满足性是一件非常困难的工作.

第五十八页，共一百二十七页，编辑于2023年，星期五2023/5/2658Herbrand定理问题： 一阶逻辑公式的永真性（永假性）的判定是否能在有限步内完成？第五十九页，共一百二十七页，编辑于2023年，星期五2023/5/2659Herbrand定理1936年图灵(Turing)和邱吉(Church)互相独立地证明了：“没有一般的方法使得在有限步内判定一阶逻辑的公式是否是永真（或永假）。但是如果公式本身是永真（或永假）的，那么就能在有限步内判定它是永真（或永假）。对于非永真（或永假）的公式就不一定能在有限步内得到结论。判定的过程将可能是不停止的。”

第六十页，共一百二十七页，编辑于2023年，星期五2023/5/2660Herbrand定理Herbrand的思想要证明一个公式是永假的,采用反证法思想,就是寻找一个已给的公式是真的解释。然而，如果所给定的公式的确是永假的，就没有这样的解释存在，并且算法在有限步内停止。因为量词是任意的，所讨论的个体变量域D是任意的，所以解释的个数是无穷的，不可数的，要找到所有解释是不可能的。第六十一页，共一百二十七页，编辑于2023年，星期五2023/5/2661Herbrand定理Herbrand的思想思想：判断任何一个解释是困难的。所以简化讨论域，建立一个比较简单、特殊的域，使得只要在这个论域上，原谓词公式仍是不可满足的，即保证不可满足的性质不变。因此引入H域等概念。D域H域H域与D域关系示意图第六十二页，共一百二十七页，编辑于2023年，星期五2023/5/2662Herbrand定理H域H解释结论：Herbrand定理第六十三页，共一百二十七页，编辑于2023年，星期五2023/5/2663Herbrand定理H域H解释结论：Herbrand定理第六十四页，共一百二十七页，编辑于2023年，星期五2023/5/2664Herbrand定理（H域）H域构造方法（定义4.7）：设S为公式F所对应的子句集，则按下述方法构造的域H称为H域。令H0是S中所有个体常量的集合，若S中不含个体常量，则令H0={a}，其中a为任一个体常量。令Hi+1=Hi∪

{S中所有形如f(x1,x2,……,xn)的元素}，其中f(x1,x2,……,xn)是出现在F中任一函数符号，i=0,1,2,3,…。

※

例题请参考教科书P128第六十五页，共一百二十七页，编辑于2023年，星期五2023/5/2665Herbrand定理（H域）例题1:

S={P(a),P(x)∨P(f(x))},求H域。H0={a}H1={a,f(a)}H2={a,f(a),f(f(a))}H=H0∪H1∪H2∪......={a,f(a),f(f(a)),……}例题2:

S={P(z),

P(x)∨Q(y)},求H域。H0={a}H1={a}H2={a}H=H0∪H1∪H2∪......={a}第六十六页，共一百二十七页，编辑于2023年，星期五2023/5/2666Herbrand定理（H域）例题3:

S={P(x),Q(y,f(z,b)),R(a)},求H域。H0={a,b}H1={a,b,f(a,b),f(b,b)}H2={a,b,f(a,b),f(b,b),f(f(a,b),b),f(f(b,b),b),……}H=H0∪H1∪H2∪......

={a,b,f(a,b),f(b,b),……}第六十七页，共一百二十七页，编辑于2023年，星期五2023/5/2667Herbrand定理（H域）几个基本概念基子句：用H域中的元素代换子句中的变元所得到的子句，即不含变量的子句。基原子：基子句中的谓词，即没有变量出现的原子。原子集A：子句集中所有基原子构成的集合。如

A={所有形如P(t1,t2,…tn)的元素}

（其中P(t1,t2,…tn)

是出现于S中的任一谓词符号，而t1,t2,…tn

是S的H域的任意元素）

即把H中的东西填到S的谓词里去。S中的谓词是有限的，H是可数的，因此，A也是可数的。第六十八页，共一百二十七页，编辑于2023年，星期五2023/5/2668Herbrand定理（H域）原子集举例:S={P(a),P(x)∨P(f(x))},H={a,f(a),f(f(a)),……}

A={P(a),P(f(a)),P(f(f(a))),……}S={P(z),

P(x)∨Q(y)},H={a}

A={P(a),Q(a)}S={P(x),Q(y,f(z,b)),R(a)},H={a,b,f(a,b),f(a,a),f(b,a),f(b,b),…}

A={P(a),P(b),Q(a,a),Q(a,b),R(a),R(b),……}第六十九页，共一百二十七页，编辑于2023年，星期五2023/5/2669Herbrand定理（H域）原子集一旦原子集内真值确定好（规定好），则S在H上的真值可确定。S中的谓词是有限的，可数的，H域中的元素是可数的，因此，原子集A中的元素也是可数的。由此可见，在无限不可数的个体域D上的问题转化成为可数的问题。把谓词公式的不可满足性讨论从D转换到H域，其复杂程度得到相应减少。不可解问题变为可解问题。第七十页，共一百二十七页，编辑于2023年，星期五2023/5/2670Herbrand定理H域H解释结论：Herbrand定理第七十一页，共一百二十七页，编辑于2023年，星期五2023/5/2671Herbrand定理H域H解释结论：Herbrand定理第七十二页，共一百二十七页，编辑于2023年，星期五2023/5/2672Herbrand定理（H解释）H解释I（定义4.8）：取一个值得到一个结论解释I：谓词公式F在论域D上任何一组真值的指定称为一个解释。公式F的一个解释就是公式F在其论域上的一个实例化。H解释：子句集S在其H域上的解释称为H解释。子句集S在H域上的一个解释I满足下列条件：I映射S中所有常量符号到它们本身。(即原子集)令f是n元函数，I是f下的一个指派，即H中的元素到f的一个映射（函数值）。简单地说(P129)，A中的各元素真假组合都是H的解释。（或真或假只取一个）第七十三页，共一百二十七页，编辑于2023年，星期五2023/5/2673Herbrand定理（H解释）例：子句集S={P(x)∨Q(x),R(f(y))}有

H域H={a,f(a),f(f(a)),……}

原子集A={P(a),Q(a),R(a),P(f(a)),Q(f(a)),R(f(a)),……}

凡是对A中各元素真假值的一个具体设定都是S的一个H解释。如

I1*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}I2*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}I3*={P(a),Q(a),R(a),Q(f(a)),R(f(a)),……}

I1*I2*I3*中出现的P(a)指P(a)取值为T，出现的

P(a)指P(a)取值为F。第七十四页，共一百二十七页，编辑于2023年，星期五2023/5/2674Herbrand定理（H解释）I1*I2*I3*中出现的P(a)指P(a)取值为T，出现的

P(a)指P(a)取值为F。显然在H域上，这样定义I*下，S的真假值就确定了。如问题：对于所有的解释，全是假才可判定。因为所有解释代表了所有的情况，如果可以被穷举，问题便可解决。一般来说，一个子句集的基原子有无限多个，它在H域上的解释也有无限多个。

S的不可满足问题

H上的不可满足问题，有Herbrand定理支持。第七十五页，共一百二十七页，编辑于2023年，星期五2023/5/2675Herbrand定理（H解释）如下三个定理保证了归结法的正确性：定理1（定理4.2’）

：

设I是S的论域D上的解释，存在对应于I的H解释I*，使得若有S|I=T，必有S|I*=T。定理2（定理4.2）

： 子句集S是不可满足的，当且仅当所有的S的H解释下为假。定理3（定理4.3）

： 子句集S是不可满足的，当且仅当对每一个解释I下，至少有S的某个子句的某个基例为假。第七十六页，共一百二十七页，编辑于2023年，星期五2023/5/2676Herbrand定理（H解释）基例S中某子句中所有变元符号均以S的H域中的元素代入时，所得的基子句C’称为C的一个基例。若一个子句为假，则此解释为假。一般来说，D是无穷不可列的，因此，子句集S也是无穷不可列的。但S确定后H是无穷可列的。不过在H上证明S的不可满足性仍然是不可能的。计算机实现是困难的，提出归结原理第七十七页，共一百二十七页，编辑于2023年，星期五2023/5/2677Herbrand定理H域H解释结论：Herbrand定理第七十八页，共一百二十七页，编辑于2023年，星期五2023/5/2678Herbrand定理H域H解释结论：Herbrand定理第七十九页，共一百二十七页，编辑于2023年，星期五2023/5/2679Herbrand定理（结论）Herbrand定理：子句集S是不可满足的，当且仅当存在不可满足的S的有限基例集。

第八十页，共一百二十七页，编辑于2023年，星期五2023/5/2680Herbrand定理（结论）定理的意义Herbrand定理已将证明问题转化成了命题逻辑问题。由此定理保证，可以放心的用机器来实现自动推理了。（归结原理）注意Herbrand定理给出了一阶逻辑的半可判定算法，即仅当被证明定理是成立时，使用该算法可以在有限步得证。而当被证定理并不成立时，使用该算法得不出任何结论。但是

第八十一页，共一百二十七页，编辑于2023年，星期五2023/5/2681Herbrand定理（结论）仍存在的问题：基例集序列元素的数目随子句集的元素数目成指数增加。因此，Herbrand定理是30年代提出的，始终没有显著的成绩。直至1965年Robinson提出了归结原理，才使得Herbrand定理的光彩得以发挥。第八十二页，共一百二十七页，编辑于2023年，星期五2023/5/2682第四章经典逻辑推理概述命题逻辑的归结法子句形Herbrand定理归结原理归结过程的策略控制第八十三页，共一百二十七页，编辑于2023年，星期五2023/5/2683归结原理基本思想通过归结方法不断扩充待判定的子句集，并设法使其包含指示矛盾的空子句。空子句是不可满足（即永假）的子句（P.126），既然子句集中子句间隐含着合取关系，空子句的出现实际上判定了子句集的不可满足。定义4.9：若P是原子谓词公式，则称P与P为互补文字。第八十四页，共一百二十七页，编辑于2023年，星期五2023/5/2684命题逻辑的归结法归结（定义4.10）

设有子句C1,C2，如果C1中的文字L1与C2中的文字L2互补，则消除互补对，余下部分析取求得新子句→得到归结式C12

。例：C1

C2

C12

PP∨Q

Q假言推理

P∨QP∨Q

Q∨Q=Q合并

P∨QP∨

Q

Q∨

Q重言式

P∨QP∨

Q

P∨PPP

□或

NIL空子句

P∨QQ∨R

P∨R

三段论第八十五页，共一百二十七页，编辑于2023年，星期五2023/5/2685命题逻辑的归结法归结式性质定理4.4：两个子句C1和C2的归结式C12是C1和C2的逻辑推论，即C1∧C2C12（在任一个使子句C1和C2为真的解释I下，必有归结式C12为真）推论1：子句集S中子句C1和C2的归结式为C12，若用C12

代替C1和C2后得到新子句集S1，则S1不可满足性

S的不可满足性推论2：子句集S中子句C1和C2的归结式为C12，若把C12

加入S中得到新子句集S2，则S2不可满足性

S的不可满足性第八十六页，共一百二十七页，编辑于2023年，星期五2023/5/2686谓词逻辑的归结法归结（含有变量子句的归结，定义4.11）设有两个没有相同变元的子句C1,C2，L1是C1中的文字与L2是C2中的文字，若是L1和L2的mgu，则称C12=(C1

-{L1

})∨

(C2

-{L2

})为子句C1,C2的二元归结式。第八十七页，共一百二十七页，编辑于2023年，星期五2023/5/2687谓词逻辑的归结法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1为P[x,f(A)]，L2为

P[z,f(A)]

则={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x)例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(z)

取L1为Q(y)，L2为

Q(z)

则={y/z}得C12=P[x,f(A)]∨P[x,f(y)]∨

P[y,f(A)]

可进一步归结得到

P[x,f(x)]

第八十八页，共一百二十七页，编辑于2023年，星期五2023/5/2688谓词逻辑的归结法例：P[x,f(A)]∨P[x,f(y)]∨Q(y)P[z,f(A)]∨

Q(x)

修改C2变元名

P[z,f(A)]∨Q(x1)

取L1为P[x,f(A)]，L2为

P[z,f(A)]

则={x/z}得C12=P[x,f(y)]∨Q(y)∨Q(x)

则={x/z}得C12=P[x,f(y)]∨Q(y)∨

Q(x1)第八十九页，共一百二十七页，编辑于2023年，星期五2023/5/2689归结反演归结原理正确性的根本在于，找到矛盾可以肯定不真。方法：和命题逻辑一样。但由于有函数，所以要考虑合一和置换。第九十页，共一百二十七页，编辑于2023年，星期五2023/5/2690归结反演置换和合一的注意事项：谓词的一致性，P()与Q()，不可以常量的一致性，P(a,…)与P(b,….)，不可以 变量，P(a,….)与P(x,…)，可以变量与函数，P(a,x,….)与P(x,f(x),…)，不可以；但P(a,z,…)与P(x,f(y),…)，可以不能同时消去两个互补对，P∨Q与P∨Q的空，不可以先进行内部简化（置换、合并）第九十一页，共一百二十七页，编辑于2023年，星期五2023/5/2691归结反演—在定理证明中的应用归结反演的基本思想

目标公式被否定并化为子句集，添加到命题公式集中，用归结反演应用于联合集，并力图推导出一个空子句（□或NIL）表示产生一个矛盾，定理得证。第九十二页，共一百二十七页，编辑于2023年，星期五2023/5/2692归结反演—在定理证明中的应用归结反演的过程（证明F→Q）(P.133)写出谓词关系公式F（前提）和Q（目标、结论）否定目标Q加入公式集F,写出谓词表达式{F,Q}求SKOLEM标准形化为子句集S对S中可归结的子句做归结归结式仍放入S中，反复归结过程得到空子句□(NIL)

，得证第九十三页，共一百二十七页，编辑于2023年，星期五2023/5/2693归结反演—在定理证明中的应用证明：每个储蓄钱的人都获得利息，若没有利息就没有人去储蓄钱。令：S(x,y)表示x储蓄yM(x)表示x是钱

I(x)表示x是利息E(x,y)表示x获得y则前提为

(x)[(y)(

S(x,y)∧M(y))(y)(I(y)∧E(x,y))]

结论为

(x)I(x)(x)(y)(

S(x,y)

M(y))第九十四页，共一百二十七页，编辑于2023年，星期五2023/5/2694归结反演—在定理证明中的应用F:

(x)[(y)(

A(x,y)∧B(y))(y)(C(y)∧D(x,y))]

G:

(x)C(x)(x)(y)(

A(x,y)

B(y))F化为子句得

A(x,y)∨

B(y)∨C(f(x))………….(1)

A(x,y)∨

B(y)∨D(x,f(x))………….(2)

G化为子句得

C(z)……….(3)A(a,b)………..(4)B(b)……….(5)第九十五页，共一百二十七页，编辑于2023年，星期五2023/5/2695归结反演—在定理证明中的应用A(x,y)∨B(y)∨D(x,f(x))A(x,y)∨B(y)∨C(f(x))C(z)A(a,b)B(b)(1)(2)(3)(4)(5)NIL(8)B(b)∨C(f(a))(6){a/x,b/y}B(b)(7){f(a)/z}第九十六页，共一百二十七页，编辑于2023年，星期五2023/5/2696归结反演—在定理证明中的应用归结反演基本算法：给定公式F对应的子句集S，求证目标公式G成立。①CLAUSES←S∪{G}②UntilNIL是CLAUSES的成员，do：③begin④在子句集CLAUSES中选择二个不同的可归结的子句Ci,Cj⑤计算Ci,Cj的归结式Cij⑥CLAUSES←将Cij加入到CLAUSES中⑦end说明：可归结子句的选择次序可以是任意的。第九十七页，共一百二十七页，编辑于2023年，星期五2023/5/2697归结反演—在定理证明中的应用证明：梯形的对角线与上下底构成的内错角相等。xvuy梯形上下底平行平行内错角相等引入谓词：T(x,y,u,v)表示xy为上底，uv为下底的梯形。

P(x,y,u,v)表示xy//uv。

E(x,y,z,v,u,w)表示∠xyz=∠vuw。第九十八页，共一百二十七页，编辑于2023年，星期五2023/5/2698归结反演—在定理证明中的应用问题描述：A1:(x)(y)(u)(v)((T(x,y,u,v)P(x,y,u,v))

//上下底平行A2:(x)(y)(u)(v)((P(x,y,u,v)E(x,y,u,v,u,y))

//平行内错角相等A3:T(a,b,c,d)

G:E(a,b,d,c,d,b)第九十九页，共一百二十七页，编辑于2023年，星期五2023/5/2699归结反演—在定理证明中的应用化为子句：

A1:T(x,y,u,v)∨P(x,y,u,v)A2:P(x,y,u,v)∨E(x,y,u,v,u,y)A3:T(a,b,d,c)

G:E(a,b,d,c,d,b)acdb第一百页，共一百二十七页，编辑于2023年，星期五2023/5/26100归结反演—在定理证明中的应用

T(x,y,u,v)∨P(x,y,u,v)

P(x,y,u,v)∨E(x,y,u,v,u,y)T(a,b,d,c)

E(a,b,d,c,d,b)(1)(2)(3)(4)(6)(5)

P(a,b,d,c)

P(a,b,d,c)NIL第一百零一页，共一百二十七页，编辑于2023年，星期五2023/5/26101归结反演—在定理证明中的应用证明如下公式G是否为F的逻辑结论

F:答案:

是第一百零二页，共一百二十七页，编辑于2023年，星期五2023/5/26102归结反演—求解问题的答案基于归结法的问答系统问答系统要解决的问题形式：有二种类型：直接问答：求证当x=A时，G(A)成立。即：真假证明间接问答：求证当x=？时，G(x)成立。即：求值证明前面的证明方法都属于直接问答。间接问答方法需要采用构造方法。第一百零三页，共一百二十七页，编辑于2023年，星期五2023/5/26103归结反演—求解问题的答案例题：如果Peter去那儿，则John就去那儿。如果Peter在学校。问题：

John去哪儿？第一百零四页，共一百二十七页，编辑于2023年，星期五2023/5/26104归结反演—求解问题的答案解：用谓词公式表达所有前提以及结论。结论：第一百零五页，共一百二十七页，编辑于2023年，星期五2023/5/26105归结反演—求解问题的答案子句集：上面证明了：在给定前提下结论成立。但是没有给出：John在哪儿。解决问题的办法是：第一百零六页，共一百二十七页，编辑于2023年，星期五2023/5/26106归结反演—求解问题的答案解决问题的办法：①由目标公式的否定与目标公式的析取构成重言式(G∨G)，将其加入到公式集中，取代原来公式集中目标公式的否定式。②依据反演树的构造方法进行归结，直到得到某个子句为止。③以该子句作为对问题的回答。第一百零七页，共一百二十七页，编辑于2023年，星期五2023/5/26107归结反演—求解问题的答案上例中，用取代答案是：John在学校。第一百零八页，共一百二十七页，编辑于2023年，星期五2023/5/26108归结反演—求解问题的答案求解的过程(P.136)写出谓词关系公式F（已知前提）求SKOLEM标准形，化为子句集S写出待求解问题的谓词公式，然后把它否定并与形式谓词ANSWER构成析取式（变元一致）把该析取式化为子句集并入到S中，得到子句集S’对S’中可归结的子句做归结归结式仍放入S中，反复归结过程得到归结式ANSWER，则答案就在ANSWER中。问题得到解。第一百零九页，共一百二十七页，编辑于2023年，星期五2023/5/26109归结反演—求解问题的答案求猴子吃香蕉问题的答案：A1(x)(y)(z)(s)(P(x,y,z,s)P(z,y,z,Walk(x,z,s)))(猴子香蕉箱子各在一处…)A2(x)(y)(s)(P(x,y,x,s)P(y,y,y,Carry(x,y,s)))(猴先到箱处搬箱再到香蕉)A3(s)(P(b,b,b,s)R(Climb(s)))(同处,爬)A4P(a,b,c,s)(初始状态)A5R(s)∨ANS(s)第一百一十页，共一百二十七页，编辑于2023年，星期五2023/5/26110归结反演—求解问题的答案化为子句：A1P(x,y,z,s)∨P(z,y,z,Walk(x,z,s))………….(1)A2P(x,y,x,s)∨P(y,y,y,Carry(x,y,s))………….(2)A3P(b,b,b,s)∨R(Climb(s))…………..(3)A4P(a,b,c,s)…………..(4)A5R(s)∨ANS(s)…………..(5)第一百一十一页，共一百二十七页，编辑于2023年，星期五2023/5/26111归结反演—求解问题的答案归结P(x1,y,z,s3)∨P(z,y,z,Walk(x1,z,s3))(1)P(x,y,x,s2)∨P(y,y,y,Carry(x,y,s2))(2)P(a,b,c,s4)(4)

R(s1)∨ANS(s1)(5)P(b,b,b,s)∨R(Climb(s))(3)P(b,b,b,s)∨ANS(Climb(s))(6)P(x1,b,z,s3)∨ANS(Climb(Carry(z,b,Walk(x1,z,s3))))(8)ANS(Climb(Carry(c,b,Walk(a,c,s4))))(9){Climb(s)/s1}{b/y,Carry(x,b,s2)/s}{z/x,b/y,Walk(x1,z,s3)/s2}{a/x1,c/z,s4/s3}P(x,b,x,s2)∨

ANS(Climb(Car