Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation
Logical Methods in Computer Science, 2012.
AC-completion efficiently handles equality modulo associative and commutative function symbols. When the input is ground, the procedure terminates and provides a decision algorithm for the word problem. In this paper, we present a modular extension of ground AC-completion for deciding formulas in the combination of the theory of equalit...More
PPT (Upload PPT)