Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties

Deepak Kapur

Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are pr…