(PQ) (PR)P ( P R) (Q P)( QR)
因为(P(QR)) ((PQ) (PR))的合取范式 计算机学院 (PQ) (PR)P ( P R) (Q P)( QR) 所以子句集合 Ω={ P,PQ, PQ, PR ,PR , QR}。
计算机学院
计算机学院
6
6
机械式方法
若证明Q1,…,Qn|=R，只要证明Q1…QnR 不可满足。 机械式证明：
• 公式Q1…QnR的合取范式； • 合取范式的所有简单析取范式，即Ω； • 证明Ω不可满足
则有Q1,…,Qn|=R。
计算机学院
机械式地证明Ω不可满足是关键问题
Q1=q
Q2=q Q3=□
Q1Ω
Q2Ω
计算机学院
因此，Q1, Q2,Q3是反驳.
计算机学院
15
15
(3).根据命题逻辑紧致性定理，若子句集合Ω 不可满足，则有有穷子句集合Ω0，Ω0Ω，使 得Ω0是不可满足的。
计算机学院
计算机学院
16
16
若有穷子句集合Ω0是不可满足的，则Ω0中的子句必 出现相反文字。 假设有穷子句集合Ω0是不可满足的，且Ω0中的子句 不出现相反文字，那么，对于Ω0中子句的每个文字 qk，有赋值函数σ使得σ(qk)=1，因此，σ(Ω0)=1，Ω0是 可满足的，这样与Ω0是不可满足的相矛盾。
(2).若Ω|=Qi，Ω|=Qj并且Qk是Qi, Qj的归结子句，则 Qi, Qj|=Qk。因此，Ω|=Qk。
(3).因为Qn=□，所以有Qn-1和Qk是相反文字，不妨设 是q和q。 计算机学院 因此，Ω|=q，Ω|=q。Ω|=qq，Ω不可满足。
计算机学院
14
14
又证：设子句集合Ω是不可满足的。 (1).不妨设子句集合Ω不含永真式。因为从Ω中去掉永真 式不改变Ω的不可满足性。 (2).若Ω含有相反文字，不妨设是q，则
归结法原理
马殿富 北航计算机学院 dfma@ 2012-4
主要内容
机械证明简介
命题逻辑归结法
谓词逻辑归结法
计算机学院
计算机学院
2
2
自动推理早期的工作主要集中在机器定理证明。 机械定理证明的中心问题是寻找判定公式是否是有效的 通用程序。 对命题逻辑公式，由于解释的个数是有限的，总可以建 立一个通用判定程序，使得在有限时间内判定出一个公 式是有效的或是无效的。 对一阶逻辑公式，其解释的个数通常是任意多个，丘奇 （A.Church）和图灵（A.M.Turing）在1936年证明了不存 计算机学院 在判定公式是否有效的通用程序。
计பைடு நூலகம்机学院
23
23
Q1= PQ Q2=PQ Q3=□
Q1Ω Q2Ω Q3= (Q1-P-Q) (Q2-P-Q) 分配律
P(QR)├ (PQ) (PR)
计算机学院
计算机学院
24
24
例题：PQR├(PR) (QR) 证明： (PQR) ((PR) (QR)) (( PQ) R) (PRQR)
计算机学院
计算机学院
22
22
例题：P(QR)├ (PQ) (PR) (P(QR)) ((PQ) (PR)) (P(QR)) ((PQ) (PR))
分配律
(PQ) (PR))( P (PR)) (Q (PR))
• 如果一阶逻辑公式是有效的，则存在通用程序可以验证它 是有效的 • 对于无效的公式这种通用程序一般不能终止。 计算机学院
3
3
1930年希尔伯特（Herbrand）为定理证明建立了一种重 要方法，他的方法奠定了机械定理证明的基础。 开创性的工作是赫伯特〃西蒙（H. A. Simon）和艾伦〃 纽威尔（A. Newel）的 Logic Theorist。 机械定理证明的主要突破是1965年由鲁宾逊（ J.A.Robinson）做出的，他建立了所谓归结原理，使机械 定理证明达到了应用阶段。 归结法推理规则简单, 而且在逻辑上是完备的, 因而成为 计算机学院 逻辑式程序设计语言Prolog的计算模型。
计算机学院 10 计算机学院
10
定理：如果子句Q是Q1, Q2的归结子句，则Q1, Q2|=Q 证明： 设Q1=pq1…qn，Q2=pr1…rm。
赋值函数σ(Q1)=1，即σ(pq1…qn)=1， σ(p) σ(q1…qn)=1.
赋值函数σ(Q2)=1，即σ(pr1…rm)=1， 计算机学院 σ(p) σ(r1…rm)=1. 有σ(q1…qn r1…rm)=1，即σ(Q)=1。 证毕
计算机学院
11
11
反驳
定义：设Ω是子句集合，如果子句序列 Q1,…,Qn满足如下条件，则称子句序列 Q1,…,Qn为子句集合Ω的一个反驳。 (1).对于每个1≤k<n，QkΩ
• Qk是Qi和Qj的归结子句，i<k，j<k。
(2). Qn是□。
计算机学院
计算机学院
12
12
例题：(QR)Q├Q 证明：
计算机学院
4
4
主要内容
机械证明简介
命题逻辑归结法
谓词逻辑归结法
计算机学院
计算机学院
5
5
基本原理
Q1,…,Qn|=R，当且仅当Q1…QnR不可满足
证明Q1,…,Qn|=R
• (1). Q1…QnR化为合取范式； • (2). 构建Ω子句集合，Ω为Q1…QnR合取范式 的所有简单析取范式组成集合； • (3).若Ω不可满足，则Q1,…,Qn|=R。
皮尔斯律
因为((QR)Q)Q的合取范式Q(RQ)Q，所以 子句集合Ω={Q, RQ, Q}
Q1 = Q
Q2= Q Q3=□
Q1Ω
Q2Ω Q3= (Q1-Q) (Q2-Q)
计算机学院
计算机学院
13
13
定理：子句集合Ω是不可满足的当且仅当存在Ω的反 驳。 证明：设为Q1,…,Qn是反驳。 (1).若QkΩ，Ω|=Qk.
σ'(qPi)=1，其中，qPiΩq
σ'(qQj)=1，其中，qQiΩq σ'(Rk)=1，其中，RkΩC 若Ω1是可满足的，则有σ'，使得σ'(Ω0)=1，这样就产生了 矛盾，所以，Ω1是不可满足的。
计算机学院
计算机学院
21
21
因此，Ω1有n-1个命题变元并且Ω1是不可满足的。 对于所有的n进行处理获得Ωn，必有反驳，否则必有Ωn 可满足，进而有Ω0可满足。 证毕
计算机学院
7
7
子句与空子句
定义：原子公式及其否定称为文字(literals)； 文字的简单析取范式称为子句，不包含文字 的子句称为空子句，记为□。 例如
• p、q、r和s都是文字 • 简单析取式pqrs是子句
–字p、q、r和s
计算机学院
• 因为pqrs不是简单析取范式，所以 pqrs不是子句。
Ω1 =ΩCΩR
Ω1有n-1个命题变元。 若有rΩ1并且rΩ1，则存在反驳。
计算机学院
计算机学院
19
19
若Ωq Ωq ΩC 不可满足，则Ω1 =ΩCΩR不可满足。 若Ω1是可满足的，则有赋值函数σ，使得σ(Ω1)=1。 如果σ(Pi)=1，i=1,...,m1，那么有σ'(q)=0，而其他命题变元 r有σ'(r)=σ(r)。 σ'(qPi)=1，其中，qPiΩq σ'(qQj)=1，其中，qQjΩq σ'(Rk)=1，其中，RkΩC
计算机学院
计算机学院
17
17
设Ω0有n种相反文字，有相反文字q和q ，Ω0中的子句分为三类， • 一类是有文字q的子句， • 另一类是有文字q的子句， • 再一类是没有文字q和q的子句
计算机学院
计算机学院
18
18
Ωq ={ qPk| qPkΩ}，Ωq ={qQk| qQkΩ}， ΩC=Ω-Ωq-Ωq |Ωq |=m1，|Ωq |=m2，|ΩC|=m3。 ΩR={ Pi Qj| qPiΩq, qQjΩq}
(PQR) PQR
因为(PQR)((PR)(QR))的合取范式 计算机学院 (PQR) PQR 所以子句集合 Ω={P,Q, R ,PQR }
计算机学院
25
25
Q1=PQR Q2=P Q3=QR Q4=Q
Q1Ω Q3= (Q1-P) (Q2-P) Q4Ω
Q2Ω
Q5=R
Q6=R Q7=□ 证毕
Q5= (Q3-Q) (Q4-Q)
Q6Ω Q7= (Q5-R) (Q6-R) 计算机学院
因此PQR├(PR) (QR)
计算机学院
26
26
计算机学院
8
8
定义：设Q是简单析取范式，q是Q的文字，在Q中 去掉文字q，记为Q-q。 例如，Q是子句pqrs，Q - q是简单析取范式 p rs。
计算机学院
计算机学院
9
9
归结子句
定义：设Q1,Q2是子句，q1和q2是相反文字，并且在子句 Q1和Q2中出现，称子句(Q1-q1)(Q2-q2)为Q1和Q2的归结 子句。 例如，Q1是子句pqr，Q2是子句pqws，q和q 是相反文字，子句prws是Q1和Q2的归结子句。 例如，Q1是子句q，Q2是子句q，q和q是相反文字， 子句□是Q1和Q2的归结子句。 例如，Q1是子句pqr，Q2是子句pws，在子句Q1 和Q2中没有相反文字出现，子句Q1Q2，即 pqrws不是Q1和Q2的归结子句。
计算机学院
因此，若Ω1是可满足的，则有σ'，使得σ'(Ω0)=1，这样就 产生了矛盾，所以，Ω1是不可满足的。