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 / Anleitung

Schnelldurchlauf

Nach dem Start des Prototypen erscheint ein Fenster mit einer leeren linken Seite und einer rechten Seite mit Karteireitern. Links werden die aktuell im Zugriff befindlichen QEDEQ-Module angezeigt, rechts werden je nach Karteireiter entsprechende Informationen zu dem (auf der linken Seite) markierten Modul angezeigt. Um nun ein Modul zu laden kann über das Menu beispielsweise der Punkt "File" und der Untermenupunkt "Check and Load Module" ausgewählt werden. Anschliessend sollte das Modul http://www.qedeq.org/0_00_53/proptheo1_1.00.00_1.00.00.qedeq ausgewählt werden. Nun läd der Prototyp das angeforderte QEDEQ-Modul aus dem Internet und speichert es als lokale Datei ab. Das Modul wird analysiert und überprüft. Dabei stellt der Prototyp fest, dass ein weiteres QEDEQ-Modul referenziert wird. Dieses Modul propaxiom wird vom Prototypen nun ebenfalls geladen, lokal gespeichert und überprüft. Beide Überprüfungen waren (hoffentlich) erfolgreich und auf der linken Seite erscheinen zwei grüne Kreise neben den Namen der erwähnten QEDEQ-Module. Jetzt kommt auch eine Meldung, die das erfolgreiche Laden des ursprünglich angeforderten Moduls bestätigt.

Nach dem Anklicken von proptheo1 werden auch auf der rechten Seite weitere Informationen zu diesem Modul angezeigt. Mittels des Karteireiters "Qedeq" kann das QEDEQ-Modul in einfacher Textansicht dargestellt werden. Über das "Generate"-Menu wird nach Auswahl von "HTML" ein HTML-Dokument (eigentlich zwei, siehe unten) für das markierte Modul erzeugt. Nach Bestätigung der Hinweismeldung wird (wenn alles gut geht) automatisch der Default-Webbrowser gestartet und das neu erzeugte Dokument angezeigt.

Konfiguration

Zur weiteren Konfiguration dient das über "Settings / Preferences" aufrufbare Fenster. Dort können die lästigen Hinweisfenster abgestellt werden, indem das Häkchen bei "Direct message response for actions" entfernt wird.

Es kann eingestellt werden, ob nach der HTML-Erzeugung für ein einziges Modul der Default-Webbrowser geöffnet werden soll. Falls dieses der Fall ist wird mittels "Use System font HTML at web browser start" eingestellt werden, ob das HTML-Dokument genommen werden soll, welches den System-Font zur Sonderzeichendarstellung benutzt (das HTML-Dokument, welches auf "o.html" endet). Andernfalls wird beim Starten das "normale" HTML-Dokument geöffnet (welches z. B. die Zeichenentität ∧ benutzt. Letzteres ist beispielsweise von den Web-Browsern Mozilla und Netscape besser zu lesen. Bei HTML-Darstellungsproblemen siehe auch unter Aussagenlogik.

Die Einstellung "Auto loading of in last session successfully checked modules" wird beim Start der Anwendung ausgewertet. Falls das Kästchen aktiviert ist, werden alle zum Zeitpunkt der letztmaligen Beendigung der Anwendung grünen Module erneut geladen.

Weiterhin können verschiedene Pfade angesehen und angepasst werden. Siehe auch unter Konfiguration.

Dateinamen und Versionen von QEDEQ-Modulen

Der Dateiname eines QEDEQ-Moduls setzt sich zusammen aus dem Namen des Moduls (alphanumerisch) einem Unterstrich der Versionsnummer des Moduls (in der Form n.nn.nn) einem Unterstrich und der von dem Modul vorausgesetzten Regelversionsnummer (in der.Form n.nn.nn). Die Modulversionsnummer macht verschiedene Versionen eines Moduls unterscheidbar. Falls die Modulversionsnummer gleich 1.00.00 ist, wird sie in der Anzeige auf der linken Seite weggelassen.

Die Regelversionsnummer kennzeichnet die für das Modul erlaubten Regeln. Nur Regeln von kleinerer oder gleicher Versionsnummer dürfen von dem Modul verwendet werden. Weiterhin muss jede Regel vor einer Verwendung deklariert werden. Die Regelversionsnummer wird auf der linken Seite nicht mitangezeigt, Module mit einer Regelversionsnummer von 1.02.00 werden allerdings mit dem Zeichen ' gekennzeichnet.

Die Basisregeln besitzten die Reglversion 1.00.00. Eine Übersicht aller Regeln und ihrer Versionszugehörigkeit ist unter Rules zu finden.

Laden und Löschen von QEDEQ-Modulen

Das Laden von QEDEQ-Modulen erfolgt über das "File"-Menu. Neben dem bereits zuvor erwähnten "Check and Load Module", welches die Eingabe einer URL erwartet, kann auch mit "Check and Load Local File Module" ein im lokalen Dateisystem befindliches QEDEQ-Modul geladen werden.

Durch Start von "Load All Modules From Project Home Page" werden automatisch alle dem Prototypen bekannten QEDEQ-Module von der Website geladen (siehe Aussagenlogik und Prädikatenlogik).

Alle (nicht lokalen) QEDEQ-Module werden im Dateipuffer zwischengespeichert, so dass beim erneuten Laden des Moduls nicht mehr über das Internet zugegriffen werden muss. Ein komplettes Löschen dieses Zwischenspeichers ist durch den Aufruf von "Special / Clear Local File Buffer" möglich, bei einer Neuanforderung von Modulen wird dann im Zwischenspeicher nichts mehr gefunden, und es wird deshalb über das Internet wieder eine Kopie geholt.

Um ein bzw. alle Module aus der linken Anzeige (und aus dem Hauptspeicher) zu entfernen, sind die Menueinträge "Remove Module" und "Remove All Modules" aufzurufen. Falls ein Modul entfernt werden auch alle abhängigen Module entfernt, d.h. dass beispielsweise bei der Entfernung von propaxiom alle (oder fast alle) anderen QEDEQ-Module ebenfalls verschwinden.

Erzeugung und Bearbeitung von neuen QEDEQ-Modulen

Über den Menupunkt "File / Create New Local Module" kann ein neues QEDEQ-Modul erzeugt werden. Es wird eine Datei new_1.00.n_1.02.00 angelegt, dabei wird die Zahl n fortlaufend hochgezählt (und mindestens auf zwei Stellen aufformatiert).

Anschliessend kann dieses neue Modul auch bearbeitet und gespeichert werden.

Sonstiges

Unter dem Karteireiter "Log" ist für die aktuelle Sitzung in chronologischer Reihenfolge aufgelistet, welche Vorgänge stattgefunden haben.


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