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