*Wissenschaftliches Programm*   *Liste der Vortragenden*

Sektion Plenum
Dienstag, 19.09.2000, 9.00 Uhr, Großer Mathematik-Hörsaal, Trefftz-Bau

Computer-unterstütztes mathematisches Beweisen: Theorie oder Praxis?

Bruno Buchberger, Johannes-Kepler-Universität Linz

Auf dem Gebiet des automatischen Beweisens mathematischer Sätze wurden in den letzten Jahrzehnten große Fortschritte erzielt. Es wurden aber hauptsächlich Nebeneffekte dieser Forschung genutzt. Zum Beispiel ist das gesamte Gebiet des logischen Programmierens (PROLOG) ein Spezialresultat des Resolutionsverfahrens von A. Robinson für das automatische Beweisen. Ein anderes Gebiet, in welchem automatisierte Beweisverfahren mit großem Erfolg eingesetzt wurden, ist die Verifikation von Hardware. Überraschenderweise werden aber Systeme zum automatischen Beweisen noch kaum von Mathematikern für die Erleichterung ihrer täglichen Beweisarbeit oder für die Unterstützung der mathematischen Ausbildung eingesetzt.

Im Vortrag analysieren wir, warum dies so ist und nach welchen Kriterien zukünftige Software-Systeme zum automatischen Beweisen aufgebaut sein sollten, damit sie für die Praxis der mathematischen Arbeit nützlich sein können. Es wird auch das System Theorema vorgestellt, das unter der Leitung des Vortragenden am Institut RISC entworfen und entwickelt wird. In diesem System wird versucht, die vorgeschlagenen Kriterien weitgehend zu erfüllen. Details zu Theorema finden sich unter  http://www.theorema.org.

Eine Übersicht über Theorema gibt die Arbeit

B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. Proc. of the Calculemus 2000 Conference, St. Andrews, UK, August 2000, 8 Seiten.

Danksagung: Das Theorema-Projekt wird vom Österreichischen Fonds zur Förderung der wissenschaftlichen Forschung (Projekt SFB 1302) und vom Land Oberösterreich (Projekt “Prove”) unterstützt.