Hilbert II |
|
|
|
Prototyp
Es gibt einen funktionierenden Prototypen, Principia Mathematica II genannt. Er beherrscht die Prädikatenlogik erster Stufe und besitzt die Haupteigenschaften von Hilbert II. Der Prototyp demonstriert die logischen Grundlagen dieses Projekts.
Er arbeitet mit (prototypspezifischen) Qedeq-Moduldateien zusammen, die sich irgendwo im Internet befinden können. Es kommen die Protokolle Aus erfolgreich geladenen und überprüften Modulen können weitere Dokumente erzeugt werden. Der Prototyp kann HTML- und LaTeX-Dateien generieren. Der Prototyp kannn auch alle verwendeten Metaregeln automatisch eliminieren und die Beweise so abändern, dass nur die Basisregeln vorkommen. Dazu wird jede Anwendung einer Metaregel in eine Abfolge von Anwendungen der Basisregeln umgewandelt. Das neu erzeugte Qedeq-Modul wird dann gesondert gespeichert. Auch können Qedeq-Module von doppelten Beweiszeilen befreit werden. Der Prototyp kann seit der Version 0.00.53 auch über eine graphische Benutzeroberläche bedient werden. Er ist sogar von der Seite Java-Web-Start aus startbar, falls Ihr Browser das unterstüzt. Ansonsten kann der ausführbare Prototyp und sein Source-Code auch über die Download-Seiten heruntergeladen werden. Innerhalb des Prototypen können eigene Qedeq-Module erzeugt und editiert werden. Es kann aber auch jeder einfache Texteditor Verwendung finden. Das Dateiformat ist im Abschnitt Qedeq beschrieben. Bereits im Netz befindliche Qedeq-Module können durch einfache Referenzierung benutzt werden. Das Hauptprojekt benötigt nicht die extreme Detailtiefe der Beweise des Prototypen, aber diese detaillierte Form sollte dort auch generierbar sein. |