[Termtools] certified - strange proofs

[Koprowski, A.]

>> Of course, the participating tool is the combination. I understand
>> this is a collaboration, and that the error is in the scripts, that
is
>> the communication between the 2 components.
> Then it was a misunderstanding on my part. In that setting
> I can understand disqualification--if necessary :).

 Well, indeed it seems reasonable to interpret participation as a
combination of a termination prover and a certifier. And indeed then
CoLoR+TTT give wrong answers which can be a reason for a
disqualification. But given the fact that to the best of our knowledge
both CoLoR and TTT give correct answers and it's only the
miscommunication between the two that is faulty, I wouldn't go as far as
to disqualify this entry. But of course it's not up to me to make such
decisions, especially that I'm involved in this competition entry. I
think this only shows that it would be good to have means of checking
that the claim proven by certifier is the termination of the system in
question and I guess it's good to keep that in mind for the next edition
of the competition.

  Best wishes,
   Adam

--
========================================================================
 Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
 Department of Mathematics and Computer Science
 Eindhoven University of Technology (TU/e)
 The difference between impossible and possible lies in determination
      Tommy Lasorda 
========================================================================