本文關(guān)鍵詞：對核證邏輯的研究，，由筆耕文化傳播整理發(fā)布。

【摘要】：核證的概念自柏拉圖時代以來就是認(rèn)知研究中的一個重要部分,柏拉圖對知識有三個準(zhǔn)則：核證,真,信念,但是,盡管邏輯研究者在知識和信念的形式化的邏輯模型中處理了信念和真,核證卻一直缺少相應(yīng)的處理,直到核證邏輯出現(xiàn)后,核證才被引入到知識的邏輯模型中。 哥德爾在1938年就對核證邏輯有所論述,阿爾捷莫夫和施特拉森提出了證明邏輯的雛形,阿爾捷莫夫在1994年首次給出了證明邏輯LP,在2001年完全正式地、比較系統(tǒng)地給出了證明邏輯LP,由此可以引出許多新的核證邏輯系統(tǒng)。核證邏輯的第一個標(biāo)準(zhǔn)的可能世界模型是姆克爾特切夫在1997年給出的姆克爾特切夫模型,菲廷在2005年正式給出了LP的可能世界模型,此外還有模式模型、極小模型等模型。核證邏輯的保守擴張問題也是一個重要問題。 亞沃爾斯卡婭把可證明性邏輯GL和LP組合在一起得到了LPP,阿爾捷莫夫和諾吉娜給出了GLA的公理系統(tǒng),二人也對同時帶有經(jīng)典模態(tài)算子和核證的系統(tǒng)S4LP和S4LPN進(jìn)行了研究。阿爾捷莫夫引入了基于證據(jù)的知識,進(jìn)而在知識的多主體邏輯的基礎(chǔ)上得到了基于證據(jù)的知識系統(tǒng),他給出了與TnLP, S4nLP和S5nLP對應(yīng)的核證知識系統(tǒng)TnJ,S4nJ和S5nJ、,此外,還有對混合-JT、否定邏輯和核證摹狀邏輯的研究。我們用T3J給出了泥孩難題的一種解決方法。 菲廷給出了QLP,迪安和黑川用QLP分析了知道者悖論,但阿洛-科斯塔和岸田反對這種分析,量化的菲廷模型是在LP的菲廷模型的基礎(chǔ)上添加了階量化機制得到的,阿爾捷莫夫和亞沃爾斯卡婭提出了一階證明邏輯FOLP,菲廷基于LP的菲廷模型給出了FOLP的可能世界模型,我們得到了一種新的系統(tǒng)QLP’,比QLP更為簡單和自然。 LP的表列系統(tǒng)是在2004年首次由雷恩給出,菲廷給出了S4LP的一種表列系統(tǒng),雷恩之后給出了LP和S4LP的另一種表列系統(tǒng),芬格爾給出了LP的兩種分析的表列系統(tǒng)KELP和PREKELP,黑川給出了S4LPN的一種前綴表列系統(tǒng)TS4LPN,菲廷給出了K+J,S4LP,S4LPN和S5LPN的一種前綴表列系統(tǒng)。 阿爾捷莫夫在1995年就給出了LP的實現(xiàn)概念和實現(xiàn)算法。勃列日涅夫和庫茲涅茨給出了證明多項式至多是平方長度的實現(xiàn)算法,菲廷給出了直接對核證進(jìn)行推理的機制,布呂納、格奇和庫茲涅茨證明了一種語法的實現(xiàn)定理,格奇和庫茲涅茨之后給出了一種證明實現(xiàn)定理的更為一般的構(gòu)造性的方法,并給出了統(tǒng)一實現(xiàn)定理,菲廷基于表列系統(tǒng)給出了LP的一種新的實現(xiàn)算法,還給出了LP的實現(xiàn)的一種Prolog執(zhí)行程序。我們將菲廷的實現(xiàn)算法擴展到了FOLP的情況,并詳細(xì)地證明了FOLP的準(zhǔn)實現(xiàn)到實現(xiàn)的算法的正確性。 核證邏輯源自主流認(rèn)知理論、數(shù)理邏輯、計算機科學(xué)和人工智能等理論,它吸收了源自主流認(rèn)知理論和證明論的基本原理,為直覺主義邏輯提供了一種算術(shù)語義,也為知識邏輯提供了一種新的以證據(jù)為基礎(chǔ)的語義,它的出現(xiàn)解決了經(jīng)典模態(tài)系統(tǒng)S4的哥德爾可證明性語義的問題和直覺主義命題邏輯的BHK語義的形式化問題,也解決了認(rèn)知邏輯中“核證”這一概念在知識模型方面的問題,使認(rèn)知邏輯的表達(dá)力更強了,核證項也為核證邏輯的復(fù)雜度問題提供了一種較為自然的衡量機制。當(dāng)前,邏輯研究者對核證邏輯的研究仍然較為活躍,核證邏輯具有較多的改進(jìn)余地、廣闊的研究空間和巨大的發(fā)展?jié)摿Α?br/> 【關(guān)鍵詞】：核證 核證邏輯 證明邏輯 模型 實現(xiàn)
【學(xué)位授予單位】：南開大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2014
【分類號】：B81-06
【目錄】：

