Beschreibung der wesentlichen Methoden für das automatische Schließen.
Lehrinhalte
Zusammenfassung der Prädikatenlogik erster Stufe; das Resolutionsverfahren; Vollständigkeit der Resolution (Herbrand-Theorem, semantische Bäume);
Verfeinerungen der Resolution; die DPLL Methode für das Erfüllbarkeitsproblem; Sequenzenkalkül; das Theorema-System.
Beurteilungskriterien
Schriftliche Klausur.
Abhaltungssprache
Englisch
Lehrinhalte wechselnd?
Nein
Frühere Varianten
Decken ebenfalls die Anforderungen des Curriculums ab (von - bis) 201LOSDAURU13: UE Automated Reasoning (2013W-2023S)
