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