[Termination tools] small hard string termination problem

[Salvador Lucas]

Dear all,

Thanks for this nice example!

I got a very simple proof with the AProVE's version
on the Web: http://aprove.informatik.rwth-aachen.de

Just try:

[X]
1(0(1(X))) -> 0(0(0(X)))
0(0(0(X))) -> 1(1(1(X)))

Regards,

Salvador.

Johannes Waldmann wrote:

>Dear termination provers,
>
>for a few weeks we (jambox, matchbox, torpa) have been trying
>to decide termination of the string rewriting system
>
>   ( RULES 1 0 1 -> 0 0 0 , 0 0 0 -> 1 1 1 )
>
>None of the available tools seem to find a proof
>(and neither do two of the not-yet-available tools...)
>and we really don't know the termination status ourselves.
>
>I think this is a very nice problem so it shouldn't get hidden
>among the (secret) submissions to the next competition
>and that's why I'm posting it here.
>
>Perhaps there is a machine proof outside the one-minute
>competition format, or one that requires hand-tuned parameter settings.
>I'd encourage other tool authors to give it a try.
>
>Best regards,
>  
>