       |
OMEGA: Ein mathematisches Assistenzsystem |
In dem Projekt OMEGA wird ein Deduktionssystem für die mathematische
Forschung und Lehre entwickelt, das als mathematisches Assistenzsystem
den Benutzer bei den vielen Aufgaben unterstützt, die beim Beweisen
mathematischer Sätze anfallen. Das System besteht aus einem
Beweisplaner und einer Reihe anderer Problemlösekomponenten,
insbesondere verschiedenen traditionellen automatischen Beweisern, wie
OTTER und SPASS, einem System für Beweise durch vollständige Induktion
(INKA), einem Constraintlöser und mehreren integrierten
Computeralgebrasytemen. Diese Komponenten können abhängig von der
jeweiligen Situation automatisch oder interaktiv eingesetzt werden.
Weitere Komponenten helfen dem Benutzer bei der Problemformulierung
und der abschiessenden Präsentation der Beweise in natürlicher
Sprache. Diese Konzeption des OMEGA-Systems ist stark
kognitionswissenschaftlich motiviert im Gegensatz zum eher
technologiedominierten automatischen Beweisen traditioneller Prägung.Das System kann sowohl in Gebieten der mathematischen Forschung eingesetzt werden, als auch in der Mathematikausbildung. Für die Mathematikforschung ist es interessant, ähnlich wie in Computeralgebrasytemen, über verschiedene spezialisierte Tools zu verfügen und in der Zusammenarbeit mit einem Mathematiker einen Beweis zu finden und auf seine Korrektheit zu überprüfen. Für die Mathematikausbildung ist es eher wichtig, das im jeweiligen Gebiet der Mathematik implizit vorhandene Methoden- und Vorgehenswissen explizit zu machen und dem Benutzer zur Verfügung zu stellen, zu strukturieren und zu erklären. Diese Anforderungen werden einerseits durch die verteilten mathematischen ``Services'' in OMEGA erfüllt und andererseits durch ein hierarchisches wissensbasiertes Beweisplanen.
Unsere derzeitigen Forschungsfragen sind der ressourcenabhängige
Einsatz verschiedener Problemlösestrategien, das Erarbeiten von
Vorschlägen für den Benutzer, die effiziente Verwaltung und Nutzung
eines grossen Fundus mathematischen Wissens, der in der Wissensbank,
MBase, abgelegt wird und die Beschäftigung mit einer kognitiv
adäquaten Präsentation der Beweise und Beweisversuche.
|