可計算性邏輯是新近提出的關(guān)于可計算性的形式理論.它采取交互的博弈語義,是一種資源邏輯.經(jīng)典邏輯、直覺邏輯和線性邏輯(在廣義上)只是可計算性邏輯的三個特殊部分.相比于傳統(tǒng)邏輯,可計算性邏輯具有更強(qiáng)的表達(dá)能力和更高的證明效率,這使得它有望在知識庫系統(tǒng)、人工智能行為規(guī)劃系統(tǒng)、電路等價性驗證等領(lǐng)域得到廣泛的應(yīng)用. 本文主要利用可計算性邏輯的Cirquent演算方法,對其若干形式系統(tǒng)及算子進(jìn)行了研究,主要工作和創(chuàng)新概括如下： ●證明了Cirquent演算系統(tǒng)CL6關(guān)于可計算性邏輯語義的可靠性與完備性.首先給出與證明相關(guān)的所有語法定義；然后利用形式系統(tǒng)CL2關(guān)于可計算性邏輯語義的可靠完備性,間接地從語法角度證明了系統(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的語義;然后在此定義基礎(chǔ)上證明關(guān)于平行復(fù)發(fā)算子的Cirquent演算系統(tǒng)的可靠性,得到由不可數(shù)分支復(fù)發(fā)算子誘導(dǎo)的邏輯是由平行復(fù)發(fā)算子誘導(dǎo)的邏輯的真子集；最后,...

【文章頁數(shù)】：113 頁

【學(xué)位級別】：博士

【文章目錄】：
作者簡介
算子符號說明
摘要
ABSTRACT
第一章 緒論
    1.1 可計算性邏輯的背景與現(xiàn)狀
        1.1.1 研究背景與意義
        1.1.2 研究進(jìn)展與現(xiàn)狀
    1.2 博弈語義
    1.3 形式系統(tǒng)CL4
    1.4 Cirquent演算系統(tǒng)CL8
    1.5 本文的主要工作與結(jié)構(gòu)安排
第二章 Cirquent演算系統(tǒng)CL6的可靠性與完備性
    2.1 引言
    2.2 Cirquent、系統(tǒng)CL5及系統(tǒng)CL2
    2.3 形式系統(tǒng)CL6
    2.4 形式系統(tǒng)CL6的可靠性與完備性
    2.5 小結(jié)
第三章 平行復(fù)發(fā)算子與不可數(shù)分支復(fù)發(fā)算子的關(guān)系
    3.1 引言
    3.2 關(guān)于平行復(fù)發(fā)算子的形式系統(tǒng)CL15
    3.3 Cirquent的語義
    3.4 平行復(fù)發(fā)算子與不可數(shù)分支復(fù)發(fā)算子的關(guān)系
    3.5 小結(jié)
第四章 可數(shù)分支復(fù)發(fā)算子與不可數(shù)分支復(fù)發(fā)算子的關(guān)系
    4.1 引言
    4.2 關(guān)于可數(shù)分支復(fù)發(fā)算子的形式系統(tǒng)CL15
    4.3 可數(shù)分支復(fù)發(fā)算子的新定義
    4.4 Cirquent的語義
    4.5 可數(shù)分支復(fù)發(fā)算子與不可數(shù)分支復(fù)發(fā)算子的關(guān)系
    4.6 小結(jié)
第五章 可計算性邏輯的優(yōu)越性
    5.1 引言
    5.2 命題邏輯公式的壓縮表示及其相應(yīng)的形式系統(tǒng)
    5.3 Cirquent演算系統(tǒng)CL8S的演繹定理及其證明復(fù)雜度
    5.4 基于可計算性邏輯的知識庫系統(tǒng)
    5.5 小結(jié)
結(jié)束語
致謝
參考文獻(xiàn)
在讀博士期間撰寫(發(fā)表)的論文
在讀期間參加研究的科研項目



本文編號：3925937