Lehrende: Prof. Dr. rer. nat. Reiner Hähnle
Veranstaltungsart: Integrierte Veranstaltung
Orga-Einheit: FB20 Informatik
Anzeige im Stundenplan: Automatisches Beweis
Fach:
Anrechenbar für:
Semesterwochenstunden: 4
Unterrichtssprache: Deutsch und Englisch
Min. | Max. Teilnehmerzahl: - | -
Digitale Lehre: Die Kurswebseite ist unter https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1114 erreichbar. Der Kurs wird digital gehalten. Alle Informationen werden rechtzeitig vor der ersten Vorlesung auf der Moodlewebsite bekannt gegeben.
Lehrinhalte: - Theoretische Grundlagen der im automatischen Beweisen verwendeten Kalküle für Logik erster Stufe - Korrektheits- und Vollständigkeitsbeweise - Algorithmen und Datenstrukturen, die in automatischen Beweisern für Logik erster Stufe eingesetzt werden - Vergleich verschiedener Ansätze im automatischen Beweisen - Grundlagen moderner SAT- und SMT-Lösungswerkzeuge
Literatur: Robinson, Voronkov: Handbook of Automated Reasoning, 2 vols., North-Holland
Voraussetzungen: Stark empfohlen wird die Teilnahme an der Vorlesung “Aussagen- und Prädikatenlogik” oder vergleichbarer Module. Ansonsten genügt eine gewisse mathematische Reife.
Automatisches Beweisen - Übung
Prof. Dr. rer. nat. Reiner Hähnle
Fr, 22. Okt. 2021 [13:30]-Fr, 18. Feb. 2022 [15:10]
