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.
Eine vorläufige version des Fortsetzungsantrags ist verfügbar.
|