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

目錄
前言
第1章導論1
1.1邏輯的基本概念和術語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形式邏輯—推理形式與內容的分離9
1.3.2數(shù)理邏輯14
1.4計算機科學中的邏輯19
1.4.1邏輯是計算理論的天然基礎19
1.4.2計算機科學技術領域的形式語言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關系和關系代數(shù)49
2.2.1笛卡兒積49
2.2.2關系52
2.2.3等價關系和劃分55
2.2.4關系代數(shù)58
2.2.5關系的圖示61
2.3函數(shù)64
2.4集合、關系、函數(shù)和謂詞的聯(lián)系與統(tǒng)一66
2.4.1關系和函數(shù)的統(tǒng)一67
2.4.2集合、關系、函數(shù)、謂詞和布爾代數(shù)的統(tǒng)一67
2.5數(shù)學歸納法68
2.6集合上的序關系69
2.6.1偏序集70
2.6.2從已知的偏序集構造偏序集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邏輯蘊涵的性質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關于否定命題的證明與推演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形式語言的語法層次結構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形式化算術226
7.4.1算術的形式化226
7.4.2與皮亞諾算術的關系228
7.4.3形式化算術的模型及完備性問題229
7.5公理集合論230
7.5.1ZF公理系統(tǒng)230
7.5.2ZF公理系統(tǒng)的模型232
7.6相容性和模型之間的關系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結構化操作語義251
8.3.4完整的結構化操作語義255
8.4程序語言的指稱語義258
8.4.1基本思想和技術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