[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