第一章导论 1
亲属关系示例和子句形式 2
子句形式的更精确定义 4
自顶向下和自底向上的定义表示方式 5
目 录 6
原序 6
子句形式的语义学 6
“易犯错误的希腊人”示例 7
“求阶乘”示例 8
个体域与解释 9
矛盾性的更精确定义 11
不同结论的语义学 11
Horn子句 12
蘑菇（Mushroom）和菌蕈（Toadstoo1） 12
习题 13
第二章子句形式表示法 16
中缀（Infix）表示法 16
变量与个体类型 17
存在 18
否定式 20
蕴含式结论的否定 21
蕴含式条件 22
定义与“当且仅当”（If-and-only-if） 23
语义网络 24
扩充语义网络（Extended SemanticNetwork） 24
信息的二元谓词符号表示法 25
二元表示方式的优点 26
数据库 28
数据查询语言 29
完整性约束 30
数据描述 30
一个大学院系的数据库 31
等号 32
习题 34
第三章 自顶向下和自底向上Horn子句证明过程 38
引言 38
语法分析问题 38
语法分析问题的谓词逻辑表示方式 39
自底向上推理 41
自顶向下推理 42
亲属关系示例 44
推理规则与搜索策略 46
无限搜索空间——自然数 49
一些定义 51
代换与匹配 53
推理系统的正确性与完备性 54
习题 54
路径寻找 57
容器灌水问题 57
第四章Horn子句解题 57
一个简化的路径寻找问题 58
搜索空间的图表示方式 59
容器灌水问题的搜索空间 60
路径寻找的搜索策略 62
问题化简的与－或树表示方式 63
Horn子句的解题解释 65
分裂法与独立子目标 66
非独立子目标 67
寻找与证明 68
引理（Lemmas）、重复子目标和循环 69
问题化简空间中的搜索策略 70
双向解题方式 73
双向解题方式的图示法 74
路径寻找问题的另一种形式 75
问题求解的其它方面 75
习题 76
第五章Horn子句的过程解释 78
作为数据结构的项 78
输入与输出参数的变化 80
逐次向输出量逼近的计算操作 80
第一类非确定性—若干过程匹配一个过程调用 81
被看作迭代的顺序搜索 82
“不知”或“不管”的第一类非确定性 83
第二类非确定性—过程调用的调度 84
程序的自底向上执行 87
逻辑程序的语用学内容 89
数据结构的分离 89
以项或关系作为数据结构 91
数据库形式体系与程序设计语言 92
算法＝逻辑＋控制 93
控制成分的规范 94
自然语言＝逻辑＋控制 96
习题 96
第六章制订规划和框架问题 99
制订规划和积木世界 99
积木世界问题的子句表示方式 100
状态空间公理（12）的自底向上执行方式 103
框架公理（15）的自底向上执行方式 103
框架公理的自顶向下和自底向上的混合执行方式 104
状态空间和框架公理的自顶向下执行方式 106
规划制订的应用 107
一些限制 108
习题 109
第七章消解 110
否定的目标与断言 110
消解 111
应用Horn子句的中间向外推理方式 112
命题逻辑的示例 113
非Horn子句的箭头图示法 116
非Horn子句问题的析取解（Disjunctive Solutions） 117
提取因子（Factoring） 118
习题 119
第八章连接图证明过程 121
原始连接图 121
连接图中连线的消解 122
自顶向下和自底向上混合搜索——语法分析问题 124
宏处理（Macro-processing）和中间向外的推理过程 125
控制连线选择的箭头图示法 126
自消解（Self-resolving）子句 128
连接图证明过程 129
消解式为重言式（Tautology）的连线删除 129
习题 131
第九章全局解题策略 132
冗余子目标的删除 132
增添代理子目标（Addition of Surrogate Subgoals） 133
舍弃矛盾的目标语句 134
几何学中图示法应用的推广 135
将目标作为广义解 135
目标变换与信息爆炸 136
使用差别分析的循环检测 136
阶乘示例 138
过程的不变性 139
习题 140
第十章子句形式与标准形式的比较 142
逻辑标准形式引论 142
转换成子句形式 145
子句形式与标准形式的比较 147
合取的结论与析取的条件 148
析取的结论 149
定义的“仅当”（Only-if）部分 149
用蕴含式作为蕴含式的条件 150
从规范推导程序 151
习题 152
第十一章 “当且仅当” 155
对定义“仅当”部分的需要 155
项或关系作为数据结构 156
未被说明的“仅当”部分假说 157
“仅当”的歧义性 158
目标语言与元语言解答 159
关于否定的目标语言与元语言解释 160
扩充“否定被解释为失败”内容的Horn子句 161
程序性质的证明 163
对逻辑结论单调性的批评 164
习题 164
第十二章可证性形式体系 166
正确表达性（CorrectRepresentability） 166
一个简单的可证性关系的定义 167
直接执行与模拟 168
假说的增加和抑制 170
自举（Bootstrapping） 170
目标语言与元语言结合 171
目标语言与元语言结合的不完备性 172
Demonstrate关系的较广泛形式 173
习题 174
第十三章逻辑、变化与矛盾 176
信息系统 176
信息系统变化运动学 177
一致性的恢复 178
一个处理自然语言的逻辑程序 180
结束语 182
参考文献 183