1、計(jì)算機(jī)學(xué)院1計(jì)算機(jī)學(xué)院1主要內(nèi)容主要內(nèi)容 機(jī)械證明簡(jiǎn)介機(jī)械證明簡(jiǎn)介 命題邏輯歸結(jié)法命題邏輯歸結(jié)法 謂詞邏輯歸結(jié)法謂詞邏輯歸結(jié)法計(jì)算機(jī)學(xué)院2計(jì)算機(jī)學(xué)院2 自動(dòng)推理早期的工作主要集中在機(jī)器定理證明。自動(dòng)推理早期的工作主要集中在機(jī)器定理證明。 機(jī)械定理證明的中心問(wèn)題是尋找判定公式是否是有效的機(jī)械定理證明的中心問(wèn)題是尋找判定公式是否是有效的通用程序。通用程序。 對(duì)命題邏輯公式，由于解釋的個(gè)數(shù)是有限的，總可以建對(duì)命題邏輯公式，由于解釋的個(gè)數(shù)是有限的，總可以建立一個(gè)通用判定程序，使得在有限時(shí)間內(nèi)判定出一個(gè)公立一個(gè)通用判定程序，使得在有限時(shí)間內(nèi)判定出一個(gè)公式是有效的或是無(wú)效的。式是有效的或是無(wú)效的。 對(duì)一階

2、邏輯公式，其解釋的個(gè)數(shù)通常是任意多個(gè)，丘奇對(duì)一階邏輯公式，其解釋的個(gè)數(shù)通常是任意多個(gè)，丘奇（A.ChurchA.Church）和圖靈（）和圖靈（A.M.TuringA.M.Turing）在）在19361936年證明了不存年證明了不存在判定公式是否有效的通用程序。在判定公式是否有效的通用程序。如果一階邏輯公式是有效的，則存在通用程序可以驗(yàn)證它如果一階邏輯公式是有效的，則存在通用程序可以驗(yàn)證它是有效的是有效的對(duì)于無(wú)效的公式這種通用程序一般不能終止。對(duì)于無(wú)效的公式這種通用程序一般不能終止。計(jì)算機(jī)學(xué)院3計(jì)算機(jī)學(xué)院3 19301930年希爾伯特（年希爾伯特（HerbrandHerbrand）為定理證明建

3、立了一種重）為定理證明建立了一種重要方法，他的方法奠定了機(jī)械定理證明的基礎(chǔ)。要方法，他的方法奠定了機(jī)械定理證明的基礎(chǔ)。 開(kāi)創(chuàng)性的工作是赫伯特開(kāi)創(chuàng)性的工作是赫伯特西蒙（西蒙（H. A. SimonH. A. Simon）和艾倫）和艾倫紐威爾（紐威爾（A. NewelA. Newel）的）的 Logic Theorist Logic Theorist。 機(jī)械定理證明的主要突破是機(jī)械定理證明的主要突破是19651965年由魯賓遜（年由魯賓遜（J.A.RobinsonJ.A.Robinson）做出的，他建立了所謂歸結(jié)原理，使機(jī)械）做出的，他建立了所謂歸結(jié)原理，使機(jī)械定理證明達(dá)到了應(yīng)用階段。定理證明達(dá)到

4、了應(yīng)用階段。 歸結(jié)法推理規(guī)則簡(jiǎn)單歸結(jié)法推理規(guī)則簡(jiǎn)單, , 而且在邏輯上是完備的而且在邏輯上是完備的, , 因而成為因而成為邏輯式程序設(shè)計(jì)語(yǔ)言邏輯式程序設(shè)計(jì)語(yǔ)言PrologProlog的計(jì)算模型。的計(jì)算模型。計(jì)算機(jī)學(xué)院4計(jì)算機(jī)學(xué)院4主要內(nèi)容主要內(nèi)容 機(jī)械證明簡(jiǎn)介機(jī)械證明簡(jiǎn)介 命題邏輯歸結(jié)法命題邏輯歸結(jié)法 謂詞邏輯歸結(jié)法謂詞邏輯歸結(jié)法計(jì)算機(jī)學(xué)院5計(jì)算機(jī)學(xué)院5基本原理基本原理 Q Q1 1, ,Q,Qn n|=R|=R，當(dāng)且僅當(dāng)，當(dāng)且僅當(dāng)Q Q1 1 Q Qn nR R不可滿足不可滿足 證明證明Q Q1 1, ,Q,Qn n|=R|=R(1). Q(1). Q1 1 Q Qn nR R化為合取范式；

