www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Einführung
News
Mathematik
QEDEQ
Planung
Download
Glossar
Entwicklung
Prototyp
Links
Kontakt
Sitemap
Einführung

David HilbertZiel des Projekts Hilbert II ist der freie und dezentrale Zugang zu verifiziertem und lesbarem mathematischem Wissen. Dieses Projekt steht, wie der Name schon andeutet, in der Tradition von Hilberts Programm.

Hilbert II will eine weltweite mathematische Wissensbasis werden, die mathematische Sätze und Beweise in formal korrekter Form enthält. Alle zugehörigen Dokumente werden unter der GNU Free Documentation License veröffentlicht. Wir wollen die übliche mathematische Argumentation in eine formale Syntax überführen. D. h., wann immer in der Mathematik eine bestimmte Argumentation häufig benutzt wird, wird sie in die formale Sprache von Hilbert II integriert. Diese formale Sprache wird hier auch als QEDEQ-Format bezeichnet.

Hilbert II stellt eine Programmsuite zur Verfügung, die es einer Mathematikerin ermöglicht Propositionen und Beweise dieser Wissensbasis hinzuzufügen. Dabei werden die Beweise automatisch auf Korrektheit überprüft. Auch Texte in "normaler mathematischer Sprache" können eingebunden werden. Die mathematischen Axiome, Definitionen und Sätze sind in sogenannten QEDEQ-Modulen zusammengefasst. Ein solches Modul kann auch als mathematisches Textbuch aufgefasst werden, das formal korrekte Beweise enthält. Da das System nicht zentral adminstriert wird und Verweismöglichkeit auf andere QEDEQ-Module überall im Internet möglich sind, kann ein weltweites mathematisches Wissensnetz aufgebaut werden. Jeder Beweis einer Proposition in diesem Wissensnetz kann auf die ganz elementaren Regeln und Axiome und Definitionen zurückgeführt werden. Im Idealfall gibt es eine riesige Anzahl von mathematischen Textbüchern mit Querverweisen und jeder vorkommende Beweis kann durch Hilbert II auf Korrektheit überprüft werden. Auch die Abhängigkeit von anderen Propositionen, Definitionen und Axiomen kann auf einfache Weise ermittelt werden.

Das Hauptprojekt befindet sich noch in der Entwicklung, aber die aktuelle Anwendung kann schon heruntergeladen werden. Die Anwendung besitzt eine GUI und kann QEDEQ-Module, die irgendwo im Internet liegen, laden. Aus QEDEQ-Modulen könnnen LaTeX- und UTF-8-Textdateien generiert werden. Tatsächlich wurden fast alle PDF-Dokumente dieser Web-Seite bereits von dieser Anwendug erzeugt. Es können auch einfache formale Beweise überprüft werden. Für die Mengelehre gibt es auch simple diskrete Modelle, welche zur Überprüfung der Gültigkeit von Formeln verwendet werden könnnen. In neuen QEDEQ-Modulen können ereits im Netz befindliche QEDEQ-Module durch einfache Referenzierung benutzt werden.

Weitere Informationen sind unter Status and Planung und Development zu finden.

Es gibt auch einen funktionierenden Prototypen der den Namen Principia Mathematica II trägt. Er beherrscht die Prädikatenlogik erster Stufe und besitzt die Haupteigenschaften von Hilbert II.


update 2014-01-20 09:20:48+0100