12.7.1 Allowing Equality Assertions

If you do not allow equality assertions, the only thing that is equal to a term is itself. This can be captured as though you had the assertion X=X. This means that for any ground term t, t denotes the same individual as t.

If you want to permit equality assertions (e.g., stating that chairOnRight=chair2), the representation and reasoning system must be able to derive what follows from a knowledge base that includes clauses with equality in the head. There are two major ways of doing this. The first is to axiomatize equality like any other predicate. The second is to build special-purpose inference machinery for equality. Both of these ways are considered here.