數(shù)理邏輯引論：計算機科學與系統(tǒng)的天然基礎

目錄
前言
第1章導論1
1.1邏輯的基本概念和術(shù)語1
1.2邏輯學3
1.2.1概念與命題3
1.2.2推理論證5
1.2.3自然語言的歧義性與悖論7
1.3從亞里士多德經(jīng)典邏輯到現(xiàn)代數(shù)理邏輯的演化8
1.3.1形式邏輯—推理形式與內(nèi)容的分離9
1.3.2數(shù)理邏輯14
1.4計算機科學中的邏輯19
1.4.1邏輯是計算理論的天然基礎19
1.4.2計算機科學技術(shù)領域的形式語言20
1.4.3形式證明與驗證26
第2章離散數(shù)學基礎29
2.1集合與集合代數(shù)30
2.1.1集合：概念、表示法和意義30
2.1.2子集34
2.1.3集合代數(shù)37
2.2關(guān)系和關(guān)系代數(shù)49
2.2.1笛卡兒積49
2.2.2關(guān)系52
2.2.3等價關(guān)系和劃分55
2.2.4關(guān)系代數(shù)58
2.2.5關(guān)系的圖示61
2.3函數(shù)64
2.4集合、關(guān)系、函數(shù)和謂詞的聯(lián)系與統(tǒng)一66
2.4.1關(guān)系和函數(shù)的統(tǒng)一67
2.4.2集合、關(guān)系、函數(shù)、謂詞和布爾代數(shù)的統(tǒng)一67
2.5數(shù)學歸納法68
2.6集合上的序關(guān)系69
2.6.1偏序集70
2.6.2從已知的偏序集構(gòu)造偏序集72
2.6.3偏序集間的函數(shù)74
2.7格、完全格和完全偏序集75
2.7.1偏序集的特殊子集和元素75
2.7.2格和完全格77
2.7.3保持上下確界的函數(shù)81
2.7.4塔斯基不動點理論82
2.7.5完全偏序集及不動點理論83
2.8集合的基數(shù)87
第3章樸素命題邏輯91
3.1引言91
3.2斷言和連接詞92
3.3連接詞的真值函數(shù)和真值表95
3.4斷言形式97
3.4.1斷言形式的真值函數(shù)和真值表98
3.4.2斷言形式的語法樹101
3.5重言式和矛盾式102
3.6邏輯等價和邏輯蘊涵104
3.6.1邏輯等價104
3.6.2等價替換106
3.6.3邏輯蘊涵的性質(zhì)111
3.7對偶式和斷言范式114
3.7.1對偶式114
3.7.2斷言形式的范式116
3.7.3充分連接詞集合118
3.7.4子句形式119
3.8推理及推理的有效性120
第4章形式化命題邏輯122
4.1形式邏輯系統(tǒng)123
4.2形式命題邏輯系統(tǒng)L125
4.3L中的演繹推理130
4.3.1演繹定理131
4.3.2關(guān)于否定命題的證明與推演134
4.4形式系統(tǒng)L的有效性137
4.5相容性和L的充分性定理138
第5章樸素謂詞邏輯147
5.1謂詞和量詞148
5.1.1謂詞149
5.1.2變量、量詞和函數(shù)149
5.2一階形式語言154
5.2.1字母表155
5.2.2一階語言的實例156
5.2.3合式公式157
5.2.4形式語言的語法層次結(jié)構(gòu)158
5.2.5變元的自由與約束出現(xiàn)159
5.2.6換名和代換161
5.3解釋165
5.3.1概念166
5.3.2賦值167
5.3.3合式公式可滿足性168
5.3.4真值和模型171
5.4重言式和邏輯等價175
5.4.1重言式175
5.4.2邏輯有效的公式177
5.4.3邏輯蘊涵和邏輯等價178
5.5斯科倫定理181
第6章形式化謂詞邏輯184
6.1形式系統(tǒng)KL184
6.1.1KL的有效性186
6.1.2KL的演繹定理188
6.2可證明等價和代換192
6.3KL的充分性定理199
6.3.1KL的擴展199
6.3.2充分性定理的證明201
6.4模型206
6.5范式209
6.5.1量詞轄域的變換209
6.5.2前束范式211
6.5.3子句形式213
第7章數(shù)學系統(tǒng)215
7.1帶等詞的一階系統(tǒng)216
7.2公理化群論221
7.2.1群的非形式定義221
7.2.2形式化群論222
7.3公理化布爾代數(shù)225
7.4形式化算術(shù)226
7.4.1算術(shù)的形式化226
7.4.2與皮亞諾算術(shù)的關(guān)系228
7.4.3形式化算術(shù)的模型及完備性問題229
7.5公理集合論230
7.5.1ZF公理系統(tǒng)230
7.5.2ZF公理系統(tǒng)的模型232
7.6相容性和模型之間的關(guān)系234
第8章程序設計理論導引236
8.1計算、計算機和計算機程序236
8.1.1可計算性和計算機236
8.1.2程序語法的非形式定義240
8.1.3程序的非形式語義242
8.2程序語言的形式語法244
8.3程序語言的操作語義246
8.3.1棧-狀態(tài)-控制抽象機解釋語義247
8.3.2基于操作語義的程序分析和驗證249
8.3.3結(jié)構(gòu)化操作語義251
8.3.4完整的結(jié)構(gòu)化操作語義255
8.4程序語言的指稱語義258
8.4.1基本思想和技術(shù)258
8.4.2核心問題260
8.4.3Mini的指稱語義定義261
8.5指稱語義和操作語義的一致性265
8.6程序語言的公理語義268
8.6.1非形式霍爾邏輯269
8.6.2霍爾邏輯271
8.6.3霍爾邏輯可靠性和完全性276
8.7抽象數(shù)據(jù)類型281
參考文獻284
索引285