[Termtools] Problem with some proofs

Salvador Lucas slucas at dsic.upv.es
Thu Jun 7 18:10:49 CEST 2007


Dear all,

Martin Korp (from the TTT2 team) noticed that MU-TERM's proof
for TRS/secret2007/TTT2-6.trs is wrong. He has shown that the system
is actually non-terminating.

We have a bug in the implementation of narrowing of DPs which
we have already fixed, but anyway some examples in the TRS
competition would not be solved by the new version of MU-TERM
(we also have checked this).

We would like then to have the MU-TERM column removed from
the web of the TRS competition.

Still, we would be able to participate in the CSR and innermost
subcategories if the organizers are willing to accept our repaired
version of MU-TERM.

Best regards,

Salvador.



More information about the Termtools mailing list