David Aspinall
Daniel Winterstein
ABSTRACT
Interactive theorem proving is the art of constructing electronic proofs. Proof development, based around a proof script, has much in common with program development, based around a program text. Proof developers use rather primitive tools for developing and manipulating proof scripts at present. The Proof General project aims at to change this, by providing powerful generic tools and interfaces. The flagship tool is our Eclipse plugin, which brings the features of a industrial-strength IDE to theorem proving for the first time. In this paper we give an overview of the Eclipse plugin and its underlying architecture.
- D. Aspinall and C. Lüth. Commentary on PGIP. http://proofgeneral.inf.ed.ac.uk/kit/, 2006.Google Scholar
- D. Aspinall, C. Lüth, and D. Winterstein. Parsing, editing, proving: The PGIP display protocol. In User Interfaces for Theorem Provers UITP'05, Apr. 2005.Google Scholar
- D. Aspinall, C. Lüth, and B. Wolff. Assisted proof document authoring. In Proc. Intl. conf. Mathematical Knowledge Management 2005, LNAI 3863. Springer, 2005. Google ScholarDigital Library
- B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, and S. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge, 2005.Google Scholar
- Y. Bertot and L. Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7):161--194, Feb. 1998. Google ScholarDigital Library
- G. Gonthier. A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge, 2004. http://research. microsoft.com/~gonthier/4colproof.pdf.Google Scholar
- T. C. Hales. The Flyspeck project page. http://www.math.pitt.edu/~thales/flyspeck/index.html.Google Scholar
- R. Kaivola and K. R. Kohatsu. Proof engineering in the large: formal verification of Pentium 4 floating-point divider. STTT, 4(3):323--334, 2003.Google ScholarCross Ref
- M. Kohlhase. OMDoc: An Open Markup Format for Mathematical Documents. LNAI 4180. Springer, 2006. Google ScholarDigital Library
- TeXmacs. Web page, 2006. http://www.texmacs.org/.Google Scholar
- D. von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13(13):1173--1214, 2001.Google ScholarCross Ref
- Mathematical markup language (MathML). W3C Recommendation, 1999.Google Scholar
- M. Wenzel. Isabelle/Isar --- a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München, 2001.Google Scholar
Index Terms
- Proof general in Eclipse: system and architecture overview
Comments