[Termtools] polytool proof output

[ManhThang Nguyen]

Dear Claude,

Following is the link to a new version of polytool which provides proof 
traces.
http://www.cs.kuleuven.be/~manh/polytool/wst.zip

After adding some code for the proof trace, it turns out that the new system 
can prove 211 examples, one more than in the competition.
After hours of checking for the new, I found that it is 
../LP/talp/maria - grammar

I don't know why it happened, possiblly because of correcting (changing) the 
output text.

Hope that the other results will not be different.

Best Regards,
Thang



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