機器證明的邏輯推定

前言

第1章 邏輯演算系統FPC和FQC 1
1.1 命題邏輯演算系統FPC 1
1.1.1 系統FPC的形式語言 1
1.1.2 系統FPC的推理規則 3
1.2 謂詞演算系統FQC 8
1.2.1 系統FQC的形式語言 8
1.2.2 系統FQC的推理規則 11

第2章 人工對邏輯系統定理的證明 14
2.1 人工對系統FPC定理的證明 14
2.2 人工對系統FQC定理的證明 41

第3章 演算系統的樹證明 66
3.1 樹證明規則 66
3.1.1 FPC的樹證明規則 66
3.1.2 FQC的樹證明規則 69
3.2 電腦自動證明器TPG簡介 72
3.2.1 TPG的功能 72
3.2.2 TPG的使用說明 72
3.3 FPC定理的樹證明 73
3.4 FQC定理的樹證明 120

第4章 邏輯演算系統的擴充系統 157
4.1 命題演算系統FPC的擴充系統FPC 157
4.2 謂詞演算系統FQC的擴充系統FQC 159
4.3 邏輯系統FPC的推理規則一覽表 160
4.3.1 系統FPC推理規則一覽表 160
4.3.2 系統FQC推理規則一覽表 162

第5章 邏輯演算系統的Fitch證明 163
5.1 Fitch簡介 163
5.2 Fitch的部分證明規則 164
5.2.1 Fitch的命題規則 164
5.2.2 Fitch的部分一階規則 167
5.2.3 Fitch證明的部分結論規則 168
5.3 系統FPC定理的Fitch證明 169
5.4 系統FQC定理的Fitch證明 221

參考文獻 256