模態(tài)herbrand定理研究

1、南開大學(xué)學(xué)位論文原創(chuàng)性聲明本人鄭重聲明：所呈交的學(xué)位論文，是本人在導(dǎo)師指導(dǎo)下，進(jìn)行碲究工作所取得的成果。除文中已經(jīng)注明引用的內(nèi)容外，本學(xué)位論文的研究成果不包含任何他人創(chuàng)作的、已公開發(fā)表或者沒有公開發(fā)表的作品的內(nèi)容。對(duì)本論文所涉及的研究工作做出貢獻(xiàn)的其他個(gè)人和集體，均己在文中以明確方式標(biāo)明。本學(xué)位論文原創(chuàng)性聲明的法律責(zé)任由本人承擔(dān)。學(xué)位論文作者簽名：薇蕉1 走咖西年 廠月7 y 日摘要H e r b r 趾d 定理是經(jīng)典邏輯中一條重要的元

2、定理，它不僅為人工智能中的機(jī)器定理證明提供了理論基礎(chǔ)，更可以成為哥德爾完全性定理的替代物；此外，H e r b r a I l d 定理還被應(yīng)用于可判定問題，并取得了成果。盡管H e r b r 觚d 定理本身有著良好的性質(zhì)，但它的影響力仍然停留在經(jīng)典邏輯中。誠然，在2 0 世紀(jì)7 0年代至9 0 年代早期，人們做過把H e r b m d 定理推廣到模態(tài)邏輯的各種嘗試，但都未能取得完全令人滿意的結(jié)果。直到1 9 9 6 年美國當(dāng)代邏輯

3、學(xué)家、證明論專家F i 位i n g 的工作，模態(tài)邏輯領(lǐng)域的H e r b r a n d 定理才取得突破性進(jìn)展。F i t t i n g 通過把“謂詞抽象”這一裝置引入通常的一階模態(tài)邏輯，以一種很自然的方式加強(qiáng)了一階模態(tài)邏輯語言的表達(dá)力，從而獲得一個(gè)沒有B a r c a I l 公式的模態(tài)系統(tǒng)K的H 咖r a n d 定理，這是迄今為止與經(jīng)典H e r b 啪d 定理最為接近的一種模態(tài)H e r b r a I l d 定理形式。

4、后來F i t t i n g 又指出：類似的結(jié)果也可以從其它的模態(tài)系統(tǒng)獲得，這是一個(gè)可以解決模態(tài)H e r b r a l l d 定理范圍的有趣問題。但是F i t t i n g 后來不再從事這方面的研究工作，而且他本人也沒有指出在從其它的模態(tài)系統(tǒng)獲得“類似”的結(jié)果時(shí)會(huì)遇到哪些困難。本文力圖在充分考察F i t t i n g 工作的基礎(chǔ)上，嘗試給出其它寸些模態(tài)系統(tǒng)的H e r b r a n d 定理，擴(kuò)大模態(tài)H 曲砌咀定理成果

5、的范圍。概括說來，本文的工作包括以下三個(gè)方面。第一，詳細(xì)闡述F i t t i n g 在探索模態(tài)邏輯領(lǐng)域的H e r b r a n d 定理方面所做的工作。在F i t t i n g 的論文中，由于篇幅有限，許多重要定理的證明過程和許多重要的轉(zhuǎn)換規(guī)則、轉(zhuǎn)換步驟都被省略掉了。本文力圖將它們補(bǔ)充完整，為后面探索其它模態(tài)系統(tǒng)的H e r b r a n d 定理工作做好準(zhǔn)備。首先，給出了模態(tài)邏輯的s k o l 鋤化定理的詳細(xì)證明過程，

6、可以說這一定理是F i t t i n g 所有工作的精華之處，關(guān)系到整個(gè)模態(tài)邏輯領(lǐng)域H e r b r 趾d 定理的成敗。其次，給出了加標(biāo)公式表列系統(tǒng)K的可靠性和完全性的詳細(xì)證明過程，為模態(tài)系統(tǒng)K 的H e r b r a I l d 定理從左到右方向的證明做好準(zhǔn)備。再次，在給出模態(tài)H e r b r a n d 膨脹的矢列演算規(guī)則中，補(bǔ)充了合取規(guī)則、析取規(guī)則和可能算子規(guī)則。最后，給出了在加標(biāo)公式表列系統(tǒng)K中，從公式x 的表列證明序列