Mathematische Beweisführung im Beweisassistenten Rocq - Einzelansicht

In diesem Kurs werden wir lernen, mit dem Beweisassistenten Rocq mathematische Beweise zu führen.

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 Rocq, 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.

Vorteile von Beweisassistenten:

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.

Themenübersicht:     ( alle Themen werden im Beweissassistenten Rocq behandelt)

1. Logik als Grundlage der Beweisstruktur
   1. Aussagenlogik
   2. Prädikatenlogik
2. Datenstrukturen
   1. Nicht-rekursive Datenstrukturen
   2. Listen
   3. Natürliche Zahlen als induktive Datenstruktur
   4. Binärbäume
3. Erweiterte Themen, z.B.:
   1. Entwurf und Nutzung algebraischer Taktiken mittels Ltac
   2. Abhängige Datenstrukturen
   3. Gleichheiten in der Typentheorie
   4. Simulation anderer Theorien
   5. Praxisbeispiel
   6. Induktion in der Praxis
   7. Coercions