Congruence-Anticongruence Closure
Jan Kl ' uka · 2005
We present in this paper a method for deciding sets of closed, quantifier-free formulas with identities. The method is based on reduction of such a set into a set of identities by introduction of new special function symbols. For the special function symbols, identity in this set is assumed to have a property which is dual to congruence. We prove that under this property, which we call anticongruence, the set of identities is a conservative extension of the original set of formulas. We introduce a simple two-rule proof system (the CA-proof system) for the sets of identities with anticongruence symbols, and show the system to be sound and complete. We then formulate the congruence closure algorithm in an abstract way that we believe facilitates its understanding, and extended it to the CA-closure algorithm to implement the CA-proof system.