Proof General Kit

Proof General Kit is a new component-based architecture for the Proof General project, based around a uniform protocol for communication between interactive proof tools, called PGIP.

Software

Work which is currently in progress includes:

• An Eclipse plugin for Proof General.
  See the wiki for download and installation instructions.
  New! Easy installations are now available at our update site.
• PG Kit broker, the central middleware component of the PG Kit framework.
  Binaries are available here:
  • Linux/x86
  (NB: this is not currently required by the Eclipse plugin)
• With assistance from Isabelle developers at Munich: a PGIP-enabled version of Isabelle/Isar.
  This is now integrated into the Isabelle distribution (the CVS version of Isabelle 2007 is most up-to-date).

Schemas and documentation

• Recent versions of the RELAX NG schemas for PGIP and PGML.
  • Master source, in compact syntax: Kit/dtd/pgip.rnc (43k), Kit/dtd/pgml.rnc (7k).
  • The derived DTDs: Kit/dtd/pgip.dtd (35k), Kit/dtd/pgml.dtd (3k).
  • The derived XML Schema files: Kit/dtd/pgip.xsd (66k), Kit/dtd/pgml.xsd (13k).
  • Viewable (but badly laid out) HTML files: Kit/dtd/pgip.html (246k), Kit/dtd/pgml.html (43k).
• A draft commentary on PGIP, Kit/docs/commentary.pdf (229k).
  
• Further documentation and development notes can be found on the PG wiki, especially the PGIP page.

Publications

• 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).

Other papers

• Daniel Winterstein, David Aspinall, and Christoph Lüth.
  Proof General Eclipse: A Generic Interface for Interactive Proof. Draft paper.
  Download as pdf (389k).

Planning

The ideas behind the Proof General Kit are described in these papers:

• David Aspinall. Protocols for Interactive e-Proof. Draft version, see here.
• David Aspinall. Proof General Kit (white paper). Draft version, see here.
• David Aspinall. Plans for Eclipse Proof General, an Eclipse front end for Proof General (project partly sponsored by IBM award).

Click here to go back to the front page.