 Authors
 Serge Autexier, Christoph Benzmüller, Dominik Dietrich, Andreas
Meier, ClausPeter Wirth
 Title
 A Generic Modular Data Structure for Proof Attempts Alternating
on Ideas and Granularity
 In
 Mathematical Knowledge Management: 4th International Conference, MKM 2005,
Bremen, Germany, July 1517, 2005, Revised Selected Papers,
LNAI 3863, pp. 126142, Springer, 2006, ISBN 354031430X.
Bibtex Entry.
 Copyright Owner
 Springer
 Abstract

A practically useful mathematical assistant system requires the
sophisticated combination of interaction and automation. Central in
such a system is the proof data structure, which has to maintain the
current proof state and which has to allow the flexible interplay of
various components including the human user. We describe a
parameterized proof data structure for the management of proofs,
which includes our experience with the development of two proof
assistants. It supports and bridges the gap between
abstract level proof explanation and lowlevel proof verification.
The proof data structure enables, in particular, the flexible
handling of lemmas, the maintenance of different proof alternatives,
and the representation of different granularities of proof attempts.
 Review
 No review yet
 Full paper



 Format
 all.ps.gz
 Size
 .2 Mbytes

 Format
 .dvi
 Size
 .1 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 .pdf
 Size
 .2 Mbytes