Certification Problem Format

Introduction

Welcome to the certification problem format (CPF) website.

The CPF is an extendable format for certification problems where the current focus is on properties of first order term rewrite systems (TRSs). Its main structure consists of

The major design of CPF was done by the CeTA / IsaFoR and CiME / Coccinelle groups where additionally the comments of the Rainbow / CoLoR group where helpful. The format tries to unify and extend all three previous XML-formats that have been developed for termination proofs, namely the AProVE-format (aprove.dtd), the CiME-format (a3pat.dtd), and the Rainbow-format (problem.xsd and proof.xsd).

There also is a graphical representation of CPF. It can be used for inspecting the overall structure of CPF. However, it is not immediately updated with every new element of CPF, so the main reference is still the .xsd-file. (The linked .png-file corresponds to version 2.3 (June 21, 2015).)

The format has been developed with financial support from the Austrian Science Fund (FWF): P22767.

Viewing Certification Problems

We designed an XSLT-transformation that displays the XML-structure as a readable HTML-document. It just needs one line to tell the browser that it should do this automatically.

Certifying Proofs using CPF

There are two different workflows on how to certify proofs using CPF.

Downloads

You can browse the repository, or download all files in an archive including several examples or checkout the mercurial repository calling:

hg clone http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF
In the latter case, every new update can be received by invoking
hg pull; hg update

In the repository there is the latest version 2.3 that will be used within the 2015 termination competition. On this site the main changes are listed to older version of CPF. On that that site also a converter from version 1.0 to version 2.0 and a converter from version 2.0 to version 2.3 is available.

Developer Version

There also is a repository for developments (hg clone http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/CPF-devel) which contain changes and extensions which are under discussion and are not yet fixed. Currently there is no difference to the official repository.

Certifiers that support CPF

Automated provers that generate CPF

Completion tools

Complexity tools

Confluence tools

Termination tools

Contact

For general questions / detected bugs / proposals for extensions / ... send a mail to the mailing list cpf at informatik.uibk.ac.at. Everyone is invited to subscribe to this list.

If you want to add or modify the entry for your termination prover or certifier on this page, please contact René Thiemann.