TWiki> PG Web>PGIP (revision 7)EditAttach

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.

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

The syntax of the protocol is defined with a RELAX NG schema in compact notation, available at:

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.

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.

We regard this protocol as under development. We hope to keep it as small and lightweight as possible, so that implementors are not overly fearful of its size. With this concern in mind, we are open to suggestions for extensions or improvements to the protocol. Please see PGIPDevelNotes for current development notes.

ALERT! According to, 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.

Edit | Attach | Print version | History: r11 | r9 < r8 < r7 < r6 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r7 - 05 Sep 2006 - 09:13:32 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies