Changes from Version 2.1 to Version 2.2

Versions 2.2 and 2.3 are backwards-compatible extensions of version 2.1 where several new proof techniques have been added. Please look at the changelog to see the list of newly added techniques.

Changes from Version 2 to Version 2.1

There are some extensions in CPF version 2.1 which have been added to CPF version 2.

• uncurrying (on TRSs, relative TRSs, DP-problems)
• top-uncurrying on DP-problems (can also be used for freezing)
• match- and roof-bounds for TRSs
• new optional tag for root-labeling in combination with FC1

In the metadata, the toolname and version are now mandatory in versions 2.1 - 2.3. This is a minor incompatibility to version 2. To update existing proofs, one can use the converter cpf_v2.x_to_cpf_v2.3.xsl which changes the version number to 2.3 and enters some default toolname and toolversion if these entries are not present. To invoke the converter, just call:

xsltproc --maxdepth 1000000 --maxparserdepth 10000000 cpf_v2.x_to_cpf_v2.3.xsl myproof.xml

Changes from Version 1 to Version 2

(all changes have been developed with financial support from the france focus of the University of Innsbruck)

There are several extensions and changes to CPF when comparing CPF version 1 (cpf.xsd) and the current version 2. Below we tried to give a complete list.

• new techniques: there have been several new techniques added to the format, including
  • relative termination proofs
  • relative non-termination proofs
  • non-termination proofs in the DP framework
  • interpretations over the tropical semiring
• incomplete proofs: there is now the possibility to specify incomplete proofs such that at least those parts of the proofs that are present can be checked. This includes the possibility to use unsupported orders.
• a mandatory version entry: to know which version of CPF is the intended one
• new inputs: there is now the possibility to just check satisfiability of given sets of constraints.
• All these new features required some small changes which are NOT backwards compatible. This is the complete list of elements that have been changed and need to be adapted when you would like to switch from version 1 to version 2.
  All of these changes are trivial to integrate: We already have a small automatic translator from CPF version 1 to version 2 (350 lines) which converts from version 1 to version 2. It is contained in this archive which contains all CPFs from the 2009-competition in both CPF version 1 and 2. In this archive now also an updated pretty printer is contained.
  • dpProof, trsTerminationProof, ...: In version 1 these elements have been element-groups. That means that in XML-documents no dpProof, ... elements occurred. In version 2 dpProof, ... are now elements so they have to be given in XML documents.
    The reason for this change is that now one can reuse the same name within different proof-kinds which was not possible in version 1. For example, now both trsTerminationProof and relativeTerminationProof can have the proof-technique ruleRemoval.
  • arctic: In version 1 there have been explicit tags for arctic and arcticBelowZero. Since the lifting of arctic can be done over several domains, in version 2 there is only one element arctic which has a subdomain like naturals, integers, or rationals.
  • rationals: In version 1 for the rationals no delta was given. Since there are now methods where not always the minimal delta can be chosen, it is now required in version 2 to explicitly give the delta.
    We choose the proposal to add the delta as an element (instead of an attribute), because there is already an element for rational numbers, and for an attribute one would have to perform more string parsing.
  • loop: Since rewrite sequences are now also required for the extended subterm criterion, version 2 contains a special element rewriteSequence which is also used to specify various kinds of loops. The major difference to the loops in version 1 is that in version 2 a triple (p, r, t) corresponds to a reduction at position p with rule r to term t, whereas in version 1 a triple (t, p, r) encoded a reduction of t at position p with rule r.
  • component: There was a confusion in version 1 whether the option to add 0 forwardArcs indicates that forward arcs are optional at all, or whether there just is no forward arc. Therefore, in version 2 there now is an optional separating element arcs. If this is present then the forward arcs should be correct. Although the arcs-element is optional, termination tool authors are encouraged to provide this information, as some certifiers will produce more costly certificates if these arcs are not given.
  • flatContextClosureProc: There is now an optional argument freshSymbol. It is used to distinguish the two variants of the flat context closure processor that are available. (Only one of them requires a fresh symbol).
  • redPair: all techniques that use reduction pairs, e.g., ruleRemoval, redPairProc, ..., now take the reduction pair within some orderingConstraintsProof. (The reason is that now incomplete proofs can be output where an assumption is used instead of the reduction pair.) In practice, one just has to wrap an orderingConstraintsProof around every redPair.
  • sizeChangeCriterion: renamed to sizeChangeProc for consistency.
  • certificationProblem: there is no goal anymore, as the type of proof directly determines the goal.