[Termtools] polytool proof output

[Claude Marché]

Since polytool is only in the LP category, I think it is reasonable
(in time) to rerun it again on every problem. Please send me a new
version producing output, as soon as possible.


>>>>> "Peter" == Peter Schneider-Kamp <psk at informatik.rwth-aachen.de> writes:

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

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

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

    Peter> Regards,
    Peter> Peter

    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.

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

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

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |