[Termtools] competition

[Zantema, H.]

In the mean time Cime produced two YES answers where other tools
produced NO:
TRSCS_Ex_4_4_Luc96B_FR and TRSCS_Ex_4_4_Luc96B_Z.

Since the NO is correct, unfortunately now Cime is disqualified
according the rules.

I expect that the MU-Term proof of Zantema-z12 is not correct. Salvador
(or any other having MUTerm running): can you check the system 

(VAR x y )
(RULES
f(x,a(b(y))) -> f(a(a(b(b(x)))),y)
f(a(x),y) -> f(x,a(y))
f(b(x),y) -> f(x,b(y))
)

and tell me the outcome?

I propose to extend the second round list by a few extra systems. Claude
already put a system in the second round list since the only termination
proof found (by Cime) was wrong. I propose also to add Zantema-z09 and
Zantema-z10: these are two variants of the famous SUBST system for
explicit substitution. I think it is not fair that the fact that TPA
found proofs very fast causes that no 5 minute attempt will be done for
these interesting systems for the other tools. In case the second round
would have a formal meaning I can imagine to exclude these extensions
for the formal results; but I am curious about the outcome. Even if
Jambox would find a proof for these systems in several hours of
computation time, this would be an interesting observation.

            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 16 juni 2006 11:13
To: termtools at lri.fr
Subject: [Termtools] TRS/Zantema - z12

I am having trouble understanding this proof:
http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?com
mand=viewres&tool=muterm&prob=TRS.Zantema.z12.trs

This is an encoding of Zantema's system aabb -> bbbaaa
So I'd expect it requires RFC match-bounds (Aprove does this)
or matrices (Jambox does this).
I don't understand how Muterm can do without either.
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

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

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