TY - INPR
A1 - Huang, Xiaorong
A1 - Kerber, Manfred
A1 - Kohlhase, Michael
A1 - Melis, Erica
A1 - Nesmith, Dan
A1 - Richts, Jörn
A1 - Siekmann, Jörg
T1 - OMEGA MKRP - A Proof Development Environment
N2 - This report presents the main ideas underlyingtheOmegaGamma mkrp-system, an environmentfor the development of mathematical proofs. The motivation for the development ofthis system comes from our extensive experience with traditional first-order theoremprovers and aims to overcome some of their shortcomings. After comparing the benefitsand drawbacks of existing systems, we propose a system architecture that combinesthe positive features of different types of theorem-proving systems, most notably theadvantages of human-oriented systems based on methods (our version of tactics) andthe deductive strength of traditional automated theorem provers.In OmegaGamma mkrp a user first states a problem to be solved in a typed and sorted higher-order language (called POST ) and then applies natural deduction inference rules inorder to prove it. He can also insert a mathematical fact from an integrated data-base into the current partial proof, he can apply a domain-specific problem-solvingmethod, or he can call an integrated automated theorem prover to solve a subprob-lem. The user can also pass the control to a planning component that supports andpartially automates his long-range planning of a proof. Toward the important goal ofuser-friendliness, machine-generated proofs are transformed in several steps into muchshorter, better-structured proofs that are finally translated into natural language.This work was supported by the Deutsche Forschungsgemeinschaft, SFB 314 (D2, D3)
T3 - SEKI Report - 92,22
Y1 - 1999
UR - https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/340
UR - https://nbn-resolving.org/urn:nbn:de:hbz:386-kluedo-3114
ER -