Automatisierte Logik und Programmierung II

Universität Potsdam, Sommersemester 2004


Veranstalter: Prof. Dr. Christoph Kreitz
Zielgruppe: ab 5. Semester
Umfang: 6 SWS (3 SWS Vorlesung, 1 SWS Übung; 2 SWS Praktikum)
Informatikfach-
zuordnung:		 Theoretische Informatik, Angewandte Informatik
Leistungspunkte: 9 benotete Punkte
Zeit: Vorlesung:
  • montags 13.30-15.00 Uhr (wöchentlich)
  • dienstags 13.30-15.00 Uhr (14-tägig)
    Übungen:
  • dienstags 13.30-15.00 Uhr (14-tägig)
    Praktikum:
  • donnerstags 11.00-12.30 Uhr (wöchentlich)
    Sprechstunde:
  • mittwochs 11.00-12.30 Uhr oder nach Vereinbarung
    • Ort: Vorlesungen und Übungen:   3.04.1.02
    Praktikum:   3.04.1.03
    Beginn: Vorlesung: 13.4.2004
    Übungen:   20.4.2004
    Praktikum:  16.4.2004
    Aktuelles:
  • Die Abschlußprüfung zur Automatisierte Logik und Programmierung I wird gemäß dem Wunsch der Mehrheit der Teilnehmer als mündliche Prüfung von ca 20 Minuten gehalten. Die Prüfungen werden nach Absprache in der ersten Sommersemesterwoche (14.4.-16.4) stattfinden.
  • Sollte der Umfang für manche Teilnehmer zu groß sein, kann eine reduzierte Version der Veranstaltung vereinbart werden.

    • Zielstellung:

    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, den 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 2 Semester verteilt. Im ersten Teil (Wintersemester 2003/2004) wurde die inutitionistische Typentheorie als theoretisches Fundament vorgestellt. Thema dieses zweiten Teils sind Aufbau, Automatisierung und Anwendung von Beweissystemen.

    Gliederung :

    Literaturhinweise :

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

    Leistungserfassung :

     Zur Leistungserfassung des zweiten Semesters wird zu 50% eine mündliche Abschlußprüfung und zu 50% ein selbstgewähltes praktisches Beweiserprojekt des Praktikums herangezogen. Die Bearbeitung von Aufgaben auf den Übungsblättern ist freiwillig. Als Mittel der Selbstkontrolle können Übungsaufgaben zur Korrektur eingereicht werden.

    Belegung:

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

    Übungsaufgaben: