[Termination tools] Competition 2005 is over !

[Claude Marche]

>>>>> "Aart" == Aart Middeldorp <aart.middeldorp at uibk.ac.at> writes:

    Aart> + Raising the timeout doesn't make sense: some tools can solve
    Aart>    some more problems, so what? The outcome remains the same. The

I understand this criticism like this: you think that the score will
hardly change, and the tool classification will remain the same. I
agree.

But for me, The main goal of the competition is not to classify
tools, but to promote research of termination techniques, so that
tools may discover automatically more and more termination
proofs. Being able to solve open termination problem is even more
interesting. 

Take the short example 

a a -> c b , b b -> c a , c c -> b a 

that no tool could solve. Imagine that one tool could solve it within
5 minutes but not in 1 minute, it would be great to have the proof !
Juergen mentioned that some problems could have been solved by Aprove
if there was a bit more time. I have at least one example like this
for CiME too.

Generally speaking, I am primarily interested in obtaining termination
proofs, I don't mind how much time it took to find it.

I understand the technical issues, having a competition that would run
too long in particular. But we could find solutions. For example, I
could manage to run the competition not on only one computer but
several of them in parallel. As far as I know, the CASC competition
(the one on the TPTP database) runs like this, in parallel, and the
timeout used to be 5 minutes.

Also, the timeout needs not to be necessarily the same for each
problem. One could imagine a way to enlarge the timeout, for all the
problems that have not been solved this year. It could even be done
automatically : if a problem is not solved by any tool, then we rerun
the tools with a larger timeout. Imagine we do that
first with 1 second, then 10, then 1 minute, then 5 minutes : I guess
TTT will be pleased with that !

- Claude

-- 
| 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    |