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

12.7.2 Unique Names Assumption

Instead of being agnostic about the equality of each term and expecting the user to axiomatize which names denote the same individual and which denote different individuals, it is often easier to have the convention that different ground terms denote different individuals.

Example 12.43: Consider a student database example where a student must have two courses as science electives. Suppose a student has passed math302 and psyc303; then you only know whether they have passed two courses if you know math302≠psyc303. That is, the constants math302 and psyc303 denote different courses. Thus, you must know which course numbers denote different courses. Rather than writing n×(n-1) inequality axioms for n individuals, it may be better to have the convention that every course number denotes a different course and thus the use of inequality axioms is avoided.

This approach to handling equality is known as the unique names assumption.

The unique names assumption (UNA) is the assumption that distinct ground terms denote different individuals. That is, for every pair of distinct ground terms t1 and t2, assume t1 ≠t2, where "≠" means "not equal to."

Note that this does not follow from the semantics for the definite clause language. As far as that semantics was concerned, distinct ground terms t1 and t2 could denote the same individual or could denote different individuals.

In the logic presented thus far, the unique names assumption only matters if explicit inequalities exist in the bodies of clauses or equality in the head of clauses. With the unique names assumption, equality does not appear in the head of clauses, other than in the clauses defining equality presented earlier. Other clauses implying equality would be either tautologies or inconsistent with the unique name axioms.

The unique names assumption can be axiomatized with the following axiom schema for inequality, which consists of the axiom schema for equality together with the axiom schema:

  • c≠c' for any distinct constants c and c'.
  • f(X1,...,Xn)≠g(Y1,...,Ym) for any distinct function symbols f and g.
  • f(X1,...,Xn)≠f(Y1,...,Yn)←Xi≠Yi, for any function symbol f. There are n instances of this schema for every n-ary function symbol f (one for each i such that 1 ≤ i ≤ n).
  • f(X1,...,Xn)≠c for any function symbol f and constant c.
  • t≠X for any term t in which X appears (where t is not the term X).

With this axiomatization, two ground terms are not equal if and only if they do not unify, because ground terms are identical if and only if they unify. This is not the case for non-ground terms. For example, a≠X has some instances that are true - for example, when X has value b - and an instance which is false, namely, when X has value a.

The unique names assumption is very useful for database applications, in which you do not, for example, want to have to state that kim≠sam and kim≠chris and chris≠sam. The unique names assumption allows us to use the convention that each name denotes a different individual.

Sometimes the unique names assumption is inappropriate - for example, 2+2 ≠4 is wrong, nor may it be the case that clark_kent≠superman.