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.