#### 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(X*

_{1},...,X_{n})=f(Y_{1},..., Y_{n})←X_{1}=Y_{1}∧···∧X_{n}=Y_{n}.For each *n*-ary predicate symbol *p*, there is a rule of the form

*p(X*

_{1},...,X_{n})←p(Y_{1},..., Y_{n})∧X_{1}=Y_{1}∧···∧X_{n}=Y_{n}.**Example 12.42:**The binary function

*cons(X,Y)*requires the axiom

*cons(X*

_{1},X_{2})=cons(Y_{1},Y_{2})←X_{1}=Y_{1}∧X_{2}=Y_{2}.The ternary relationship *prop(I,P,V)*
requires the axiom

*prop(I*

_{1},P_{1},V_{1})←prop(I_{2},P_{2},V_{2})∧I_{1}=I_{2}∧P_{1}=P_{2}∧V_{1}=V_{2}.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.