數(shù)理邏輯引論：計(jì)算機(jī)科學(xué)與系統(tǒng)的天然基礎(chǔ)

目錄
前言
第1章導(dǎo)論1
1.1邏輯的基本概念和術(shù)語(yǔ)1
1.2邏輯學(xué)3
1.2.1概念與命題3
1.2.2推理論證5
1.2.3自然語(yǔ)言的歧義性與悖論7
1.3從亞里士多德經(jīng)典邏輯到現(xiàn)代數(shù)理邏輯的演化8
1.3.1形式邏輯—推理形式與內(nèi)容的分離9
1.3.2數(shù)理邏輯14
1.4計(jì)算機(jī)科學(xué)中的邏輯19
1.4.1邏輯是計(jì)算理論的天然基礎(chǔ)19
1.4.2計(jì)算機(jī)科學(xué)技術(shù)領(lǐng)域的形式語(yǔ)言20
1.4.3形式證明與驗(yàn)證26
第2章離散數(shù)學(xué)基礎(chǔ)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等價(jià)關(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ù)學(xué)歸納法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塔斯基不動(dòng)點(diǎn)理論82
2.7.5完全偏序集及不動(dòng)點(diǎn)理論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斷言形式的語(yǔ)法樹(shù)101
3.5重言式和矛盾式102
3.6邏輯等價(jià)和邏輯蘊(yùn)涵104
3.6.1邏輯等價(jià)104
3.6.2等價(jià)替換106
3.6.3邏輯蘊(yùn)涵的性質(zhì)111
3.7對(duì)偶式和斷言范式114
3.7.1對(duì)偶式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一階形式語(yǔ)言154
5.2.1字母表155
5.2.2一階語(yǔ)言的實(shí)例156
5.2.3合式公式157
5.2.4形式語(yǔ)言的語(yǔ)法層次結(jié)構(gòu)158
5.2.5變?cè)淖杂膳c約束出現(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重言式和邏輯等價(jià)175
5.4.1重言式175
5.4.2邏輯有效的公式177
5.4.3邏輯蘊(yùn)涵和邏輯等價(jià)178
5.5斯科倫定理181
第6章形式化謂詞邏輯184
6.1形式系統(tǒng)KL184
6.1.1KL的有效性186
6.1.2KL的演繹定理188
6.2可證明等價(jià)和代換192
6.3KL的充分性定理199
6.3.1KL的擴(kuò)展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ù)學(xué)系統(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ù)的模型及完備性問(wèn)題229
7.5公理集合論230
7.5.1ZF公理系統(tǒng)230
7.5.2ZF公理系統(tǒng)的模型232
7.6相容性和模型之間的關(guān)系234
第8章程序設(shè)計(jì)理論導(dǎo)引236
8.1計(jì)算、計(jì)算機(jī)和計(jì)算機(jī)程序236
8.1.1可計(jì)算性和計(jì)算機(jī)236
8.1.2程序語(yǔ)法的非形式定義240
8.1.3程序的非形式語(yǔ)義242
8.2程序語(yǔ)言的形式語(yǔ)法244
8.3程序語(yǔ)言的操作語(yǔ)義246
8.3.1棧-狀態(tài)-控制抽象機(jī)解釋語(yǔ)義247
8.3.2基于操作語(yǔ)義的程序分析和驗(yàn)證249
8.3.3結(jié)構(gòu)化操作語(yǔ)義251
8.3.4完整的結(jié)構(gòu)化操作語(yǔ)義255
8.4程序語(yǔ)言的指稱語(yǔ)義258
8.4.1基本思想和技術(shù)258
8.4.2核心問(wèn)題260
8.4.3Mini的指稱語(yǔ)義定義261
8.5指稱語(yǔ)義和操作語(yǔ)義的一致性265
8.6程序語(yǔ)言的公理語(yǔ)義268
8.6.1非形式霍爾邏輯269
8.6.2霍爾邏輯271
8.6.3霍爾邏輯可靠性和完全性276
8.7抽象數(shù)據(jù)類型281
參考文獻(xiàn)284
索引285