[Termtools] HofWald 7

Zantema, H. h.zantema at TUE.nl
Thu Jun 15 17:55:47 CEST 2006


As far as I know producing a wrong answer, i.e., YES for a non-terminating system or NO for a terminating system causes disqualification due to the rules; about other situations the rules are not clear.
So if Cime produces YES and we know in some way that the system is non-terminating then Cime will be disqualified, otherwise it is not yet clear.
 
Since in the past we observed wrong proofs several times without disqualifying the tools generating them, I think we should not fully disqualify Cime now.
 
Removing the YES outcome in the results table is a correct action I think.
 
Best regards, Hans Zantema.

	-----Oorspronkelijk bericht----- 
	Van: termtools-bounces at lists.lri.fr namens Claude Marche 
	Verzonden: do 15-6-2006 13:53 
	Aan: termtools at lri.fr 
	CC: 
	Onderwerp: [Termtools] HofWald 7
	
	


	CiME produced a wrong answer on the Hofwald 7 example. I removed that
	answer so that other tools still have a chance to solve it with the 300
	seconds time limit.
	
	CiME has of course to be assumed "disqualified".
	
	If you see any other mistake like this, please mail me.
	
	- Claude
	
	--
	| Claude Marché           | mailto:Claude.Marche at lri.fr |
	| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
	| Université de Paris-Sud | phoneto: ჭ 1 69 15 64 85  |
	| F-91405 ORSAY Cedex     | faxto: ჭ 1 69 15 65 86    |
	_______________________________________________
	Termtools mailing list
	Termtools at lists.lri.fr
	http://lists.lri.fr/mailman/listinfo/termtools
	

-------------- next part --------------
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools


More information about the Termtools mailing list