Mizar-System

Mizar
Paradigmen:deklarativ
Erscheinungsjahr:1973
Designer:Andrzej Trybulec
Entwickler:Andrzej Trybulec
Typisierung:statisch, schwach
Beeinflusst von:Automath
Beeinflusste:OMDoc, HOL Light, Coq
http://www.mizar.org/

Das Mizar-System besteht aus einer formalen Sprache, um mathematische Definitionen und Beweise zu schreiben, einem Beweisassistenten, der in dieser Sprache erfasste Beweise mechanisch prüft, und einer Bibliothek formalisierter Mathematik, auf welche im Beweis neuer Theoreme zurückgegriffen werden kann.[1] Das System wird vom Mizar Project, früher unter der Leitung seines Gründers Andrzej Trybulec, unterhalten und weiterentwickelt.

Die Mizar Mathematical Library ist die weltweit größte Sammlung strikt formalisierter Mathematik.[2]

Geschichte

Das Mizar-Projekt wurde 1973 von Andrzej Trybulec begonnen im Versuch, die mathematische Fachsprache so zu rekonstruieren, dass sie von einem Computer überprüft werden kann.[3] Das momentane Ziel, neben Weiterentwicklung des Mizar-Systems, ist die kollaborative Erstellung einer großen Bibliothek formal verifizierter Beweise, die den Großteil der modernen Mathematik abdecken soll. Dies ist ganz im Sinne des QED-Manifests.[4]

Momentan wird das Projekt unterhalten und weiterentwickelt von Forschungsgruppen der Universität Białystok (Polen), der University of Alberta (Kanada) und der Shinshū-Universität (Japan). Während das Programm zur Beweisprüfung proprietär bleibt,[5] ist die Mizar Mathematical Library – die Bibliothek formal verifizierter Mathematik – open-source lizenziert.[6]

Papers im Zusammenhang mit dem Mizar-System erscheinen regelmäßig in Fachzeitschriften der Akademischen Gesellschaft für mathematische Formalisierung. Diese umfassen Studies in Logic, Grammar and Rhetoric, Intelligent Computer Mathematics, Interactive Theorem Proving, Journal of Automated Reasoning und das Journal of Formalized Reasoning.

Name

Nach den Angaben von Andrzej Trybulec ist der Doppelstern Mizar im Sternbild des großen Wagen der Namensgeber des Projekts.[7]

Mizar-Sprache

Das herausragende Merkmal der Mizar-Sprache ist ihre Lesbarkeit. Wie bei mathematischen Texten üblich, basiert sie auf klassischer Logik und deklarativem Stil.[8] Mizar-Artikel werden in gewöhnlichem ASCII verfasst, aber die Sprache wurde so entwickelt, dass sie nahe genug an der mathematischen Fachsprache ist, dass die meisten Mathematiker Mizar-Artikel ohne spezielles Training verstehen können.[1] Dennoch erlaubt die Sprache ein erhöhtes Maß an Formalität, nötig zur automatischen Beweisprüfung.

Damit ein Beweis akzeptiert wird, müssen alle Schritte begründet werden, entweder mit elementaren logischen Argumenten oder durch Zitierung bereits verifizierter Beweise.[9] Daraus resultiert ein höheres Level an Ausführlichkeit als üblich in gewöhnlichen mathematischen Lehrbüchern und Publikationen. Deswegen ist ein typischer Mizar-Artikel etwa viermal länger als ein äquivalentes Paper, das in gewöhnlichem Stil verfasst wurde.

Die Formalisierung eines Theorems in der Mizar-Sprache ist relativ arbeitsaufwändig, aber nicht unmöglich schwierig. Ist man einmal mit dem System vertraut, braucht es etwa eine Woche Vollzeitarbeit, um eine Textbuchseite formal verifizieren zu lassen. Dies deutet an, dass die Vorteile des Systems in Reichweite von angewandten Gebieten wie Wahrscheinlichkeitstheorie und Wirtschaft sind.[2]

Mizar Mathematical Library

The Mizar Mathematical Library (MML) enthält alle Theoreme, auf welche sich neue Artikel beziehen können. Sobald Artikel vom Beweisprüfer akzeptiert werden, werden sie weiter extern begutachtet und Stil und Wert des Beitrags untersucht. Wenn sie akzeptiert werden, werden sie im eigenen Journal of Formalized Mathematics[10] publiziert und zur MML hinzugefügt.

Breite

Im Juli 2012 umfasste die MML 1150 Artikel geschrieben von 241 Autoren.[11] Zusammen umfassen diese mehr als 10.000 formale Definitionen mathematischer Objekte und etwa 52.000 bewiesene Theoreme über diese Objekte. Mehr als 180 benannte mathematische Fakten konnten formal kodiert werden.[12] Beispiele sind der Satz von Hahn-Banach, das Lemma von König, der Fixpunktsatz von Brouwer, der gödelsche Vollständigkeitssatz und der jordansche Kurvensatz.

Die Breite der Abdeckung veranlasste einige Personen dazu[13], Mizar als eine der führenden Approximationen an das QED-Manifesto, der Kodierung der gesamten Mathematik in Computer verifizierbarer Form, vorzuschlagen.

Verfügbarkeit

