123,123

內(nèi)容簡(jiǎn)介

　　邏輯定理的機(jī)器證明是人工智能領(lǐng)域人們最早從事研究的課題。《機(jī)器證明的邏輯推定》從邏輯定理的人工證明和機(jī)器證明兩方面來(lái)展現(xiàn)邏輯定理證明的藝術(shù)，而機(jī)器證明又從定理的自動(dòng)證明和計(jì)算機(jī)輔助證明兩個(gè)方面來(lái)展現(xiàn)?！稒C(jī)器證明的邏輯推定》首先用作者構(gòu)造的命題演算系統(tǒng)FPC和狹謂詞演算系統(tǒng)FQC完成常用邏輯定理的人工證明（一種自然推理證明）。其次，用邏輯定理的機(jī)器證明工具TPG（Tree Proof Generator）實(shí)現(xiàn)邏輯定理的自動(dòng)證明（一種樹證明）。最后，用交互式定理機(jī)器證明工具Fitch實(shí)現(xiàn)了邏輯定理的計(jì)算機(jī)證明（一種自然推理證明）。

作者簡(jiǎn)介

暫缺《機(jī)器證明的邏輯推定》作者簡(jiǎn)介

圖書目錄

目錄前言第1章邏輯演算系統(tǒng)FPC和FQC 11.1 命題邏輯演算系統(tǒng)FPC 1 1.1.1 系統(tǒng)FPC的形式語(yǔ)言 1 1.1.2 系統(tǒng)FPC的推理規(guī)則 3 1.2 謂詞演算系統(tǒng)FQC 8 1.2.1 系統(tǒng)FQC的形式語(yǔ)言 8 1.2.2 系統(tǒng)FQC的推理規(guī)則 11 第2章人工對(duì)邏輯系統(tǒng)定理的證明 14 2.1 人工對(duì)系統(tǒng)FPC定理的證明 14 2.2 人工對(duì)系統(tǒng)FQC定理的證明 41 第3章演算系統(tǒng)的樹證明 66 3.1 樹證明規(guī)則 66 3.1.1 FPC的樹證明規(guī)則 66 3.1.2 FQC的樹證明規(guī)則 69 3.2 計(jì)算機(jī)自動(dòng)證明器TPG簡(jiǎn)介 72 3.2.1 TPG的功能 72 3.2.2 TPG的使用說(shuō)明 72 3.3 FPC定理的樹證明 73 3.4 FQC定理的樹證明 120 第4章邏輯演算系統(tǒng)的擴(kuò)充系統(tǒng) 157 4.1 命題演算系統(tǒng)FPC的擴(kuò)充系統(tǒng)FPC 157 4.2 謂詞演算系統(tǒng)FQC的擴(kuò)充系統(tǒng)FQC 159 4.3 邏輯系統(tǒng)FPC的推理規(guī)則一覽表 160 4.3.1 系統(tǒng)FPC推理規(guī)則一覽表 160 4.3.2 系統(tǒng)FQC推理規(guī)則一覽表 162 第5章邏輯演算系統(tǒng)的Fitch證明 163 5.1 Fitch簡(jiǎn)介 163 5.2 Fitch的部分證明規(guī)則 164 5.2.1 Fitch的命題規(guī)則 164 5.2.2 Fitch的部分一階規(guī)則 167 5.2.3 Fitch證明的部分結(jié)論規(guī)則 168 5.3 系統(tǒng)FPC定理的Fitch證明 169 5.4 系統(tǒng)FQC定理的Fitch證明 221 參考文獻(xiàn) 256