Axiomatizing Equality

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 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


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.