數(shù)理邏輯歸結(jié)法原理

數(shù)理邏輯歸結(jié)法原理第1頁，共27頁，2023年，2月20日，星期六主要內(nèi)容機(jī)械證明簡介命題邏輯歸結(jié)法謂詞邏輯歸結(jié)法第2頁，共27頁，2023年，2月20日，星期六自動推理早期的工作主要集中在機(jī)器定理證明。機(jī)械定理證明的中心問題是尋找判定公式是否是有效的通用程序。對命題邏輯公式，由于解釋的個數(shù)是有限的，總可以建立一個通用判定程序，使得在有限時間內(nèi)判定出一個公式是有效的或是無效的。對一階邏輯公式，其解釋的個數(shù)通常是任意多個，丘奇（A.Church）和圖靈（A.M.Turing）在1936年證明了不存在判定公式是否有效的通用程序。如果一階邏輯公式是有效的，則存在通用程序可以驗(yàn)證它是有效的對于無效的公式這種通用程序一般不能終止。第3頁，共27頁，2023年，2月20日，星期六1930年希爾伯特（Herbrand）為定理證明建立了一種重要方法，他的方法奠定了機(jī)械定理證明的基礎(chǔ)。開創(chuàng)性的工作是赫伯特·西蒙（H.A.Simon）和艾倫·紐威爾（A.Newel）的LogicTheorist。機(jī)械定理證明的主要突破是1965年由魯賓遜（J.A.Robinson）做出的，他建立了所謂歸結(jié)原理，使機(jī)械定理證明達(dá)到了應(yīng)用階段。歸結(jié)法推理規(guī)則簡單,而且在邏輯上是完備的,因而成為邏輯式程序設(shè)計語言Prolog的計算模型。第4頁，共27頁，2023年，2月20日，星期六主要內(nèi)容機(jī)械證明簡介命題邏輯歸結(jié)法謂詞邏輯歸結(jié)法第5頁，共27頁，2023年，2月20日，星期六基本原理Q1,…,Qn|=R，當(dāng)且僅當(dāng)Q1…QnR不可滿足證明Q1,…,Qn|=R(1).Q1…QnR化為合取范式；(2).構(gòu)建Ω子句集合，Ω為Q1…QnR合取范式的所有簡單析取范式組成集合；(3).若Ω不可滿足，則Q1,…,Qn|=R。第6頁，共27頁，2023年，2月20日，星期六機(jī)械式方法若證明Q1,…,Qn|=R，只要證明Q1…QnR不可滿足。機(jī)械式證明：公式Q1…QnR的合取范式；合取范式的所有簡單析取范式，即Ω；證明Ω不可滿足則有Q1,…,Qn|=R。機(jī)械式地證明Ω不可滿足是關(guān)鍵問題第7頁，共27頁，2023年，2月20日，星期六子句與空子句定義：原子公式及其否定稱為文字(literals)；文字的簡單析取范式稱為子句，不包含文字的子句稱為空子句，記為□。例如p、q、r和s都是文字簡單析取式pqrs是子句字p、q、r和s因?yàn)閜qrs不是簡單析取范式，所以pqrs不是子句。第8頁，共27頁，2023年，2月20日，星期六定義：設(shè)Q是簡單析取范式，q是Q的文字，在Q中去掉文字q，記為Q-q。例如，Q是子句pqrs，Q-q是簡單析取范式prs。第9頁，共27頁，2023年，2月20日，星期六歸結(jié)子句定義：設(shè)Q1,Q2是子句，q1和q2是相反文字，并且在子句Q1和Q2中出現(xiàn)，稱子句(Q1-q1)(Q2-q2)為Q1和Q2的歸結(jié)子句。例如，Q1是子句pqr，Q2是子句pqws，q和q是相反文字，子句prws是Q1和Q2的歸結(jié)子句。例如，Q1是子句q，Q2是子句q，q和q是相反文字，子句□是Q1和Q2的歸結(jié)子句。例如，Q1是子句pqr，Q2是子句pws，在子句Q1和Q2中沒有相反文字出現(xiàn)，子句Q1Q2，即pqrws不是Q1和Q2的歸結(jié)子句。第10頁，共27頁，2023年，2月20日，星期六定理：如果子句Q是Q1,Q2的歸結(jié)子句，則Q1,Q2|=Q證明：設(shè)Q1=pq1…qn，Q2=pr1…rm。

