Publication
A Framework for Interactive Proof
David Aspinall; Christoph Lüth; Daniel Winterstein
In: 6th International Conference on Mathematical Knowledge Management (MKM 2007). International Conference on Mathematical Knowledge Management (MKM-2007), June 27-30, Hagenberg, Australia, Pages 161-175, Lecture Notes in Artificial Intelligence (LNAI), Vol. 4573, Springer, 2007.
Abstract
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.