Automatisierte Logik und Programmierung I

Universität Potsdam, Wintersemester 2003/2004


Veranstalter: Prof. Dr. Christoph Kreitz
Zielgruppe: ab 5. Semester
Umfang: 4 SWS (3 SWS Vorlesung, 1 SWS Übung)
Informatikfach-
zuordnung:		 Theoretische Informatik, Angewandte Informatik
Leistungspunkte: 6 benotete Punkte
Zeit: Vorlesung:
  • montags 11.00-12.30 Uhr (wöchentlich)
  • freitags 13.30-15.00 Uhr (14-tägig)
    Übungen:
  • freitags 13.30-15.00 Uhr (14-tägig)
    • Ort: Vorlesungen und Übungen:   3.04.1.02
    Beginn: Vorlesung: 13.10.2003
    Übungen:   24.10.2003
    Aktuelles: Die Abschlußprüfung wird gemäß dem Wunsch der Mehrheit der Teilnehmer als mündliche Prüfung von ca 20 Minuten gehalten. Die Termine wurden den Teilnehmern per e-mail mitgeteilt.
    Sollte ein Teilnehmer keine e-mail von mir erhalten haben bitte ich um schnellstmoegliche Rueckmeldung

    Zielstellung:

    Softwareprodukte sind in den vergangenen Jahren ein integraler Bestandteil unseres allt&auuml;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, den Anwendungsbereich und Programmiertechniken verwendet und zu einem Grossteil schematisiert werden kann. Durch den Einsatz logisch-formaler Methoden kann 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 2 Semester verteilt. Schwerpunkt des ersten Semesters sind das theoretische Fundament und der Aufbau von Beweissystemen. Thema des zweiten Semesters sind Automatisierung und Anwendung von Beweissystemen.

    Gliederung :

    Literaturhinweise :

     Zur Zeit existiert kein Lehrbuch, das die gesamte Thematik abdeckt. Lesenswert sind Ein ausführliches Skript, Vorlesungsfolien und das Nuprl Manual werden online bereitgestellt.

    Leistungserfassung :

     Zur Leistungserfassung des ersten Semesters wird je nach Teilnehmerzahl eine abschliessende Klausur oder mündliche Prüfung herangezogen. Die Bearbeitung von Aufgaben auf den Übungsblättern ist freiwillig. Als Mittel der Selbstkontrolle können Übungsaufgaben zur Korrektur eingereicht werden.

    Im zweiten Teil wird ein selbstgewähltes praktisches Beweiserprojekt zu 50% gewichtet.

    Belegung:

     Die Belegung erfolgt elektronisch entsprechend der Bestimmungen des Instituts für Informatik.

    Übungsaufgaben: