Published in

Springer Verlag, Lecture Notes in Computer Science, p. 256-271

DOI: 10.1007/978-3-319-24246-0_16

Links

Tools

Export citation

Search in Google Scholar

Proofs and Reconstructions

Proceedings article published in 2015 by Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson
This paper is available in a repository.
This paper is available in a repository.

Full text: Download

Green circle
Preprint: archiving allowed
Green circle
Postprint: archiving allowed
Red circle
Published version: archiving forbidden
Data provided by SHERPA/RoMEO

Abstract

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.