Abstract: A Framework for Interactive Proof

A Framework for Interactive Proof

David Aspinall
LFCS, School of Informatics, The University of Edinburgh
Christoph Lüth
Deutsches Forschungszentrum für Künstliche Intelligenz, Bremen
Daniel Winterstein
LFCS, School of Informatics, The University of Edinburgh

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 middleware component which manages proof-in-progress and mediates between components.


Christoph Lüth, 21.06.07