• 摘要5-7
• Abstract7-9
• 目錄9-11
• 引言11-18
• 第一章 核證邏輯概述18-44
• 第一節(jié) 哥德爾的建議18-20
• 第二節(jié) 核證邏輯早期的發(fā)展20-26
• 第三節(jié) 核證邏輯的系統(tǒng)26-34
• 第四節(jié) 核證邏輯的經(jīng)典可能世界模型34-42
• 一、姆克爾特切夫模型34-36
• 二、菲廷模型36-38
• 三、模式模型38-42
• 第五節(jié) 核證邏輯的保守性42-44
• 第二章 與其它邏輯組合的核證邏輯與多主體核證邏輯44-66
• 第一節(jié) LPP和GLA44-48
• 第二節(jié) S4LP和S4LPN48-50
• 第三節(jié) 核證知識系統(tǒng)50-58
• 第四節(jié) 混合-JT、否定邏輯和核證摹狀邏輯58-61
• 第五節(jié) 對泥孩難題的解決61-66
• 第三章 量化核證邏輯66-85
• 第一節(jié) QLP66-71
• 第二節(jié) 量化的菲廷模型71-74
• 第三節(jié) FOLP74-77
• 第四節(jié) FOLP的菲廷模型77-79
• 第五節(jié) 一種更為自然的系統(tǒng)QLP~*79-85
• 第四章 核證邏輯的表列演算85-101
• 第一節(jié) 前期的研究85-89
• 第二節(jié) 芬格爾的進(jìn)路89-94
• 第三節(jié) 當(dāng)前的發(fā)展94-101
• 第五章 核證邏輯的實現(xiàn)101-134
• 第一節(jié) 傳統(tǒng)實現(xiàn)算法101-104
• 第二節(jié) 后來的一些發(fā)展104-107
• 第三節(jié) 對應(yīng)表列演算的實現(xiàn)107-117
• 第四節(jié) 擴展到FOLP的實現(xiàn)117-134
• 一、準(zhǔn)實現(xiàn)117-118
• 二、一些基本的概念118-122
• 三、準(zhǔn)實現(xiàn)到實現(xiàn)的算法122-125
• 四、算法的正確性證明125-134
• 結(jié)語134-135
• 參考文獻(xiàn)135-143
• 致謝143-144
• 個人簡歷144

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 查非;劉虎;;狀態(tài)相似性與流量限制模型[J];邏輯學(xué)研究;2011年02期

2 郭美云;;分布式知識的研究進(jìn)展[J];哲學(xué)動態(tài);2007年11期

3 ;[J];;年期

4 ;[J];;年期

5 ;[J];;年期

6 ;[J];;年期

7 ;[J];;年期

8 ;[J];;年期

9 ;[J];;年期

10 ;[J];;年期

中國重要報紙全文數(shù)據(jù)庫 前2條

1 趙宗祥;模型廠商 你聞到收藏的香味了嗎？　[N];中國商報;2002年

2 郁　雨;科技收藏：為了明天加緊收藏今天[N];中國藝術(shù)報;2004年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前3條

1 丁軼群;基于概率生成模型的文本主題建模及其應(yīng)用[D];浙江大學(xué);2010年

2 陳亞瑞;基于消息傳播的圖模型近似變分推理[D];天津大學(xué);2010年

3 李巍;對核證邏輯的研究[D];南開大學(xué);2014年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前7條

1 聶燕飛;基于層次分析法和灰色關(guān)聯(lián)分析的油田科技人才評價模型研究[D];上海交通大學(xué);2011年

2 申云成;UML模型到XMI的映射方法研究[D];昆明理工大學(xué);2010年

3 楊國勝;心肌細(xì)胞電生理模型通用表達(dá)方法研究及可視化實現(xiàn)[D];哈爾濱工業(yè)大學(xué);2007年

4 王光明;基于小波的隨機CARMA模型多尺度辨識方法的研究[D];遼寧科技大學(xué);2007年

5 王瑞;算子邏輯中公式恒真水平模型的生成算法研究[D];大連海事大學(xué);2010年

6 王一鳴;基于主題模型的場景視覺理解研究[D];南京大學(xué);2012年

7 張麗;時態(tài)公開宣告邏輯初探[D];西南大學(xué);2009年

  本文關(guān)鍵詞：對核證邏輯的研究，由筆耕文化傳播整理發(fā)布。

本文編號：492313