| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
David Aspinall, Christoph Lüth, Daniel Winterstein |
| Titel: |
A Framework for Interactive Proof |
| Buch / Sammlungs-Titel: |
Mathematical Knowledge Management MKM 2007 |
| Band: |
4573 |
| Seite(n): |
161 – 175 |
| Serie / Reihe: |
Lecture Notes in Artificial Intelligence |
| Erscheinungsjahr: |
2007 |
| Verleger: |
Springer |
| Abstract / Kurzbeschreibung: |
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 |
| Letzte Aktualisierung: |
03. 09. 2008 |
