[Termtools] "unknown method String reversal" (in TRS relative certified)

[Carsten Fuhs]

Dear all,

here the issue is that the proof contains a step that is currently not
representable in the Certification Problem Format.

In the termination proof found by AProVE, a relative TRS with function
symbols of arities in {0,1} is transformed to a relative TRS with
function symbols of arity 1 only, which makes string reversal
applicable. This replacement of function symbols ("constantToUnary") is
sound for relative termination proving by Theorem 9 (i) of the paper

R. Thiemann, H. Zantema, J. Giesl, and P. Schneider-Kamp
Adding Constants to String Rewriting
Applicable Algebra in Engineering, Communication and Computing,
19(1):27-38, 2008.

http://verify.rwth-aachen.de/giesl/papers/AAECC07-distribute.ps

However, the current CPF version 2.2 allows for constantToUnary to be
exported only for standard rewriting, but not for relative rewriting.
This is why AProVE here exports an "unknownProof", which allows a
certifier to check at least the remaining proof steps.

However, since the termination competition is about /full/
certification, a tools that exports CPF should of course only use
termination techniques that can also be exported to a CPF proof which
can be certified completely. In other words, for output of CPF files for
the certified competition, AProVE should not have applied
constantToUnary for relative TRSs.

This bug is fixed now, and the processor is not applicable on relative
TRSs any more if

* not only function symbols of arity 1, but also of arity 0 are present
and
* full certification is desired

Best regards,

  Carsten

On 20.07.2014 16:45, Johannes Waldmann wrote:
> CeTA (2.15) rejected this (in TRS relative certified):
> 
> http://nfa.imn.htwk-leipzig.de/termcomp/display_proof/26938788
> 
> actual certifier output is:
> 
> $ ceta-2.15 rt2-4.cpf
> 
> REJECTED
> relative termination proof not accepted
> 1: the proof contains a termination assumption or unknown proof
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
Carsten Fuhs                       mailto:c.fuhs at cs.ucl.ac.uk
Department of Computer Science     http://www.cs.ucl.ac.uk/staff/C.Fuhs/
University College London          phone: +44 20 7679 0386
Programming Principles, Logic and Verification