Beweiskompetenz durch Beweisassistenz

Abstract

Beweiskompetenz, also die Fähigkeit mathematische Beweise sowohl verstehen als auch eigenständig führen zu können, wird üblicherweise vorrangig durch Beispiele, Feedback und Diskussion zwischen Lernenden und Lehrenden erworben. Wir setzen einen interaktiven Theorembeweiser – einen sogenannten Beweisassistenten – ein, um Lernenden ein zusätzliches möglichst direktes Feedback zu ermöglichen. Das Führen von Beweisen mit solchen Assistenten ähnelt der Entwicklung von Software mit schnellem und zuweilen spielerischem Explorieren von Lösungsansätzen. Wir erarbeiten daher die Konzeption eines dedizierten Kurses im Bereich der Theoretischen Informatik, in dem Beweiskompetenz mit passenden didaktischen Ansätzen durch Beweisassistenten effizienter und auch spielerischer vermittelt wird.