Hilbert II-Projekt ist die dezentrale Zugriff auf überprüft und lesbar mathematische Kenntnisse. Wie der Name schon vermuten lässt, ist das Projekt in der Tradition von Hilberts Programm.
Hilbert II will eine kostenlose, weltweite mathematische Wissensbasis, die mathematische Sätze und Beweise in einem formellen richtige Form enthält wird. Alle gehörenden Unterlagen sind unter der GNU Lizenz für freie Dokumentation veröffentlicht.
Wir wollen die üblichen mathematischen Argumentation auf eine formale Syntax anpassen. Das bedeutet, dass immer dann, wenn in der Mathematik eine bestimmte Art von Argumentation wird häufig verwendet, wir freuen uns, sie in der Formensprache der Hilbert II zu integrieren. Diese Formensprache wird als QEDEQ Format.
Hilbert II bietet ein Programm-Suite, die ein Mathematiker ermöglicht, Sätze und Beweise in diese Wissensbasis setzen. Diese Beweise werden automatisch von einem Proof Checker überprüft. Auch Texte in "gemeinsamen Sprache der Mathematik" integriert werden.
Die mathematischen Axiome, Definitionen und Sätze werden zu so genannten QEDEQ Module. Ein solches Modul kann als ein mathematisches Lehrbuch, die formal korrekte Beweise enthält sehen. Da dieses System nicht zentral verwaltet und Verweise zu jedem beliebigen Ort im Internet möglich sind, könnte ein weltweites mathematisches Wissensbasis bauen.
Jeder Beweis eines Satzes in diesem "mathematische web" könnte gebohrt werden bis hin zu den elementarer Regeln und Axiomen. Stellen Sie sich eine unglaubliche Anzahl von mathematischen Lehrbücher mit Hyperlinks und jeder seiner Beweise könnte durch Hilbert II überprüft werden. Für jeden Satz die Abhängigkeit von anderen Theoreme, Definitionen und Axiomen leicht abgeleitet werden
Das Grundkonzept dieses Projektes ist als PDF-Dokument veröffentlicht:. Grundkonzept. Dieses Dokument ist bereits der folgenden XML-Datei erzeugt: qedeq_basic_concept.xml. Das Hauptprojekt ist in der ersten Phase develompment finden in der Entwicklung.
Es gibt einen funktionierenden Prototyp namens Principia Mathematica II. Es ist durchaus in der Lage Prädikatenlogik erster Stufe und zeigt die wichtigsten Funktionen von Hilbert II. Es ist zu überprüfen (Prototyp) QEDEQ Moduldateien überall im Internet befindet.
Der Prototyp hat eine GUI und kann QEDEQ Module in HTML und LaTeX Dateien zu übertragen. Sie können erstellen und bearbeiten Sie Ihre eigenen neuen QEDEQ Modul und veröffentlicht sie im Internet. Im Web können bereits vorhandene QEDEQ Module nur durch Verweis auf sie verwendet werden
Was ist neu in dieser Version:.
Kommentare nicht gefunden