[Termtools] polytool proof output

[Peter Schneider-Kamp]

Dear Johannes,

I think that simply re-running it with a new executable that
produces a proof trace should be ok. I trust Thang to provide
an executable that only has this option flipped on but is
otherwise identical to the version that has been run now.

Due to Claude's "new non-deterministic effect" the output of
Polytool might still differ from the previous output. I would
consider it strange to punish Polytool for this effect.

Please also consider that Polytool is a first-time participant.
The rules do state that the first line "should be followed by
a proof trace of the claimed result". This "should be" is
somewhat weaker than e.g. a "must be" and could be the reason
for this misunderstanding.

Regards,
Peter

Johannes Waldmann schrieb:
> The requirements are that the first line is YES or NO,
> and the following lines provide some explanation
> that conveys the essence of the termination proof to a human.
> 
> I suggest you quickly provide an executable that adds proof output,
> and Claude runs it when computer time will become available.
> 
> If the status (YES/NO/MAYBE) of the new output
> differs from the previous output (that is now in the table),
> we will consider it as MAYBE
> (but I see no reason why this should happen).
> 
> Formally, this procedure is a suggestion that still has to be approved
> by the competition committee (consisting of Claude, Hans and me).
> Also, if any of the competitors sees any problems, then please speak up.
> 
> Best regards, Johannes.

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools