XML-Format

From version 3.x onwards, CeTA uses the CPF format, version 3.x as input. The schema description as well as a pretty printer to HTML are part of the archive containing the sources of IsaFoR/CeTA. This archive also contains a number of examples in the CPF format.

There also is a converter from CPF 2.x to 3.x

Since most elements of CPF are fully supported, we just list some items which might be useful to know when creating proofs that should be read by CeTA.

• The technique argumentFilterProc is unsupported.
• One can use linear polynomial interpretations with matrices over naturals, rationals, arctic, or arcticBelowZero as possible domains. Here, in the functions, everything has to be a matrix, even the constant parts. Non-linear polynomial interpretations are only supported for rationals and naturals. Make sure that the degree element is at least 2 if you want to use non-linear interpretations.
  Also matrixInterpretations where the constants are vectors are supported. These are automatically extended to matrices by filling in zeros.
• Polynomials with negative constants are supported using Pleft and Pright approximations for linear interpretations. Here, one must not use max-elements (to indicate that Pol(f(x)) = x - 1 means Pol(f(x)) = max(0, x-1), but one just has to encode x - 1.
• Any set of usable rules can be used (ren/cap or tcap or icap, with or without regarding argument filter). However, the given set of usable rules must be closed under usable rules of right-hand sides.
• Any dependency graph estimation can be used that is subsumed by E(I)DG^*** (root-symbol-comparison, ren/cap, tcap, icap, looking both forward and backward).