[Termination tools] termination competition

[H. Zantema]

On Wed, 23 Mar 2005, Juergen Giesl wrote:

> Did you already decide which categories we should have
> for the competition? My proposal would be to determine
> the categories based on syntactical criteria:
... 
> Then every TRS- and SRS-example should hopefully fall into exactly one
> category (or did I miss something?). 

Yes, Claude and I already discussed this and came to the same categories
followed by the observation that none of the participating tools will
do outermost rewriting, by which outermost will be removed from the 
competition.

> Every tool can then
> decide on the categories it wants to participate in.
> If there is a category where there are less than 2 tools
> competing, my proposal would be not to have a competition in
> the category, but to keep the examples in the TPDB nevertheless
> (similar to the LP-category).
> 
> What do you think?

I think this is a very good idea. As far as I can see this would mean 
that apart from outermost, also the conditional category would be 
removed. Since the latter only contains 5 TRSs, I think this is a 
good idea. May be I am missing something, in case new facilities 
for conditional rewriting have been added to the tools, please let
me know.

Summarizing, I propose to have the following subcategories:

TRS termination
 
TRS innermost termination
 
TRS context-sensitive termination

TRS termination modulo theory

TRS relative termination

SRS termination
 
SRS relative termination


I have some doubts about context-sensitive termination. Since 
MUTerm does not participate, these systems will only be dealt
by applying a standard transformation and then applying the 
tool for TRS termination. But TPDB already consists many
systems which are the results of these standard transformations,
so then the same results will be counted twice in two separate
categories. Again I may be missing something, since I am not 
aware of all new facilities of all tools.
What do you think of canceling the context-sensitive category
for this year's competition? 

Anyhow, I propose that every tool makes clear in which of these
categories it wants to participate, and then it will be run only on 
these categories. 

For the secret problems I propose that only the categories TRS and 
SRS count as was announced before, so a tool on TRS also running 
on SRS may submit 5 secret TRSs and 5 secret SRSs.

Best Regards,

		Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+