Canonized rewriting and ground AC completion modulo shostak theories
TACAS, pp. 45-59, 2011.
equality modulo associativeuser-defined ac symbolshostak theoryground ac completion moduloarbitrary signature disjoint shostakMore(9+)
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 ACcompletion for deciding formulas in the combination of the theory of equality w...More
PPT (Upload PPT)