Seminar: Programmextraktion aus Beweisen

Zeit und Ort

Mo 14-16, B252; Beginn Montag, 12. Oktober 2015

Inhalt

Es sollen die Grundlagen der konstruktiven Analysis sowie der Extraktion von Programmen aus Beweisen erarbeitet werden. Vorausgesetzt werden Kenntnisse in Mathematischer Logik (eine einführende Vorlesung). Ferner wird vorausgesetzt, daß die Teilnehmer das Tutorium des Beweisassistenten Minlog durchgearbeitet haben.
Nach erfolgreichem Besuch des Seminars ist es möglich, eine Bachelorarbeit zu einem Thema aus diesem Umkreis zu schreiben.

Vorträge

Die Vorträge wurden in der ersten Seminarsitzung am 12. Oktober verteilt.

• Introduction to Minlog.
  parens.scm. Helmut Schwichtenberg. 19. Oktober.
• Inductive and coinductive predicates. (First part of Section 3. From gray.scm up to line 1045.) 2 Vorträge.
  Quirin Schroll, Theresa Ullmann. 26. Oktober und 2. November.
  Materialien zum Vortrag Schroll: rec-op.hs und extract.scm.
• Average for reals coded by signed digit sequences. (Section 4.1 and 6.1 - 6.3. From gray.scm lines 1187 - 1732.) 2 Vorträge (Folien).
  Franziskus Wiesnet. 9. und 16. November.
  
• Gray-code for reals. CoG subseteq CoI. (Second part of Section 3. Sections 4.2 and 6.4. From gray.scm lines 1046 - 1187, and 1733 - 1857.)
  Mirza Canovicz. 23. November.
• CoI subseteq CoG. (Sections 4.3 and 6.5. Simultaneous corecursion. From gray.scm lines 1858 - 2070.) (Folien)
  Till Überrück-Fries. 30. November.
• Average for Gray-coded reals. (Sections 4.4 and 6.6. From gray.scm lines 2071 - 2826.) 2 Vorträge.
  Simone Herzner. 7. und 14. Dezember.
• A parametrized normal form for pre-Gray code. (Sections 4.5 and 6.7. From gray.scm lines 2827 - 3138.)
  Tomy Kufner. 21. Dezember.
• Modified Gray expansion. (Sections 5 and 6.8. From gray.scm lines 3139 - 3879.) 2 Vorträge.
  Andreas Franz. 11. und 13. Januar.

Materialien

Die aktuelle Version von Minlog ist auf den CIP-Rechnern des Mathematischen Instituts installiert (Aufruf: minlog).

• Skript Logic for Gray-code computation.
• gray.scm.
• gray.hs.

sowie als ergänzende Literatur

• Bishop/Bridges, Constructive Analysis, Kapitel 2. Springer 1985.
• Bridges/Vita, Techniques of Constructive Analysis. Springer 2006.
• Skript Constructive analysis with witnesses.

Sprechstunde

• Helmut Schwichtenberg, Mi 13-14, B421.

Studienordnungen

Das Seminar ist unter P8 und WP6.3 (bzw. P15.1 und WP6.3) in der Bachelorstudienordnung Mathematik (bzw. Wirtschaftsmathematik) aufgelistet (3 ECTS Punkte). Im Masterstudium Mathematik (bzw. Wirtschaftsmathematik) kann es als Teilmodul 14.2 (zusammen mit 14.1 Tutorentraining) oder 16.2 (zusammen mit 16.1 Seminar) eingebracht werden.

Letzte Änderung

2. Dezember 2015