[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