[Termtools] Bug in MU-TERM

[Akihisa Yamada]

Dear all,

so there will be another conflict when MnM is fixed. It’ll be nice to know which (or none or both) should be penalized (or fixed). Anyway exciting motivation for certification. :)

Best,
Akihisa

> On Mar 23, 2019, at 2:17, Salvador Lucas <slucas at dsic.upv.es> wrote:
> 
> 
> 
>> El 22/3/19 a las 18:05, Johannes Waldmann escribió:
>>> On 22.03.19 08:42, Raul Gutierrez wrote:
>>> 
>>> ... bug in the last version of  MU-TERM.
>> also visible in SRS_Standard/Gebhardt_06/10
>> (which has a loop, found by MnM, last year)
> We already detected this...
> 
> However, in our proof this year we do not use
> innermost transformation. Thus, the problem reported
> this morning by Raúl does not happen and should be ok.
> 
> The proof this year was possible due to the use of
> simple-mixed interpretations over the rationals (which
> were somehow disabled in 2018).
> 
> Unfortunately, there is no alternative proof this year to
> double check this.
> 
> If the SRS competition is repeated (as we suggested) we
> expect to obtain a confirmation of our proof with MU-TERM 6.0.1.
> 
> Regards,
> 
> Salvador.
> 
> 
>> 
>> - J.W.
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools