Focus windows A new technique for proof presentation.pdf

Focus Windows: A New Technique for Proof Presentation F. Piroi, B. Buchberger RISC-Linz Research Institute for Symbolic Computation A-4232 Hagenberg, Austria {Florina.Piroi, Bruno.Buchberger}@risc.uni-linz.ac.at 1 Introduction The idea of focus windows as a technique for proof presentation was introduced in [Buchberger 2000]. The present paper describes the implementation of the technique in the frame of the Theorema system [Buchberger et al. 2000]. The implementation was done by the first author under the guidance of the second author. Proofs in mathematical publications are linear texts. In each proof step, a new formula is derived from formulae appearing in earlier portions of the text using an inference rule. Typically, in long proofs, the formulae used in a proof steps occur a couple of lines, paragraphs, or even pages distant from the place in the text at which the proof step occurs. Reference to these formulae is usually done by labels and the reader has to jump back and forth between the formulae referenced and the proof step in which they are needed. This is unpleasant and makes understanding of proofs quite difficult even if the proofs are nicely structured and well presented. Most automated theorem provers do not put emphasis on producing proofs that are easy to read and understand. (A very telling illustration of this is provided by the collection of proofs produced for the irrationality of r 2 by 15 different current prover in [Weijdeck 2001].) However, even those that provide tools for studying proofs have the problem described above. This is even true for natural deduction provers as, for example, the Omega system [Omega], that display the entire proof tree in tree form and not in linearized presentation: Still, when studying one particular proof step, one may have to jump to various formulae in the tree for being able to check