第一章 绪论——知识工程、形式系统理论与机器发现 1
1．1 知识工程对传统软件工程的挑战 1
1．2 形式系统理论——知识工程的理论基础 3
1．3 知识工程能从科学哲学中学习什么 5
1．4 Lakatos的证伪方法论 8
第一篇 一阶形式系统理论 12
第二章 形式系统理论基础 12
2．1 谓词演算 12
2．2 一阶理论 41
第三章 哥德尔不完全性定理 68
3．1 引论 68
3．2 可表达性 70
3．3 递归函数和递归关系 79
3．4 哥德尔数 88
3．5 不完全性的证明 93
第四章 可计算性和判定问题 100
4．1 图灵机 100
4．2 判定 108
第二篇 机器推理与机器发现 122
第五章 机器定理证明 122
5．1 Herbrand定理 122
5．2 归结原理 136
5．3 一阶树推理方法 146
5．4 一阶线性归结、Horn归结及PROLOG系统 158
第六章 机器定理发现 172
6．1 机器定理发现与机器定理证明 172
6．2 二阶树推理系统 174
6．3 二阶树推理与数学发现 179
6．4 二阶线性归结 189
6．5 二阶线性归结与逻辑程序自动设计 195
参考文献 209