Hello. When a symbol is declared AC in the TRS format, which relation is (dis)proved terminating? Is it rewriting with matching modulo AC or rewriting modulo AC, i.e. rewriting on AC-classes?
Hi Frédéric, at least in the certified categories, for CeTA AC-termination is formalized as termination with rewriting modulo AC. Best, René
Am 23.07.2021 um 09:44 schrieb Frédéric Blanqui <frederic.blanqui@inria.fr>:
Hello. When a symbol is declared AC in the TRS format, which relation is (dis)proved terminating? Is it rewriting with matching modulo AC or rewriting modulo AC, i.e. rewriting on AC-classes?
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Hi Frédéric, yes, I agree with René (also for the non-certified categories). Best Regards Jürgen Am Fr., 23. Juli 2021 um 13:19 Uhr schrieb Thiemann, René < Rene.Thiemann@uibk.ac.at>:
Hi Frédéric,
at least in the certified categories, for CeTA AC-termination is formalized as termination with rewriting modulo AC.
Best, René
Am 23.07.2021 um 09:44 schrieb Frédéric Blanqui < frederic.blanqui@inria.fr>:
Hello. When a symbol is declared AC in the TRS format, which relation is (dis)proved terminating? Is it rewriting with matching modulo AC or rewriting modulo AC, i.e. rewriting on AC-classes?
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
_______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
participants (3)
-
Frédéric Blanqui -
Juergen Giesl -
Thiemann, René