Parsing, editing, proving: The PGIP display protocol

David Aspinall; Christoph Lüth; Daniel Winterstein

Parsing, editing, proving: The PGIP display protocol

David Aspinall, Christoph Lüth, Daniel Winterstein

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 language	English
Title of host publication	International Workshop on User Interfaces for Theorem Provers
Volume	2005
Publication status	Published - 2005

Access to Document

pgipdispSubmitted manuscript, 236 KB

Cite this

@inproceedings{a428066dab7d4c64b7179127fcbcd2d0,

title = "Parsing, editing, proving: The PGIP display protocol",

abstract = "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.",

author = "David Aspinall and Christoph L{\"u}th and Daniel Winterstein",

year = "2005",

language = "English",

volume = "2005",

booktitle = "International Workshop on User Interfaces for Theorem Provers",

}

TY - GEN

T1 - Parsing, editing, proving: The PGIP display protocol

AU - Aspinall, David

AU - Lüth, Christoph

AU - Winterstein, Daniel

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

M3 - Conference contribution

VL - 2005

BT - International Workshop on User Interfaces for Theorem Provers

ER -

Parsing, editing, proving: The PGIP display protocol

Abstract

Access to Document

Fingerprint

Cite this