13.7 Equality

13.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 13.45.

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 math302psyc303. 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)/2 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.

Under the unique names assumption (UNA) distinct ground terms denote different individuals. That is, for every pair of distinct ground terms t1 and t2, it assumes t1t2, where “” means “not equal to.”

The unique names assumption 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.

With the unique names assumption, inequality () can be in the bodies of clauses. If you want to use equality in the body of clauses, you can define equality by adding the clause X=X.

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:

  • cc 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)XiYi, 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 1in).

  • f(X1,,Xn)c for any function symbol f and constant c.

With this axiomatization, ground terms are identical if and only if they unify. This is not the case for non-ground terms. For example, aX 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 want, for example, to have to state that kimsam and kimchris and chrissam.

Sometimes the unique names assumption is inappropriate – for example, 2+24 is wrong, and it may not be the case that clark_kentsuperman.

Top-Down Proof Procedure for the Unique Names Assumption

The top-down proof 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 t1t2, for terms t1 and t2 there are three cases:

  1. 1.

    t1 and t2 do not unify. In this case, t1t2 succeeds.

    For example, the inequality f(X,a,g(X))f(t(X),X,b) succeeds because the two terms do not unify.

  2. 2.

    t1 and t2 are identical, including having the same variables in the same positions. In this case, t1t2 fails.

    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.

  3. 3.

    Otherwise, there are instances of t1t2 that succeed and instances of t1t2 that fail.

    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 of 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 13.4, 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 13.46.

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


For the query

𝘢𝘴𝘬 passed_two_courses(sam),

the subgoal C1C2 cannot be determined and so must be delayed. The top-down proof procedure can, instead, select passed(sam,C1), which binds engl101 to C1. It can then call passed(sam,C2), which in turn calls grade(sam,C2,M), which can succeed with substitution {C2/engl101,M/87}. At this stage, the variables for the delayed inequality are bound enough to determine that the inequality should fail.

Another clause can be chosen for grade(sam,C2,M), returning substitution {C2/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.