Hi all,
After your comments about the proposals of modification of the rules,
which were not very positive, I propose to change only few things :
1) one round with 1 minute time limit
then a second round with 5 minutes time limit, for problems where
no tool give any answer.
The time limit will be passed to the "runme" executable as a second
argument. You may ignore this info of course.
2) To encourage the idea of having the tool provide evidence of
termination (or non-termination), the answer given on standard
output will be expected to have the form
first line : YES or NO
remaining : a proof trace in english, with reference to criteria
involved.
On the other hand, I'd like to encourage more kinds of input problems,
so
. the LP category will be resurrected
. the TRS subcategories with only one participant, cancelled last
year, will be resurrected too.
Remark: for the categories with strategies : in principle any tool could
participate, by ignoring the strategy if it does not support it.
it appears that in the TPDB, several problems classified in the
innnermost or context-sensitive category are in fact strongly
terminating. So I encourage author of tool to accept any strategy
in the input file, and not to fail like it is the case now.
. I'd like to propose new categories for functional programs and
imperative programs. I have no proposal for a official input
syntax, but if you are interested plase tell me.
. I suggest also a category for OBJ programs, which are close to
rewriting, but have sorts, programmable strategies, conditions.
. Also, there could be a category for higher-order rewriting
Any comment welcome !
--
| 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 serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools