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) 4573 Springer 2007.


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.

mkm07.pdf (pdf, 316 KB )

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz