Mizar Language
The distinctive feature of the Mizar language is its readability. As is common in mathematical text, it relies on classical logic and a declarative style. Mizar articles are written in ordinary ASCII, but the language was designed to be close enough to the mathematical vernacular that most mathematicians could read and understand Mizar articles without special training. Yet, the language enables the increased level of formality necessary for automated proof checking.
For a proof to be admitted, all steps have to be justified either by elementary logical arguments or by citing previously verified proofs. This results in a higher level of rigor and detail than customary in mathematical text-books and publications. Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style.
Formalization is relatively labor intensive, but not impossibly difficult. Once one is versed in the system, it takes about one week of full-time work to have a text-book page formally verified. This suggests that its benefits are now in the reach of applied fields such as probability theory and economics.
Read more about this topic: Mizar System
Famous quotes containing the word language:
“Had Dr. Johnson written his own life, in conformity with the opinion which he has given, that every man’s life may be best written by himself; had he employed in the preservation of his own history, that clearness of narration and elegance of language in which he has embalmed so many eminent persons, the world would probably have had the most perfect example of biography that was ever exhibited.”
—James Boswell (1740–95)