Mathematisches Beweisen lernen mithilfe des Beweisassistenten Coq (SoSe 2022)

Informatik-Studierende finden Themen der Theoretischen Informatik grundsätzlich interessant, aber korrespondierende Übungsaufgaben -- insbesondere Beweisaufgaben -- stellen immer wieder eine große Herausforderung dar. Der Kurs greift diesen Punkt auf und stellt das mathematische Beweisen in den Mittelpunkt der Auseinandersetzung.

Zum Erlernen der klassischen „Papier&Stift”-Beweise werden wir einen indirekten Weg einschlagen: Zunächst werden wir lernen, mit dem Beweisassistenten Coq Beweise zu führen (Erklärung Beweisassistent s.u.). Später werden wir daran arbeiten, diese Form der Beweise in „Papier&Stift”-Beweise zu übertragen. Schließlich wird auch eingeübt werden, „Papier&Stift”-Beweise direkt zu führen.

Die Inhalte, anhand derer wir die Beweismethodik einstudieren werden, sind die folgenden:
1) Logik
  a) Aussagenlogik
  b) Prädikatenlogik
2) Datenstrukturen
  a) Nicht-rekursive Datenstrukturen (Records)
  b) Listen
  c) Natürliche Zahlen
  d) Binärbäume
Das Ziel allerdings ist hierbei weniger einen konkreten Themenbereich der Mathematik oder Theoretischen Informatik durchzuarbeiten, sondern den Teilnehmerinnen und Teilnehmern des Kurses ein grundlegendes Verständnis mathematischer Beweisformen, formaler Methoden und dem dazugehörigen Handwerkszeug zur Entwicklung und Erstellung dieser zu vermitteln.

Was sind Beweisassistenten?

Computergestützte Systeme zur Durchführung mathematischer Beweise werden seit den 1960ern entwickelt. Man unterscheidet zwischen Systemen, die Beweise erzeugen, sowie solchen, die Menschen beim Erzeugen von Beweisen unterstützen. Letztere werden auch Beweisassistenten oder interaktive Theorembeweiser genannt, ein solches System ist Coq, welches wir im Kurs einsetzen werden.

Bei Beweisassistenten im engeren Sinne des Begriffes kann der Nutzer Schritt für Schritt Wissen aus den Voraussetzungen generieren und das bisherige Ziel durch ein leichter zu zeigendes, aber hinreichendes Ziel ersetzen. Konkret werden Beweise durch eine Auflistung von sogenannten Taktiken innerhalb einer dem Programmieren ähnlichen Entwicklungsumgebung gewonnen, wobei den Taktiken systemintern Inferenzregeln zugrunde liegen. Das System führt die durch die Taktiken vermittelten Inferenzregeln aus. Dabei prüft es jeden Beweisschritt auf seine formale Korrektheit. Dies ist in erster Näherung mit dem Compilereinsatz beim Programmieren vergleichbar.

Beweisassistenten haben gegenüber Stift und Papier verschiedene Vorteile:
-    Sie liefern unmittelbares Feedback auf eine Beweisidee, indem sie genau anzeigen, ob ein Beweisschritt erfolgreich anwendbar ist und welche Schritte noch auszuführen sind, damit ein Beweis vollständig abgeschlossen ist.
-    Studierende können zu Beginn verschiedene Beweisideen ausprobieren, indem sie mit dem jeweiligen System spielen. Das garantiert höhere Flexibilität gegenüber Stift- und Papierbeweisen, in denen man nur sehr schlecht Dinge streichen oder verbessern kann, ohne den Beweis neu aufschreiben zu müssen. Aus dem gleichen Grund sollte ein Beweisassistent auch besser darin unterstützen, mit einem Beweis überhaupt zu beginnen.