Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 

Foto: Matthias Friel

Sie sind hier: Startseite

Automatisierte Logik und Programmierung: Formale Kalküle und Beweissysteme - Einzelansicht

Veranstaltungsart Vorlesung Veranstaltungsnummer 554511
SWS Semester WiSe 2016/17
Einrichtung Institut für Informatik und Computational Science   Sprache deutsch
Belegungsfristen 04.10.2016 - 10.11.2016

Belegung über PULS
04.10.2016 - 20.11.2016

Belegung über PULS
Gruppe 1:
     jetzt belegen / abmelden
    Tag Zeit Rhythmus Dauer Raum Lehrperson Ausfall-/Ausweichtermine Max. Teilnehmer/-innen
Einzeltermine anzeigen
Vorlesung Do 08:00 bis 10:00 wöchentlich 20.10.2016 bis 09.02.2017  3.04.1.02 Prof. Dr. Kreitz 22.12.2016: Akademische Weihnachtsferien
29.12.2016: Akademische Weihnachtsferien
Einzeltermine ausblenden
Vorlesung Do 10:00 bis 12:00 14-täglich 20.10.2016 bis 09.02.2017  3.04.1.02 Prof. Dr. Kreitz 29.12.2016: Akademische Weihnachtsferien
Einzeltermine:
  • 20.10.2016
  • 03.11.2016
  • 17.11.2016
  • 01.12.2016
  • 15.12.2016
  • 12.01.2017
  • 26.01.2017
  • 09.02.2017
Kommentar 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 sind 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
Voraussetzungen Gute Logikvorkenntnisse dringend empfohlen.
Teilnahme fuer Bachelorstudenten ab 5. Fachsemester nach Ruecksprache moeglich
Leistungsnachweis Muendliche Abschlusspruefung. Bei mehr als 15 Teilnehmern wird die Pruefung in Form einer Klausur abgenommen

Strukturbaum
Keine Einordnung ins Vorlesungsverzeichnis vorhanden. Veranstaltung ist aus dem Semester WiSe 2016/17 , Aktuelles Semester: SoSe 2024

© Copyright HIS
Hochschul-Informations-System eG