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

14 Termine

Regelmäßige Termine der Lehrveranstaltung

Mo, 09:00 - 17:00 14 Termine

Mo, 18.09.2017 09:00 - 17:00

Di, 19.09.2017 09:00 - 17:00

Mi, 20.09.2017 09:00 - 17:00

Do, 21.09.2017 09:00 - 17:00

Fr, 22.09.2017 09:00 - 17:00

Mo, 25.09.2017 09:00 - 17:00

Di, 26.09.2017 09:00 - 17:00

Mi, 27.09.2017 09:00 - 17:00

Do, 28.09.2017 09:00 - 17:00

Fr, 29.09.2017 09:00 - 17:00

Mo, 02.10.2017 09:00 - 17:00

Mi, 04.10.2017 09:00 - 17:00

Do, 05.10.2017 09:00 - 17:00

Fr, 06.10.2017 09:00 - 17:00

Zur Modulübersicht

Ort: SR 007/008/A6 Seminarraum

Zeit: Termine siehe LV-Details

Erster Termin: 18.09.2017

Unterrichtssprache: Deutsch

SWS: 2

Platzbeschränkung: Nein

Teilnahmepflicht: Ja

Module zu dieser LV:

Freie Universität Berlin

Service Nav

Vorlesungsverzeichnis

SoSe 17: WYSIWYG-Editor for Higher Order Logic

Christoph Benzmüller

Kommentar

14 Termine

Freie Universität Berlin

Studienfächer A-Z