Proof General Kit
A framework for interactive proof. This paper introduces Proof General Kit, a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called PGIP. The main channel connects provers to displays. Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a broker middleware component which manages proof-in-progress and mediates between components.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Gast, Holger: Engineering the prover interface (2012)
- Meikle, Laura I.; Fleuriot, Jacques D.: Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover’s palette (2012)
- Wenzel, Makarius: Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit (2012)
- Aspinall, David; Autexier, Serge; Lüth, Christoph; Wagner, Marc: Towards merging Plat$\Omega$ and PGIP (2009)
- Aspinall, David; Lüth, Christoph; Winterstein, Daniel: A framework for interactive proof (2007)
- Narboux, Julien: A graphical user interface for formal proofs in geometry (2007)
- Aspinall, David; Lüth, Christoph; Wolff, Burkhart: Assisted proof document authoring (2006)
- Melis, Erica; Meier, Andreas; Pollet, Martin: Adaptive access to a proof planner (2004)