機器證明的邏輯推定

目錄 前言 第1章 邏輯演算系統(tǒng)FPC和FQC 11.1 命題邏輯演算系統(tǒng)FPC 1 1.1.1 系統(tǒng)FPC的形式語言 1 1.1.2 系統(tǒng)FPC的推理規(guī)則 3 1.2 謂詞演算系統(tǒng)FQC 8 1.2.1 系統(tǒng)FQC的形式語言 8 1.2.2 系統(tǒng)FQC的推理規(guī)則 11 第2章 人工對邏輯系統(tǒng)定理的證明 14 2.1 人工對系統(tǒng)FPC定理的證明 14 2.2 人工對系統(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 計算機自動證明器TPG簡介 72 3.2.1 TPG的功能 72 3.2.2 TPG的使用說明 72 3.3 FPC定理的樹證明 73 3.4 FQC定理的樹證明 120 第4章 邏輯演算系統(tǒng)的擴充系統(tǒng) 157 4.1 命題演算系統(tǒng)FPC的擴充系統(tǒng)FPC 157 4.2 謂詞演算系統(tǒng)FQC的擴充系統(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簡介 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 參考文獻 256