[Termtools] disqualifications

[Zantema, H.]

-----Original Message-----
From: termtools-bounces at lists.lri.fr
[mailto:termtools-bounces at lists.lri.fr] On Behalf Of Claude Marche
Sent: maandag 19 juni 2006 10:16
To: termtools at lri.fr
Subject: Re: [Termtools] disqualifications

> About the disqualification rules : although the rules do not say that
a wrong proof is a reason for disqualification, I think it should be
the case. For the next competition, I propose it is.




I agree, but it is hard to give objective criteria for a "wrong proof",
as the pure formal meaning of "wrong" may be too strict. And who decides
that a proof is wrong? 

For the present situation it is clear I think. Cime is disqualified by
the rule we already have. For MU-Term a serious error has been found in
the heart of termination detection: the analysis of the dependency
graph, causing not only wrong proofs, but also a YES answer on an
obviously non-terminating modification of one of the systems in TPDB. At
least, after I asked Salvador to apply his tool on the non-terminating
TRS
(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))
)
he replied that MU-Term was wrong.

So I think this is sufficient reason for disqualifying MU-Term in the
subcategory of standard rewriting. Since most proofs of MU-Term also use
dependency graph analysis, I think the same should hold for the
context-sensitive subcategory. Apart from these formalities it remains
interesting to know whether after repairing this error the same score is
achieved for this subcategory or not.


            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