[Termtools] new project: online database for hard SRS termination problems

[Johannes Waldmann]

Dear all,

my student Andreas Gebhardt has just completed
a preliminary version of an online data-base
containing hard SRS termination problems:

http://autotool.imn.htwk-leipzig.de/websrs/

The basic idea is that you can enter an SRS,
then all termination provers are run on it,
and if *none* gives an answer, the SRS enters the database.
(Otherwise, you'll see the proof(s), but the SRS is discarded.)

Perhaps you find this useful for preparing your
problem submission (the deadline of which will soon arrive,
that's why we are a bit in a hurry - so expect some quirks and bugs).

Let us underline that the intention is to *support*
the official termination competition (by collecting hard problems),
and not to side-step it. Also, all data is public,
(if you want to check, read the source
http://141.57.11.163/cgi-bin/cvsweb/websrs/ :-)
so  Matchbox  cannot use this for any unfair advantage.

We installed all provers that took part in last year's competition,
in the version from the competition web site
or in an updated version, if one was available from authors' web sites.

Computational resources are limited,
and the server will refuse to run provers if it thinks it is too busy.

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

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools