Organize your proofs!  Home  Features  Download  Documentation  About  News  Screenshots  Development  Publications  Related

Papers about Proof General

Ideas for the future of Proof General

• David Aspinall and Christoph Lüth Beyond Script Management. Talk given at CIAO 2007. Slides in [pdf] (420k).
• David Aspinall. Eclipse Proof General. An Eclipse version of Proof General. Brief outline of plan available as [pdf] (128k).
• David Aspinall. Protocols for Interactive e-Proof. Unpublished draft. Available on request.
• David Aspinall. Proof General Kit (white paper). Unpublished draft. Available on request.
• See also the Proof General Kit web page.

Proof General Kit and PGIP

• David Aspinall, Christoph Lüth and Daniel Winterstein. A Framework for Interactive Proof. Appears in Towards Mechanized Mathematical Assistants, Springer LNAI 4573, pp.161--175, 2007. Download as pdf (315k).
• David Aspinall, Christoph Lüth and Burkhart Wolff.
  Assisted Proof Document Authoring.
  Appears in Mathematical Knowledge Management 2005 (MKM '05), Springer LNAI 3863, p. 65--80, 2005.
  Download as pdf (307k).
• David Aspinall and Christoph Lüth.
  Proof General meets IsaWin --- combining text-based and graphical user interfaces.
  Long version of paper presented at UITP '03. Appears in ENTCS,
  Download as pdf (344k).
• Daniel Winterstein, David Aspinall, and Christoph Lüth.
  Proof General Eclipse: A Generic Interface for Interactive Proof. Draft paper.
  Download as pdf (389k).

An Overview of Emacs Proof General

• David Aspinall. Proof General: A Generic Tool for Proof Development. Tools and Algorithms for the Construction and Analysis of Systems, Proc TACAS 2000, LNCS 1785.
  Here are some slides used for this talk and some other presentations of Proof General.

Related work and older documentation

• Yves Bertot and Laurent Théry. A generic approach to building user interfaces for theorem provers. Journal of Symbolic Computation, 25(7), pp. 161-194, February 1998.
  This paper describes Script Management, also supported by Proof General.

• Yves Bertot, Thomas Kleymann-Schreiber and Dilip Sequeira. Implementing Proof by Pointing without a Structure Editor. LFCS Technical Report ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA Sophia Antipolis RR-3286
  This paper describes PG's implementation of Proof by Pointing.