Edinburgh Research Explorer

A Framework for Interactive Proof

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Original languageEnglish
Title of host publicationTowards Mechanized Mathematical Assistants
Subtitle of host publication14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings
EditorsManuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-540-73086-6
ISBN (Print)978-3-540-73083-5
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


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.

ID: 16403539