15 Individuals and Relations 15.7 Applications in Natural Language 15.9 Complete Knowledge Assumption

15.8 Equality

Sometimes it is useful to use more than one term to name a single individual. For example, the terms $4*4$ , $2^{4}$ , $273-257$ , and $16$ may denote the same number. Sometimes, you want to have each name refer to a different individual. For example, you may want unique names for different courses in a university. Sometimes you do not know whether or not two names denote the same individual – for example, whether the 8 a.m. delivery person is the same as the 1 p.m. delivery person.

This section considers the role of equality, which allows us to represent whether or not two terms denote the same individual in the world. Note that, in the definite-clause language presented earlier in the chapter, all of the answers were valid whether or not terms denoted the same individuals.

Equality is a special predicate symbol with a standard domain-independent intended interpretation.

Term $t_{1}$ equals term $t_{2}$ , written $t_{1}=t_{2}$ , is true in interpretation $I$ if $t_{1}$ and $t_{2}$ denote the same individual in $I$ .

Equality does not mean similarity. If $a$ and $b$ are constants and $a=b$ , it is not the case that there are two things that are similar or even identical. Rather, it means there is one thing with two names.

Refer to caption — Figure 15.13: Two chairs

Example 15.38.

Consider the world consisting of two chairs given in Figure 15.13. In this world it is not true that $chair1=chair2$ , even though the two chairs may be identical in all respects; without representing the exact position of the chairs, they cannot be distinguished. It may be the case that $chairOnRight=chair2$ . It is not the case that the chair on the right is similar to chair2. It is chair2.

15.8.1 Allowing Equality Assertions

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 $chairOnRight=chair2$ . 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.

If $t_{1}=t_{2}$ , any occurrence of $t_{1}$ can be replaced by $t_{2}$ . 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., $4*4$ , $13+3$ , $273-257$ , $2^{4}$ , $4^{2}$ , $16$ ), but typically the sequence of digits (in base 10) is used 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.

Each rewrite rule should make the description closer to the canonical representation. In theorem proving, using equality as rewriting rules is called paramodulation. Determining the canonical representation is sometimes referred to as determining the identity of the description (e.g., determining the identity of a student who submitted as assignment without a name).

15.8.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 15.39.

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\neq 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)/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 $t_{1}$ and $t_{2}$ , it assumes $t_{1}\neq t_{2}$ , where “ $\neq$ ” means “not equal to.”

The unique names assumption is very useful for database applications. You may not want to have to state that, for example, $kim\neq sam$ and $kim\neq chris$ and $chris\neq sam$ , and similarly for each pair of entities.

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 $t_{1}$ and $t_{2}$ could denote the same individual or could denote different individuals.

With the unique names assumption, inequality ( $\neq$ ) can be in the bodies of clauses.

Ground terms are different if and only if they do not unify. This is not the case for non-ground terms. For example, $a\neq 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$ .

Sometimes the unique names assumption is inappropriate – for example, $2+2\neq 4$ is wrong, and it may not be the case that $clark\_kent\neq superman$ .

Top-Down Proof Procedure for the Unique Names Assumption

A 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 of the form $t_{1}\neq t_{2}$ , for terms $t_{1}$ and $t_{2}$ there are three cases:

1.

$t_{1}$ and $t_{2}$ do not unify. In this case, $t_{1}\neq t_{2}$ succeeds.

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

$t_{1}$ and $t_{2}$ are identical, including having the same variables in the same positions. In this case, $t_{1}\neq t_{2}$ fails.

For example, $f(X,a,g(X))\neq f(X,a,g(X))$ fails.

Note that, for any pair of ground terms, one of these first two cases must occur.
3.

Otherwise, there are instances of $t_{1}\neq t_{2}$ that succeed and instances of $t_{1}\neq t_{2}$ that fail.

For example, consider the subgoal $f(W,a,g(Z))\neq f(t(X),X,Y)$ . The most general unifier 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 15.5, when selecting an atom in the body of the answer clause $G$ , 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 15.40.

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

passed\_two\_courses(S)\leftarrow\mbox{}

C_{1}\neq C_{2}\wedge\mbox{}

passed(S,C_{1})\wedge\mbox{}

passed(S,C_{2}).

passed(S,C)\leftarrow\mbox{}

grade(S,C,M)\wedge\mbox{}

M\geq 50

grade(sam,engl101,87).

grade(sam,phys101,89).

For the query

\mbox{{ask}~{}}~{}passed\_two\_courses(sam)

the subgoal $C_{1}\neq C_{2}$ cannot be determined and so must be delayed. The top-down proof procedure can, instead, select $passed(sam,C_{1})$ , which binds $engl101$ to $C_{1}$ . It can then call $passed(sam,C_{2})$ , which in turn calls $grade(sam,C_{2},M)$ , which can succeed with substitution $\{C_{2}/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,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.

Artificial Intelligence 3E