#### 12.7.2.1 Top-Down Procedure for the Unique Names Assumption

The top-down procedure incorporating the unique names assumption should not treat inequality as just another predicate, mainly because too many different individuals exist for any given individual.

If there is a subgoal *t _{1}≠t_{2}*, for terms

*t*and

_{1}*t*there are three cases:

_{2}*t*and_{1}*t*do not unify. In this case,_{2}*t*succeeds._{1}≠t_{2}For example, the inequality

*f(X,a,g(X))≠f(t(X),X,b)*succeeds because the two terms do not unify.*t*and_{1}*t*are identical, including having the same variables in the same positions. In this case,_{2}*t*fails._{1}≠t_{2}For example,

*f(X,a,g(X))≠f(X,a,g(X))*fails.Note that, for any pair of ground terms, one of these first two cases must occur.

- Otherwise, there are instances of
*t*that succeed and instances of_{1}≠t_{2}*t*that fail._{1}≠t_{2}For example, consider the subgoal

*f(W,a,g(Z))≠f(t(X),X,Y)*. The MGU of*f(W,a,g(Z))*and*f(t(X),X,Y)*is*{X/a*,*W/t(a)*,*Y/g(Z) }*. Some instances of the inequality, such as the ground instances consistent with the unifier, should fail. Any instance that is not consistent with the unifier should succeed. Unlike other goals, you do not want to enumerate every instance that succeeds because that would mean unifying*X*with every function and constant different than*a*, as well as enumerating every pair of values for*Y*and*Z*where*Y*is different than*g(Z)*.

The top-down proof procedure can be extended to incorporate the unique names
assumption. Inequalities of the
first type can succeed and those of the second type can fail.
Inequalities the third type can be
**delayed**, waiting for
subsequent goals to unify variables so that one of the first two cases
occur. To delay a goal in the proof procedure of
Figure 12.3, when selecting an atom in the body of *ac*,
the algorithm should select one of the atoms that is not being delayed. If there are no other
atoms to select, and neither of the first two cases is applicable,
the query
should succeed. There is always an instance of the inequality
that succeeds, namely, the instance where every variable gets a
different constant that does not appear anywhere else. When this
occurs, the user has to be careful when interpreting the free variables in the
answer. The answer does not mean that it is true for every instance of
the free variables, but rather that it is true for some instance.

**Example 12.44:**Consider the rules that specify whether a student has passed at least two courses:

*passed_two_courses(S) ←*

*C*

_{1}≠C_{2}∧*passed(S,C*

_{1})∧*passed(S,C*

_{2}).*passed(S,C) ←*

*grade(S,C,M)∧*

*M ≥ 50*.

*grade(mike,engl101,87).*

*grade(mike,phys101,89).*

For the query

askpassed_two_courses(mike),

the subgoal
*C _{1} ≠C_{2}* cannot be determined and so must be delayed.
The top-down proof procedure can, instead, select

*passed(mike,C*, which binds

_{1})*engl101*to

*C*. It can then call

_{1}*passed(mike,C*, which in turn calls

_{2})*grade(mike,C*, which can succeed with substitution

_{2},M)*{C*. At this stage, the variables for the delayed inequality are bound enough to determine that the inequality should fail.

_{2}/engl101,M/87}Another clause can be chosen for *grade(mike,C _{2},M)*,
returning substitution

*{C*,

_{2}/phys101*M/89}*. The variables in the delayed inequality are bound enough to test the inequality and, this time, the inequality succeeds. It can then go on to prove that

*89>50*, and the goal succeeds.

One question that may arise from this example is "why not simply
make the inequality the last call, because then it does not need to be
delayed?" There are two reasons. First, it may be more
efficient to delay. In this example, the delayed inequality can be
tested before checking whether *87>50*. Although this particular
inequality test may be fast, in many cases substantial computation
can be avoided by noticing violated inequalities as soon as possible.
Second, if a subproof were to return one of the values before it is
bound, the proof procedure should still
remember the inequality constraint, so that any future
unification that violates the constraint can fail.