19317212

SoSe 17: WYSIWYG-Editor for Higher Order Logic

Christoph Benzmüller

Kommentar

Es soll ein WYSIWYG-Editor (What-you-see-is-what-you-get-Editor) für das maschinenlesbare Format TPTP THF entwickelt werden. Dieses wird zum Repräsentieren und Formalisieren von logischen Aussagen und Problemen in klassischer Prädikatenlogik höherer Stufe genutzt. Der Editor soll ein in THF formuliertes logisches Problem menschenlesbar und -editierbar machen sowie übersichtlich aufbereiten. Die Kernkomponenten sind hierbei:

Öffnen und Speichern von THF-Dateien sowie die Darstellung und Editiermöglichkeit in konventioneller Logikschreibweise ähnlich der des interaktiven Theorembeweisers Isabelle;
übersichtliche Darstellung eines Problems durch ein Inhaltsverzeichnis der Axiome/Theoreme, eventuell "Ein-" und "Ausklappen" von Axiomen im Problem,
Filebrowser.

Je nach Interesse und Anzahl der Teilnehmer wird zusätzlich eine Auswahl der folgenden features implementiert:

Syntax highlighting;
syntax error notification;
semantical error notifications z.B. type errors;
auto completion von Bezeichnern/Typen;
code generation z.B. für bereits benutzte aber undefinierte Konstantensymbole;
Bezeichner-Following bei Shift-Klick;
Auto linebreaking/-spacing für große Formeln
gleichzeitiges Editieren der WYSIWYG-Darstellung und THF;
Interface zum Bearbeiten/Einstellen der Semantik von nicht-klassischen Logiken in THF;
Darstellung von Formeln als Graph;
Volltextsuche.

Neben der Editierkomponente soll die Software auch eine Anbindung an gängige TPTP-konforme Theorembeweiser (lokal und remote) schaffen. Theorembeweiser sind Softwaresysteme, die logische Aussagen und Probleme lösen können. Mögliche Features könnten folgende sein:

Aufbereitung der Rückgabewerte der Beweiser;
Ein- und Ausblenden einzelner Axiome/Theoreme für den Beweiser;
automatisches Testen auf Redundanzen von Axiomen;
automatisches Testen auf unbenötigte Axiome;
automatisches Testen auf widersprüchliche Axiome;
Anbindung an zusätzliche tools z.B. zur Formatierung, Umwandlung in andere Formate, semantischen Einbettung eines Problems usw., evtl. Möglichkeit zur Erstellung einer Toolchain;
Testframework.

Schließen