Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).

12.7.1.1 Axiomatizing Equality

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

X=X.
X=Y←Y=X.
X=Z←X=Y∧Y=Z.

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 general idea is that you can substitute a term with a term that is equal in functions and in relations. For each n-ary function symbol f, there is a rule of the form

f(X1,...,Xn)=f(Y1,..., Yn)←X1=Y1 ∧···∧Xn=Yn.

For each n-ary predicate symbol p, there is a rule of the form

p(X1,...,Xn)←p(Y1,..., Yn)∧X1=Y1 ∧···∧Xn=Yn.
Example 12.42: The binary function cons(X,Y) requires the axiom
cons(X1,X2)=cons(Y1,Y2)←X1=Y1 ∧X2=Y2.

The ternary relationship prop(I,P,V) requires the axiom

prop(I1,P1,V1)←prop(I2,P2,V2)∧I1=I2∧P1=P2∧V1=V2.

Having these axioms explicit as part of the knowledge base turns out to be very inefficient. 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.