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

【文章頁數】：113 頁

【學位級別】：博士

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



本文編號：3925937