[Termtools] polytool proof output

[ManhThang Nguyen]

Dear Claude,
On Tuesday 05 June 2007 09:30, Claude Marché wrote:
> 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.

Ok, then I will do something with the tool and send it back to you as soon as 
possible.

Regards,
Thang

> >>>>> "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

-- 
--------------------------------------------
Manh Thang NGUYEN
Department of Computer Science, K.U.Leuven
200A Celestijnenlaan, 3001 Heverlee, Belgium