PGIP, the Proof General Interaction Protocol
PGIP is a protocol for conducting interactive proof and a framework for connecting
theorem provers to interfaces and other components. It is being used for
the next generation of Proof General interfaces in the
Proof General Kit project.
Structure of PGIP
The protocol is based on XML messages which are passed in an RPC-like exchange between different software components. The protocol has several subsets
- Prover protocol, for connecting the theorem prover
See AddingPGIPSupportHowTo for hints about adding PGIP support to a new theorem prover.
- Display protocol, for connecting the interfaces
See PGIPDisplaysHowTo for hints on implementing a PGIP-enabled interface component.
- Configuration messages, for describing available components
- PGML, a simple markup language used for annotating concrete syntax
Specification of PGIP
The
syntax of the protocol is defined with a RELAX NG schema in compact notation,
available at:
http://proofgeneral.inf.ed.ac.uk/Kit/dtd/pgip.rnc
or (for the latest version) in the
ProofGeneralCVSRepository at
Kit/dtd/pgip.rnc
.
The
meaning of messages
exchanged and the protcol itself is elaborated in the
PGIPCommentary.
Implementations of PGIP
Please see
ProofGeneralKit for the wiki page with details of our implementation of the
PGIP protcol
and links to some of the available software which uses it.
The protocol is designed to use a fixed middleware component (the
ProofGeneralBroker
of Proof General Kit), together with
provers and interfaces which each need to support only their own part of the protocol.
Development of PGIP
We regard this protocol as under development. We hope to keep it as small, simple and lightweight as possible,
while supporting the features that we need. With this concern in mind, we are open
to suggestions for extensions or improvements to the protocol.
Please see
PGIPDevelNotes for current development notes.

According to
http://acronymfinder.com,
Acronym:PGIP stands for
Proof General Interface Protocol. This was our interpretation
of the protocol in early versions. Now it has been extended to allow more
programmatic usage, we prefer
Proof General Interaction Protocol.