绪论 1
第一章 命题演算基础 3
1．1 命题和联结词 3
1．1．1 命题 3
1．1．2 联结词 4
1．1．3 合式公式 8
1．1．4 关于公式的表示法 10
1．2 真假性 16
1．2．1 解释 16
1．2．2 等价公式 17
1．2．3 联结词的完备集 19
1．2．4 对偶式和内否式 20
1．3 范式及其应用 23
1．3．1 范式 23
1．3．2 主范式 25
1．3．2 范式的应用 28
第二章 命题演算的推理理论 31
2．1 命题演算的公理系统 31
2．1．1 公理系统的组成部分 32
2．1．2 公理系统的推理过程 33
2．2 命题演算的假设推理系统 38
2．2．1 假设推理系统的组成 38
2．2．2 假设推理系统的推理过程 39
2．3 命题演算的归结推理法 40
2．3．2 归结证明举例 41
2．3．1 归结证明过程 41
第三章 非标准逻辑简介 44
3．1 模态逻辑 44
3．2 多值逻辑 45
3．2．1 克利恩三值逻辑 45
3．2．2 卢卡西维茨三值逻辑 45
3．2．3 波兹瓦三值逻辑 46
3．3．3 非单调逻辑 46
第四章 谓词演算基础 48
4．1 谓词和个体 48
4．1．1 个体 48
4．1．2 谓词 48
4．2．2 量词 52
4．2 函数和量词 52
4．2．1 函数项 52
4．3 自由变元和约束变元 55
4、3．1 自由出现和约束出现 55
4．3．2 改名和代入 56
4．4 永真性和可满足性 58
4．4．1 真假性 58
4．4．2 同真假性、永真性和可满足性 60
4．4．3 范式 63
4．5 唯一性量词和摹状词 65
4．5．1 唯一性量词 65
4．5．2 摹状词 65
5．1．1 公理系统的组成部分 68
5．1 谓词演算的永真推理系统 68
第五章 谓词演算的推理理论 68
5．1．2 公理系统的推理过程 70
5．2 谓词演算的假设推理系统 73
5．2．1 假设推理系统的组成及证明方法 73
5．2．2 定理的推导过程 74
第六章 归结系统及其应用 77
6．1 合一 78
6．1．1 置换 78
6．1．2 合一 79
6．2 归结的策略 79
6．2．2 支持集策略 80
6．2．1 删除策略 80
6．2．3 线性策略 81
6．2．4 单元优先策略 81
6．2．5 输入形策略 81
6．3 归结反演系统 81
6．3．1 谓词演算公式子句的形成 81
6．3．2 一般归结 83
6．4 归结反演系统的应用 83
6．4．1 问题求解 83
6．4．2 规划生成 88
6．4．3 程序综合 89
6．4．4 程序分析和程序验证 90
7．1 正向演绎系统 95
7．1．1 事实表达式的表示形式 95
第七章 基于规则的演绎系统 95
7．1．2 用规则来变换与或图 96
7．1．3 用与或图证明目标公式 98
7．1．4 含变量表达式的与或图及其目标公式的证明 99
7．2 逆向演绎系统 101
7．2．1 子句的蕴含表示形式 101
7．2．2 霍恩子句逻辑 104
7．2．3 逆向演绎系统的控制策略 105
7．2．4 基于规则的逆向演绎系统例 106
第八章 事物的结构化表示方法 110
8．1 谓词演算的单元表示法 110
8．1．1 事件-中心表示法 110
8．1．2 谓词的二元化 111
8．1．3 槽 112
8．2 图表表示法：语义网络图 115
8．2．1 简单语句的语义网络 115
8．2．2 含有变量和联结词的语句的网络图 117
第九章 递归函数论 120
9．1 数论函数和数论谓词 120
9．1．1 数论函数 120
9．1．2 数论谓词和特征函数 121
9．2 函数的构造 124
9．2．1 迭置法 124
9．2．2 算子法 126
9．2．3 原始递归函数 127
9．3 函数的定义过程 129
参考文献 131