[Termtools] disqualifications

[Salvador Lucas]

Dear all,

Well, to be honest, apart from formalities, I do not
see a big difference between CiME and MU-TERM regarding
disqualification. Once one important bug has been
identified, the whole set of 'proofs' obtained by a
tool is under suspect (I think it works like that).

Furthermore, I could check, for instance, that MU-TERM's
positive answer for

   TRS/CSR_Maude/palindrome - PALINDROME_complete-noand

in the CSR subcategory also had a similar problem.
The corrected version of MU-TERM does not prove the
mu-termination of this system anymore...

Best regards,

Salvador.

Johannes Waldmann wrote:

> 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,