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

• an input:
  some TRS or relative TRS or ...
• a proof: some termination / nontermination / confluence / completion / complexity / ... - proof
  The proof can be handwritten, but it is usually supplied by some automated prover. The current proof structure can express several proofs in an explicit manner. For example, if a reduction pair processor is applied, then of course, one has to give the reduction pair itself. And one also has to give the remaining set of dependency pairs, but not the new TRS. The reason is that the TRS cannot be changed by the reduction pair processor whereas the set of dependency pairs can.
  Note that not all techniques that are expressible in CPF are supported by all certifiers. And of course, there might be techniques of certifiers that are not yet integrated in CPF.

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.

• example which is automatically transformed
• same example where XSLT-transformation line is commented out

Certifying Proofs using CPF

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

• Standalone certification:
  Here, a CPF-file is given as starting point and a certifier just has to check whether the input satisifies the goal, e.g., whether the TRS in the CPF-file is (non)terminating by applying the given proof in a certified way.
  Examples:
  • ceta div.proof.xml
  • cime3 -icpf div.proof.xml -ocoq div.proof.v && coqc -I ... div.proof.v
• Certified proof for a TRS:
  Here, a TRS without any proof is given as starting point. Then a automated prover is used to generate a CPF-file from this which can then be checked as before.
  Note that to ensure that the TRS in the CPF-file corresponds to the original TRS (given in the XTC format that is used in the upcoming competitions), we have written a small shell-script which compares both TRSs and ensures that they are equal. Everyone who is interested can have a look at the comparison procedure which is based on XML-transformations and diff.
  Examples:
  • (cime3 | ttt2 | ...) div.xml > div.proof.xml;
    (YES answer)
    checkEqualityYes.sh div.xml div.proof.xml && (ceta | cime3 | CoLoR) div.proof.xml (as in standalone certification)
  • (cime3 | ttt2 | ...) nonterm.xml > nonterm.proof.xml;
    (NO answer)
    checkEqualityNo.sh nonterm.xml nonterm.proof.xml && (ceta | cime3 | CoLoR) nonterm.proof.xml

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

• CeTA
  usage: ceta example.proof.xml
  
• CiME / Coccinelle
  usage: cime3 -icpf example.proof.xml -ocoq example.v && coqc -I ... example.v
  (the includes ... for Coq are given in the last line of example.v)
• CoLoR / Rainbow

Automated provers that generate CPF

Completion tools

• mkbTT
• KBCV

Complexity tools

• TcT
• CaT

Confluence tools

• CSI

Termination tools

• AProVE
• CiME
• Matchbox
• Tyrolean Termination Tool 2

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.