| Publication type: |
Article in Proceedings |
| Author: |
David Aspinall, Christoph Lüth, Daniel Winterstein |
| Title: |
A Framework for Interactive Proof |
| Book / Collection title: |
Mathematical Knowledge Management MKM 2007 |
| Volume: |
4573 |
| Page(s): |
161 – 175 |
| Series: |
Lecture Notes in Artificial Intelligence |
| Year published: |
2007 |
| Publisher: |
Springer |
| Abstract: |
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.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/mkm07.pdf |
| Status: |
Reviewed |
| Last updated: |
03. 09. 2008 |
