Die Beweisentwicklungsumgebung
W\Omega
-Mkrp |
| |
| Authors: | Xiaorong Huang Manfred Kerber Michael Kohlhase Erica Melis Dan Nesmith J?rn Richts und J?rg Siekmann |
| |
| Institution: | (1) Fachbereich Informatik, Universit?t des Saarlandes, D-66041 Saarbrücken ({ huang|kerber|kohlhase|melis| nesmith|richts}@cs.uni-sb.de siekmann@dfki.uni-sb.de) , DE |
| |
| Abstract: | Zusammenfassung.
Die Beweisentwicklungsumgebung -Mkrpsoll
Mathematiker bei einer ihrer
Hauptt?tigkeiten, n?mlich dem Beweisen mathematischer Theoreme
unterstützen. Diese Unterstützung mu? so komfortabel sein,
da? die
rechnergestützte Suche nach formalen Beweisen leichter und insbesondere
weniger aufwendig ist, als ohne das System. Dazu mu? die verwendete
Objektsprache ausdrucksstark sein, man mu? die M?glichkeit haben, abstrakt
über Beweispl?ne zu reden, die gefundenen Beweise müssen in einer am
Menschen orientierte Form pr?sentiert werden und vor allem mu? eine
effiziente Unterstützung beim Füllen von Beweislücken zur Verfügung
stehen. Das im folgenden vorgestellte $\Omega$-Mkrp-System ist
der Versuch einer
Synthese der Ans?tze des vollautomatischen, des interaktiven und des
planbasierten Beweisens. Dieser Artikel soll eine übersicht über unsere
Arbeit an diesem System geben.
Eingegangen am 24. Juni 1994 / Angenommen am 3. November 1995 |
| |
| Keywords: | Schlüsselw?rter: Automatisches Beweisen mathematische Assistenzsysteme Beweisentwicklungsumgebung Beweisplanung Analogie Beweispr?sentation |
| 本文献已被 SpringerLink 等数据库收录！ |
|
