Computer Proving Of Basic Formulas In Vector Function, Differential And Partial Differentiation

Mizar system as a formalized system is initiated by the professor Andrzej Trybulec of Warsaw University (Poland) in the 1970s, with the function of logical proof, automated reasoning, verifying and typesetting, complex computation and scientific research and teaching. At the same time, it's widely used in research areas such as automation control, voice recognition and image recognition. Nowadays, the system has the world's largest database MML.This paper firstly introduces the history of Mizar system, then describes the basic structure of Mizar articles. Vector function is presented and its properties are discussed through the Mizar language system. Vector function differential and partial differentiation operators are defined and their related basic formulas are derived and proved.The main work of this paper is as follows:1. Vector function's Mizar denotation is given in the basis of definitions of metric space and euclidean space and its properties are discussed.2. Differential's Mizar form of vector function is given by dint of the definition of real function differentiability. Then their basic formulas are proved.3. In Mizar system, making use of partial differentiation operator's definition on normed linear spaces R n, partial differentiation's definition of vector function is realized. And Mizar forms of correlative formulas are derived.These results are verified to be correct by Mizar system and published in Formalized Mathematics in the form of paper.