| 摘要 | 第1-6页 |
| Abstract | 第6-12页 |
| 1 绪论 | 第12-20页 |
| ·选题背景及意义 | 第12-13页 |
| ·在一阶谓词逻辑推理中使用Petri网的理由 | 第13-15页 |
| ·国内外研究现状 | 第15-18页 |
| ·本文研究工作的主要内容 | 第18-19页 |
| ·本文的组织结构 | 第19-20页 |
| 2 基本知识 | 第20-32页 |
| ·Petri网 | 第20-22页 |
| ·谓词/变迁系统 | 第22-25页 |
| ·网逻辑与一阶谓词逻辑推理 | 第25-31页 |
| ·小结 | 第31-32页 |
| 3 一阶谓词公式的建模及其关联矩阵的直接构造 | 第32-57页 |
| ·谓词/变迁系统对一阶谓词公式的建模 | 第32-45页 |
| ·一阶谓词公式的Pr/T系统模型化简 | 第45-49页 |
| ·一阶谓词公式对应的关联矩阵的直接构造法 | 第49-55页 |
| ·小结 | 第55-57页 |
| 4 一阶谓词公式等价性的证明 | 第57-72页 |
| ·一阶谓词公式的等价前束合取范式唯一性的实现 | 第57-61页 |
| ·两个一阶谓词公式等价性判定的充分条件 | 第61-65页 |
| ·两个WFV-1Q一阶谓词公式等价性判定的充要条件 | 第65-71页 |
| ·小结 | 第71-72页 |
| 5 一阶谓词逻辑的图形推理法 | 第72-93页 |
| ·目标制导的图形推理法 | 第72-85页 |
| ·采用变迁框的图形推理法 | 第85-92页 |
| ·小结 | 第92-93页 |
| 6 一阶谓词逻辑推理的关联矩阵初等变换法 | 第93-97页 |
| ·关联矩阵初等变换法用于一阶谓词逻辑推理 | 第93-96页 |
| ·小结 | 第96-97页 |
| 7 结论 | 第97-99页 |
| ·本文的主要工作 | 第97-98页 |
| ·进一步的研究 | 第98-99页 |
| 致谢 | 第99-100页 |
| 附录A | 第100-102页 |
| 参考文献 | 第102-106页 |
| 作者在读期间的研究成果 | 第106-107页 |
| 详细摘要 | 第107-121页 |