| 第一章 绪论 | 第1-30页 |
| ·自动推理 | 第9-21页 |
| ·自动推理的早期历史 | 第9-11页 |
| ·自动推理的现在 | 第11-12页 |
| ·自动推理证明方法 | 第12-18页 |
| ·自动定理证明器 | 第18-19页 |
| ·自动推理的应用 | 第19-21页 |
| ·模态逻辑 | 第21-27页 |
| ·可能世界语义学 | 第21-22页 |
| ·结合模态逻辑 | 第22-24页 |
| ·模态逻辑中的推理方法 | 第24-27页 |
| ·本文工作 | 第27-30页 |
| 第二章 改进的命题扩展规则方法 | 第30-48页 |
| ·命题扩展规则方法 | 第30-34页 |
| ·基本命题扩展规则方法ER | 第30-33页 |
| ·命题扩展规则方法IER | 第33-34页 |
| ·改进的命题扩展规则方法 | 第34-38页 |
| ·带化简规则的命题扩展规则方法 | 第34-36页 |
| ·带化简规则与启发式的命题扩展规则方法 | 第36-38页 |
| ·实验结果 | 第38-42页 |
| ·算法RER、RIER、ER、IER 以及DR 的比较 | 第38-41页 |
| ·算法IER、RIER 和HRIER 的比较 | 第41-42页 |
| ·命题逻辑中扩展规则方法和归结方法的结合 | 第42-47页 |
| ·小结 | 第47-48页 |
| 第三章 一阶扩展规则方法 | 第48-66页 |
| ·基础知识 | 第48-49页 |
| ·一阶逻辑中部分实例化推理方法 | 第49-56页 |
| ·部分实例化和阻塞 | 第49-53页 |
| ·部分实例化方法 | 第53-56页 |
| ·一阶逻辑中扩展规则方法及其实现 | 第56-64页 |
| ·一阶扩展规则方法 | 第56-59页 |
| ·一阶扩展规则方法证明器 | 第59-64页 |
| ·小结 | 第64-66页 |
| 第四章 关系扩展规则方法和破坏性扩展规则方法 | 第66-87页 |
| ·模态逻辑 | 第66-70页 |
| ·语法 | 第66-68页 |
| ·语义 | 第68-70页 |
| ·关系扩展规则 | 第70-74页 |
| ·关系转换 | 第70-71页 |
| ·关系扩展规则方法 | 第71-73页 |
| ·讨论 | 第73-74页 |
| ·破坏性扩展规则 | 第74-86页 |
| ·非子句形式的扩展规则方法 | 第75-78页 |
| ·命题模态逻辑K 中的推理 | 第78-83页 |
| ·其它命题模态逻辑中的推理 | 第83-84页 |
| ·实验结果 | 第84-86页 |
| ·小结 | 第86-87页 |
| 第五章 函数扩展规则方法 | 第87-108页 |
| ·函数转换 | 第87-98页 |
| ·函数语义 | 第87-91页 |
| ·对应理论 | 第91-94页 |
| ·函数转换 | 第94-98页 |
| ·路径与语法合一 | 第98-103页 |
| ·路径和前缀稳定 | 第98-100页 |
| ·语法合一 | 第100-103页 |
| ·函数转换扩展规则方法 | 第103-107页 |
| ·连续函数扩展规则方法 | 第103-105页 |
| ·一般函数扩展规则方法 | 第105-107页 |
| ·小结 | 第107-108页 |
| 第六章 总结与展望 | 第108-111页 |
| 参考文献 | 第111-121页 |
| 作者读博士期间完成的论文与参加的科研项目 | 第121-123页 |
| 致谢 | 第123-124页 |
| 摘要 | 第124-128页 |
| ABSTRACT | 第128-132页 |