线性空间理论在定理证明器HOL中的形式化

摘要

目前，计算机系统的设计正确性检验问题已成为人们关注的重点，形式化方法就是一种新兴的系统设计验证方法，它有效地弥补了传统的测试、模拟等方法在系统设计验证中的“不完备性”问题。本文以一种典型的形式化方法——定理证明方法为研究方向，主要对定理证明器HOL进行了研究，完成了以下一些工作:
　　 首先对形式化方法进行了简要的介绍，主要包括形式化方法的两个方面——系统规范和形式化验证的基本概念，以及三种形式化验证方法的基本原理和各自的优缺点。
　　 接着对定理证明器HOL的发展历史，以及HOL系统的最新版本HOL4系统的结构进行了详细的分析、研究与归纳小结，并总结出了HOL4系统中一般理论建立的基本步骤。
　　 根据对HOL4系统基本结构的研究发现HOL4系统现有的理论体系并不完善，针对这一点，本文完成了HOL4系统中缺少的一个重要理论——线性空间理论在HOL4系统中的形式化工作。
　　 最后，利用已形式化的线性空间理论，在HOL4系统中完成了线性空间理论的几个应用实例的实现，从而展现了HOL4系统中已形式化的线性空间理论的应用价值，进一步说明了在HOL4系统中形式化线性空间理论的意义。

目录

声明

学位论文数据集

摘要

第一章 绪论

1．1 研究背景及意义

1．2 国内外研究现状

1．3 课题研究的主要内容

1．4 本文的组织结构

第二章 形式化方法概述

2．1 形式化方法

2．2 系统规范

2．3 形式化验证

2．3．1 等价性检验

2．3．2 模型检验

2．3．3 定理证明

2．4 形式化方法的局限性与发展趋势

第三章 定理证明器HOL简介

3．1 HOL系统的发展历史

3．2 HOL4系统结构

3．2．1 HOL4系统的逻辑

3．2．2 HOL4系统的编程语言

3．2．3 HOL4系统的证明方法

3．2．4 HOL4系统的理论与库

3．3 HOL4系统中一般理论的建立

第四章 线性空间理论在HOL4系统中的形式化

4．1 线性空间理论在HOL4系统中形式化的意义

4．2 拟形式化的线性空间理论的主要内容

4．3 线性空间在HOL4系统中的形式化

4．3．1 线性空间中的类型的建立

4．3．2 线性空间定义的形式化描述

4．3．3 线性空间相关性质的形式化证明

4．4 线性组合、线性相关和线性无关在HOL4系统中的形式化

4．4．1 线性组合、线性相关和线性无关定义的形式化描述

4．4．2 线性组合、线性相关和线性无关相关性质的形式化证明

4．5 维数、基和坐标在HOL4系统中的形式化

4．5．1 维数、基和坐标定义的形式化描述

4．5．2 维数、基和坐标相关性质的形式化证明

第五章 形式化的线性空间理论在HOL4系统中的应用举例

5．1 数学领域中的应用举例

5．2 工业领域中的应用举例

第六章 结论与展望

6．1 结论

6．2 展望

参考文献

致谢

研究成果及发表的学术论文

作者及导师简介