ISSN:
0949-2925
Keywords:
Schlüsselwörter: Automatisches Beweisen, mathematische Assistenzsysteme, Beweisentwicklungsumgebung, Beweisplanung, Analogie, Beweispräsentation
;
Key words: Automated theorem proving, mathematical assistance systems, proof development environment, proof planning, analogy, proof presentation
;
CR Classification:I.2.3
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Description / Table of Contents:
Abstract. The proof development environment $\Omega$ -Mkrpis intended to lend automated assistance to mathematicians in one of their main activities – the proving of mathematical theorems – in such a way that the system is a help, not a hindrance. Among the requisites for such a system are: an expressive object language; a way to speak abstractly about proof plans; a human-oriented presentation of constructed proofs; extensive assistance in filling proof gaps. The $\Omega$ -Mkrpsystem presented in the following is an attempt to meet these requirements by fusing the paradigms of fully automated, interactive, and plan-based theorem proving into a single framework. This article gives a survey of our work with this system.
Notes:
Zusammenfassung. Die Beweisentwicklungsumgebung $\Omega$ -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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/s004500050036
Permalink
