www.qedeq.org

 Hilbert II

English   Deutsch
Hilbert II bei SourceForge
Einführung
News
Mathematik
QEDEQ
Planung
Download
Glossar
Entwicklung
Prototyp
Installation
Anleitung
Aussagenlogik
Prädikatenlogik
QEDEQ
Fehler
Links
Kontakt
Sitemap
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 http und ftp zum Einsatz, aber auch lokale Dateien können angegeben werden. Nach der Eingabe einer URL eines Qedeq-Moduls wird der lokale Datei-Puffer durchsucht. Wenn dieser die gesünschte Qedeq-Datei nicht enthält, dann wird die durch die URL angegebene Datei heruntergeladen und in dem lokalen Datei-Puffer gespeichert. Anschliessend wird versucht das Qedeq-Modul zu laden, dabei findet eine Prüfung auf Korrektheit statt. Falls andere Qedeq-Module referenziert werden, wird versucht diese ebenfalls zu laden. Erst wenn alle notwendigen Qedeq-Module erfolgreich geladen und überprüft worden sind, bekommt das ursprüglich angeforderte Qedeq-Modul seinen "grünen Korrektheitspunkt". Im Fehlerfalle wird eine detaillierte Problembeschreibung angegeben und auch die Problemstelle im entsprechenden Modul angezeigt.

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.


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