64-665 Mathematisch Argumentieren und Beweisen

Lehrende: Prof. Dr. Maria Joanna Knobelsdorf

Veranstaltungsart: Vorlesung + Übung

Anzeige im Stundenplan: Math. Argumentieren

Semesterwochenstunden: 2

Credits: 3,0

Unterrichtssprache: Deutsch

Min. | Max. Teilnehmerzahl: - | 50

Weitere Informationen:
Der Kurs richtet sich in erster Linie an Bachelor-Studierende in der Studieneingangsphase (d.h. im Fachsemester 1-4), die einen Informatikstudiengang am Fachbereich Informatik belegt haben (d.h. auch Wirtschaftsinformatik, Lehramt oder MCI).  Freie Plätze werden gerne an Studierende anderer Fachrichtungen (z.B. Mathematik) oder an Informatik-Studierende im Master vergeben.

Für den Kurs sind keine Voraussetzungen nötig. Thematisch nahe Veranstaltungen wie „Diskrete Mathematik“, „Mathematik für Informatiker“ oder „Formale Grundlagen der Informatik 1“ können aber müssen nicht vorher besucht worden sein.

Zeit und Räume:
Der Kurs findet als zweiwöchige Blockveranstaltung statt. Achtung: wegen Feiertag am 3.10. startet die erste Woche am Dienstag, dem 4.10. und geht bis einschließlich Samstag dem 8.10.2016.
Der Kurs findet täglich von 9-16 Uhr im Geomatikum statt. Es gibt jeweils am Vormittag (9-10 Uhr) und am Nachmittag (13-14 Uhr) einen Vorlesungsteil mit anschließendem Übungsteil. Von 12-13 Uhr ist eine Mittagspause vorgesehen. Die Vorlesungen finden in der ersten Woche im Raum 740 (7.OG) und in der zweiten Woche in Raum 531 (5.OG) statt. Die Übungen finden in den Poolräumen 142, 143 und 144 im 1. OG statt.
Wenn möglich, kann gerne der eigene Laptop mitgebracht und damit gearbeitet werden. Es wird empfohlen, ein Linux-basiertes Betriebssystem zu nutzen. Es wird zu Beginn eine Hilfestellung bei der Installation von Coq gegeben werden.

Kontakt:
Der Kurs ist eine neue Veranstaltung, die im Rahmen eines MIN-Lehrlabor Projekts stattfindet und eine Kooperation zwischen dem Arbeitsbereich „Computer Science Education“ von Prof. Dr. Maria Knobelsdorf, Fachbereich Informatik, und dem Lehrstuhl „Theoretischen Informatik“ an der Universität Potsdam darstellt.
Bei weiteren Fragen kontaktieren Sie bitte Prof. Dr. Maria Knobelsdorf: knobelsdorf@informatik.uni-hamburg.de oder den Dozenten der Veranstaltung, Herrn Sebastian Böhne von der Universität Potsdam: boehne@uni-potsdam.de.


 

Kommentare/ Inhalte:
Informatik-Studierende finden Themen der Theoretischen Informatik grundsätzlich interessant, aber korrespondierende Übungsaufgaben insbesondere Beweisaufgaben stellen immer wieder eine große Herausforderung dar. Der zweiwöchige Blockkurs greift diesen Punkt auf und stellt mathematisches Argumentieren und Beweisen in den Mittelpunkt der Auseinandersetzung. Neben dem klassischen Werkzeug „Papier&Stift“ wird hierbei der interaktive Beweisassitent Coq eingeführt und im Kurs eingesetzt werden. Inhaltlich wird in der ersten Woche eine Einführung in Aussagen- und Prädikatenlogik und entsprechende Sätze und Beweise stattfinden, wie sie z.B. auch bereits in FGI 1 thematisiert wurden. In der zweiten Woche liegt der thematische Fokus auf Datenstrukturen. Das Ziel hierbei ist weniger einen konkreten Themenbereich der Mathematik oder Theoretischen Informatik durch zuarbeiten, 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.

Mathematisches Argumentieren und Beweisen lernen mit einem  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 und wird im Kurs eingesetzt 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.

 

Zusätzliche Hinweise zu Prüfungen:
Die abschließende Prüfung ist eine schriftliche Klausur, die am Rechner Ende Oktober in den Poolräumen des Fachbereichs Informatik (Campus Stellingen) stattfinden wird. Termine siehe STiNE