[christian.sternagel@uibk.ac.at: Re: [Termtools] certified - strange proofs]

[Christian Sternagel]

----- Forwarded message from Christian Sternagel <christian.sternagel at uibk.ac.at> -----
sorry I forgot to send also to the list

Date: Wed, 6 Jun 2007 13:44:47 +0200
From: Christian Sternagel <christian.sternagel at uibk.ac.at>
To: Claude March� <Claude.Marche at lri.fr>
Subject: Re: [Termtools] certified - strange proofs

On Wed, Jun 06, 2007 at 01:31:05PM +0200, Claude March� wrote:
> 
> I think you are correct: Coq is given an empty file and considers it
> OK. It means the runme/checkme scripts are wrong.
Yes.
> 
> I must say that I spent quite a lot of time in adapting these scripts,
> to make them OK. For example, in checkme I needed first to make a copy
> of the given file, because it was not ending with .v. The modified
> scripts are of course visible on the web by clicking on the tool name
> and following the link "tool executable". The fact that ttt2 and tpa
> are sharing the same back-end Rainbow/Color, and that this backend
> changed significantly between the preliminary and the final version
> was much trouble. But I do not think this error comes from my
> modifications.
> 
> I grep'ed for the faulty answer "not a proofMAYBE" in the generated
> proofs for ttt2, and found 36 such examples. 
> 
> If we follow the rules, ttt2 should be disqualified.
I do not understand your reasons for that. Certainly it depends on
how you define a participating tool: Is it
(1) the combination of termination-prover + certifier
or
(2) only the termination-prover that provides certifiable output
(XML in the case of Rainbow).

In case (1) ttt2-cert would not have participated, since we did
not contribute to CoLoR+Rainbow.

In case (2) the answer of ttt2-cert is correct--namely MAYBE.

cheers

christian
> 
> - Claude
> 
> 
> >>>>> "Frederic" == Frederic Blanqui <blanqui at loria.fr> writes:
> 
>     Frederic> On Wed, 6 Jun 2007, Koprowski, A. wrote:
>     >> The really bad outcome of the whole thing is that TTT2 gets points for 
>     >> systems for which it essentially fails. Of course this should be avoided and 
>     >> even more so in the certified competition!
> 
>     Frederic> this means that proofs have to be checked and points have to be computed by 
>     Frederic> hand...
>     Frederic> _______________________________________________
>     Frederic> Termtools mailing list
>     Frederic> Termtools at lists.lri.fr
>     Frederic> 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                    |
> 
> 
> 
> 
>  
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
> 

----- End forwarded message -----