5、化為合取范式；(2). (2). 構(gòu)建構(gòu)建 子句集合，子句集合， 為為Q Q1 1 Q Qn nR R合取范合取范式的所有簡(jiǎn)單析取范式組成集合；式的所有簡(jiǎn)單析取范式組成集合；(3).(3).若若 不可滿足，則不可滿足，則Q Q1 1, ,Q,Qn n|=R|=R。計(jì)算機(jī)學(xué)院6計(jì)算機(jī)學(xué)院6機(jī)械式方法機(jī)械式方法 若證明若證明Q Q1 1, ,Q,Qn n|=R|=R，只要證明，只要證明Q Q1 1 Q Qn nR R不可滿足。不可滿足。 機(jī)械式證明：機(jī)械式證明：公式公式Q Q1 1 Q Qn nR R的合取范式；的合取范式；合取范式的所有簡(jiǎn)單析取范式，即合取范式的所有簡(jiǎn)單析取范式，即 ；證明證明

6、不可滿足不可滿足 則有則有Q Q1 1, ,Q,Qn n|=R|=R。 機(jī)械式地證明機(jī)械式地證明 不可滿足是關(guān)鍵問(wèn)題不可滿足是關(guān)鍵問(wèn)題計(jì)算機(jī)學(xué)院7計(jì)算機(jī)學(xué)院7子句與空子句子句與空子句 定義：原子公式及其否定稱為文字定義：原子公式及其否定稱為文字(literals)(literals)；文字的簡(jiǎn)單析取范式稱為子句，不包含文字文字的簡(jiǎn)單析取范式稱為子句，不包含文字的子句稱為空子句，記為。的子句稱為空子句，記為。 例如例如p p、 q q、 r r和和s s都是文字都是文字簡(jiǎn)單析取式簡(jiǎn)單析取式p pq qr r s s是子句是子句字字p p、 q q、 r r和和s s因?yàn)橐驗(yàn)閜 pq qr r s

7、 s不是簡(jiǎn)單析取范式，所以不是簡(jiǎn)單析取范式，所以p pq qr r s s不是子句。不是子句。計(jì)算機(jī)學(xué)院8計(jì)算機(jī)學(xué)院8 定義：設(shè)定義：設(shè)Q Q是簡(jiǎn)單析取范式，是簡(jiǎn)單析取范式，q q是是Q Q的文字，在的文字，在Q Q中中去掉文字去掉文字q q，記為，記為Q-qQ-q。 例如，例如，Q Q是子句是子句p pq qr r s s，Q - Q - q q是簡(jiǎn)單析取范式是簡(jiǎn)單析取范式p p r r s s。計(jì)算機(jī)學(xué)院9計(jì)算機(jī)學(xué)院9歸結(jié)子句歸結(jié)子句 定義：設(shè)定義：設(shè)Q Q1 1,Q,Q2 2是子句，是子句，q q1 1和和q q2 2是相反文字，并且在子句是相反文字，并且在子句Q Q1 1和和Q Q2

