Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala

AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm…