Systém Mizar - Mizar system

Pro hvězdný systém viz Mizar (hvězda).
Mizar
Logo systému Mizar.gif
Snímek obrazovky
Mizar MathWiki screenshot.png
Snímek obrazovky Mizar MathWiki
ParadigmaDeklarativní
NavrhlAndrzej Trybulec
Poprvé se objevil1973
Psací disciplínaSlabý, statický
Přípony názvu souboru.miz .voc
webová stránkawww.mizar.org
Ovlivněno
Automath
Ovlivněno
OMDoc, HOL Light a Coq režimy mizar

The Systém Mizar sestává z a formální jazyk pro psaní matematických definic a důkazů, a důkaz asistent, který je schopen mechanicky zkontrolovat důkazy napsané v tomto jazyce a knihovna formalizovaná matematika, které lze použít v důkazu nových vět.[1] Systém udržuje a vyvíjí projekt Mizar, dříve pod vedením jeho zakladatele Andrzej Trybulec.

V roce 2009 byla Mizarova matematická knihovna největším soudržným souborem přísně formalizované matematiky.[2]

Dějiny

Projekt Mizar byl zahájen kolem roku 1973 Andrzej Trybulec jako pokus o rekonstrukci matematiky lidový takže to může být zkontrolováno počítačem.[3] Jejím současným cílem, kromě neustálého vývoje systému Mizar, je společné vytváření velké knihovny formálně ověřených důkazů pokrývající většinu jádra moderní matematiky. To je v souladu s vlivným Manifest QED.[4]

V současné době je projekt vyvíjen a udržován výzkumnými skupinami v Białystok University, Polsko, University of Alberta, Kanada a Univerzita Shinshu, Japonsko. Zatímco Mizar proof checker zůstává chráněný,[5] Matematická knihovna Mizar - značný soubor formované matematiky, který ověřovala - je licencován jako open-source.[6]

Články týkající se systému Mizar se pravidelně objevují v recenzovaných časopisech akademické komunity matematické formalizace. Tyto zahrnují Studium logiky, gramatiky a rétoriky, Inteligentní počítačová matematika, Interaktivní dokazování věty, Journal of Automated Reasoning a Žurnál formalizovaného uvažování.

Jazyk Mizar

Charakteristickým rysem jazyka Mizar je jeho čitelnost. Jak je v matematickém textu běžné, spoléhá se na klasická logika a a deklarativní styl.[7] Články Mizar jsou psány obyčejně ASCII, ale jazyk byl navržen tak, aby byl dostatečně blízký matematické lidové řeči, aby většina matematiků dokázala číst a rozumět článkům Mizar bez zvláštního školení.[1] Jazyk přesto umožňuje vyšší úroveň formality nezbytnou pro automatická kontrola kontroly.

Aby byl důkaz přijat, musí být všechny kroky zdůvodněny buď elementárními logickými argumenty, nebo citováním dříve ověřených důkazů.[8] Výsledkem je vyšší úroveň přesnosti a podrobností, než je obvyklé v matematických učebnicích a publikacích. Typický článek Mizar je tedy asi čtyřikrát delší než ekvivalentní práce napsaná v běžném stylu.[9]

Formalizace je relativně náročná na pracovní sílu, ale není nemožně obtížná. Jakmile se člověk orientuje v systému, trvá formální ověření stránky učebnice přibližně jeden týden práce na plný úvazek. To naznačuje, že jeho výhody jsou nyní v dosahu aplikovaných oblastí, jako je teorie pravděpodobnosti a ekonomika.[2]

Matematická knihovna Mizar

Matematická knihovna Mizar (MML) obsahuje všechny věty, na které mohou autoři odkazovat v nově napsaných článcích. Po schválení korektorem jsou dále hodnoceny v procesu peer-review za odpovídající příspěvek a styl. Pokud budou přijaty, budou publikovány v přidruženém Journal of Formalized Mathematics[10] a přidán do MML.

Šířka

V červenci 2012 zahrnoval MML 1150 článků od 241 autorů.[11] Souhrnně obsahují více než 10 000 formálních definic matematických objektů a asi 52 000 vět prokázaných na těchto objektech. Více než 180 pojmenovaných matematických faktů tak těží z formální kodifikace.[12] Některé příklady jsou Hahnova – Banachova věta, Kőnigovo lemma, Brouwerova věta o pevném bodě, Gödelova věta o úplnosti a Jordanova věta o křivce.

Tato šíře pokrytí některé vedla[13] navrhnout Mizara jako jednu z hlavních aproximací k QED utopie kódování celé základní matematiky ve formě ověřitelné počítačem.

Dostupnost

Všechny články MML jsou k dispozici v PDF formulář jako papíry Journal of Formalized Mathematics.[10] Celý text MML je distribuován pomocí nástroje Mizar checker a lze jej volně stáhnout z webových stránek Mizar. V probíhajícím nedávném projektu[14] knihovna byla také zpřístupněna v experimentu wiki formulář[15] který povoluje úpravy, pouze když jsou schváleny kontrolou Mizar.[16]

Web MML Query[11] implementuje výkonný vyhledávač pro obsah MML. Mimo jiné dokáže načíst všechny MML věty o jakémkoli konkrétním typu nebo operátorovi.[17][18]

Logická struktura

MML je postaven na axiomech Teorie množin Tarski – Grothendieck. I když sémanticky všechny objekty jsou sady, jazyk umožňuje definovat a používat syntaktické slabé typy. Například může být deklarována sada typu Nat pouze v případě, že jeho vnitřní struktura odpovídá určitému seznamu požadavků. Tento seznam zase slouží jako definice přirozená čísla a množina všech množin, které odpovídají tomuto seznamu, je označena jako NAT.[19] Tato implementace typů se snaží odrážet způsob, jakým většina matematiků formálně myslí na symboly[20] a tak zefektivnit kodifikaci.

Kontrola důkazů Mizar

Distribuce nástroje Mizar Proof Checker pro všechny hlavní operační systémy jsou volně k dispozici ke stažení na webových stránkách projektu Mizar. Použití kontroly důkazů je zdarma pro všechny nekomerční účely. Je napsán v Free Pascal a zdrojový kód je k dispozici všem členům Asociace uživatelů Mizar.[21]

Viz také

Reference

  1. ^ A b Naumowicz, Adam; Artur Korniłowicz (2009). "Stručný přehled Mizar". Věta prokazující logiku vyšších řádů. Přednášky z informatiky. 5674: 67–72. doi:10.1007/978-3-642-03359-9_5. ISBN  978-3-642-03358-2.
  2. ^ A b Wiedijk, Freek (2009). „Formalizace Arrowovy věty“. Sadhana. 34 (1): 193–220. doi:10.1007 / s12046-009-0005-1. hdl:2066/75428.
  3. ^ Matuszewski, Roman; Piotr Rudnicki (2005). „Mizar: prvních 30 let“ (PDF). Mechanizovaná matematika a její aplikace. 4.
  4. ^ Wiedijk, Freek. "Mizar". Citováno 24. července 2018.
  5. ^ Diskuse o konferenci Archivováno 09.10.2011 na Wayback Machine s odkazem na blízké získávání Mizar.
  6. ^ Oznámení o seznamu adresátů s odkazem na open-source MML.
  7. ^ Geuvers, H. (2009). „Asistenti důkazu: Historie, nápady a budoucnost“. Sadhana. 34 (1): 3–25. doi:10.1007 / s12046-009-0001-5.
  8. ^ Wiedijk, Freek (2008). „Formální důkaz - Začínáme“ (PDF). Oznámení AMS. 55 (11): 1408–1414.
  9. ^ Wiedijk, Freek. „Faktor de Bruijn"". Citováno 24. července 2018.
  10. ^ A b Journal of Formalized Mathematics
  11. ^ A b Vyhledávací stroj MML Query
  12. ^ "Seznam pojmenovaných vět v MML". Citováno 22. července 2012.
  13. ^ Wiedijk, Freek (2007). "Manifest QED se vrátil". Od Insight k Proof: Festschrift na počest Andrzeje Trybuleca. Studium logiky, gramatiky a rétoriky. 10 (23).
  14. ^ Domovská stránka projektu MathWiki
  15. ^ MML ve formě wiki
  16. ^ Alama, Jesse; Kasper Brink; Lionel Mamane; Josef Urban (2011). "Velké formální Wikis: Problémy a řešení". Inteligentní počítačová matematika. Přednášky z informatiky. 6824: 133–148. arXiv:1107.3212. doi:10.1007/978-3-642-22673-1_10. ISBN  978-3-642-22672-4.
  17. ^ Příklad dotazu MML, poskytující všechny věty prokázané na exponent operátor, podle počtu případů, kdy jsou citovány v následujících větách.
  18. ^ Další příklad dotazu MML, poskytující všechny věty prokázané dne sigma pole.
  19. ^ Grabowski, Adam; Artur Kornilowicz; Adam Naumowicz (2010). "Mizar v kostce". Žurnál formalizovaného uvažování. 3 (2): 152–245.
  20. ^ Taylor, Paul (1999). Praktické základy matematiky. Cambridge University Press. ISBN  9780521631075. Archivovány od originál dne 2015-06-23. Citováno 2012-07-24.
  21. ^ Web Asociace uživatelů Mizar

externí odkazy