Das Mizar System besteht aus einer Sprache, um zu schreiben, ausschließlich hat mathematische Definitionen und Beweise, ein Computerprogramm formalisiert, das im Stande ist, Beweise zu überprüfen, die auf dieser Sprache und einer Bibliothek von Definitionen geschrieben sind, und Lehrsätze bewiesen hat, in denen Verweise angebracht und in neuen Artikeln verwendet werden kann. Mizar hat Absichten, die denjenigen QED Projekt ähnlich sind, das von Bob Boyer 1993 vorgeschlagen ist. Mizar ist Eigentums-, seine Bibliothek wird seit 2011 offen lizenziert.

Geschichte

Das System wurde geschaffen, 1973 von Andrzej Trybulec beginnend, und wird an der Białystok Universität, Polen, der Universität von Alberta, Kanada und Shinshu Universität, Japan aufrechterhalten.

Artikel von Mizar werden in gewöhnlichem ASCII geschrieben. Die Mizar Sprache ist an der mathematischen Mundart nah genug, dass Mathematiker lesen und Artikel Mizar fast sofort verstehen können; es ist formell genug, dass Beweise automatisch überprüft werden können. Alle Schritte in einem Beweis müssen gerechtfertigt werden, und es ist geschätzt worden, dass ein Artikel Mizar ungefähr viermal so lang ist wie eine gleichwertige mathematische im gewöhnlichen Stil geschriebene Zeitung.

Der Probekontrolleur verwendet klassische Logik, wird in Pascal geschrieben, und kann heruntergeladen und frei zu nichtkommerziellen Zwecken verwendet werden. Es läuft auf PC-Plattformen, Windows, Solaris, FreeBSD und Linux und Mac OS X/Darwin. Der Quellcode ist nur für Mitglieder der Vereinigung von Mizar Benutzern verfügbar.

Der Mizar Vertrieb schließt Mizar Mathematical Library (MML) ein, die aus vielen Definitionen und Lehrsätzen besteht, auf die in kürzlich schriftlichen Artikeln verwiesen werden kann. Diese neuen Artikel, nachgeprüft und überprüft automatisch, können in der verbundenen Zeitschrift der Formalisierten Mathematik veröffentlicht werden und dann ein Teil des MML werden.

Auf den MML werden auf den Axiomen der Tarski-Grothendieck Mengenlehre gebaut. Bezüglich des Februars 2010 hat es ungefähr 9500 Definitionen und 49,500 Lehrsätze enthalten. Beispiele sind der Hahn-Banach Lehrsatz, das Lemma von König, Brouwer befestigter Punkt-Lehrsatz, der Vollständigkeitslehrsatz von Gödel, und Tatsachen über den Kantoren gehen unter.

Wenn auch semantisch alle Gegenstände MML Gespräche darüber sind Sätze, die Sprache dennoch, erlauben, syntaktische Typen zu definieren und zu verwenden: Eine Variable kann zum Beispiel des Typs erklärt werden, wenn es für eine natürliche Zahl, oder des Typs eintritt, wenn es eine Gruppe anzeigt. Das macht die Notation günstiger und näher an der Weise, wie Mathematiker an Symbole denken.

Auszüge von Browsable von Artikeln MML sind als die Zeitschrift der Formalisierten Mathematik verfügbar, und MML-Abfrage führt einen Suchmotor für MML durch.

Siehe auch

• QED Projekt
• Automathematik
• Metamath

Außenverbindungen

• Mizar Hauptseite, enthält Verbindungen zum MML, zur Zeitschrift der Formalisierten Mathematik und einer Bibliografie-Abteilung, die sich zu mehreren Einführungen ins System verbindet
• MML Abfrage, ist ein Suchmotor für MML.
• Die Mizar Seite von Freek Wiedijk, enthält Gleiten eines Konferenzgespräches über das System, sowie einen einleitenden 40-Seite-Artikel
• Vereinigung von Mizar Benutzern
• Eine Zeitung über die Geschichte von Mizar (ps)
• Ein Vergleich zwischen Mizar und einer anderen (Automatheähnlichen) formellen Sprache für die Mathematik, Schwache Typ-Theorie.
• Mizar wiki