[Termtools] disqualifications

[Claude Marche]

The competition engine is restarted now. CiME answers are displayed in
different colors, and results are ignored when decided if the problem
is solved or not.

About the disqualification rules : although the rules do not say that
a wrong proof is a reason for disqualification, I think it should be
the case. For the next competition, I propose it is.

I think we should not be too strict about wrong answers,
especially about special cases like a variable of the rhs not
appearing in the lhs. On the other hand, if it is clear that there is
a major bug in the tool, such as :

. for CiME : a bug in the RPO
. for Muterm :  a bug in the computation of the dependency graph

then we should disqualify the tool. The main reason being that we cannot
trust the answer. Of course, it is possible to check the proof given
to see if it is correct. But for that, we need a formal language for
proofs and an automatic  proof checker. This is indeed a very good
reason why we should go further into this direction !

For the moment, I did not mark MuTerm as disqualified, I wait for your
opinions. 
 
>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:

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

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

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

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

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

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools