Mizar жүйесі: Математикалық дәлелдерді формалдау және тексеру құралы
Mizar system
Mizar жүйесі – математикалық анықтамалар мен дәлелдерді формалдау тілі, дәлелді тексеру құралы және математика кітапханасы. Қазіргі мақсаты – математиканы тексеру.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
жұлдыз жүйесі
the star system
Мизар жүйесі математикалық анықтамалар мен дәлелдемелерді жазуға арналған формальді тілден, осы тілде жазылған дәлелдемелерді механикалық түрде тексеруге қабілетті дәлелдеме көмекші құралынан және жаңа теоремаларды дәлелдеуде пайдаланылатын формальданған математика кітапханасынан тұрады. Жүйені Мизар жобасы күтіп, дамытады, бұрын оның негізін қалаушы Анджей Трибулец басшылығымен. 2009 жылы Мизар математикалық кітапханасы – қатаң формальданған математиканың бар болған ең ірі және біртұтас жиынтығы еді.
The Mizar system consists of a formal language for writing mathematical definitions and proofs, a proof assistant, which is able to mechanically check proofs written in this language, and a library of formalized mathematics, which can be used in the proof of new theorems. The system is maintained and developed by the Mizar Project, formerly under the direction of its founder Andrzej Trybulec. In 2009 the Mizar Mathematical Library was the largest coherent body of strictly formalized mathematics in existence.
Тарих
Мизар жобасын 1973 жыл шамасында Анджей Трибулец математикалық терминологияны компьютермен тексеруге болатындай қайта құруға жасаған әрекет ретінде бастады. Қазіргі кездегі мақсаты, Мизар жүйесін үздіксіз дамытудан басқа, қазіргі заманғы математиканың негізгі бөлігін қамтитын, формалды түрде тексерілген дәлелдемелердің үлкен кітапханасын бірлесіп құру болып табылады. Бұл ықпалды QED манифестімен үндеседі. Қазіргі уақытта жобаны Польшадағы Беласток университетінің, Канададағы Альберта университетінің және Жапониядағы Шиншу университетінің зерттеу топтары дамытып, қолдап келеді. Мизар дәлелдеуші құрал әлі де коммерциялық құқықпен қорғалған, бірақ ол тексерген формалды математиканың үлкен көлемін қамтитын Мизар математикалық кітапханасы ашық лицензиямен қолжетімді. Мизар жүйесіне қатысты мақалалар математикалық формализация саласындағы ғылыми қауымдастықтың рецензиядан өткен журналдарында тұрақты түрде жарияланып тұрады. Олардың ішінде логика, грамматика және риторика, интеллектуалды компьютерлік математика, интерактивті теоремаларды дәлелдеу, автоматтандырылған ойлау және формалды ойлау журналдары бар.
The Mizar Project was started around 1973 by Andrzej Trybulec as an attempt to reconstruct mathematical vernacular so it can be checked by a computer. Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in line with the influential QED manifesto. Currently the project is developed and maintained by research groups at Białystok University, Poland, the University of Alberta, Canada, and Shinshu University, Japan. While the Mizar proof checker remains proprietary, the Mizar Mathematical Library—the sizable body of formalized mathematics that it verified—is licensed open source. Papers related to the Mizar system regularly appear in the peer reviewed journals of the mathematic formalization academic community. These include Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning and the Journal of Formalized Reasoning.
Мизар тілі
Мизар тілінің ерекшелігі – оның оқуға қолайлылығы. Математикалық мәтіндердегідей, ол классикалық логика мен декларативтік стильге негізделген. Мизар мақалалары қарапайым ASCII форматында жазылады, бірақ тіл математикалық терминологияға настолько жақын жасалған, сондықтан көптеген математиктер арнайы оқусыз Мизар мақалаларын оқи да, түсіне де алады. Бұл математикалық оқулықтар мен жарияланымдарға қарағанда жоғары дәрежеде қатаңдық пен толықтыққа алып келеді. Сондықтан, әдеттегі Мизар мақаласы, дәстүрлі стильде жазылған мақаладан шамамен төрт есе ұзын болады. Формалдау салыстырмалы түрде көп еңбек талап етеді, бірақ оны жасау мүмкін емес емес. Жүйеге толыққанды үйренгеннен кейін, оқулықтың бір бетін формалды түрде тексеруге шамамен бір апта уақыт жұмсалады. Бұл оның артықшылықтары енді қолданбалы салалар, мысалы, ықтималдықтар теориясы мен экономика сияқты салалардың қол жеткізімінде екенін көрсетеді және MML-ге қосылады.
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. This results in a higher level of rigor and detail than is customary in mathematical textbooks 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 textbook page formally verified. This suggests that its benefits are now in the reach of applied fields such as probability theory and economics. and added to the MML.
Кеңдігі
2012 жылдың шілдесіне қарай MML-ге 241 автордың жазған 1150 мақаласы енгізілді. Бұл мақалаларда математикалық объектілердің 10 000-нан астам ресми анықтамасы және осы объектілер бойынша дәлелденген шамамен 52 000 теорема қамтылған. 180-нен астам атаулы математикалық факт ресми түрде кодтау арқасында пайда тапты. Мысалдардың ішінде Хан-Банах теоремасы, Кёниг леммасы, Брауэрдің бекітілген нүкте теоремасы, Гёдельдің толықтығы туралы теоремасы және Жордан қисығы теоремасы бар. Осы кең ауқымды қамту Mizar-ды математиканың барлық негізгі бөлімдерін компьютерде тексерілетін формада кодтаудың QED утопиясына жақындаған алдыңғы қатарлы жобалардың бірі деп санауға мүмкіндік берді.
As of July 2012, the MML included 1150 articles written by 241 authors. In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have so benefited from formal codification. Some examples are the Hahn–Banach theorem, Kőnig's lemma, Brouwer fixed point theorem, Gödel's completeness theorem and Jordan curve theorem. This breadth of coverage has led some to suggest Mizar as one of the leading approximations to the QED utopia of encoding all core mathematics in computer verifiable form.
Логикалық құрылым
MML Тарски–Гротендик көптемелер теориясының аксиомаларымен құрылған. Мағыналық тұрғыдан барлық объектілер жиын болғанымен, тіл синтаксистік әлсіз типтерді анықтауға және қолдануға мүмкіндік береді. Мысалы, жиын тек оның ішкі құрылымы нақты талаптарға сай келген жағдайда ғана Nat типі деп жариялануы мүмкін. Бұл тізім табиғи сандардың анықтамасы болып табылады, ал осы тізімге сәйкес келетін барлық жиындар жиынтығы NAT деп белгіленеді. Осы типтерді енгізудің мақсаты – көптеген математиктердің символдарды формалды түрде қабылдауын бейнелеу және осы арқылы кодтауды жеңілдету.
The MML is built on the axioms of the Tarski–Grothendieck set theory. Even though semantically all objects are sets, the language allows one to define and use syntactical weak types. For example, a set may be declared to be of type Nat only when its internal structure conforms with a particular list of requirements. In turn, this list serves as the definition of the natural numbers and the set of all the sets that conform to this list is denoted as NAT. This implementation of types seeks to reflect the way most mathematicians formally think of symbols and so streamline codification.
Мизар дәлелдеуші
Mizar Proof Checker-дің барлық негізгі операциялық жүйелерге арналған нұсқалары Mizar жобасының веб-сайтынан тегін жүктеуге қолжетімді. Дәлел тексерушіні коммерциялық емес мақсаттарда пайдалану тегін. Ол Free Pascal тілінде жазылған және бастапқы коды GitHub-та бар.
Distributions of the Mizar Proof Checker for all major operating systems are freely available for download at the Mizar Project website. Use of the proof checker is free for all non commercial purposes. It is written in Free Pascal and the source code is available on GitHub.