Arbeitsgemeinschaft zur Formalen Mathematik
Leitung
- Prof. Dr. Peter Koepke
- Dr. Ioanna Dimitriou
Termin
- Dienstags, 14:15 - 16:00 Uhr, CIP-Pool im Mathematikzentrum, Raum N.0.004
- Begin: Dienstag, 12.05.2015.
Beschreibung
Die mathematische Logik zeigt, dass alle mathematischen Beweise im Prinzip vollkommen formal durchgefürt werden können. In der Formalen Mathematik geht es um die tatsächliche Umsetzung dieses Programms mit Hilfe von Computersystemen. In der Arbeitsgemeinschaft wollen wir uns in das System Isabelle sowie Formalisierungen im Bereich der Mengenlehre einarbeiten.
Die Arbeitsgemeinschaft richtet sich an die Hörerinnen und Hörer der "Einfürung in die Mathematische Logik" und an andere Interessierte. Aus der Arbeitsgemeinschaft können Projekte für das Modul "Praktikum Mathematische Logik" (P2A1) hervorgehen.
Die Arbeitsgemeinschaft findet im CIP-Pool statt. Die Benutzung eines eigenen Laptops ist sehr zu empfehlen, es können aber auch die Rechner des Instituts benutzt werden. In der ersten Sitzung am 12.5. ging es um eine allgemeine Einführung in Isabelle und die Installation der Software. Eine kurze Installationsanleitung finden Sie hier .
Ab der zweiten Sitzung werden wir mit dem Skriptum "Programming and Proving" anfangen.
Weiteres Programm:
- 2 Juni Ioanna Dimitriou: "Programming and
Proving" Zusammenfassung
- 9 Juni Regula Krapf: "Logic and Proof Beyond Equality" Logikregeln, Lösungen zu den Aufgaben, Beispiele
- 16 Juni Thekla Hamm, Luisa Vogel: "Isar: A Language for Structured Proofs", Lösungen zu den Aufgaben, Beispiele
- 23 Juni Benjamin Valdez, Robert Paßmann: "Group theory in Isabelle/Isar/HOL" Informationen zu Locales und Sublocales, Theory-Dateien: Lemmas über die triviale Gruppe, die zyklische Gruppe Z4 mit Definition 1, Definition 2.
- 30 Juni Calvin Pfeifer, Thorben Tröbst: "ZF Set Theory in Isabelle/Isar/HOL"Theory-Datei mit Beispiele.
- 7 Juli Thorben Tröbst: "Zorns Lemma in Isar" Theory-Datei
14 Juli Abschlusssitzung