TWiki> PG Web>ProofGeneralKit>PGKitDevelopment>PGKitProjectIdeas>PlatoAndProofGeneral (revision 1)~~Edit~~~~Attach~~

I had some discussions in Edinburgh in August 2006 about the possibility of connecting Proof General with the PLATO component of the new version of the OMEGA system.

PLATO was developed by Marc Wagner and Serge Autexier.

From PG's point of view, this connection might give Proof General an appealing document-centred interface using TeXmacs. There might also be the chance to interpret the richer architecture based on OMDoc (or some version of it?) in our setting.

From PLATO/Omega's point of view, there may be the chance to connect to Isabelle and similar theorem provers.

At the moment the architecture of the two systems overlaps somewhat. The ProofGeneralBroker is intended to manage interactive proofs-in-progress in a similar way to the PLATO system itself, although it does not yet implement development graphs.

One difference is that Proof General is designed as a framework
for interpreting different many proof languages in a uniform way, and providing
facilities for manipulating *native proof scripts* based on this. By contrast,
I think that the Omega architecture would instead fix its notion of proof
language and then map that down to (possibly) different provers.

-- DavidAspinall - 05 Sep 2006

- Maybe start by looking at a log of PGIP interaction between Broker and Display?
- Perhaps some use-cases for particular interactions

Topic revision: r1 - 05 Sep 2006 - 18:11:33 - DavidAspinall

Copyright © 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

Ideas, requests, problems regarding TWiki? Send feedback

This Wiki uses Cookies