System Mizar - Mizar system
 | |
Zrzut ekranu
 Zrzut ekranu Mizar MathWiki
| |
| Paradygmat | Deklaracyjny |
|---|---|
| Zaprojektowany przez | Andrzej Trybulec |
| Po raz pierwszy pojawiły się | 1973 |
| Dyscyplina typowania | Słaby , statyczny |
| Rozszerzenia nazw plików | .miz .voc |
| Stronie internetowej | www.mizar.org |
| Wpływem | |
| Automath | |
| Pod wpływem | |
| Tryby OMDoc , HOL Light i Coq mizar | |
System Mizar składa się z formalnego języka do pisania definicji i dowodów matematycznych, asystenta dowodu , który jest w stanie mechanicznie sprawdzić dowody napisane w tym języku oraz biblioteki sformalizowanej matematyki , która może być wykorzystana w dowodach nowych twierdzeń. System jest utrzymywany i rozwijany przez Mizar Project, wcześniej kierowany przez jego założyciela Andrzeja Trybulca .
W 2009 roku Mizar Mathematical Library była największym istniejącym spójnym zbiorem ściśle sformalizowanej matematyki.
Historia
Projekt Mizar został zapoczątkowany około 1973 roku przez Andrzeja Trybulca jako próba rekonstrukcji matematycznego języka potocznego tak, aby można go było sprawdzić komputerowo. Jego obecnym celem, poza ciągłym rozwojem Systemu Mizar, jest wspólne tworzenie dużej biblioteki formalnie zweryfikowanych dowodów, obejmujących większość rdzenia współczesnej matematyki. Jest to zgodne z wpływowym manifestem QED .
Obecnie projekt jest rozwijany i utrzymywany przez grupy badawcze z Uniwersytetu w Białymstoku w Polsce, Uniwersytetu Alberty w Kanadzie i Uniwersytetu Shinshu w Japonii. Podczas gdy narzędzie do sprawdzania dowodów Mizar pozostaje zastrzeżone, Mizar Mathematical Library - pokaźny zbiór sformalizowanej matematyki, którą zweryfikowała - jest licencjonowanym oprogramowaniem typu open source.
Artykuły związane z systemem Mizar regularnie pojawiają się w recenzowanych czasopismach społeczności akademickiej zajmującej się formalizacją matematyczną. Obejmują one studia z logiki, gramatyki i retoryki , inteligentną matematykę komputerową , interaktywne dowodzenie twierdzeń , Journal of Automated Reasoning i Journal of Formalized Reasoning .
Język mizarski
Charakterystyczną cechą języka mizar jest jego czytelność. Jak to często bywa w tekście matematycznym, opiera się on na logice klasycznej i stylu deklaratywnym . Artykuły Mizar są pisane w zwykłym ASCII , ale język został zaprojektowany tak, aby był na tyle zbliżony do matematycznego języka ojczystego, że większość matematyków mogłaby czytać i rozumieć artykuły Mizar bez specjalnego szkolenia. Jednak język ten umożliwia zwiększony poziom formalności niezbędny do automatycznego sprawdzania dowodów .
Aby dowód został dopuszczony, wszystkie kroki muszą być uzasadnione albo przez elementarne argumenty logiczne, albo przez przytoczenie wcześniej zweryfikowanych dowodów. Skutkuje to wyższym poziomem dokładności i szczegółowości niż jest to zwykle przyjęte w podręcznikach i publikacjach matematycznych. Tak więc typowy artykuł mizarowy jest około cztery razy dłuższy niż równoważny artykuł napisany zwykłym stylem.
Formalizacja jest stosunkowo pracochłonna, ale nie jest niemożliwie trudna. Kiedy ktoś jest zaznajomiony z systemem, zajmuje około tygodnia pracy w pełnym wymiarze godzin, aby formalnie zweryfikować stronę podręcznika. Sugeruje to, że jego zalety są obecnie w zasięgu dziedzin stosowanych, takich jak teoria prawdopodobieństwa i ekonomia .
Mizar Mathematical Library
Biblioteka Mizar Mathematical Library (MML) zawiera wszystkie twierdzenia, do których autorzy mogą się odwoływać w nowo napisanych artykułach. Po zatwierdzeniu przez weryfikatora są one dalej oceniane w procesie wzajemnej oceny pod kątem odpowiedniego wkładu i stylu. Jeśli zostaną zaakceptowane, zostaną opublikowane w powiązanym Journal of Formalized Mathematics i dodane do MML.
Szerokość
W lipcu 2012 r. MML zawierało 1150 artykułów napisanych przez 241 autorów. W sumie zawierają one ponad 10 000 formalnych definicji obiektów matematycznych i około 52 000 twierdzeń udowodnionych na temat tych obiektów. Ponad 180 nazwanych faktów matematycznych skorzystało w ten sposób na formalnej kodyfikacji. Niektóre przykłady to twierdzenie Hahna-Banacha , lemat König , Twierdzenie Brouwera o punkcie stałym , kompletności twierdzenie Gödla i Krzywa Jordana .
Ten zakres omawianych zagadnień skłonił niektórych do zasugerowania Mizara jako jednego z wiodących przybliżeń utopii QED polegającej na kodowaniu całej podstawowej matematyki w formie weryfikowalnej komputerowo.
Dostępność
Wszystkie artykuły MML są dostępne w formacie PDF jako artykuły w Journal of Formalized Mathematics . Pełny tekst MML jest rozpowszechniany wraz z narzędziem do sprawdzania Mizara i można go bezpłatnie pobrać ze strony internetowej Mizar. W trwającym niedawno projekcie biblioteka została również udostępniona w eksperymentalnej formie wiki, która dopuszcza zmiany tylko wtedy, gdy zostaną zatwierdzone przez Mizar checker.
Witryna MML Query implementuje potężną wyszukiwarkę treści MML. Oprócz innych możliwości, może pobrać wszystkie twierdzenia MML udowodnione o określonym typie lub operatorze.
Struktura logiczna
MML jest zbudowany na aksjomatach teorii mnogości Tarskiego – Grothendiecka . Chociaż semantycznie wszystkie obiekty są zbiorami , język pozwala na definiowanie i używanie składniowych typów słabych . Na przykład zestaw można zadeklarować jako typ Nat tylko wtedy, gdy jego struktura wewnętrzna jest zgodna z określoną listą wymagań. Z kolei lista ta służy jako definicja liczb naturalnych, a zbiór wszystkich zbiorów zgodnych z tą listą jest oznaczony jako NAT . Ta implementacja typów stara się odzwierciedlić sposób, w jaki większość matematyków formalnie myśli o symbolach, a tym samym usprawnić kodyfikację.
Mizar Proof Checker
Dystrybucje Mizar Proof Checker dla wszystkich głównych systemów operacyjnych są bezpłatnie dostępne do pobrania na stronie internetowej Mizar Project. Korzystanie z narzędzia do sprawdzania dowodów jest bezpłatne do wszystkich celów niekomercyjnych. Został napisany w języku Free Pascal, a kod źródłowy jest dostępny dla wszystkich członków Stowarzyszenia Użytkowników Mizara.