Proof Presentation Based on Proof Plans
Erica Melis⋆ · 1998
The paper addresses two problems of comprehensible proof presentation, the hierarchically structured presentation at the level of proof methods and different presentation styles of construction proofs. It provides solutions for these problems that can make use of proof plans generated by an automated proof planner. 1 Introduction The traditional automated theorem provers' output is at best a presentation of steps representing logic calculus rules. 1 Therefore, this output is hardly readable for an untrained user, let alone understandable as a mathematical proof, even for mathematicians. For instance, the proof of the theorem Theorem: Let K be an ordered field. If a 2 K, then 1 ! a implies 0 ! a \\Gamma1 ! 1 (and vice-versa). is Let 1 ! a. According to lemma 1.10 we then have a \\Gamma1 ? 0. Therefore a \\Gamma1 = 1a \\Gamma1 ! aa \\Gamma1 = 1, [10] whereas its proof as provided by the automated theorem prover OTTER [11] is the following 1 [] x=x. 2 [] -(x!y)--- -(0!z)---x*z!...