13.5.1 Proof Procedures with Function Symbols

The proof procedures with variables carry over for the case with function symbols. The main difference is that the class of terms is expanded to include function symbols.

The use of function symbols involves infinitely many terms. This means that, when forward chaining on the clauses, we have to ensure that the selection criterion for selecting clauses is fair.

Example 13.30.

To see why fairness is important, consider the following clauses:

	$\displaystyle{num(0).}$
	$\displaystyle{num(s(N))\leftarrow\mbox{}num(N).}$
	$\displaystyle{a\leftarrow\mbox{}b.}$
	$\displaystyle{b.}$

An unfair strategy could initially select the first of these clauses to forward chain on and, for every subsequent selection, select the second clause. The second clause can always be used to derive a new consequence. This strategy never selects either of the last two clauses and thus never derives $a$ or $b$ .

This problem of ignoring some clauses forever is known as starvation. A fair selection criterion is one such that any clause available to be selected will eventually be selected. The bottom-up proof procedure can generate an infinite sequence of consequences and if the selection is fair, each consequence will eventually be generated and so the proof procedure is complete.

The top-down proof procedure is the same as for Datalog (see Figure 13.4). Unification becomes more complicated, because it must recursively descend into the structure of terms. There is one change to the unification algorithm: a variable $X$ does not unify with a term $t$ in which $X$ occurs and is not $X$ itself. Checking for this condition is known as the occurs check. If the occurs check is not used and a variable is allowed to unify with a term in which it appears, the proof procedure becomes unsound, as shown in the following example.

Example 13.31.

Consider the knowledge base with only one clause:

lt(X,s(X)).

Suppose the intended interpretation is the domain of integers in which $l t$ means “less than” and $s(X)$ denotes the integer after $X$ . The query $\mbox{{ask}~{}}~{}lt(Y,Y)$ should fail because it is false in the intended interpretation; there is no number less than itself. However, if $X$ and $s(X)$ could unify, this query would succeed. In this case, the proof procedure would be unsound because something could be derived that is false in a model of the axioms.

The unification algorithm of Figure 13.3 requires one change to find the most general unifier of two terms with function symbols. The algorithm should return $\bot$ if it selects an equality $\alpha=\beta$ , where $\alpha$ is a variable and $\beta$ is a term that is not $\alpha$ , but contains $\alpha$ (or the other way around). This step is the occurs check. The occurs check is sometimes omitted (e.g., in Prolog), because removing it makes the proof procedure more efficient, even though removing it does make the proof procedure unsound.

The following example shows the details of SLD resolution with function symbols.

Example 13.32.

