Parsing, editing, proving: The PGIP display protocol

David Aspinall, Christoph Lüth, Daniel Winterstein

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


This paper describes how proof texts are constructed and edited in the Proof General Kit framework. Proof texts are the central object of development within our framework and we want to allow flexible ways to construct them, both explicitly via text editing and implicitly by graphical manipulation or meta-manipulation. To this end, the framework allows for user-oriented display components, connected to provers via a central broker component. The display components and the broker exchange messages in a format specified by the PGIP display protocol, which facilitates parsing, editing and proving of proof texts.
Original languageEnglish
Title of host publicationInternational Workshop on User Interfaces for Theorem Provers
Publication statusPublished - 2005


Dive into the research topics of 'Parsing, editing, proving: The PGIP display protocol'. Together they form a unique fingerprint.

Cite this