智能推理是實現智能化的基礎,它包括經典的單調推理和非單調推理。《智能推理及其在信念修正中的應用》首先介紹了經典的單調推理中的命題推理系統和謂詞推理系統,以及推理的公理化系統和自然推理系統;其次,介紹了單調推理系統下的自動推理算法和可滿足性驗證算法:然后介紹了非單調推理的主要理論和方法,包括非單調推理邏輯、自知邏輯、缺省邏輯和限定邏輯、信念修正的理論和方法,以及信念修正的實現算法;最后介紹了Petri網用于邏輯推理和信念修正的方法。
《智能推理及其在信念修正中的應用》可供人工智能、邏輯學、智能信息處理、智能控制、計算機科學與技術、軟件工程等專業的教師、研究生以及相關領域科研工作者參考。
對于智能的研究可以追溯到圖靈。圖靈在他的文章《計算機與智能》中提出了“機器思維”的概念,討論了人類智能機械化的可能性和圖靈機的理論模型,為智能的研究確定了目標,指明了方向。他還設計了著名的“圖靈測試”,試圖讓機器模仿人來回答某些問題,通過實驗和觀察來判斷機器是否具備智能。“圖靈測試”要求觀察者不斷提出各種問題,根據回答來辨別哪一個是人,哪一個是機器。人工智能作為計算機學科的一個重要分支,是由麥卡錫(McCarthy)于1956年在達特茅斯舉行的會議上正式提出的,并將其研究內容概括為研究人類智能活動的規律、構造具有一定智能行為的人工系統;也就是,研究用人工的方法和技術,模仿、延伸和拓展人的智能,實現機器的智能;其長期目標是實現人類水平的智能。
人工智能通過一段時間的發展,形成符號主義學派、連接主義學派和行為主義學派。符號主義,又稱為邏輯主義、心理學派或計算機學派,其原理主要為物理符號系統假設和有限合理性原理,認為人工智能的研究方法應該是功能模擬方法,通過分析人類認知系統所具備的功能和機能,用計算機模擬這些功能,實現人工智能。這種方法目前主要是用數理邏輯方法來建立人工智能的統一理論體系,但遇到了很多暫時無法解決的困難。連接主義,又稱為仿生學派或生理學派,其原理主要為神經網絡和神經網絡之間的連接機制與學習算法,主張人工智能應著重于結構模擬,即模擬人的生理神經網絡結構,并認為功能、結構和智能行為是密切相關的;不同結構表現出不同的功能和行為,目前已經提出多種人工神經網絡結構和眾多的學習算法。行為主義,又稱為進化主義或控制論學派,其原理為控制論及感知.動作型控制系統:認為人工智能的研究方法應采用行為模擬方法,也認為功能、結構和智能行為是不可分的;且不同的行為表現出不同的功能和不同的控制結構,其代表作品為六足行走機器人。
人工智能研究的領域有很多方面,總體上分為兩個方面:機器智能、智能機器。在機器智能方面,經典的研究領域有問題求解、機器定理證明、專家系統、自然語言理解、神經網絡等。在問題求解方面就是下棋程序,在下棋程序中使用的某些技術,如向前看幾步的思想、把難問題分成幾個比較容易求解的子問題,后來發展成為搜索技術和問題規約技術,這些技術成為人工智能的基本技術。機器定理證明是人工智能研究領域中最經典的研究方向之一,并且在人工智能方法的發展中曾經產生過重要的影響,如謂詞邏輯語言演繹過程的形式化有助于更清楚地理解推理過程;還可以把許多非形式化的問題和定理證明問題一樣加以形式化,使得機器定理證明的技術在生產和生活中得到應用,如醫療診斷和信息檢索等。
前言
第1章 緒論
1.1 邏輯推理的發展歷史
1.1.1 邏輯演算
1.1.2 證明論
1.1.3 模型論
1.1.4 遞歸論
1.1.5 公理化集合論
1.1.6 非單調推理理論
1.1.7 自動推理技術
1.1.8 不確定性推理
1.2 信念修正簡介
1.2.1 信念狀態的模型
1.2.2 信念變化的基本形式
1.2.3 信念修正理論的應用
1.3 自動推理理論和信念修正之間的關系
1.3.1 自動推理理論是實現信念修正的一種途徑
1.3.2 信念修正可以實現非單調推理
參考文獻
第2章 單調邏輯
2.1 命題演算邏輯系統
2.1.1 命題演算的基本概念
2.1.2 命題邏輯的合式公式及范式
2.2 謂詞邏輯
2.2.1 謂詞演算中的基本概念
2.2.2 謂詞邏輯的合式公式
2.2.3 謂詞形式系統的語義
2.3 邏輯演算的形式系統
2.3.1 公理系統
2.3.2 自然推理系統
參考文獻
第3章 自動推理與可滿足性驗證
3.1 斯科倫標準形
3.2 埃爾布朗域和埃爾布朗定理
3.2.1 埃爾布朗域
3.2.2 語義樹
3.3 DP算法
3.4 置換與合
3.5 歸結原理
3.5.1 命題邏輯的歸結
3.5.2 謂詞邏輯的歸結
3.5.3 歸結原理的完備性及過程控制策略
3.6 可滿足性問題的非完全算法
3.7 二元可滿足性問題和霍恩可滿足性問題的快速算法
3.7.1 二元可滿足性問題的快速算法
3.7.2 霍恩可滿足性問題的快速算法
3.8 極大可滿足問題的算法
3.8.1 貪心算法
3.8.2 局部搜索算法
3.8.3 模擬退火算法
參考文獻
第4章 非單調推理
4.1 非單調邏輯產生的背景
4.1.1 非單調推理產生的基礎
4.1.2 常識推理促使了非單調推理的產生
4.2 非單調邏輯
4.3 缺省邏輯
4.3.1 基本定義
4.3.2 封閉缺省理論的性質
4.3.3 封閉正規缺省理論
4.3.4 封閉正規缺省理論的證明論
4.4 限定邏輯
4.4.1 限定的定義
4.4.2 優先序限定
4.5 自認知邏輯
4.5.1 自知邏輯的語法
4.5.2 自知邏輯的語義
參考文獻
第5章 信念修正理論
5.1 信念修正的定義
5.2 信念修正的AGM理論
5.2.1 約減和修正的合理公設
5.2.2 選擇約減
5.2.3 安全約減
5.3 認知牢固度的方法
5.4 信念基的方法
5.5 迭代信念修正理論
5.5.1 基于條件函數的迭代修正
5.5.2 具有記憶的迭代修正
5.5.3 基于有限偏序牢固度秩的迭代修正
5.6 信念修正的應用
參考文獻
第6章 單調推理技術在信念修正中的應用
6.1 基于核的信念基修正
6.1.1 核約減和修正
6.1.2 極小割集
6.1.3 計算核的算法
6.1.4 計算極大協調子集的算法
6.1.5 核和極大協調子集之間的關系
6.2 基于模型的修正和基于語法的修正
6.2.1 基于模型的方法
6.2.2 基于語法的方法
6.3 信念修正的轉換系統
6.3.1 求極大協調子集的轉換系統
6.3.2 求極小不協調子集的轉換系統
6.4 基于歸結的有限子句集上的信念修正實現算法
6.4.1 極大協調子集的方法
6.4.2 子句集上求所有極小不協調子集的方法
6.4.3 典型的信念修正方法的實現
6.5 信念修正的近似算法
6.5.1 修正的近似算法
6.5.2 具有完整性約束的信念修正方法
6.5.3 有限信念基上的修正和約減過程
參考文獻
第7章 非單調推理技術在信念修正中的應用
7.1 信念修正和缺省推理
7.2 限定推理與信念修正
參考文獻
第8章 信念修正的Petri網方法
8.1 Petri與邏輯推理
8.1.1 Petri網的基本概念
8.1.2 霍恩子句的Petri網描述
8.1.3 一般子句化為Petri網
8.2 Petri網與歸結原理
8.2.1 霍恩基子句集的網刪除歸結原理
8.2.2 一般基子句集的網刪除歸結原理
8.3 基于Petri網的修正方法
8.3.1 命題規則知識庫的Petri網描述
8.3.2 知識庫更新的代數方法
8.3.3 擴充邏輯程序的知識庫更新
參考文獻