Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
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 t1=t2, any occurrence of t1 can be replaced by t2. Equality can thus be treated as a 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, 24, 42, 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.
