212
Natur- und Ingenieurwissenschaftliches Kolleg
1. Formale Mathematik
Leitung
Prof. Dr. Peter Koepke
Mathematisches Institut, Universität Bonn
Die formale Mathematik ist ein interdisziplinäres Gebiet zwischen Mathematik, Logik,
und Informatik. Ihr Ziel ist die praktische Realisierung von vollständig formalen Bewei-
sen mathematischer Sätze. Das ist auf Grund des Gödelschen Vollständigkeitssatzes zwar
prinzipiell möglich, jedoch mit großen Komplexitätsproblemen verbunden. Erst vor weni-
gen Jahren gelang es durch massiven Einsatz von Computern und durch die Entwicklung
geeigneter Beweissprachen und Beweisalgorithmen, formale Beweise prominenter Theo-
reme wie des Vier-Farben-Satzes oder des Primzahlsatzes zu konstruieren. Inwieweit die
formale Mathematik die mathematische Praxis beeinflussen kann, ist eine offene Frage.
In der Kolleggruppe „Formale Mathematik“ werden wir theoretische Grundlagen erar-
beiten, etablierte Systeme studieren und eigene Programmier- und Formalisierungspro-
jekte verfolgen. Dabei interessieren wir uns besonders für die Verbindung verschiedener
Techniken unter Einbeziehung von Methoden der Computerlinguistik zu einer möglichst
natürlichen formalen Mathematik, deren Eingabesprache und Schlussweisen üblichen
mathematischen Texten nahe kommen.
Zur Einführung:
A Special Issue on Formal Proof, in: Notices of the American Mathematical Society 55/11,
2008, passim.
Fitting, M., First-Order Logic and Automated Theorem Proving, Springer Verlag 1990.
Blackburn, P./Bos, J., Representation and Inference for Natural Language. A First Course
in Computational Semantics, University of Chicago Press 2005.
