Abstract
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.
partially supported by the RISC PhD scholarship program of the government of Upper Austria and by the FWF (Austrian Science Foundation) SFB project P1302
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
B. Buchberger. Focus Windows Presentation: A New Approach to Presenting Mathematical Proofs (in Automated Theorem Proving Systems). Theorema Technical Report, 2000-01-30, RISC, http://www.risc.uni-linz.ac.at/people/buchberg/downloads.html
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.
The HOL System. Developed at the University of Cambridge, directed by R. Milner. http://www.cl.cam.ac.uk/Research/HVG/HOL/.
Mizar System. Developed at the University of Warsaw, directed by A. Trybulec. http://mizar.uwb.edu.pl/system/.
Omega System. Developed at the University of Saarbrücken, directed by J. Siekmann. http://www.ags.uni-sb.de/ omega/intro.html.
D. Vasaru-Dupré, Automated Theorem Proving by Integrating Proving, Solving and Computing. RISC Institute, May 2000, RISC report 00-19. PhD Thesis.
F. Wiedijk, The Fourteen Provers of the World. 2001, http://www.cs.kun.nl/freek/notes/index.html
W. Windsteiger, A Set Theory Prover in Theorema: Implementation and Practical Applications, RISC Institute, May 2001, RISC report 01-03. PhD Thesis.
S. Wolfram. The Mathematica Book, Wolfram Media and Cambridge University Press, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Piroi, F., Buchberger, B. (2002). Focus Windows: A New Technique for Proof Presentation. In: Calmet, J., Benhamou, B., Caprotti, O., Henocque, L., Sorge, V. (eds) Artificial Intelligence, Automated Reasoning, and Symbolic Computation. AISC Calculemus 2002 2002. Lecture Notes in Computer Science(), vol 2385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45470-5_30
Download citation
DOI: https://doi.org/10.1007/3-540-45470-5_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43865-6
Online ISBN: 978-3-540-45470-0
eBook Packages: Springer Book Archive