Exploitation And Application Of Mizar Language

The idea that an automatic device should check our logical derivations is by no means new. It can be traced back not only to Pascal and Leibniz, but to Ramon Lull. In recent years, several projects have aimed at providing computer assistance for doing mathematics. Among the better known there are: AUTOMATH, THEAX, ALF, ELF, HOL, LEGO and so on. The specific goals of these projects vary. However, they have one common feature: the human writes mathematical texts and the machine verifies their correctness. The project Mizar started 30 years age under the leadership of Andrzej Trybulec at the Plock Scientific Society, Poland. Its original goal was not to write or check mathematical proofs but rather to design and implement of a software environment to assist the process of preparing mathematical papers. Since then, however, Mizar has evolved to a proof checker with the largest known repository of formally verified mathematical knowledge covering a number of topics such as analysis, algebra, topology, graph theory, category theory, and others. The most...