[Termtools] Competition: qualification rounds

[Claude Marché]

Done. With 20 seconds time limit, no tool find any proof. 

Notice that TORPA seems to face a "syntax error" problem. You might
want to fix that for the final version.

Other suggestions ?

- Claude

>>>>> "Zantema," == Zantema, H <h.zantema at TUE.nl> writes:

    Zantema,> Dear Claude,
    Zantema,> Indeed nice to see how the present tools find completely different termination proofs for the SRS consisting of the single rule a -> b.

    Zantema,> The fact that this is terminating is not surprising, but the fact that Matchbox needs a 13 levels deep nested unreadable proof for this, is....

    Zantema,> As extra test cases for string rewriting I propose the old challenges 
    Zantema,> Zantema/z086.srs and Waldmann/jw1.srs.




    Zantema,>             Best regards, Hans Zantema.

    Zantema,> _________________________________________________________
    Zantema,> Dr Hans Zantema            
    Zantema,> Technische Universiteit Eindhoven, Department of Computer Science 
    Zantema,> P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
    Zantema,> e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
    Zantema,> office: Hoofdgebouw room 6.73, tel: (040)2472749
 

    Zantema,> -----Original Message-----
    Zantema,> From: termtools-bounces at lists.lri.fr [mailto:termtools-bounces at lists.lri.fr] On Behalf Of Claude Marché
    Zantema,> Sent: woensdag 30 mei 2007 17:01
    Zantema,> To: termtools at lri.fr
    Zantema,> Subject: [Termtools] Competition: qualification rounds


    Zantema,> As for previous editions, I'm currently "qualification rounds" to
    Zantema,> check whether tools are running correctly. The results are available
    Zantema,> on the web page :

    Zantema,> http://www.lri.fr/~marche/termination-competition/2007/

    Zantema,> I'm still facing difficulties: minor problems with aprove and TTT2,
    Zantema,> and a major difficulty with TPA and Rainbow.

    Zantema,> These must be solved before actually running the competition, so I
    Zantema,> expect some delay. Therefore, I give some extra delays for sending the
    Zantema,> final versions of tools: they must reach me on monday morning, June
    Zantema,> 4th, before 7am, GMT time. Same delay for sending secret problems.
    Zantema,> I will start competition as soon as everything is OK.

    Zantema,> In the meantime, I can run some extra tests on qualification rounds:
    Zantema,> if there is one particular example you would like me to run to test
    Zantema,> your tools, I can do it: just send me the name of the corresponding
    Zantema,> file in the TPDB 4.0.

    Zantema,> - Claude

    Zantema,> -- 
    Zantema,> Claude Marché                          | tel: +33 1 72 92 59 69           
    Zantema,> INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
    Zantema,> Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
    Zantema,> 3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
    Zantema,> F-91893 ORSAY Cedex                    |




 

    Zantema,> _______________________________________________
    Zantema,> Termtools mailing list
    Zantema,> Termtools at lists.lri.fr
    Zantema,> http://lists.lri.fr/mailman/listinfo/termtools

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |