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.