[Termtools] certified - strange proofs

[Christian Sternagel]

On Wed, Jun 06, 2007 at 01:51:25PM +0200, Claude March� wrote:
> >>>>> "Christian" == Christian Sternagel <christian.sternagel at uibk.ac.at> writes:
> 
>     >> If we follow the rules, ttt2 should be disqualified.
>     Christian> I do not understand your reasons for that. Certainly it depends on
>     Christian> how you define a participating tool: Is it
>     Christian> (1) the combination of termination-prover + certifier
>     Christian> or
>     Christian> (2) only the termination-prover that provides certifiable output
>     Christian> (XML in the case of Rainbow).
> 
>     Christian> In case (1) ttt2-cert would not have participated, since we did
>     Christian> not contribute to CoLoR+Rainbow.
> 
>     Christian> In case (2) the answer of ttt2-cert is correct--namely MAYBE.
> 
>     Christian> cheers
> 
> I expected such an answer. I said "If we follow the rules, ttt2 should
> be disqualified". Please do not be upset.
I'm sorry if I seemed upset... I was just wondering.
> 
> Of course, the participating tool is the combination. I understand
> this is a collaboration, and that the error is in the scripts, that is
> the communication between the 2 components.
Then it was a misunderstanding on my part. In that setting
I can understand disqualification--if necessary :).

- christian

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