ATP Construction Project
- Projekt, N.N., Frank, Mo. 10:00-12:00, 3.04.0.02
Allgemeines
In dem Projekt werden von den Studierenden verschiedene Kalküle und Entscheidungsprozeduren für das automatische Theorembeweisen implementiert. Aus den Implementierungen wird gemeinsam mit dem Dozenten ein Theorembeweiser konstruiert, der sowohl für verschiedene Logiken anwendbar ist, als auch verschiedene, für entsprechende Logiken optimierte Kalküle beherrscht. Einer der Schwerpunkte liegt dabei bei der Performanz der Implementierungen. Abschließend wird der konstruierte Theorembeweiser mithilfe von Problem-Bibliotheken getestet und seine Performanz sowie seine Fähigkeiten mit aktuellen Theorembeweisern verglichen.
Voraussetzungen
Um für alle Themen geeignet zu sein, braucht man Grundkenntnisse in:
Themen aus Vorlesungen wie "Angewandte Logik":
- Aussagenlogik (Syntax, Semantik)
- Prädikatenlogik erster Stufe (Syntax,Semantik)
- Normalformen
Themen aus Vorlesungen der theoretischen Informatik:
- Komplexitätstheorie (Abschätzung der Zeit- und Platz-Komplexität)
- Formale Sprachen (Kontextfreie Grammatiken)
Interesse und Spaß am Implementieren.
Manche Themen sind auch mit weniger Vorkenntnissen handhabbar.
Inhalte
Mögliche Projekt-Themen sind (unter anderem):
Kalküle:
- DPLL/CDCL
- Resolution/Hyper-Resolution
- Konnektion
- Inst-Gen
- Paramodulation
- Superposition
- Konsolution
Entscheidungsprozeduren:
- Unifikation (Verschiedene Varianten möglich)
- Kongruenz-Hüllen
- Sup-Inf
Leistungserfassung
Als Leistung wird eine Implementierung des gewählten Kalkül (respektive der Entscheidungsprozedur) sowie eine Dokumentation gefordert.
Um die Implementierungen besser zu steuern werden die gewählten Kalküle im Vorlauf analysiert.
Gewichtung:
- Analyse: 40 %
- Implementierung: 40 %
- Dokumentation: 20 %
Die Implementierung muss lauffähig sein. Wenn die Implementierung nicht kompiliert, gilt das als nicht bestanden.
Kurs-Organisation
Die Organisation des Kurses erfolgt über Moodle.
Die Inhalte aus dem letzten Semester können auf folgender Seite abgerufen werden: https://moodle2.uni-potsdam.de/course/view.php?id=6088
Die zusätzlichen Inhalte dieses Semesters werden auf folgender Seite zur Verfügung gestellt: https://moodle2.uni-potsdam.de/course/view.php?id=7886
Literatur
Als Literatur werden Fachartikel zu den einzelnen Kalkülen/Entscheidungsprozeduren genutzt.
Weiterhin können Vortragsfolien/Wiki-Einträge Studierender aus dem Wintersemester für die Vorbereitung nachgenutzt werden.