A Framework for Interactive Proof

This paper introduces Proof General Kit, a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called PGIP. The main channel connects provers to displays. Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a broker>/i> middleware component which manages proof-in-progress and mediates between components.
David Aspinall, Christoph Lüth and Daniel Winterstein.
A Framework for Interactive Proof
Towards Mechanized Mathematical Assistants, Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger (eds).
Springer LNAI 4573, p. 161--175, 2007.
Download as pdf.

Click here to return to my papers page.

my Vcard
David R. Aspinall, email david.aspinall@ed.ac.uk.
Contact GPG key (Instant HOWTO)