[Termtools] Bug in MU-TERM

[Salvador Lucas]

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