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