| Detailinformationen |
| Quellcurriculum |
Bachelorstudium Technische Mathematik 2023W |
| Ziele |
Die Studierenden lernen die Grundlagen der computerbasierten Logik kennen, d.h., derjenigen Aspekte der Logik, die von Software unterstützt werden können und auch relevant für die moderne Softwareentwicklung sind: Verfahren zur Lösung des Erfüllbarkeitsproblem der Aussagenlogik und zum computerunterstützten bzw. vollautomatischen Beweisen in der Prädikatenlogik, sowie Entscheidungsverfahren für gewisse (Kombinationen) von logischen Theorien. Dem Gegenstand der Lehrveranstaltung entsprechend wird die Theorie anhand von Software demonstriert, die diese Verfahren implementiert. Weiters präsentieren wir Logik-basierte Werkzeuge, die in realen Anwendungen eingesetzt werden und demonstrieren deren praktische Nutzung.
|
| Lehrinhalte |
- Aussagenlogik: Syntax und Semantik, Beweise, Verfahren zur Lösung des
Erfüllbarkeitsproblems, Software und Anwendungen.
- Prädikatenlogik: Syntax und Semantik, Beweise, die Methode der Analytischen Tableaus, das Resolutionsverfahren, Beweisen über Gleichheit, Software zum Beweisen.
- Entscheidbare Theorien, Entscheidungsverfahren und deren Kombination.
|
| 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)
|
