Direkt zum Inhalt | Direkt zur Navigation

Sektionen
Benutzerspezifische Werkzeuge

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.

Artikelaktionen
Auf einen Blick
Sprechzeiten

Montags, 12:30-14:00, Raum 1.23

Lehrform Projekt
Empfohlen ab FS 4
Voraussetzungen

TI I - Notwendig

TI II - Sehr empfohlen

Belibieger Logik-Kurs - Sehr empfohlen

Benotet Ja
Punkte gesamt 6
davon praktisch 6
Sprache deutsch/englisch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000), Wahlfrei(7000)
Studiengang Bachelor, Master
Belegung via PULS