目录 1
1.1 思维：感知的概念化和理性化 1
1.2 现代逻辑学求助数学——符号化 1
第一章 绪论 1
1.3 现代逻辑学追随数学——公理化 3
1.4 现代逻辑学改造数学——形式化 3
1.5 现代逻辑学与计算机科学 5
第二章 命题演算形式系统 7
2.1 命题演算基本概念 7
2.1.1 命题与联结词 7
2.1.2 命题公式及其真值 9
2.1.3 范式 12
2.1.4 联结词的扩充与归约 14
2.2 命题演算形式系统 17
2.2.1 命题演算形式系统PC 17
2.2.2 命题演算形式系统ND 22
习题 26
第三章 一阶谓词演算 28
3.1 一阶谓词演算基本概念 28
3.1.1 谓词和函词 28
3.1.2 变元和常元 30
3.1.3 量词 31
3.2 一阶谓词演算形式系统 33
3.2.1 一阶语言 33
3.2.2 一阶逻辑 35
3.3 一阶谓词演算形式系统的语义 40
3.4 关于FC的重要元定理 42
3.4.1 FC的合理性及其它 42
3.4.2 FC的完备性及其它 43
3.4.3 FC的半可判定性 47
习题 47
4.1 使用五个真值联结词和两个量词的一阶谓词演算系统 49
第四章 其它形式的一阶谓词演算系统 49
4.2 带等词的一阶谓词演算系统 52
4.3 谓词演算自然推理系统 54
4.4 多型变元一阶谓词演算系统 57
4.5 直觉主义的一阶谓词演算系统 59
4.5.1 一阶谓词演算的直觉主义系统 60
4.5.2 直觉主义一阶谓词演算系统的语义 65
4.6 一阶谓词演算系统的形式表述能力 68
习题 72
5.1 消解原理 74
5.1.1 斯柯伦标准形和子句集 74
第五章 消解原理及其应用 74
5.1.2 赫布兰德结构 76
5.1.3 赫布兰德定理 79
5.1.4 消解原理 82
5.2 消解的策略 89
5.2.1 删除策略 89
5.2.2 支集策略 89
5.2.3 锁消解 90
5.2.5 输入消解 91
5.2.6 单位消解 91
5.2.4 线性消解 91
5.3 消解原理的应用 92
5.3.1 问题求解 92
5.3.2 规划生成 93
5.3.3 程序综合 94
5.3.4 程序分析和程序验证 96
5.4 带等词一阶谓词演算的消解及其它 99
习题 100
6.1 子句的蕴涵表示形式 102
第六章 霍恩子句逻辑和逻辑程序设计 102
6.2 霍恩子句逻辑 105
6.2.1 霍恩子句及其过程解释 105
6.2.2 关于霍恩子句逻辑程序的讨论 107
6.2.3 霍恩子句逻辑程序设计举例 111
6.3 Prolog语言简介 115
6.3.1 Prolog程序的基本构成与执行方式 115
6.3.2 Prolog语言的基本文法 117
6.3.3 Prolog的控制成分及Prolog程序实例 118
6.3.4 Prolog的基本特点 121
习题 121
第七章 二阶谓词演算 123
7.1 二阶语言 123
7.2 二阶谓词演算形式系统 124
7.3.1 满结构语义 128
7.3 二阶语义及其与二阶谓词演算系统的关系 128
7.3.2 一般结构语义 130
7.4 知识表示的格林方法和科瓦尔斯基方法 133
习题 136
第八章 模态逻辑 137
8.1 模态逻辑的非形式讨论 137
8.2 模态逻辑正规系统及其语义 139
8.2.1 模态语言及模态逻辑正规系统NSK 139
8.2.2 正规结构 141
8.2.3 关于正规系统的重要元定理 143
8.3 模态逻辑系统KD,KT,KB,K4,K5及其它 145
8.3.1 正规系统KD,KT,KB 145
8.3.2 正规系统K4,K5,S4,S5及其它 147
8.3.3 模态词的归约 151
8.4 模态谓词演算 155
8.5 模态逻辑的几种解释 157
8.5.2 认识论模态逻辑 157
8.5.1 真理论模态逻辑 157
8.5.3 道义论模态逻辑 160
8.5.4 时序逻辑 161
8.5.5 经验论模态逻辑 162
习题 164
第九章 时序逻辑与动态逻辑 166
9.1 MPTL的语言 166
9.2 MPTL的语义 167
9.3 时序逻辑系统MPTL 170
9.3.1 时序命题演算 170
9.3.2 带等词的一阶时序逻辑 177
9.4 动态逻辑 182
9.4.1 命题动态逻辑 182
9.4.2 一阶动态逻辑 186
9.4.3 确定型一阶动态逻辑 192
习题 195
10.1.1 克利恩三值逻辑 196
第十章 多值逻辑及模糊逻辑 196
10.1 三值逻辑 196
10.1.2 卢卡西维茨三值逻辑 199
10.1.3 波兹瓦三值逻辑 200
10.2 无穷值逻辑 202
10.2.1 卢卡西维茨无穷值逻辑 202
10.2.2 雷斯彻概率逻辑 205
10.3 模糊逻辑 206
10.3.1 模糊子集及其运算 206
10.3.2 模糊关系 210
10.3.3 模糊逻辑 212
第十一章 非单调逻辑 217
11.1 单调性与非单调性 217
11.2 非单调逻辑的产生 218
11.3 缺省推理逻辑 219
11.4 非单调逻辑系统 225
11.5 限定理论 230
第十二章 λ-演算与组合逻辑 237
12.1 逻辑系统的归约 237
12.2 λ-记号及λ-表达式 238
12.3 λ-演算 241
12.3.1 λK-演算系统 241
12.3.2 λη-演算系统及λI-演算系统 245
12.3.3 化归 247
12.4.1 λ-项上的运算 250
12.4 λ-演算的表示能力 250
12.4.2 λ-可定义的自然数函数 252
12.4.3 一阶逻辑归约为λ-演算 256
12.5 λ-表达式的机器表示 257
12.6 组合逻辑 259
12.6.1 组合逻辑形式系统 260
12.6.2 λK与CL之间的关系 262
习题 265
参考文献 266