[Termination tools] small hard string termination problem

[Peter Schneider-Kamp]

Dear all,

the strange behaviour of AProVE's web interface has been
fixed. The default value for the strategy flag for
string rewriting systems in AProVE's own format (.ses)
was set to innermost in the command line version.

In spite of intensive trying I have not been able to find
a termination proof of this nice example applying AProVE's
techniques manually (interactive mode in the graphical UI).

Kind regards,
Peter

Juergen Giesl wrote:
> Dear all,
> 
> thanks for Johannes for the nice example and for Salvador
> for the nice solution with AProVE.
> 
> However, note that AProVE only proved INNERMOST termination
> of this example. This can indeed easily be verified by AProVE.
> But whether the TRS is terminating remains unclear.
> 
> (This indicates a small strange behavior of AProVE's web interface
> which has to be fixed. This strange behavior
> doesn't happen in the downloadable version of AProVE:
> 
> If one enters the example in the format
> 
>  [X]
>  1(0(1(X))) -> 0(0(0(X)))
>  0(0(0(X))) -> 1(1(1(X))
> 
> the web interface only tries the innermost instead of the full 
> termination proof.
> This is different if one uses the WST-format:
> 
> (VAR X)
> (RULES
> 1(0(1(X))) -> 0(0(0(X)))
> 0(0(0(X))) -> 1(1(1(X)))
> )
> 
> Here, the web interface times out after 1 minute.)
> 
> 
> Best Regards
> Juergen
> 
> 
> 


-- 
Peter Schneider-Kamp   mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II     http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen            phone: ++49 241 80-21211