Focus Windows: A New Technique for Proof Presentation

  • Florina Piroi
  • Bruno Buchberger
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2385)


Whether they are hand written or generated by an automated prover, long proofs may be difficult to understand and follow. The main reason for this is that at some point in the proof formulae that occur lines, paragraphs or even pages before, are used. The proof presentation method proposed here tries to overcome this by showing, in each proof step, exactly the formulae that are relevant for the particular proof step. We describe the implementation of this method in the frame of the Theorema system.


Symbolic Computation Goal Area Automate Theorem Proof Tree Automate Theorem Prove 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    B. Buchberger. Focus Windows Presentation: A New Approach to Presenting Mathematical Proofs (in Automated Theorem Proving Systems). Theorema Technical Report, 2000-01-30, RISC,
  2. 2.
    B. Buchberger, C. Dupré, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6–7, 2000, St. Andrews, Scotland, M. Kerber and M. Kohlhase eds.), A.K. Peters, Natick, Massachusetts, pp. 98–113. ISBN 1-56881-145-4.Google Scholar
  3. 3.
    The HOL System. Developed at the University of Cambridge, directed by R. Milner.
  4. 4.
    Mizar System. Developed at the University of Warsaw, directed by A. Trybulec.
  5. 5.
    Omega System. Developed at the University of Saarbrücken, directed by J. Siekmann. omega/intro.html.
  6. 6.
    D. Vasaru-Dupré, Automated Theorem Proving by Integrating Proving, Solving and Computing. RISC Institute, May 2000, RISC report 00-19. PhD Thesis.Google Scholar
  7. 7.
    F. Wiedijk, The Fourteen Provers of the World. 2001,
  8. 8.
    W. Windsteiger, A Set Theory Prover in Theorema: Implementation and Practical Applications, RISC Institute, May 2001, RISC report 01-03. PhD Thesis.Google Scholar
  9. 9.
    S. Wolfram. The Mathematica Book, Wolfram Media and Cambridge University Press, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Florina Piroi
    • 1
  • Bruno Buchberger
    • 1
  1. 1.Research Institute For Symbolic ComputationHagenbergAustria

Personalised recommendations