[Omega]-MKRP : A Proof Development Environment

Abstract

This report presents the main ideas underlying the Ω-MKRP-system, an environment for the development of mathematical proofs. The motivation for the development of this system comes from our extensive experience with traditional first-order theorem provers and aims to overcome some of their shortcomings. After comparing the benefits and drawbacks of existing systems, we propose a system architecture that combines the positive features of different types of theorem-proving systems, most notably the advantages of human-oriented systems based on methods (our version of tactics) and the deductive strength of traditional automated theorem provers. In Ω -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 in order to prove it. He can also insert a mathematical fact from an integrated database into the current partial proof, he can apply a domain-specific problem-solving method, or he can call an integrated automated theorem prover to solve a subproblem. The user can also pass the control to a planning component that supports and partially automates his long-range planning of a proof. Toward the important goal of user-friendliness, machine-generated proofs are transformed in several steps into much shorter, better-structured proofs that are finally translated into natural language.