Sascha Böhme and Tjark Weber. In Pascal Fontaine and Aaron Stump, editors, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pages 27-32, August 2011.
Automatic provers that can produce proof certificates do not need to be trusted. The certificate can be checked by an independent tool, for example an LCF-style proof assistant such as Isabelle/HOL or HOL4. Currently, the design of proof formats is mostly dictated by internal constraints of automatic provers and less guided by applications such as checking of certificates. In the worst case, checking can be as involved as the actual proof search simply because important information is missing in the proof certificate. To address this and other issues, we describe design choices for proof formats that we consider both feasible for implementors of automatic provers as well as effective to simplify checking of certificates.
@inproceedings{boehme11designing,
author = {Sascha B{\"o}hme and Tjark Weber},
title = {Designing Proof Formats: A User's Perspective},
editor = {Pascal Fontaine and Aaron Stump},
booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving},
pages = {27--32},
month = aug,
year = {2011}
}