Fakultät für Mathematik, Informatik und Physik

Dr. Harald Zankl

Beweise in der Gleichungslogik

(Beginn 1.6.2011 Projektende 30.11.2011)

Abschlussbericht
 

Projektziel

In einem Vorgängerprojekt wurde ein Programm entwickelt, welches die Knuth-Bendix Vervollständigung durchführt. Sofern die Vervollständigung erfolgreich ist, kann dieses Verfahren benutzt werden um die Äquivalenz von zwei Termen zu zeigen. Den Äquivalenzbeweis selbst liefert dieses Verfahren allerdings in einer speziellen Form. Ziel des Projektes ist es, dieses Programm insofern zu erweitern, dass es den Äquivalenzbeweis in einer anderen (einfacheren) Form wiedergibt. Dadurch wird der Einsatzbereich der Software wesentlich erhöht, da die schwierigen Schritte im Hintergrund durchgeführt werden.
 

Mehrwert

Aufgrund der Unentscheidbarkeit des Wortroblems gibt es keinen Algorithmus, das heißt, kein Kochrezept, wie solche Äquivalenzbeweise erstellt werden können. Zudem werden sogar einfach erscheinende Äquivalenzbeweise recht groß und unübersichtlich. Somit sind derartige Beweise bei Studierenden nicht sonderlich beliebt und werden demnach nur wenig eingeübt. Die vorgeschlagenen Erweiterungen in dem bestehenden Programm ermöglichen den Studierenden einen spielerischen Umgang mit diesen Beweisen und erleichtern somit das Verständnis von solchen Beweisen. Ein zweiter wichtiger Aspekt der vorgeschlagenen Erweiterung ist die automatische Erstellung von Klausuraufgaben sowie Musterlösungen.
 

Verfügbarkeit

Das Programm ist samt Dokumentation unter folgendem Link verfügbar:

http://cl-informatik.uibk.ac.at/software/kbcv

Dort steht auch eine benutzerfreundliche Applet-Version bereit, die eine leicht eingeschränkte Funktionalität bietet. Die erstellte Software ist unter der GNU Lesser General Public License1 frei verfügbar. Dies wurde durch einen entsprechenden Antrag beim ProjektServiceBüro der Universität Innsbruck bewerkstelligt.

 
 

zurück zu E-Learning Projekte 11