Equality can be axiomatized as follows. The first three axioms state that equality is reflexive, symmetric, and transitive:

The other axioms depend on the set of function and relation symbols in the language; thus, they form what is called an axiom schema.

The first schema specifies substituting term with an equal term does not affect the value of the function. The axiom schema is that for every $n$-ary function symbol $f$, there is a rule

Similarly, for each $n$-ary predicate symbol $p$, there is a rule of the form

Having these axioms explicit as part of the knowledge base turns out to be very inefficient. Moreover, the use of these rules is not guaranteed to halt using a top-down depth-first interpreter. For example, the symmetric axiom will cause an infinite loop unless identical subgoals are noticed.

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_1$ can be replaced by $t_2$. 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$, $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.