The Certification Problem Format
Logic in Computer Science
2014-10-31 v1
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.
Cite
@article{arxiv.1410.8220,
title = {The Certification Problem Format},
author = {Christian Sternagel and René Thiemann},
journal= {arXiv preprint arXiv:1410.8220},
year = {2014}
}
Comments
In Proceedings UITP 2014, arXiv:1410.7850