 |
| Detailinformationen |
| Quellcurriculum |
Bachelorstudium Technische Mathematik 2025W |
| Lernergebnisse |
Kompetenzen |
| Die Studierenden verstehen die fundamentalen Konzepte und Methoden der
Computational Logic, d.h., derjenigen Aspekte der formalen Logik, die durch
Software unterstützt werden können und/oder relevant für die Softwareentwicklung
sind. Die Studierenden können Probleme aus verschiedenen Anwendungsbereichen
durch logische Formeln modellieren und geeignete logische Methoden anwenden, um
einfache Beispiele dieser Probleme händisch zu lösen. Zur Lösung schwierigerer
Beispiele sind sie in der Lage, logische Software-Werkzeuge effektiv
einzusetzen.
|
|
| Fertigkeiten |
Kenntnisse |
- Aussagenlogik: Berechnen von Wahrheitstabellen und von Normalformen, Vereinfachen durch logische Äquivalenzen; Entscheiden der Gültigkeit/Erfüllbarkeit durch verschiedene Kalküle/Algorithmen.
- Prädikatenlogik: Bestimmen der freien Variablen, Berechnen der Wahrheitswerte von geschlossenen Formeln über endlichen Bereichen, Vereinfachen durch logische Äquivalenzen, Berechnen von Normalformen; Beweisen der Gültigkeit/Erfüllbarkeit durch verschiedene Kalküle/Algorithmen.
- Gleichheit: Verwenden von prädikatenlogischen Schlussregeln zur Behandlung von Gleichheit, Umwandlung von Systemen von Gleichheiten in kanonische Termersetzungs-Systeme.
- Entscheidbare logische Theorien: Entscheiden der Erfüllbarkeit von Formeln in verschiedenen Theorien und in Kombinationen dieser Theorien.
- Formalisieren von Problemen aus verschienden Anwendungsbereichen durch logische Formeln, Anwenden von logischen Software-Werkzeugen zu deren Lösung: SAT solver in der Aussagenlogik, automatische Beweiser in der Prädikatenlogik, SMT solver in entscheidbaren logischen Theorien.
|
Aussagenlogik: Syntax und Semantik, Gültigkeit und Erfüllbarkeit, logische
Äquivalenz, Sequenzenkalkül, Resolution, DP-Algorithmus, DPLL-Algorithmus.
Prädikatenlogik erster Stufe: Syntax und Semantik, Gültigkeit und Erfüllbarkeit,
logische Äquivalenz, Sequenzenkalkül, Gilmore-Algorithmus, analytische Tableaus,
Resolution. Prädikatenlogik mit Gleichheit: Schlussregeln für Gleichheiten,
kanonische Termersetzungs-Systeme, Knuth-Bendix-Vervollständigung. Entscheidbare
logische Theorien: lineare reelle Arithmetik, Fourier-Motzkin-Elimination,
Theorie der Gleichheit mit uninterpretierten Funktionen, die Methode des
Kongruenzenabschlusses, die Nelson-Oppen-Methode. Software zur logischen
Ausbildung (Sequent Calculus Trainer, Tree Proof Generator), für SAT solving
(MiniSat, Limboole), prädikatenlogisches Beweisen (Vampire), SMT solving (Z3).
|
|
| Beurteilungskriterien |
Schriftliche Klausur am Ende des Semesters.
|
| Lehrmethoden |
Präsentationen mit Folien und Softwaredemonstrationen; begleitend wird eine Übung mit Aufgaben angeboten, zu deren Lösung teilweise Software eingesetzt wird.
|
| Abhaltungssprache |
Englisch |
| Literatur |
- Folien zur Vorlesung.
- John Harrison: Handbook of Practical Logic and Automated Reasoning.
- Jean H. Gallier: Logic for Computer Science - Foundations of Automated
Theorem Proving.
- Melvin Fitting: First-Order Logic and Automated Theorem Proving.
- Aaron R. Bradley, Zahor Manna: The Calculus of Computation - Decision
Procedures with Applications to Verification.
- Daniel Kroening, Ofer Strichman: Decision Procedures - An Algorithmic
Point of View.
|
| Lehrinhalte wechselnd? |
Nein |
| Sonstige Informationen |
https://risc.jku.at/courses/
|
| Äquivalenzen |
TM1PEKVSWEN: KV Software Engineering (3 ECTS)
|
|
