模態(tài)邏輯的模型構(gòu)造和完備性證明.pdf

1、模態(tài)邏輯是研究必然、可能及其相關(guān)概念的邏輯。模態(tài)邏輯是邏輯學(xué)最為重要的分支之一，它的理論、思想、技術(shù)和方法不僅是邏輯學(xué)中占有重要地位，而且在其他領(lǐng)域，如計(jì)算機(jī)科學(xué)、語(yǔ)言學(xué)等以及哲學(xué)方面有重要應(yīng)用，成為這些領(lǐng)域相關(guān)部分的理論基礎(chǔ)。
　　 模態(tài)邏輯公式的可滿足性問(wèn)題和證明系統(tǒng)的完備性問(wèn)題是模態(tài)邏輯中的兩個(gè)經(jīng)典的問(wèn)題?？蓾M足性問(wèn)題研究的是:對(duì)于一個(gè)給定的模態(tài)公式，判定是否存在模型，使得該命題在其中的某個(gè)狀態(tài)是可滿足的。對(duì)于模態(tài)邏輯的可

2、滿足性判定問(wèn)題，比較經(jīng)典的解決方法是tableau的方法，但是這個(gè)方法由于存在分支的選擇問(wèn)題，因此產(chǎn)生了不確定性。
　　 首先，我們提出了一個(gè)基于構(gòu)造模態(tài)公式的canonical model來(lái)判定可滿足性的方法。利用這個(gè)方法，對(duì)于給定模態(tài)公式(φ)，如果(φ)是可滿足的，可以得到(φ)的一個(gè)canonical model;如果(φ)是不可滿足的，還可以得到┑(φ)的證明。另外，我們基于這個(gè)方法，還得到了模態(tài)邏輯公理系統(tǒng)完備性的一