foundations of computational agents
Without allowing equality in the head of clauses, the only thing that is equal to a term in all interpretations is itself.
It is often useful to be able to assert or infer that two terms denote the same individual, such as . To allow this, the representation and reasoning system must be able to derive what follows from a knowledge base that includes clauses with equality in the head of clauses. There are two ways of doing this. The first is to axiomatize equality like any other predicate. The other is to build special-purpose inference machinery for 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 first schema specifies substituting term with an equal term does not affect the value of the function. The axiom schema is that for every -ary function symbol , there is a rule
Similarly, for each -ary predicate symbol , there is a rule of the form
The binary function requires the axiom
The ternary relationship requires the axiom
Having these axioms explicit as part of the knowledge base turns out to be very inefficient. Moreover, 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.
Paramodulation is a way to augment a proof procedure to implement equality. The general idea is that, if , any occurrence of can be replaced by . Equality can thus be treated as a rewrite rule, substituting equals for equals. This approach works best if you can select a canonical representation for each individual, which is a term that other representations for that individual can be mapped into.
One classic example is the representation of numbers. There are many terms that represent the same number (e.g., , , , , , ), but typically we treat the sequence of digits (in base ten) as the canonical representation of the number.
Universities invented student numbers to provide a canonical representation for each student. Different students with the same name are distinguishable and different names for the same person can be mapped to the person’s student number.