賦值函數(shù)σ(Q1)=1，即σ(pq1…qn)=1，σ(p)σ(q1…qn)=1.賦值函數(shù)σ(Q2)=1，即σ(pr1…rm)=1，σ(p)σ(r1…rm)=1.有σ(q1…qnr1…rm)=1，即σ(Q)=1。證畢第11頁，共27頁，2023年，2月20日，星期六反駁定義：設(shè)Ω是子句集合，如果子句序列Q1,…,Qn滿足如下條件，則稱子句序列Q1,…,Qn為子句集合Ω的一個反駁。(1).對于每個1≤k<n，QkΩQk是Qi和Qj的歸結(jié)子句，i<k，j<k。(2).Qn是□。第12頁，共27頁，2023年，2月20日，星期六例題：(QR)Q├Q皮爾斯律證明：因?yàn)?(QR)Q)Q的合取范式Q(RQ)Q，所以子句集合Ω={Q,RQ,Q}Q1=QQ1ΩQ2=QQ2ΩQ3=□Q3=(Q1-Q)(Q2-Q)第13頁，共27頁，2023年，2月20日，星期六定理：子句集合Ω是不可滿足的當(dāng)且僅當(dāng)存在Ω的反駁。證明：設(shè)為Q1,…,Qn是反駁。(1).若QkΩ，Ω|=Qk.(2).若Ω|=Qi，Ω|=Qj并且Qk是Qi,Qj的歸結(jié)子句，則Qi,Qj|=Qk。因此，Ω|=Qk。(3).因?yàn)镼n=□，所以有Qn-1和Qk是相反文字，不妨設(shè)是q和q。因此，Ω|=q，Ω|=q。Ω|=qq，Ω不可滿足。第14頁，共27頁，2023年，2月20日，星期六又證：設(shè)子句集合Ω是不可滿足的。(1).不妨設(shè)子句集合Ω不含永真式。因?yàn)閺摩钢腥サ粲勒媸讲桓淖儲傅牟豢蓾M足性。(2).若Ω含有相反文字，不妨設(shè)是q，則Q1=qQ1ΩQ2=qQ2ΩQ3=□因此，Q1,Q2,Q3是反駁.第15頁，共27頁，2023年，2月20日，星期六(3).根據(jù)命題邏輯緊致性定理，若子句集合Ω不可滿足，則有有窮子句集合Ω0，Ω0Ω，使得Ω0是不可滿足的。第16頁，共27頁，2023年，2月20日，星期六若有窮子句集合Ω0是不可滿足的，則Ω0中的子句必出現(xiàn)相反文字。假設(shè)有窮子句集合Ω0是不可滿足的，且Ω0中的子句不出現(xiàn)相反文字，那么，對于Ω0中子句的每個文字qk，有賦值函數(shù)σ使得σ(qk)=1，因此，σ(Ω0)=1，Ω0是可滿足的，這樣與Ω0是不可滿足的相矛盾。第17頁，共27頁，2023年，2月20日，星期六設(shè)Ω0有n種相反文字，有相反文字q和q，Ω0中的子句分為三類，一類是有文字q的子句，另一類是有文字q的子句，再一類是沒有文字q和q的子句第18頁，共27頁，2023年，2月20日，星期六Ωq={qPk|qPkΩ}，Ωq={qQk|qQkΩ}，ΩC=Ω-Ωq-Ωq|Ωq|=m1，|Ωq|=m2，|ΩC|=m3。ΩR={Pi

Qj|qPiΩq,qQjΩq}Ω1=ΩCΩRΩ1有n-1個命題變元。若有rΩ1并且rΩ1，則存在反駁。第19頁，共27頁，2023年，2月20日，星期六若Ωq

Ωq

ΩC

不可滿足，則Ω1=ΩCΩR不可滿足。若Ω1是可滿足的，則有賦值函數(shù)σ，使得σ(Ω1)=1。如果σ(Pi)=1，i=1,...,m1，那么有σ'(q)=0，而其他命題變元r有σ'(r)=σ(r)。σ'(qPi)=1，其中，qPiΩqσ'(qQj)=1，其中，qQjΩqσ'(Rk)=1，其中，RkΩC因此，若Ω1是可滿足的，則有σ'，使得σ'(Ω0)=1，這樣就產(chǎn)生了矛盾，所以，Ω1是不可滿足的。第20頁，共27頁，2023年，2月20日，星期六如果σ(Pi)=0，i≤m1，則有PiQjΩ1，j=1,…,m2。因?yàn)棣?Ω1)=1，所以有σ(PiQj)=1，即σ(Qj)=1，j=1,…,m2。設(shè)σ'(q)=1，而其他命題變元r有σ'(r)=σ(r)。σ'(qPi)=1，其中，qPiΩqσ'(qQj)=1，其中，qQiΩqσ'(Rk)=1，其中，RkΩC若Ω1是可滿足的，則有σ'，使得σ'(Ω0)=1，這樣就產(chǎn)生了矛盾，所以，Ω1是不可滿足的。第21頁，共27頁，2023年，2月20日，星期六因此，Ω1有n-1個命題變元并且Ω1是不可滿足的。對于所有的n進(jìn)行處理獲得Ωn，必有反駁，否則必有Ωn可滿足，進(jìn)而有Ω0可滿足。證畢第22頁，共27頁，2023年，2月20日，星期六例題：P(QR)├(PQ)(PR)分配律(P(QR))((PQ)(PR))(P(QR))((PQ)(PR))(PQ)(PR))(P(PR))(Q(PR))(PQ)(PR)P(P

R)(QP)(QR)因?yàn)?P(QR))((PQ)(PR))的合取范式(PQ)(PR)P(P

R)(QP)(QR)所以子句集合 Ω={P,PQ,PQ,PR,PR,QR}。第23頁，共27頁，2023年，2月20日，星期六Q1=PQQ1ΩQ2=PQQ2ΩQ3=□Q3=(Q1-P-Q)(Q2-P-Q)P(QR)├(PQ)(PR)分配律第24頁，共27頁，2023年，2月20日，星期六例題：PQR├(PR)(QR)證明：(PQR)((PR)(QR)