计算机的自动推理证明是数学与计算机科学相结合的一个新学科,随着计算机技术的高速发展,该学科也迅速发展,各种机器语言应运而生。利用机器语言编写程序,实现了数学问题在计算机上的证明。Mizar语言就是其中一种。Mizar语言系统是用于证明或计算数学问题的计算机语言系统,在定理自动证明的发展过程中逐步完善。如今Mizar已经成为集逻辑证明、自然演绎、复杂计算、校验排版、科研教学于一体的处理数学知识的形式化系统,拥有着世界上最大的数据库MML。本文简单介绍了Mizar语言系统,并应用Mizar语言系统对双线性函数的度量矩阵和二次型等问题给出相应的证明,主要工作如下:1.定义出双线性函数的度量矩阵,利用度量矩阵进一步探讨双线性函数。2.实现了对称双线性函数、反对称双线性函数、退化双线性函数和非退化双线性函数的定义,简单讨论了他们的度量矩阵及性质。3.给出了二次型,正定二次型,正定矩阵等相关定义。