The Certification Problem Format
Sternagel, Christian · Thiemann, René
Original · EN
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.
English translation
This paper has no Arabic translation yet. Be the first: it takes a few seconds, and the result is stored for every future reader.