可計算性邏輯中若干形式系統(tǒng)及算子的研究.pdf

1、可計算性邏輯是新近提出的關(guān)于可計算性的形式理論.它采取交互的博弈語義，是一種資源邏輯.經(jīng)典邏輯、直覺邏輯和線性邏輯(在廣義上)只是可計算性邏輯的三個特殊部分.相比于傳統(tǒng)邏輯，可計算性邏輯具有更強的表達能力和更高的證明效率，這使得它有望在知識庫系統(tǒng)、人工智能行為規(guī)劃系統(tǒng)、電路等價性驗證等領(lǐng)域得到廣泛的應用。
　　本文主要利用可計算性邏輯的Cirquent演算方法，對其若干形式系統(tǒng)及算子進行了研究，主要工作和創(chuàng)新概括如下：
　　

2、·證明了Cirquent演算系統(tǒng)CL6關(guān)于可計算性邏輯語義的可靠性與完備性.首先給出與證明相關(guān)的所有語法定義；然后利用形式系統(tǒng)CL2關(guān)于可計算性邏輯語義的可靠完備性，間接地從語法角度證明了系統(tǒng)CL6的可靠完備性，從而得到既是經(jīng)典命題邏輯又是Cirquent演算系統(tǒng)CL5的擴張。
　　·揭示了平行復發(fā)算子與不可數(shù)分支復發(fā)算子的關(guān)系.首先給出關(guān)于平行復發(fā)算子的Cirquent演算系統(tǒng)；其次定義關(guān)于平行復發(fā)算子的Cirquent的語義；

3、然后在此定義基礎上證明關(guān)于平行復發(fā)算子的Cirquent演算系統(tǒng)的可靠性，得到由不可數(shù)分支復發(fā)算子誘導的邏輯是由平行復發(fā)算子誘導的邏輯的真子集；最后，在不可數(shù)分支復發(fā)邏輯蘊含平行復發(fā)但反之不成立的意義下，得到平行復發(fā)算子嚴格地弱于不可數(shù)分支復發(fā)算子，至此徹底搞清了這兩個算子自提出以來模糊不清的關(guān)系。
　　·揭示了可數(shù)分支復發(fā)算子與不可數(shù)分支復發(fā)算子的關(guān)系.首先給出可數(shù)分支復發(fā)算子新的簡化定義，證明該定義與舊定義的邏輯等價性；然后定

4、義關(guān)于可數(shù)分支復發(fā)算子的Cirquent的語義，并在此基礎上證明關(guān)于可數(shù)分支復發(fā)算子的Cirquent演算系統(tǒng)的可靠性，得到由不可數(shù)分支復發(fā)算子誘導的邏輯是由可數(shù)分支復發(fā)算子誘導的邏輯的真子集；最后得到可數(shù)分支復發(fā)算子嚴格地弱于不可數(shù)分支復發(fā)算子.同樣，這使得可數(shù)與不可數(shù)分支復發(fā)算子的關(guān)系徹底明了化。
　　·基于可計算性邏輯Cirquent演算方法的優(yōu)越性，為命題邏輯公式提出一種壓縮表達方式，并證明基于該表達的命題邏輯系統(tǒng)比傳統(tǒng)相

5、繼式演算系統(tǒng)Gentzen＼{cut}的證明效率有指數(shù)級的提高，從而為經(jīng)典命題邏輯提供了一個可靠完備的但證明效率較高的形式系統(tǒng).其次，研究Cirquent演算系統(tǒng)CL8S的性質(zhì)，證明其中的演繹定理成立，并對比CL8S與結(jié)構(gòu)演算系統(tǒng)SKSg的證明復雜度，得到CL8S限制在命題邏輯水平p-仿真SKSg。
　　·基于可計算性邏輯博弈語義的優(yōu)越性，分析了可計算性邏輯有望取代經(jīng)典邏輯作為知識庫系統(tǒng)邏輯基礎的優(yōu)越性與可行性，并以可計算性邏輯的