數(shù)理邏輯歸結(jié)法原理_第1頁
數(shù)理邏輯歸結(jié)法原理_第2頁
數(shù)理邏輯歸結(jié)法原理_第3頁
數(shù)理邏輯歸結(jié)法原理_第4頁
數(shù)理邏輯歸結(jié)法原理_第5頁
已閱讀5頁,還剩22頁未讀, 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報(bào)或認(rèn)領(lǐng)

文檔簡介

數(shù)理邏輯歸結(jié)法原理第一頁,共二十七頁,2022年,8月28日主要內(nèi)容機(jī)械證明簡介命題邏輯歸結(jié)法謂詞邏輯歸結(jié)法第二頁,共二十七頁,2022年,8月28日自動推理早期的工作主要集中在機(jī)器定理證明。機(jī)械定理證明的中心問題是尋找判定公式是否是有效的通用程序。對命題邏輯公式,由于解釋的個(gè)數(shù)是有限的,總可以建立一個(gè)通用判定程序,使得在有限時(shí)間內(nèi)判定出一個(gè)公式是有效的或是無效的。對一階邏輯公式,其解釋的個(gè)數(shù)通常是任意多個(gè),丘奇(A.Church)和圖靈(A.M.Turing)在1936年證明了不存在判定公式是否有效的通用程序。如果一階邏輯公式是有效的,則存在通用程序可以驗(yàn)證它是有效的對于無效的公式這種通用程序一般不能終止。第三頁,共二十七頁,2022年,8月28日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è)計(jì)語言Prolog的計(jì)算模型。第四頁,共二十七頁,2022年,8月28日主要內(nèi)容機(jī)械證明簡介命題邏輯歸結(jié)法謂詞邏輯歸結(jié)法第五頁,共二十七頁,2022年,8月28日基本原理Q1,…,Qn|=R,當(dāng)且僅當(dāng)Q1…QnR不可滿足證明Q1,…,Qn|=R(1).Q1…QnR化為合取范式;(2).構(gòu)建Ω子句集合,Ω為Q1…QnR合取范式的所有簡單析取范式組成集合;(3).若Ω不可滿足,則Q1,…,Qn|=R。第六頁,共二十七頁,2022年,8月28日機(jī)械式方法若證明Q1,…,Qn|=R,只要證明Q1…QnR不可滿足。機(jī)械式證明:公式Q1…QnR的合取范式;合取范式的所有簡單析取范式,即Ω;證明Ω不可滿足則有Q1,…,Qn|=R。機(jī)械式地證明Ω不可滿足是關(guān)鍵問題第七頁,共二十七頁,2022年,8月28日子句與空子句定義:原子公式及其否定稱為文字(literals);文字的簡單析取范式稱為子句,不包含文字的子句稱為空子句,記為□。例如p、q、r和s都是文字簡單析取式pqrs是子句字p、q、r和s因?yàn)閜qrs不是簡單析取范式,所以pqrs不是子句。第八頁,共二十七頁,2022年,8月28日定義:設(shè)Q是簡單析取范式,q是Q的文字,在Q中去掉文字q,記為Q-q。例如,Q是子句pqrs,Q-q是簡單析取范式prs。第九頁,共二十七頁,2022年,8月28日歸結(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é)子句。第十頁,共二十七頁,2022年,8月28日定理:如果子句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。證畢第十一頁,共二十七頁,2022年,8月28日反駁定義:設(shè)Ω是子句集合,如果子句序列Q1,…,Qn滿足如下條件,則稱子句序列Q1,…,Qn為子句集合Ω的一個(gè)反駁。(1).對于每個(gè)1≤k<n,QkΩQk是Qi和Qj的歸結(jié)子句,i<k,j<k。(2).Qn是□。第十二頁,共二十七頁,2022年,8月28日例題:(QR)Q├Q皮爾斯律證明:因?yàn)?(QR)Q)Q的合取范式Q(RQ)Q,所以子句集合Ω={Q,RQ,Q}Q1=QQ1ΩQ2=QQ2ΩQ3=□Q3=(Q1-Q)(Q2-Q)第十三頁,共二十七頁,2022年,8月28日定理:子句集合Ω是不可滿足的當(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,Ω不可滿足。第十四頁,共二十七頁,2022年,8月28日又證:設(shè)子句集合Ω是不可滿足的。(1).不妨設(shè)子句集合Ω不含永真式。因?yàn)閺摩钢腥サ粲勒媸讲桓淖儲傅牟豢蓾M足性。(2).若Ω含有相反文字,不妨設(shè)是q,則Q1=qQ1ΩQ2=qQ2ΩQ3=□因此,Q1,Q2,Q3是反駁.第十五頁,共二十七頁,2022年,8月28日(3).根據(jù)命題邏輯緊致性定理,若子句集合Ω不可滿足,則有有窮子句集合Ω0,Ω0Ω,使得Ω0是不可滿足的。第十六頁,共二十七頁,2022年,8月28日若有窮子句集合Ω0是不可滿足的,則Ω0中的子句必出現(xiàn)相反文字。假設(shè)有窮子句集合Ω0是不可滿足的,且Ω0中的子句不出現(xiàn)相反文字,那么,對于Ω0中子句的每個(gè)文字qk,有賦值函數(shù)σ使得σ(qk)=1,因此,σ(Ω0)=1,Ω0是可滿足的,這樣與Ω0是不可滿足的相矛盾。第十七頁,共二十七頁,2022年,8月28日設(shè)Ω0有n種相反文字,有相反文字q和q,Ω0中的子句分為三類,一類是有文字q的子句,另一類是有文字q的子句,再一類是沒有文字q和q的子句第十八頁,共二十七頁,2022年,8月28日Ω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個(gè)命題變元。若有rΩ1并且rΩ1,則存在反駁。第十九頁,共二十七頁,2022年,8月28日若Ω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是不可滿足的。第二十頁,共二十七頁,2022年,8月28日如果σ(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是不可滿足的。第二十一頁,共二十七頁,2022年,8月28日因此,Ω1有n-1個(gè)命題變元并且Ω1是不可滿足的。對于所有的n進(jìn)行處理獲得Ωn,必有反駁,否則必有Ωn可滿足,進(jìn)而有Ω0可滿足。證畢第二十二頁,共二十七頁,2022年,8月28日例題: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}。第二十三頁,共二十七頁,2022年,8月28日Q1=PQQ1ΩQ2=PQQ2ΩQ3=□Q3=(Q1-P-Q)(Q2-P-Q)P(QR)├(PQ)(PR)分配律第二十四頁,共二十七頁,2022年,8月28日例題:PQR├(PR)(QR)證明:(PQR)((PR)(QR))((PQ)R)(PRQR)(PQR)PQR因?yàn)?PQR)((PR)(QR))的合取范式(PQR)PQR所以子句集合 Ω={P,Q,R,PQR}第二十五頁,共二十七頁,2022年,8月28日Q1=PQRQ1ΩQ2=PQ2ΩQ3=QR

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 人人文庫網(wǎng)僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時(shí)也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

最新文檔

評論

0/150

提交評論