[Termtools] competition dec 09 started

René Thiemann rene.thiemann at uibk.ac.at
Thu Jan 21 07:00:38 CET 2010


Dear Frederic,

>> - the correct version of CeTA will be rerun in the certified categories
> 
> But could you explain why these tools need to be rerun?
> 
> In particular, for TCT and CeTA, why are there new corrected version? Do 
> you mean that the submitted versions were buggy?

note that for CeTA the correct (but not the corrected) version should be run. 
CeTA was not buggy in the sense that it could accept wrong proofs. The reason
why I want the correct version to be rerun is that for the competition I submitted 
two versions on 14th and 15th of December where. I withdrew the one from 14th 
since only the newer version supports string reversal. (And AProVE-CeTA
relied on that fact.) However, unfortunately I named both versions "v1.08" 
since I wrongly assumed that then automatically for the competition the right 
version 1.08 would be chosen as there was only non-withdrawn version. 
But this was not the case.

So, I just want a rerun with the correct version 1.08 of CeTA which
supports string reversal. Otherwise it looks strange that there 
CeTA rejects many proofs that were generated by AProVE-CeTA.

Best regards,
Rene


More information about the Termtools mailing list