| 摘要 | 第1-6页 |
| ABSTRACT | 第6-12页 |
| 第一章 绪论 | 第12-16页 |
| ·研究背景及意义 | 第12-13页 |
| ·国内外研究现状 | 第13-14页 |
| ·课题研究的主要内容 | 第14-15页 |
| ·本文的组织结构 | 第15-16页 |
| 第二章 形式化方法概述 | 第16-26页 |
| ·形式化方法 | 第16页 |
| ·系统规范 | 第16-17页 |
| ·形式化验证 | 第17-23页 |
| ·等价性检验 | 第19-20页 |
| ·模型检验 | 第20-21页 |
| ·定理证明 | 第21-23页 |
| ·形式化方法的局限性与发展趋势 | 第23-26页 |
| 第三章 定理证明器 HOL 简介 | 第26-44页 |
| ·HOL 系统的发展历史 | 第26-27页 |
| ·HOL4 系统结构 | 第27-42页 |
| ·HOL4 系统的逻辑 | 第28-30页 |
| ·HOL4 系统的编程语言 | 第30-32页 |
| ·HOL4 系统的证明方法 | 第32-40页 |
| ·HOL4 系统的理论与库 | 第40-42页 |
| ·HOL4 系统中一般理论的建立 | 第42-44页 |
| 第四章 线性空间理论在HOL4系统中的形式化 | 第44-90页 |
| ·线性空间理论在 HOL4 系统中形式化的意义 | 第44-45页 |
| ·拟形式化的线性空间理论的主要内容 | 第45-49页 |
| ·线性空间在 HOL4 系统中的形式化 | 第49-65页 |
| ·线性空间中的类型的建立 | 第51-52页 |
| ·线性空间定义的形式化描述 | 第52-56页 |
| ·线性空间相关性质的形式化证明 | 第56-65页 |
| ·线性组合、线性相关和线性无关在 HOL4 系统中的形式化 | 第65-85页 |
| ·线性组合、线性相关和线性无关定义的形式化描述 | 第66-70页 |
| ·线性组合、线性相关和线性无关相关性质的形式化证明 | 第70-85页 |
| ·维数、基和坐标在 HOL4 系统中的形式化 | 第85-90页 |
| ·维数、基和坐标定义的形式化描述 | 第86-87页 |
| ·维数、基和坐标相关性质的形式化证明 | 第87-90页 |
| 第五章 形式化的线性空间理论在 HOL4 系统中的应用举例 | 第90-94页 |
| ·数学领域中的应用举例 | 第90-91页 |
| ·工业领域中的应用举例 | 第91-94页 |
| 第六章 结论与展望 | 第94-96页 |
| ·结论 | 第94页 |
| ·展望 | 第94-96页 |
| 参考文献 | 第96-100页 |
| 致谢 | 第100-102页 |
| 研究成果及发表的学术论文 | 第102-104页 |
| 作者及导师简介 | 第104-105页 |
| 硕士研究生学位论文答辩委员会决议书 | 第105-106页 |
