AC Dependency Pairs Revisited

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Leibniz International Proceedings in Informatics 62, pp. 8:1 – 8:16, 2016.


Rewriting modulo AC, i.e., associativity and/or commutativity of certain symbols, is among the most frequently used extensions of term rewriting by equational theories. In this paper we present a generalization of the dependency pair framework for termination analysis to rewriting modulo AC. It subsumes existing variants of AC dependency pairs, admits standard dependency graph analyses, and in particular enjoys the minimality property in the standard sense. As a direct benefit, important termination techniques are easily extended; we describe usable rules and the subterm criterion for AC termination, which properly generalize the non-AC versions.
We also perform these extensions within IsaFoR — the Isabelle formalization of rewriting — and thereby provide the first formalization of AC dependency pairs. Consequently, our certifier CeTA now supports checking proofs of AC termination.




author = "Akihisa Yamada and Christian Sternagel and Ren{\'e} Thiemann
and Keiichirou Kusakari",
title = "{AC} Dependency Pairs Revisited",
booktitle = "Proceedings of the 25th EACSL Annual Conference on Computer
Science Logic (CSL 2016)",
pages = "8:1--8:16",
series = "Leibniz International Proceedings in Informatics",
volume = 62,
year = 2016,
editor = "Jean-Marc Talbot and Laurent Regnier",
publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
doi = "",
Nach oben scrollen