The Function Differential, Difference, Difference Quotient And Continued Fraction In Mizar

The project Mizar is created and develops with the development of automatedtheorem proving which is a branch of artificial intelligence. Mizar is a proof checkerwhich is used in building Mizar Mathematical Library. Mizar project is under theleadership of Andrzej Trybulec at the Plock Scientific Society, Poland. The originalMizar is designed to help mathematicians write mathematical paper and it base on theJaskowski style of natural deduction. Today Mizar has become a formalization ofmathematical knowledge, with the function of proving, verifying and typesetting. Mizarhas a large Mizar Mathematical Library, embodying more than 960 articles written byprofessors from Poland, Japan, China, Canada. MML almost contains all branches ofmathematics. Especially in the formalization of continuous lattices theorem, Jordan'scurve theorem and Brouwer fixed point theorem, Mizar has a great advantage.This dissertation describes the history of theorem automatic proof and Mizarsystem and how to write articles in Mizar system. The main work of the paper issummarized as following:1,The automated reasoning and verification differentials for some specialcomposite functions is implemented in Mizar system.2,For the first time the functor shift, fD, bD and cD are defined in Mizar. Basedon the definitions of them, the infinite function difference sequencesforward_difference, backward_difference and central_difference aredefined and the connection of them is presented and implemented in Mizar.3,For the first time the continued fraction form of a real number and theconvergence fraction are defined and the property of them is verified inMizar.The automatic reasoning and proving process, which is related to the aboveaspects, have been completed and verified to be correct in Mizar system.