@InProceedings{pds,
year={2006},
author={Autexier, Serge 
    and Christoph Benzm{\"u}ller 
    and Dietrich, Dominik 
    and Meier, Andreas 
    and Claus-Peter Wirth},
title={A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity},
booktitle ={Mathematical Knowledge Management: 4th International Conference, {MKM 2005, Bremen, Germany, July 15-17, 2005}, Revised Selected Papers},
editor={Michael Kohlhase},
series={Lecture Notes in Artificial Intelligence},
number={3863},
pages={126--142},
publisher={Springer},
note={{\url{http://www.ags.uni-sb.de/~cp/p/pds}}},
abstract={A practically useful mathematics assistance 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 low-level 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.},
}