8、2中出現(xiàn)，稱子句中出現(xiàn)，稱子句(Q(Q1 1-q-q1 1) ) (Q(Q2 2-q-q2 2) )為為Q Q1 1和和Q Q2 2的歸結(jié)的歸結(jié)子句。子句。 例如，例如，Q Q1 1是子句是子句p pq qr r，Q Q2 2是子句是子句p p q q w w s s， q q和和q q是相反文字，子句是相反文字，子句p pr r w w s s是是Q Q1 1和和Q Q2 2的歸結(jié)子句。的歸結(jié)子句。 例如，例如，Q Q1 1是子句是子句 q q，Q Q2 2是子句是子句q q， q q和和q q是相反文字，是相反文字，子句是子句是Q Q1 1和和Q Q2 2的歸結(jié)子句。的歸結(jié)子句。 例如，例

9、如，Q Q1 1是子句是子句p pq qr r，Q Q2 2是子句是子句p p w w s s，在子句，在子句Q Q1 1 和和Q Q2 2中沒(méi)有相反文字出現(xiàn)，子句中沒(méi)有相反文字出現(xiàn)，子句Q Q1 1 Q Q2 2，即，即p pq qr r w w s s不是不是Q Q1 1和和Q Q2 2的歸結(jié)子句。的歸結(jié)子句。計(jì)算機(jī)學(xué)院10計(jì)算機(jī)學(xué)院10 定理：如果子句定理：如果子句Q Q是是Q Q1 1, Q, Q2 2的歸結(jié)子句，則的歸結(jié)子句，則Q Q1 1, Q, Q2 2|=Q|=Q 證明：證明： 設(shè)設(shè)Q Q1 1=p=p q q1 1 q qn n，Q Q2 2= = p p r r1 1 r

10、rm m。 賦值函數(shù)賦值函數(shù)(Q(Q1 1)=1)=1，即，即(p(p q q1 1 q qn n)=1)=1， (p)(p) (q (q1 1 q qn n)=1.)=1. 賦值函數(shù)賦值函數(shù)(Q(Q2 2)=1)=1，即，即( ( p p r r1 1 r rm m)=1)=1， (p)(p) (r (r1 1 r rm m)=1.)=1. 有有(q(q1 1 q qn n r r1 1 r rm m)=1)=1，即，即(Q)=1(Q)=1。 證畢證畢計(jì)算機(jī)學(xué)院11計(jì)算機(jī)學(xué)院11反駁反駁 定義：設(shè)定義：設(shè) 是子句集合，如果子句序列是子句集合，如果子句序列Q Q1 1, ,Q,Qn n滿足如下

11、條件，則稱子句序列滿足如下條件，則稱子句序列Q Q1 1, ,Q,Qn n為子句集合為子句集合 的一個(gè)反駁。的一個(gè)反駁。 (1).(1).對(duì)于每個(gè)對(duì)于每個(gè)1 1k knn，Q Qk k Q Qk k是是Q Qi i和和Q Qj j的歸結(jié)子句，的歸結(jié)子句，ikik，jkjk。 (2). (2). Q Qn n是。是。計(jì)算機(jī)學(xué)院12計(jì)算機(jī)學(xué)院12 例題：例題：(Q(QR)R)Q QQ Q 皮爾斯律皮爾斯律 證明：證明： 因?yàn)橐驗(yàn)?Q(QR)R)Q)Q)Q Q的合取范式的合取范式Q Q ( ( R R Q)Q)Q Q，所以，所以子句集合子句集合=Q, =Q, R R Q, Q, QQ Q Q1 1=

12、 Q Q= Q Q1 1 Q Q2 2= = Q QQ Q2 2 Q Q3 3= = Q Q3 3= (Q= (Q1 1-Q) -Q) (Q (Q2 2- - Q)Q)計(jì)算機(jī)學(xué)院13計(jì)算機(jī)學(xué)院13 定理：子句集合定理：子句集合 是不可滿足的當(dāng)且僅當(dāng)存在是不可滿足的當(dāng)且僅當(dāng)存在 的反的反駁。駁。 證明：設(shè)為證明：設(shè)為Q Q1 1, ,Q,Qn n是反駁。是反駁。 (1).(1).若若Q Qk k ，|=Q|=Qk. k. (2).(2).若若|=Q|=Qi i，|=Q|=Qj j并且并且Q Qk k是是Q Qi i, Q, Qj j的歸結(jié)子句，則的歸結(jié)子句，則Q Qi i, Q, Qj j|=Q

