Connecting PLATO and Proof General

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

First steps

  • Maybe start by looking at a log of PGIP interaction between Broker and Display?
  • Perhaps some use-cases for particular interactions
Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 05 Sep 2006 - 18:11:33 - 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