LARA

A Congruence Closure Theorem

Recall that we convert all relation symbols into function symbols (to simplify the Axioms for Equality).

Theorem Let $E$ be a set of ground equalities and disequalities ($E := \bigwedge_{i = 0}^m t_i = t_i^\prime \wedge \bigwedge_{i = m+1}^n t_i \neq t_i^\prime$). Then the following are equivalent:

  • $E$ is satisfiable
  • there exists a congruence on ground terms in which $E$ is true
  • $E$ is true in the least congruence $r_*$ containing $r_0 = \{(t_1,t_2) \mid (t_1=t_2) \in E \}$
  • for the least congruence $r_*$ containing $r_0 = \{(t_1,t_2) \mid (t_1=t_2) \in E \}$ we have $(t_1 \neq t_2) \in E$ implies $(t_1,t_2) \notin r_*$

Proof:

The equivalence of first two statements

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 $r$ in which $E$ is true.

Then

Therefore

Therefore

Proof End.