本文關(guān)鍵詞：基于Tableau的定理證明器的優(yōu)化技術(shù)研究，，由筆耕文化傳播整理發(fā)布。

【摘要】：語義Tableau是一種具有較強直觀性和適用性的推理方法.自該方法問世以來,一直吸引著大量人工智能研究者.基于Prolog語言,M.C.Fitting利用語義Tableau方法提出了一種一階邏輯自動定理證明器.眾所周知,系統(tǒng)的實現(xiàn)效率問題一直是人工智能界的一個熱點問題.M.C.Fitting給出的定理證明器雖然比較容易理解,但是在具體應(yīng)用過程中卻存在著一定的效率問題,論文便是針對這一問題展開了具體的研究.具體的研究內(nèi)容如下:1論文首先給出了一階邏輯語言的項、公式、子句等有關(guān)的概念,然后在此基礎(chǔ)上研究了一階邏輯語言理論及其模型系統(tǒng),并重點探討了Herbrand模型.2論文介紹語義Tableau方法的理論和實現(xiàn).首先描述了Tableau方法的概念與其在實際應(yīng)用過程中的語義Tableau擴展規(guī)則,并完成了該方法的可靠性和完備性的證明,重點介紹了在證明完備性過程中所要用到的模型存在定理;其次給出了實現(xiàn)該系統(tǒng)的算法與在Prolog語言下的代碼.3通過對M.C.Fitting給出的定理證明器中存在的效率問題進(jìn)行分析研究,提出了相關(guān)的改進(jìn),并給出了改進(jìn)后的算法以及該算法可終止性和正確性的證明.最后進(jìn)行了相應(yīng)的對比實驗,結(jié)果表明:優(yōu)化后的語義Tableau定理證明器的推理效率得到了顯著的提高.
【關(guān)鍵詞】：語義Tableau 定理證明器 Prolog
【學(xué)位授予單位】：遼寧師范大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2015
【分類號】：B812.3
【目錄】：

• 摘要4-5
• Abstract5-7
• 1 緒論7-9
• 1.1 論文的背景及意義7
• 1.2 論文研究現(xiàn)狀7-8
• 1.3 本文的工作8
• 1.4 內(nèi)容安排8-9
• 2 一階邏輯基礎(chǔ)9-16
• 2.1 一階邏輯的概念9-10
• 2.2 一階邏輯的替換10-12
• 2.3 一階邏輯語義12-14
• 2.4 Herbrand模型14-16
• 3 Tableau方法的理論16-27
• 3.1 一階邏輯的語義Tableau方法16-17
• 3.2 一階模型存在定理17-19
• 3.3 一階語義Tableau的可靠性和完備性19-20
• 3.4 通代20-23
• 3.5 通代的實現(xiàn)23
• 3.6 自由語義Tableau23-24
• 3.7 一階自由變元Tableau的完備性和可靠性24-27
• 4 一階自由語義Tableau系統(tǒng)的實現(xiàn)與改進(jìn)27-33
• 4.1 一階自由變元Tableau的實現(xiàn)27-28
• 4.2 一階自由變元Tableau的改進(jìn)28-30
• 4.3 實驗對比30-33
• 結(jié)論33-34
• 參考文獻(xiàn)34-36
• 附錄A 通代實現(xiàn)的代碼36-38
• 附錄B 一階自由變元Tableau的實現(xiàn)代碼38-43
• 攻讀碩士學(xué)位期間發(fā)表學(xué)術(shù)論文情況43-44
• 致謝44

【相似文獻(xiàn)】

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

1 江建國;iGeo：智能幾何軟件的定理證明器[D];中國科學(xué)院研究生院（成都計算機應(yīng)用研究所）;2006年

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

1 高華;基于Tableau的定理證明器的優(yōu)化技術(shù)研究[D];遼寧師范大學(xué);2015年

2 郝r;解決自動定理證明器在程序驗證中兩點能力不足的辦法[D];中國科學(xué)技術(shù)大學(xué);2015年

3 陳波;基于定理證明器HOL的硬件驗證研究[D];蘭州大學(xué);2006年

4 陳明雁;基于概率檢測組合模型的幾何定理證明器[D];華東師范大學(xué);2014年

5 程應(yīng)娥;Isabelle中自動化證明策略的設(shè)計與實現(xiàn)[D];蘭州大學(xué);2007年

6 游珍;Isabelle定理證明器的剖析及其在PAR方法/PAR平臺中的應(yīng)用[D];江西師范大學(xué);2009年

  本文關(guān)鍵詞：基于Tableau的定理證明器的優(yōu)化技術(shù)研究，由筆耕文化傳播整理發(fā)布。

本文編號：510855