The Certification Problem Format
Christian Sternagel and René ThiemannProceedings of the 11th International Workshop on User Interfaces for Theorem Provers (UITP 2014), Electronic Proceedings in Theoretical Computer Science 167, pp. 61 – 72, 2014.
Abstract
We provide an overview of CPF, the certification problem format, and explain some design decisions. Whereas CPF was originally invented to combine three different formats for termination proofs into a single one, in the meanwhile proofs for several other properties of term rewrite systems are also expressible: like confluence, complexity, and completion. As a consequence, the format is already supported by several tools and certifiers. Its acceptance is also demonstrated in international competitions: the certified tracks of both the termination and the confluence competition utilized CPF as exchange format between automated tools and trusted certifiers.
BibTeX
@inproceedings{CSRT-UITP14,
author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "The Certification Problem Format",
booktitle = "Proceedings of the 11th International Workshop on
User Interfaces for Theorem Provers",
editor = "Christoph Benzm{\"u}ller and Bruno Woltzenlogel Paleo",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = 167,
pages = "61--72",
year = 2014,
doi = "10.4204/EPTCS.167.8"
}