[
] t1 = t2 Ethen it can often checked by reducing t1 and t2 using the equations in E as rewrite rules: if t1 and t2 reduce to the same term, then the atomic proof goal has been proved.
If E is canonical as a set of rewrite rules, then reduction is a decision procedure, and the atom is false if the two terms do not reduce to the same thing. Sometimes atoms of other forms can be decided by decision procedures other than rewriting, such as Pressburger arithmetic.