Springer Verlag, Lecture Notes in Computer Science, p. 256-271
DOI: 10.1007/978-3-319-24246-0_16
Full text: Download
Implementing proof reconstruction is difficult because it involves symbolic manipulations of formal objects whose representation varies between different systems. It requires significant knowledge of the source and target systems. One cannot simply re-target to another logic. We present a modular proof reconstruction system with separate components, specifying their behaviour and describing how they interact. This system is demonstrated and evaluated through an implementation to reconstruct proofs generated by Leo-II and Satallax in Isabelle HOL, and is shown to work better than the current method of rediscovering proofs using a select set of provers.