Die Beweisentwicklungsumgebung Omega-MKRP

Xiaorong HuangXiaorong Huang, Manfred KerberManfred Kerber, Michael KohlhaseMichael Kohlhase, Erica MelisErica Melis, Dan NesmithDan Nesmith, Jörn RichtsJörn Richts, Jörg SiekmannJörg Siekmann

Xiaorong Huang, Manfred Kerber, Michael Kohlhase, Erica Melis, Dan Nesmith, Jörn Richts, Jörg Siekmann
Die Beweisentwicklungsumgebung Omega-MKRP
Informatik – Forschung und Entwicklung, 11(1):20-26, 1996

Details
Bibtex

KurzfassungAbstract
The main goal of the proof development environment Omega-MKRP is to support mathematicians in one of their main activities, namely proving mathematical theorems. This support must be so comfortable that formal proofs can be generated without undue difficulties and the correctness of the generated proofs is ensured. Such a system will only succeed if the computer supported generation of proofs is less time consuming than manual generation. In order to achieve this, there are different requirements to be fulfilled, which we describe in this paper. In particular, we discuss the expressive power of the object language, the possibility to communicate abstract proof plans, the automated support in filling proof gaps, and the human-oriented presentation of proofs generated. Omega-MKRP is a synthesis of the approaches of fully automated, interactive, and plan-based theorem proving. This article gives a survey of various aspects of the system.
Bemerkung: Note: In German
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@article{ HuangKerber+-FuE-96,
  author = {Xiaorong {Huang} and Manfred {Kerber} and Michael {Kohlhase} and Erica {Melis} and Dan {Nesmith} and J{\"o}rn {Richts} and J{\"o}rg {Siekmann}},
  journal = {Informatik -- Forschung und Entwicklung},
  note = {In German},
  number = {1},
  pages = {20--26},
  title = {Die {B}eweisentwicklungsumgebung {Omega-MKRP}},
  volume = {11},
  year = {1996},
}