Einleitung

Beweisen und rationales Argumentieren bilden die eine wichtige Grundlage in mehreren wissenschaftliche Disziplinen. Formalisierungen von Beweisen und rationalen Argumenten werden durch die Formate des TPTP-Projekts [1] unterstützt. Dies schließt das Herleiten von neuem Wissen und das automatische Führen von Beweisen durch sogenannte automatische Theorembeweiser (ATPs) mit ein. Im TPTP-Kontext gibt es viele Möglichkeiten, die automatisiertes Theorembeweisen um praktische Werkzeuge zu ergänzen und damit den Einsatz dieser Systeme ansprechender gestalten und ihre Einsatzmöglichkeiten erweitern.

Themen

Thema (I): Semantische Einbettung

Erstes Ziel des Softwareprojekts ist die Weiterentwicklung des Tools MET [2], das eine sogenannte semantische Einbettung eines Problems einer Modallogik in klassische Logik höherer Stufe durchführt. Darunter versteht man die Überführung/Kodierung eines Problems der Modallogik in ein Problem der klassischen Logik höherer Stufe um autoamtisiertes Theorembeweisen in den vielen, verschiedenen Varianten von Modallogik zu ermöglichen, ohne einen dezidierten und versierten Theorembeweiser für Modallogik programmieren zu müssen. Problemstellungen hierbei sind:

• Ergänzung der Einbettung um die Operatoren Choice, Definite Description, etc.
• Ergänzung der Einbettung um weitere Varianten von Modallogik (weltabhängige Konstanten, verschiedene Modelle propositionaler Quantifizierung, ...)
• Update der Parser-Grammatik (ANTLR) auf den neuesten Stand, entsprechende Anpassung der Einbettung und Testen der Änderungen
• Erstellung von Unit-Tests
• Aufsetzen von Continuous Integration
• Verbesserung des Interfacings der Software, Aufbau einer REST-API
• Recherche von bisherigen Einsätzen von Modallogik in Softwaresystemen und Herstellen der Interoparabilität der vorliegenden Daten mit MET
• Diverses, Code Qualität, Dokumentation, etc. siehe [3]

Thema (II): Editor

Zweites Ziel des Softwareprojekts ist die Entwicklung eines Editors für die maschinenlesbaren Formate der TPTP [1]. Dieser soll ähnlich zu einem Code Editor funktionieren und Anbindung an MET und die unten genannten Tools mit sich bringen. Der Fokus liegt dabei vor allem auf dem effizienten (partiellen) Parsen/Syntax-Highlighting auf Basis der aktuellen ANTLR Grammatik, um den Editor leicht mit weiteren, relevanten Features ausstatten und das Eingabeformat aktuell halten zu können. Der Editor soll sowohl lokal als auch im Web nutzbar sein und wird deswegen für den Browser entwickelt.

Thema (III): Tools

Drittes Ziel des Softwareprojekts ist die Implementierung von kleinen, hilfreichen Tools mit sinnvollen Interfaces und gegebenenfalls die Bündelung zu einer Software-Suite:

• Automatisches Testen auf redundante Axiome
• Automatisches Testen auf unbenötigte Axiome
• Automatisches Testen auf widersprüchliche Axiome
• Verpacken und Interfacing von Remote Theorembeweisern [4] und anderen Remote Software Tools [5] um diese ansprechen zu können
• Verpacken und Interfacing von existierenden Tools (Formatierung, Umwandlung in andere Formate, Testing Tools, ...), deren Installation oftmals schwierig ist und deren Funktionalität oftmals nur schwer nutzbar ist
•  Erstellen eines Tools zur automatischen Überprüfung der Fähigkeiten von Theorembeweisern

Organisatorisches

Thematisch

Die Aufgaben haben sehr unterschiedliche Schwierigkeit, Einarbeitungszeit und erfordern je nachdem keines, rudimentäres oder viel Vorwissen im Bereich der Logik. Die Auswahl der Aufgaben ist von der Anzahl der Teilnehmer, deren Interesse und Vorwissen abhängig. Es wird eine kurze Einführung in die TPTP [1] und (existierende) Logik-Software-Systeme geben.

Zeitlicher Rahmen

Vorbesprechung und Recherche

• Montag, 24.09.2018 14 Uhr, Uhrzeit und Datum nach Absprache mit allen Kursteilnehmern flexibel
• Anschließende Recherche der relevanten Inhalte/Technologien in Eigenregie bis zum Start des Projekts

Präsenzzeit, Konzeption und Entwicklung:

• Montag, 01.10.2018 – Freitag 05.10.2018 (5 Termine) je von 10–18 Uhr
• Montag, 08.10.2018 – Freitag 12.10.2018 (5 Termine) je von 10–18 Uhr

Eigenständige Weiterentwicklung und Abschluss der Implementierungsaufgaben in den ersten zwei Wochen der Vorlesungszeit nach eigenem Ermessen/Absprache

• Freitag, 20.10.2018 Besprechung, Uhrzeit und Datum nach Absprache mit allen Kursteilnehmern flexibel
• Freitag, 27.10.2018 Besprechung, Uhrzeit und Datum nach Absprache mit allen Kursteilnehmern flexibel

Kurzpräsentation der bearbeiteten Aufgaben und erreichten Ziele, Uhrzeit und Datum nach Absprache mit allen Kursteilnehmern flexibel Je nach Teilnehmeranzahl und Präferenzen sind die genauen Arbeitszeiten verhandelbar.

Literatur

[1] http://www.tptp.org/
[2] https://github.com/leoprover/embed_modal
[3] https://github.com/leoprover/embed_modal/blob/master/TODO.md
[4] http://www.tptp.org/cgi-bin/SystemOnTPTP
[5] http://tptp.cs.miami.edu/~tptp/cgi-bin/SystemB4TPTP