The Metric Matrix Of The Bilinear Function And The Quadratic Form In Mizar

The automatic proof on computer is a new subject which is a combination of mathematics and computer.With the development of computer technology,this subject developed quickly.Then various machine languages came out.To solve mathematical problems on computer,the machine languages are used to write programs.Mizar is one of the machine languages.The Mizar system is used to demonstrate or calculate the math problems on computer.As the automatic proof develops,it is being improved day by day.Nowadays,Mizar system has become a formalization of mathematical knowledge, with the function of proving, verifying and typesetting.Mizar system has the largest date library-MML in the world.This dissertation gives an outline of the Mizar system firstly.Secondly,its primary coverage is about the bilinear function and the quadratic form.The main contents are summarized as follows:1. Gives the definition of the metric matrix of the bilinear function and probes further into their attributes in Mizar system;2. Discusses the symmetric bilinear function,anti-symmetric bilinear function,degenerated bilinear function and non-degenerated bilinear function in Mizar system;3. The definition of the quadratic form is formalized in Mizar system, and the positive quadratic form,positive matrix etc are also given.