Fakultät für Mathematik, Informatik und PhysikDr. Harald ZanklBeweise in der Gleichungslogik(Beginn 1.6.2011 Projektende 30.11.2011) 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. |
2011.229.html - 2011.229.html