Um der Problematik der fehlenden Grundkompetenzen mathematischer Beweise zu begegnen, untersuchen wir in einem weiteren Projekt, welche Rolle interaktive Theorembeweiser oder kurz Beweisassistenten als interaktive Lernwerkzeuge für die Entwicklung fachlicher Kompetenzen im formal-mathematischen Bereich spielen können. Computergestützte Systeme zur Durchführung mathematischer Beweise werden seit den 1960ern entwickelt. Beweisassistenten wurden bereits des Öfteren in weiterführenden Veranstaltungen in der Theoretischen Informatik und Mathematik eingesetzt. In der Eingangslehre der Theoretischen Informatik hingegen sind Beweisassistenten bisher kaum genutzt worden. Dabei besitzen sie Merkmale, die als Lernwerkzeug aus didaktischer Sicht verschiedene Vorteile gegenüber Stift und Papier bzw. Tafel und Kreise haben und die wir im Rahmen eines Design-Based-Research Ansatzes untersuchen, konkret:
Das System liefert unmittelbares Feedback, ob ein Beweisschritt korrekt war und welche Schritte noch auszuführen sind, damit der Beweis vollständig abgeschlossen ist. Das direkte Feedback könnte Studierenden helfen, ihre Beweisidee selbst zu überprüfen, dabei mögliche Fehler zu finden und so zu einer insgesamt besseren Lösung zu kommen. Lehrende und Tutoren würden damit insgesamt bessere Arbeitsergebnisse der Studierenden zur Korrektur vorgelegt bekommen und im besten Fall würden mehr Studierende die Abschlussklausur erfolgreich bestehen.
Das System verlangt ohne Ausnahme eine präzise und formal korrekte Anwendung mathematischer Formalismen und könnte insbesondere mathematisch schwächeren Studierenden helfen, die formal korrekter Ausdrucks- und Schreibweise zu erlernen.
Die Nutzung eines Beweisassistenten entspricht in vielerlei Hinsicht der Tätigkeit des Programmierens und sollte daher für Informatikstudierende insgesamt ein bekannter Ansatz sein, insbesondere, wenn sie frühzeitig mit der funktionalen Programmierung vertraut gemacht werden. Hier könnte auch auf Forschungsergebnisse aus dem international gut untersuchten Forschungsbereich zum Programmieren Lernen zurückgegriffen werden.
Für eine erste Erprobung dieses Ansatzes haben wir einen zweiwöchigen Blockkurs in Coq für Bachelor-Studierende im 2. und 3. Fachsemester auf Grundlage des Cognitive Apprenticeship Ansatzes entwickelt und Anfang Oktober 2016 an der Universität Hamburg durchgeführt. Inhaltlich ging es um formale Papier- und Coqbeweise in Logik und Datenstrukturen.
Zuständige wissenschaftliche Mitarbeiter
Christiane Frede
Kooperationspartner
Prof. Dr. Maria Knobelsdorf, Arbeitsbereich Computer Science Education, Fachbereich Informatik, Universität Hamburg
Prof. Dr. Christoph Kreitz, Sebastian Böhne, Lehrstuhl für Theoretische Informatik, Fachbereich Informatik, Universität Potsdam
PD Dr. Christoph Benzmüller, Fachbereich Informatik, Freie Universität Berlin
Projektförderung
Das Projekt wurde im Sommersemester 2016 durch das Lehrlabor der MIN Fakultät der UHH gefördert, einem Teilprojekt des Universitätskollegs der UHH. Letzteres wird durch das BMBF im Rahmen des "Qualitätspakt Lehre" gefördert.
Laufzeit: Seit April 2016