Es ist eine neuere Version 2023W dieser LV im Curriculum Masterstudium Computational Mathematics 2023W vorhanden.
Workload
Ausbildungslevel
Studienfachbereich
VerantwortlicheR
Semesterstunden
Anbietende Uni
1,5 ECTS
B3 - Bachelor 3. Jahr
Mathematik
Teimuraz Kutsia
1 SSt
Johannes Kepler Universität Linz
Detailinformationen
Quellcurriculum
Bachelorstudium Technische Mathematik 2013W
Ziele
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.
