Canonized rewriting and ground AC completion modulo shostak theories

TACAS, pp. 45-59, 2011.

Cited by: 8|Bibtex|Views1|Links
EI
Keywords:
equality modulo associativeuser-defined ac symbolshostak theoryground ac completion moduloarbitrary signature disjoint shostakMore(9+)

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments