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
termtools@lists.rwth-aachen.de
-
Frédéric Blanqui -
Juergen Giesl -
Thiemann, René