[Termtools] Bug in MU-TERM

[Salvador Lucas]

Dear all,

El 22/3/19 a las 18:43, Akihisa Yamada escribió:
> 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).
I'm afraid we had a bug in our answer to SRS_Standard/Gebhardt_06/10
this year. After checking it manually, I found an error.

Furthermore, I also checked the MnM 2018 proof. It really displays the
cycling sequence with the dimensions reported in the SOFSEM 2010
paper.

We will fix the problem in our tool.

Regards,

Salvador.
>   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