#### 12.7.1.2 Special-Purpose Equality Reasoning

**Paramodulation** is a way to augment a proof procedure to
implement equality.
The general idea is that, if *t _{1}=t_{2}*, any occurrence of

*t*can be replaced by

_{1}*t*. Equality can thus be treated as a

_{2}**rewrite rule**, substituting equals for equals. This approach works best if you can select a

**canonical representation**for each individual, which is a term that other representations for that individual can be mapped into.

One classic example is the
representation of numbers. There are many terms that represent the
same number (e.g., *4×4*, *13+3*, *273-257*, *2 ^{4}*,

*4*,

^{2}*16*), but typically we treat the sequence of digits (in base ten) as the canonical representation of the number.

Universities invented student numbers to provide a canonical representation for each student. Different students with the same name are distinguishable and different names for the same person can be mapped to the person's student number.