Alle MML-Artikel sind in PDF-Form als Paper im Journal of Formalized Mathematics verfügbar.[10] Der gesamte Text der MML wird mit dem Mizar Proof Checker (Beweisüberprüfungsprogramm) verbreitet und kann kostenlos von der Mizar-Webseite heruntergeladen werden. In einem laufenden Projekt[14] wurde die Bibliothek in einer experimentellen Wiki-Form[15] verfügbar gemacht, die Bearbeitungen nur zulässt, wenn sie vom Proof Checker akzeptiert werden.[16]

Die Query-Webseite[11] implementiert eine mächtige Suchmaschine für den Inhalt der MML. Neben anderem, kann es alle MML-Theoreme, die über einen bestimmten Typ oder Operator beweisen wurden, auflisten.[17][18]

Logische Struktur

Die MML baut auf den Axiomen der Tarski-Grothendieck-Mengenlehre auf. Obwohl semantisch alle Objekte Mengen sind, erlaubt die Sprache die Definition und Verwendung schwacher Typen. Zum Beispiel kann eine Menge nur als Typ Nat deklariert werden, wenn seine Interne Struktur mit einer bestimmten Liste von Anforderungen konform ist. Im Gegenzug dient diese Liste als Definition der Natürlichen Zahlen und die Menge aller Mengen die mit dieser Liste konform sind wird mit NAT bezeichnet.[19] Diese Implementation der Typen versucht die Art und Weise wie die meisten Mathematiker über Symbole denken widerzuspiegeln[20] und so den Prozess der Kodifizierung leichter zu machen.

Mizar Proof Checker

Distributionen des Mizar Proof Checkers für die gängigen Betriebssysteme sind frei zum Download von der Mizar-Webseite verfügbar. Die Verwendung des Proof Checkers ist kostenlos für nicht-kommerzielle Anwendungen. Die Software wurde in Free Pascal geschrieben, und der Quellcode ist für alle Mitglieder der Association of Mizar Users verfügbar.[21]

Siehe auch

Weblinks

Einzelnachweise

  1. ↑ a b Adam Naumowicz, Artur Korniłowicz: A Brief Overview of Mizar. In: Theorem Proving in Higher Order Logics. 5674. Jahrgang, 2009, S. 67–72 (springer.com).
  2. ↑ a b Freek Wiedijk: Formalizing Arrow’s theorem. In: Sadhana. 34. Jahrgang, Nr. 1, 2009, S. 193–220 (springer.com).
  3. ↑ Roman Matuszewski, Piotr Rudnicki: Mizar: the first 30 years. In: Mechanized Mathematics and Its Applications. 4. Jahrgang, 2005 (mizar.org [PDF]).
  4. ↑ Freek Wiedijk: Mizar. Abgerufen am 1. Juli 2012.Vorlage:Cite web/temporär
  5. ↑ Mailing list discussion (Memento des Originals vom 9. Oktober 2011 im Internet Archive)  Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/old.nabble.com referring to the close-sourcing of Mizar.
  6. ↑ Mailing list announcement referring to the open-sourcing of MML.
  7. ↑ Mizar The first 30 Years (Memento vom 27. September 2006 im Internet Archive)
  8. ↑ H. Geuvers: Proof assistants: History, ideas and future. In: Sadhana. 34. Jahrgang, Nr. 1, 2009 (springer.com).
  9. ↑ Freek Wiedijk: Formal Proof--Getting Started. In: AMS Special Issue on Formal Proof. 2008 (ams.org).
  10. ↑ a b Journal of Formalized Mathematics
  11. ↑ a b The MML Query search engine
  12. ↑ A list of named theorems in the MML. Abgerufen am 1. Juli 2012.Vorlage:Cite web/temporär
  13. ↑ Freek Wiedijk: The QED Manifesto Revisited. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. 10. Jahrgang, Nr. 23, 2007 (edu.pl).
  14. ↑ The MathWiki project homepage (Memento des Originals vom 22. Februar 2013 im Webarchiv archive.today)  Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/foundations.cs.ru.nl
  15. ↑ The MML in wiki form (Memento des Originals vom 2. Dezember 2013 im Internet Archive)  Info: Der Archivlink wurde automatisch eingesetzt und noch nicht geprüft. Bitte prüfe Original- und Archivlink gemäß Anleitung und entferne dann diesen Hinweis.@1@2Vorlage:Webachiv/IABot/mws.cs.ru.nl
  16. ↑ Jesse Alama, Kasper Brink, Lionel Mamane and Josef Urban: Large Formal Wikis: Issues and Solutions. In: Intelligent Computer Mathematics. 6824. Jahrgang, 2011, S. 133–148 (springer.com).
  17. ↑ An example of an MML query, yielding all theorems proved on the exponent operator, by the number of times they are cited in subsequent theorems.
  18. ↑ Another example of an MML query, yielding all theorems proved on sigma fields.
  19. ↑ Adam Grabowski, Artur Kornilowicz, Adam Naumowicz: Mizar in a Nutshell. In: Journal of Formalized Reasoning. 3. Jahrgang, Nr. 2, 2010, S. 152–245 (unibo.it).
  20. ↑ Paul Taylor: Practical Foundations of Mathematics. Cambridge University Press, 1999, ISBN 978-0-521-63107-5 (man.ac.uk).
  21. ↑ The Association of Mizar Users website