[Termtools] Re: Problem with some proofs

[Salvador Lucas]

Dear all,

We are able to participate in the CSR category with
the tool we submitted before the deadline.

We cannot go ahead with the innermost category.

So, I hope it is still possible to proceed as you
suggested.

Best regards,

Salvador.

Zantema, H. wrote:

>Accepting repaired versions after the deadline is out of scope. The only
>exception that could be made is if the error is unrelated to generation
>of proofs, like could be the case if something already goes wrong with
>parsing the system.
>
>I see two options:
>
>(1) You make clear that the analysis in your tool causing the detected
>error in TRS/secret2007/TTT2-6.trs does not play a role in the CSR and
>innermost subcategories. In that case you can participate with the last
>version of your tool that you submitted before the deadline.
>
>(2) The analysis in your tool causing the detected error in
>TRS/secret2007/TTT2-6.trs is used in the CSR and innermost subcategories
>too. In that case there is no other choice than also removing MU-TERM
>from the CSR and innermost subcategories.
>
>            Best regards, Hans Zantema.
>
>_________________________________________________________
>Dr Hans Zantema            
>Technische Universiteit Eindhoven, Department of Computer Science 
>P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
>e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
>office: Hoofdgebouw room 6.73, tel: (040)2472749
> 
>
>-----Original Message-----
>From: Salvador Lucas [mailto:slucas at dsic.upv.es] 
>Sent: donderdag 7 juni 2007 18:11
>To: termtools at newwww.lri.fr
>Cc: Claude Marche; Johannes Waldmann; H. Zantema
>Subject: Problem with some proofs
>
>Dear all,
>
>Martin Korp (from the TTT2 team) noticed that MU-TERM's proof
>for TRS/secret2007/TTT2-6.trs is wrong. He has shown that the system
>is actually non-terminating.
>
>We have a bug in the implementation of narrowing of DPs which
>we have already fixed, but anyway some examples in the TRS
>competition would not be solved by the new version of MU-TERM
>(we also have checked this).
>
>We would like then to have the MU-TERM column removed from
>the web of the TRS competition.
>
>Still, we would be able to participate in the CSR and innermost
>subcategories if the organizers are willing to accept our repaired
>version of MU-TERM.
>
>Best regards,
>
>Salvador.
>
>  
>