Benutzerspezifische Werkzeuge
Sie sind hier: Startseite Willkommen Professuren Ordentliche Professuren Theoretische Informatik Lehrveranstaltungen Wintersemester 2016/2017 Automatisierte Logik und Programmierung: Formale Kalküle und Beweissysteme

Automatisierte Logik und Programmierung: Formale Kalküle und Beweissysteme

  • Vorlesung, Prof. Dr. Kreitz, Do 8:40-10:10, 3.04.1.02 (ab 3.11.2016)
  • Vorlesung/Übung, Prof. Dr. Kreitz, Do. 10:15-11:45, 3.04.1.02

Softwareprodukte sind in den vergangenen Jahren ein integraler Bestandteil unseres alltäglichen Lebens geworden. Anwendungen reichen von Steuerungsmodulen in Alltagsprodukten, e-Commerce, Telephonnetzen, bis hin zu Automobilkonstruktion und Luftfahrtkontrolle.

Die wachsende Komplexität und umfassendere Verwendung dieser Produkte macht es erforderlich, Methoden zu entwickeln, welche die Zuverlässigkeit von Software besonders in sicherheitskritischen Anwendungen sicherstellen. Aus konzeptioneller Sicht ist der Entwurf von Software im wesentlichen ein logischer Schlussfolgerungsprozess, der Wissen über Algorithmen, deren Anwendungsbereich und Programmiertechniken verwendet und zu einem Grossteil schematisiert werden kann. Durch den Einsatz logisch-formaler Methoden kann die Zuverlässigkeit dieses Prozesses erheblich gesteigert werden.

Im Rahmen der Vorlesung Automatisierte Logik und Programmierung werden die Grundlagen logisch-formaler Programmentwicklung besprochen. Die Formalisierung von Logik, Berechenbarkeit und Datentypen in der intutionistischen Typentheorie bildet das theoretische Fundament. Die Automatisierung logischer Schlüsse wird anhand des interaktiven Beweissystems Nuprl demonstriert. Aufgrund des Umfangs der Thematik wird die Veranstaltung auf zwei Semester verteilt. Schwerpunkt des ersten Semesters ist das theoretische Fundament. Thema des zweiten Semesters sind Aufbau, Automatisierung und Anwendung von Beweissystemen.

Literatur

  • Per Martin-Löf: Intuitionistic Type Theory., Studies in Proof Theory Lecture Notes, Bibliopolis, Napoli 2002
  • Robert L. Constable et. al.: Implementing Mathematics with the Nuprl proof development system. Prentice Hall, 1986
  • Lawrence C. Paulson: Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, 1987
Artikelaktionen
Auf einen Blick
Lehrform diverse Formen
Empfohlen ab FS 6
Voraussetzungen Gute Logikvorkenntnisse dringend empfohlen. Teilnahme für Bachelorstudenten ab 5. Fachsemester nach Rücksprache möglich.
Benotet Ja
Punkte gesamt 6
davon praktisch 0
Sprache deutsch
Fremdhörer zugelassen? Nein
Teilgebiete Theoretische Informatik(2000), Angewandte Informatik(4000), Wahlfrei(7000)
Studiengang Bachelor, Master
Belegung via PULS