XML-Format
From version 1.12 onwards, CeTA uses the CPF format, version 2.x as input. CeTA versions 1.06 - 1.11 use CPF version 1.0 as input. Older versions of CeTA use this proof format.
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.
- As input, only TRSs and relative TRSs are supported, where an arbitrary innermost strategy can be defined. However, no equations may be present.
- The technique argumentFilterProc is unsupported.
- The technique unlabel is no longer supported. One can use split instead.
- 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.
- For match- and roof-bounds only left-linear TRSs are supported, and the automata have to satisfy the compatibility condition of Geser et al., not quasi-compatibility of Korp et al.
- 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).
The archive containing the sources of IsaFoR/CeTA contains a number of examples in the CPF format.