[Termtools] disqualifications

[Johannes Waldmann]

Claude Marche wrote:
> So it seems that MuTERM also has a clear bug. 

Well, it gave the right answer (termination), but for the wrong reason.
This is different from giving a wrong answer. Formally, the rules do not
speak about disqualification because of a wrong proof.

Hans' example (encoding of ab -> bbaa)
perhaps makes the bug visible (i.e. leads to a wrong answer)
but that problem is not in the TPDB,
and by the rules of the competition, it cannot be added now.

I know at least one other buggy tool:
matchbox/satelite gives a wrong answer for
(VAR x)(STRATEGY INNERMOST)(RULES  a -> x)
because the *-bound computer does not handle
new-born variables correctly. For standard rewriting this bug
is hidden because the loop checker finds a loop earlier.
But the loop checker is turned off with strategies.
(I subscribe to Claude's viewpoint that this really
*is* a rewriting system and this really *is* a bug.)

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------