Inhalt

[ 201COMACOLV18 ] VL Computational Logic

Versionsauswahl
Workload Ausbildungslevel Studienfachbereich VerantwortlicheR Semesterstunden Anbietende Uni
3 ECTS B2 - Bachelor 2. Jahr Mathematik Wolfgang Schreiner 2 SSt Johannes Kepler Universität Linz
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)
Präsenzlehrveranstaltung
Teilungsziffer -
Zuteilungsverfahren Direktzuteilung