Inhalt
[ 201UCMACOLU18 ] UE Computational Logic
|
|
|
|
 |
| Workload |
Ausbildungslevel |
Studienfachbereich |
VerantwortlicheR |
Semesterstunden |
Anbietende Uni |
| 1,5 ECTS |
B2 - Bachelor 2. Jahr |
Mathematik |
Wolfgang Schreiner |
1 SSt |
Johannes Kepler Universität Linz |
|
|
|
| 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 |
Laufend auszuarbeitende schriftliche/software-basierte Übungsaufgaben.
|
| Lehrmethoden |
Siehe Vorlesung.
|
| Abhaltungssprache |
Englisch |
| Literatur |
Siehe Vorlesung.
|
| Lehrinhalte wechselnd? |
Nein |
|
|
|
| Präsenzlehrveranstaltung |
| Teilungsziffer |
25 |
| Zuteilungsverfahren |
Direktzuteilung |
|
|
|
