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

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

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

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

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

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