目录 1
第一章 形式系统概论 1
1.1 从公理系统到形式系统 2
1.2 形式系统的定义 5
1.3 命题演算及命题演算形式系统 9
1.3.1 命题演算 9
1.3.2 命题演算形式系统 16
1.4 形式系统的元语言和元理论 19
1.4.1 形式系统的元语言和元理论 20
1.4.2 元理论关于系统语构的研究 22
1.4.3 元理论关于系统语义的研究 27
1.4.4 元理论关于系统语构及语义关系的研究 31
习题 36
第二章 一阶谓词演算 38
2.1 一阶谓词演算基本概念 38
2.1.1 谓词和函词 39
2.1.2 变元和常元 41
2.1.3 量词 43
2.2.1 一阶语言 47
2.2 一阶谓词演算形式系统 47
2.2.2 一阶逻辑 51
2.3 一阶谓词演算形式系统的语义 58
2.4 关于FSFC的重要元定理 62
2.4.1 FSFC的合理性及其它 62
2.4.2 FSFC的完备性及其它 63
2.4.3 FSFC的半可判定性 69
习题 70
3.1 使用五个真值联结词和两个量词的一阶谓词演算系统 73
第三章 其它形式的一阶谓词演算系统 73
3.2 带等词的一阶谓词演算系统 78
3.3 自然演绎系统 80
3.4 多型变元一阶谓词演算系统 91
3.5 直觉主义的一阶谓词演算系统 95
3.5.1 一阶谓词演算的直觉主义系统 96
3.5.2 直觉主义一阶谓词演算系统的语义 103
3.6 一阶谓词演算系统的形式表述能力 108
习题 113
4.1.1 斯柯伦标准形和子句集 115
第四章 消解原理及其应用 115
4.1 消解原理 115
4.1.2 赫布兰德结构 119
4.1.3 赫布兰德定理 124
4.1.4 消解原理 128
4.2 消解的策略 139
4.2.1 删除策略 139
4.2.2 支集策略 140
4.2.3 锁消解 141
4.2.4 线性消解 142
4.2.5 输入消解 143
4.2.6 单位消解 143
4.3 消解原理的应用 144
4.3.1 问题求解 145
4.3.2 规划生成 146
4.3.3 程序综合 147
4.3.4 程序分析和程序验证 150
4.4 带等词一阶谓词演算的消解及其它 154
习题 156
第五章 霍恩子句逻辑和逻辑程序设计 159
5.1 子句的蕴涵表示形式 159
5.2 霍恩子句逻辑 164
5.2.1 霍恩子句及其过程解释 164
5.2.2 关于霍恩子句逻辑程序的讨论 167
5.2.3 霍恩子句逻辑程序设计举例 174
5.3 Prolog语言简介 180
5.3.1 Prolog程序的基本构成与执行方式 180
5.3.2 Prolog语言的基本文法 183
5.3.3 Prolog的控制成分及Prolog程序实例 185
5.3.4 Prolog的基本特点 189
习题 190
第六章 二阶谓词演算 192
6.1 二阶语言 192
6.2 二阶谓词演算形式系统 194
6.3 二阶语义及其与二阶谓词演算系统的关系 200
6.3.1 满结构语义 201
6.3.2 一般结构语义 204
6.4 知识表示的格林方法和科瓦尔斯基方法 209
习题 213
第七章 模态逻辑 215
7.1 模态逻辑的非形式讨论 216
7.2 模态逻辑正规系统及其语义 219
7.2.1 模态语言及模态逻辑正规系统NSK 219
7.2.2 正规结构 223
7.2.3 关于正规系统的重要元定理 225
7.3.1 正规系统NSKD,NSKT,NSKB 229
7.3 模态逻辑系统NSKD,NSKT,NSKB,NSK4,NSK5及其它 229
7.3.2 正规系统NSK4,NSK5,S4,S5及其它 232
7.3.3 模态词的归约 238
7.4 模态谓词演算 245
7.5 模态逻辑的几种解释 247
7.5.1 真理论模态逻辑 247
7.5.2 认识论模态逻辑 247
7.5.3 道义论模态逻辑 252
7.5.4 时序逻辑 254
7.5.5 经验论模态逻辑 255
习题 258
第八章 时序逻辑 260
8.1 MPTL的语言 260
8.2 MPTL的语义 262
8.3 时序逻辑系统MPTL 266
8.3.1 时序命题演算 266
8.3.2 带等词的一阶时序逻辑 279
8.4 MPTL作为并发程序验证系统 287
8.4.1 归纳原理的描述 287
8.4.2 程序结构的描述 289
8.4.3 关于程序结构的公理及规则 297
习题 302
第九章 动态逻辑 304
9.1 命题动态逻辑 304
9.2 一阶动态逻辑 310
9.2.1 一种简单的程序语言 310
9.2.2 一阶动态逻辑的语言及语义 311
9.2.3 FDL的公理系统 316
9.3 确定型一阶动态逻辑 320
9.4 一阶动态逻辑的描述能力 325
习题 330
第十章 多值逻辑及模糊逻辑 332
10.1 三值逻辑 332
10.1.1 克利恩三值逻辑 333
10.1.2 卢卡西维茨三值逻辑 337
10.1.3 波兹瓦三值逻辑 338
10.2 无穷值逻辑 341
10.2.1 卢卡西维茨无穷值逻辑 341
10.2.2 雷斯彻概率逻辑 345
10.3 模糊逻辑 347
10.3.1 模糊子集及其运算 348
10.3.2 模糊关系 353
10.3.3 模糊逻辑 356
10.4 模糊推理的一个应用 362
习题 365
第十一章 非单调逻辑 366
11.1 单调性与非单调性 367
11.2 非单调逻辑的产生 368
11.3 缺席推理逻辑 370
11.4 非单调逻辑 379
11.5 限定理论 387
第十二章 λ-演算与组合逻辑 396
12.1 逻辑系统的归约 396
12.2 λ-记号及λ-表达式 398
12.3 λ-演算 402
12.3.1 λK-演算系统 403
12.3.2 λη-演算系统及λI-演算系统 409
12.3.3 化归 412
12.4.1 λ-项上的运算 416
12.4 λ-演算的表示能力 416
12.4.2 λ-可定义的自然数函数 420
12.4.3 一阶逻辑归约为λ-演算 424
12.5 λ-表达式的机器表示 426
12.6 组合逻辑 429
12.6.1 组合逻辑形式系统 430
12.6.2 λK与CL之间的关系 433
习题 437
参考文献 439