Hauptseminar Mathematische Logik (S2A2)

Dozent

• Prof. Dr. Peter Koepke

Zeit und Ort

• Donnerstags, 14.15-18.00 Uhr, ((Seminarraum N0.008)), per ZOOM
• Beginn: 23.04.2020

Inhalt

In speziellen Theorien und Strukturen wie der Theorie der algebraisch abgeschlossenen Körper oder der Struktur der reellen Zahlen lässt sich die Wahrheit gewisser Aussagen durch die Kombination logischer und algebraischer Methoden algorithmisch entscheiden. Auch einige geometrische Fragen lassen sich durch Umformulierung in die analytische Geometrie entscheiden. In dem Seminar folgen wir Kapitel 5 des "Handbook of Practical Logic and Automated Reasoning" von John Harrison. Das Buch enthält praktische Implementierungen der Algorithmen in der funktionalen Programmiersprache OCaml. Die Teilnehmer sollen mit diesen Programmen auf eigenen Laptops experimentieren.
Allgemeine Voraussetzung für das Seminar sind Kenntnisse der mathematischen Logik wie im Modul "Einführung in die Mathematische Logik" (V2A2). Für die Anwendungen werden einfache algebraische Grundlagen über Gruppen, Ringe, Ideale und Körper benötigt. Für die praktische Vorstellung der Entscheidungsverfahren setzen wir weiter Computerkenntnisse und die Bereitschaft, sich in die Programmiersprache OCaml einzuarbeiten, voraus.

Programm

23.4.: 1. Peter Koepke: Quantifier elimination and dense linear orders [1, 328-336]

30.4.: 2. + 3. Paulina Blome und Erik Sturzenhecker: Presburger Arithmetic [1, 336-350]

14.5.: 4. + 5. Thomas v. Campenhausen und Sarah Zengl: Complex Numbers [1, 352-366]

28.5.: 6. + 7. Simon Blasinski Teil 1, Teil 3 und Moritz Hartlieb Teil 2, Teil 4: Wordproblems [1, 380-400]

18.6.: 8. Jonas Lippert: Gröbner bases [1, 400-414]

Literatur

[1] John Harrison: Handbook of practical logic and automated reasoning, Cambridge University Press, 2009.