[Termtools] Re: SRS/Zantema/z090

[Zantema, H.]

> Hans - is it true that z090 then would be the first
non-prim-rec SRS with an automatic termination proof?

It would be the first one of which I am aware of.

Indeed self-labelling in a DP setting sounds interesting, but first it
should be defined precisely.


            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749
 

-----Original Message-----
From: termtools-bounces at lists.lri.fr
[mailto:termtools-bounces at lists.lri.fr] On Behalf Of Johannes Waldmann
Sent: vrijdag 8 juni 2007 16:28
To: termtools at lri.fr
Subject: [Termtools] Re: SRS/Zantema/z090

Christian, thanks for the acknowledgment.

Here is some empirical evidence: I am running TTT2
on randomly generated looping SRSs
(so far, 7 * 12 CPU hours @ 3 GHz, on some idle machines)
and it did not claim any of them terminating...

Still, this is no substitute for
(1) formally describing the transformation
and at least (2) indicating a correctness proof.
I'd appreciate if you'd do (1) before the weekend (i.e. now).
(If you don't have it in LaTeX, we can also read ML ...)
I do not understand why you need (or want?) that additional letter.

Hans - is it true that z090 then would be the first
non-prim-rec SRS with an automatic termination proof?

But then I wonder why TTT2 cannot also do jw3, which is rather similar
http://www.lri.fr/%7Emarche/termination-competition/2007/webform.cgi?com
mand=viewpb&file=srs-standard.db&id=SRS.Waldmann.jw3.srs

Best regards, Johannes.
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools