A Congruence Closure Theorem
Recall that we convert all relation symbols into function symbols (to simplify the Axioms for Equality).
Theorem Let be a set of ground equalities and disequalities (). Then the following are equivalent:
- is satisfiable
- there exists a congruence on ground terms in which is true
- is true in the least congruence containing
- for the least congruence containing we have implies
The equivalence of last two statements follows by definition.
We show equivalence of second and third statement.
Third statement trivially implies second.
Consider any congruence in which is true.