Modelle und Theorie Verteilter Systeme

Studienreformprojek

Ziel des Studienreformprojekts ProveIT ist es, Beweiskompetenz als expliziten Lerngegenstand in Modulen der Theoretischen Informatik zu etablieren und somit das Erlernen des Führens mathematischer Beweise erleichtern. Dieses Ziel soll mit der Integration von Lernsoftware erreicht werden. Für diesen Zweck entwickeln wir seit Ende 2022 prototypisch das Webtool ProofBuddy, ein Frontend für den weit verbreiteten Beweisassistenten Isabelle.

Für unser Vorhaben konzipierten wir zudem das Seminar World of Proofcraft, in dem das genannte Webtool eingesetzt und mit dem Educational Design Research Ansatz iterativ verbessert wird. In diesem Seminar erstellen Studierende eigene Lernportfolios, ein didaktisches Instrument zur systematischen Kontextualisierung von Lernzusammenhängen. Zusätzlich werden die Lernenden in der Präsenzzeit des Seminars beobachtet. Aus diesen Beobachtungen werden in einer empirischen Studie die Fragen der Studierenden kategorisiert, um somit Fehlerkategorien bei der Beweisführung zu identifizieren. Diese werden dann mit den Verläufen der Beweisentwicklung in ProofBuddy verglichen. Durch eine datenbasierte Analyse soll sowohl die Usablity von ProofBuddy als auch das gegebene Feedback an die Lernenden verbessert werden. Schließlich, also mittel- und langfristig, sollen Studierende durch einen möglichst individuellen Lernpfad unterstützt werden.

Die Ergebnisse des Projekts fließen direkt in die Weiterentwicklung der Theorieausbildung im Rahmen des Bachelorstudiums Informatik ein, das aktuell umstrukturiert wird.

ProofBuddy

ProofBuddy ist eine Weboberfläche zum Lernen des Führens von Beweisen, basierend auf dem Beweisassistenten Isabelle. Durch die Onlinezugänglichkeit muss Isabelle nicht mehr auf dem eigenen Rechner installiert werden. Isabelle verwendet eine Art Programmiersprache, um Beweise als Abfolge von logischen Schritten aufzuschreiben. Dadurch bekommen Studierende das Gefühl, Beweise gewissermaßen zu „programmieren“, wodurch gerade Informatikstudierende einen besseren Zugang zu Beweisen erhalten können.

Das Konzept hinter ProofBuddy ist, dass Studierende lernen mit einer eingeschränkten Syntax von Isabelle – und anfänglich auch ohne die in Standard-Isabelle verfügbaren vollautomatischen Beweistaktiken – Beweise zu entwickeln und so ihre Beweiskompetenz stärken können. Der kleinere Umfang der Syntax hat den Vorteil, dass Studierende nicht mit der kompletten Mächtigkeit des Beweisassistenten konfrontiert sind. Die erstellten Beweise werden an einen Server geschickt und können dort auf ihre Korrektheit geprüft werden.

Durch die Benutzeroberfläche sollen Studierende in ihrem Lernprozess unterstützt werden. Weitere Hilfestellungen sollen die Lernenden durch verbessertes Feedback erhalten. Auf der einen Seite können – wie bei herkömmlichen Programmiersprachen – die Beweise auf Syntaxfehler untersucht werden und somit auf die Beweisversuche angepasste Hinweise gegeben werden. Auf der anderen Seite gibt ProofBuddy die Möglichkeit, das von Isabelle verfügbare Feedback auf Beweise zu verbessern.

Das Studienreformprojekt ProveIT fokussiert sich auf die Weiterentwicklung der Weboberfläche ProofBuddy. Hier stehen Benutzerfreundlichkeit, Skalierbarkeit und Sicherheit im Vordergrund. Innerhalb des Projekts soll analysiert werden, welches Feedback Lernende benötigen und dieses in ProofBuddy integriert werden. Auch ein Datenmanagement muss entwickelt werden, das
Sicherheit und Privatheit von Studierendendaten sicherstellt.

Projektteam

PersonenAufgabe
Nadine KarstenProjektleitung
Matthias VogtFrontend
Kim Jana EikenPrototyp (Bachelorarbeit) & Front- und Backend
Robin CoganFront- und Backend
Maxilian ThornBackend
Nico Joseph BurkholderBackend
Joshua KobschätzkiServer Admin und Backend
Benjamin LohmarServer Admin und Backend
Lara WittigBeobachtungsstudie
Nils TötzkeBeobachtungsstudie