Christoph Lüth, David Aspinall:
PGIP as a prover-independent proof language
The Proof General Kit is a software framework for conducting
interactive proof. It defines a component infrastructure, the syntax
of messages exchanged between components, and the protocol governing
message exchanges dubbed Proof General Interaction Protocol. The
infrastructure connects provers to one or more display components for
interacting with the user, via a broker middleware component.
In this setting, the central broker handles an abstract representation
of the proof script, by breaking up the concrete proof script into
constituting parts each of which correcponds to a transitition in the
abstract state model of the prover, which underlies PGIP. In other
words, we can view the proof script as a prover-independent proof
language and consider script and dependency management on this
abstract level.
Last modified: Mon Sep 26 12:51:19 CEST 2005