13、|=Qk k。因此，。因此，|=Q|=Qk k。 (3).(3).因?yàn)橐驗(yàn)镼 Qn n= =，所以有，所以有Q Qn-1n-1和和Q Qk k是相反文字，不妨設(shè)是相反文字，不妨設(shè)是是q q和和 q q。 因此，因此，|=q|=q，|=|= q q。|=q|=qq q， 不可滿足。不可滿足。計(jì)算機(jī)學(xué)院14計(jì)算機(jī)學(xué)院14 又證：設(shè)子句集合又證：設(shè)子句集合 是不可滿足的。是不可滿足的。 (1).(1).不妨設(shè)子句集合不妨設(shè)子句集合 不含永真式。因?yàn)閺牟缓勒媸?。因?yàn)閺?中去掉永真中去掉永真式不改變式不改變 的不可滿足性。的不可滿足性。 (2).(2).若若 含有相反文字，不妨設(shè)是含有相反文字，不妨設(shè)

14、是q q，則，則 Q Q1 1=q Q=q Q1 1 Q Q2 2= = q Qq Q2 2 Q Q3 3= = 因此，因此，Q Q1 1, Q, Q2 2,Q,Q3 3是反駁是反駁. .計(jì)算機(jī)學(xué)院15計(jì)算機(jī)學(xué)院15 (3).(3).根據(jù)命題邏輯緊致性定理，若子句集合根據(jù)命題邏輯緊致性定理，若子句集合 不可滿足，則有有窮子句集合不可滿足，則有有窮子句集合 0 0， 0 0 ，使，使得得 0 0是不可滿足的。是不可滿足的。計(jì)算機(jī)學(xué)院16計(jì)算機(jī)學(xué)院16 若有窮子句集合若有窮子句集合 0 0是不可滿足的，則是不可滿足的，則 0 0中的子句必中的子句必出現(xiàn)相反文字。出現(xiàn)相反文字。 假設(shè)有窮子句集合假設(shè)

15、有窮子句集合 0 0是不可滿足的，且是不可滿足的，且 0 0中的子句中的子句不出現(xiàn)相反文字，那么，對(duì)于不出現(xiàn)相反文字，那么，對(duì)于 0 0中子句的每個(gè)文字中子句的每個(gè)文字q qk k，有賦值函數(shù)，有賦值函數(shù) 使得使得(q(qk k)=1)=1，因此，因此，(0 0)=1)=1， 0 0是是可滿足的，這樣與可滿足的，這樣與 0 0是不可滿足的相矛盾。是不可滿足的相矛盾。計(jì)算機(jī)學(xué)院17計(jì)算機(jī)學(xué)院17 設(shè)設(shè) 0 0有有n n種相反文字，有相反文字種相反文字，有相反文字q q和和 q q， 0 0中的子句分為三類，中的子句分為三類，一類是有文字一類是有文字q q的子句，的子句，另一類是有文字另一類是有文

16、字 q q的子句，的子句，再一類是沒(méi)有文字再一類是沒(méi)有文字q q和和 q q的子句的子句計(jì)算機(jī)學(xué)院18計(jì)算機(jī)學(xué)院18 q q = q = q P Pk k| q| q P Pk k ， q q = = q q Q Qk k| | q q Q Qk k ， C C=-=-q q- q q |q q |=m |=m1 1，| q q |=m |=m2 2，|C C|=m|=m3 3。 R R= P= Pi i Q Qj j| q| q P Pi i q q, , q q Q Qj j q q 1 1 = =C C R R 1 1有有n-1n-1個(gè)命題變?cè)?。個(gè)命題變?cè)?若有若有r r 1 1并且并

