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.

Topic revision: r2 - 05 Sep 2006 - 17:39:40 - 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