Project ideas for PG Kit

PGML Viewer

A component that displays the PGML output from the prover for proofs-in-progress. Small window that can be duplicated with a click to "freeze" a particular display. Automatic split between window categories according to PGIP markup. Errors could be ignored.

PGIP Enabling Filter

Regexp-based tool for adding PGIP support to a non-PGIP enabled prover. This could use the existing regexps built into PG as a starting point.

NB: this goes against the principle of PGIP, but would give a leg-up to prover implementors and perhaps encourage native support.

A REST view on the Broker

Idea: add a web-service interface to the Broker which implements a resource-oriented view. See RESTViewForBroker for more discussion.

A connection between PG and PLATO

See PlatoAndProofGeneral for discussion.