Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage in der Lage unterschiedliche Werkzeuge, Sprachen und logikorienterte Methoden zum deklarativen Problemlösen zu benennen und zu erläutern, sowie theoretische Zusammenhänge korrekt zu argumentieren. Im Speziellen können nach positiver Absolvierung des Moduls die Studierenden

• die eingesetzten Techniken und Methoden formal analysieren,
• Methoden und Techniken für eine vorgegebene Aufgabenstellung zielgerichtet auswählen, sowie
• Lösungen und Formalismen kritisch bewerten.

Die Lehrveranstaltung behandelt unterschiedliche Formalismen zum deklarativen Problemlösen. Die Lehrveranstaltung besteht aus drei Teilen: Im ersten Teil werden Methoden des SAT und QSAT Beweisen vorgestellt, und im zweiten und dritten Teil wird Answer-Set Programmierung behandelt.

Organisation

Achtung:

• Die VO ist als Präsenzlehrveranstaltung geplant aber sie kann, abhängig von der COVID Situtation, in einen hybriden Präsenz-/Onlinemodus oder reinen Onlinemodus wechseln.

Lecturers:

• Uwe Egly: SAT and QSAT
• Hans Tompits: ASP Part I
• Tobias Geibinger: ASP Part II

Frontalvortrag.

ECTS breakdown: 3 ECTS = 75 hours

• Lectures, course introduction 24h
• Preparation for the final exam 50h
• Final exam 1h

The course material is in English; introductory courses will be held in English on demand.

Mündliche Prüfung.

Basic knowledge of Mathematical Logic (Unification, Horn-Clause Resolution).