Consider the clauses

	$\displaystyle{append(c(A,X),Y,c(A,Z))\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {append(X,Y,Z).}$
	$\displaystyle{append(nil,Z,Z).}$

For now, ignore what this may mean. Like the computer, treat this as a problem of symbol manipulation. Consider the following query:

\mbox{{ask}~{}}~{}append(F,c(L,nil),c(l,c(i,c(s,c(t,nil))))).

The following is a derivation:

	$\displaystyle{yes(F,L)\leftarrow\mbox{}append(F,c(L,nil),c(l,c(i,c(s,c(t,nil))% )))}$
	$\displaystyle\ \ \ \ {\hbox{resolve with }append(c(A_{1},X_{1}),Y_{1},c(A_{1},% Z_{1}))\leftarrow\mbox{}append(X_{1},Y_{1},Z_{1})}$
	$\displaystyle\ \ \ \ {\hbox{substitution: }{\{F/c(l,X_{1}),Y_{1}/c(L,nil),A_{1% }/l,Z_{1}/c(i,c(s,c(t,nil)))\}}}$
	$\displaystyle{yes(c(l,X_{1}),L)\leftarrow\mbox{}append(X_{1},c(L,nil),c(i,c(s,% c(t,nil))))}$
	$\displaystyle\ \ \ \ {\hbox{resolve with }append(c(A_{2},X_{2}),Y_{2},c(A_{2},% Z_{2}))\leftarrow\mbox{}append(X_{2},Y_{2},Z_{2})}$
	$\displaystyle\ \ \ \ {\hbox{substitution: }{\{X_{1}/c(i,X_{2}),Y_{2}/c(L,nil),% A_{2}/i,Z_{2}/c(s,c(t,nil))\}}}$
	$\displaystyle{yes(c(l,c(i,X_{2})),L)\leftarrow\mbox{}append(X_{2},c(L,nil),c(s% ,c(t,nil)))}$
	$\displaystyle\ \ \ \ {\hbox{resolve with }append(c(A_{3},X_{3}),Y_{3},c(A_{3},% Z_{3}))\leftarrow\mbox{}append(X_{3},Y_{3},Z_{3})}$
	$\displaystyle\ \ \ \ {\hbox{substitution: }{\{X_{2}/c(s,X_{3}),Y_{3}/c(L,nil),% A_{3}/s,Z_{3}/c(t,nil)\}}}$
	$\displaystyle{yes(c(l,c(i,c(s,X_{3}))),L)\leftarrow\mbox{}append(X_{3},c(L,nil% ),c(t,nil))}$

At this stage both clauses are applicable. Choosing the first clause gives

	$\displaystyle\ \ \ \ {\hbox{resolve with }append(c(A_{4},X_{4}),Y_{4},c(A_{4},% Z_{4}))\leftarrow\mbox{}append(X_{4},Y_{4},Z_{4})}$
	$\displaystyle\ \ \ \ {\hbox{substitution: }{\{X_{3}/c(t,X_{4}),Y_{4}/c(L,nil),% A_{4}/t,Z_{4}/nil\}}}$
	$\displaystyle{yes(c(l,c(i,c(s,X_{3}))),L)\leftarrow\mbox{}append(X_{4},c(L,nil% ),nil)}$

At this point, there are no clauses whose head unifies with the atom in the generalized answer clause’s body. The proof fails.

Choosing the second clause instead of the first gives

	$\displaystyle\ \ \ \ {\hbox{resolve with }append(nil,Z_{5},Z_{5})}$
	$\displaystyle\ \ \ \ {\hbox{substitution: }{\{Z_{5}/c(t,nil),X_{3}/nil,L/t\}}}$
	$\displaystyle{yes(c(l,c(i,c(s,nil))),t)\leftarrow\mbox{}}$

At this point, the proof succeeds, with answer $F=c(l,c(i,c(s,nil)))$ , $L=t$ .

For the rest of this chapter, we use the “syntactic sugar” notation of Prolog for representing lists. The empty list, $n i l$ , is written as $[\,]$ . The list with first element $E$ and the rest of the list $R$ , which was $cons(E,R)$ in Example 13.29 is now written as $[E\mid R]$ . There is one other notational simplification: $[X\mid[Y]]$ is written as $[X,Y]$ , where $Y$ can be a sequence of values. For example, $[a\mid[\,]]$ is written as $[a]$ , and $[b\mid[a\mid[\,]]]$ is written as $[b,a]$ . The term $[a\mid[b\mid C]]$ is written as $[a,b\mid C]$ .

Example 13.33.

Using the list notation, $a p p e n d$ from the previous example can be written as

	$\displaystyle{append([A\mid X],Y,[A\mid Z])\leftarrow\mbox{}}$
	$\displaystyle\ \ \ \ {append(X,Y,Z).}$
	$\displaystyle{append([\,],Z,Z).}$

The query

\mbox{{ask}~{}}~{}append(F,[L],[l,i,s,t])

has an answer $F=[l,i,s]$ , $L=t$ . The proof is exactly as in the previous example. As far as the proof procedure is concerned, nothing has changed; there is just a renamed function symbol and constant.

Artificial Intelligence 2E

13.5.1 Proof Procedures with Function Symbols

Example 13.30.

Example 13.31.

Example 13.32.

Example 13.33.

Artificial
Intelligence 2E