17、且 r r 1 1，則存在反駁。，則存在反駁。計(jì)算機(jī)學(xué)院19計(jì)算機(jī)學(xué)院19 若若 q q q q C C 不可滿足，則不可滿足，則 1 1 = =C C R R不可滿足。不可滿足。 若若 1 1是可滿足的，則有賦值函數(shù)是可滿足的，則有賦值函數(shù) ，使得，使得(1 1)=1)=1。 如果如果(P(Pi i)=1)=1，i i=1,.,m=1,.,m1 1，那么有，那么有(q)=0(q)=0，而其他命題變?cè)渌}變?cè)猺 r有有(r)=(r)(r)=(r)。 (q(q P Pi i)=1)=1，其中，其中，q q P Pi i q q ( q q Q Qj j)=1)=1，其中，其中， q q

18、Q Qj j q q (R(Rk k)=1)=1，其中，其中，R Rk k C C 因此，若因此，若 1 1是可滿足的，則有是可滿足的，則有 ，使得，使得(0 0)=1)=1，這樣就，這樣就產(chǎn)生了矛盾，所以，產(chǎn)生了矛盾，所以， 1 1是不可滿足的。是不可滿足的。計(jì)算機(jī)學(xué)院20計(jì)算機(jī)學(xué)院20 如果如果(P(Pi i)=0)=0，i im m1 1，則有，則有P Pi i Q Qj j 1 1，j=1,j=1,m,m2 2。 因?yàn)橐驗(yàn)?1 1)=1)=1，所以有，所以有(P(Pi i Q Qj j)=1)=1，即，即(Q(Qj j)=1)=1，j=1,j=1,m,m2 2。 設(shè)設(shè)(q)=1(q)=

19、1，而其他命題變?cè)?，而其他命題變?cè)猺 r有有(r)=(r)(r)=(r)。 (q(q P Pi i)=1)=1，其中，其中，q q P Pi i q q ( q q Q Qj j)=1)=1，其中，其中， q q Q Qi i q q (R(Rk k)=1)=1，其中，其中，R Rk k C C 若若 1 1是可滿足的，則有是可滿足的，則有 ，使得，使得(0 0)=1)=1，這樣就產(chǎn)生了，這樣就產(chǎn)生了矛盾，所以，矛盾，所以， 1 1是不可滿足的。是不可滿足的。計(jì)算機(jī)學(xué)院21計(jì)算機(jī)學(xué)院21 因此，因此， 1 1有有n-1n-1個(gè)命題變?cè)⑶覀€(gè)命題變?cè)⑶?1 1是不可滿足的。是不可滿足的。 對(duì)于

20、所有的對(duì)于所有的n n進(jìn)行處理獲得進(jìn)行處理獲得 n n，必有反駁，否則必有，必有反駁，否則必有 n n可滿足，進(jìn)而有可滿足，進(jìn)而有 0 0可滿足。可滿足。 證畢證畢計(jì)算機(jī)學(xué)院22計(jì)算機(jī)學(xué)院22 例題：例題：P P(Q(Q R)R) (P (PQ)Q) (P (PR) R) 分配律分配律 (P(P(Q(Q R) R) (P (PQ)Q) (P (PR)R) ( ( P P (Q(Q R) R) (P (PQ) Q) (P (PR)R) ( ( P P Q) Q) ( ( P P R)R) ( P( P (P (PR) R) ( ( Q Q (P (PR)R) ( ( P P Q) Q) ( ( P P R)R) P P ( P( P R) R) ( ( Q Q P) P) ( ( Q QR)R) 因?yàn)橐驗(yàn)?P(P(Q(Q R) R) (P (PQ)Q) (P (PR)R)的合取范式的合取范式 ( ( P P Q) Q) ( ( P P R)R) P P ( P( P R) R) ( ( Q Q P) P) ( ( Q QR) R) 所以子句集合所以子句集合 = P,P= P,PQ, Q, P P Q, PQ, PR ,R , P P R , R , Q QRR。計(jì)算機(jī)學(xué)院23計(jì)算機(jī)學(xué)院23 Q Q1 1= P= PQ QQ Q1 1 Q Q2