Full text of the second edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2017 is now available.

### 12.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 12.29:**To see why fairness is important, consider the following clauses as part of a larger program:

*num(0).*

*num(s(N))←num(N).*

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 any other clauses and thus never derives the consequences of these other clauses.

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 is complete only if it is fair.

The top-down proof procedure is the same as for Datalog [see
Figure 12.3]. 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 12.30:**Consider the knowledge base with only one clause:

lt(X,s(X)).

Suppose the intended interpretation is the domain of integers in which *lt* means "less than" and *s(X)* denotes the integer after *X*.
The query * ask lt(Y,Y)* should fail because it is

*false*in our intended interpretation that 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 12.5 finds the MGU of two terms with function symbols with one
change. The algorithm should return *⊥* if it selects an equality
*x=y*, where *x* is a variable and *y* is a term that is not *x*, but
contains *x*. This last 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 makes the proof
procedure unsound.

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

**Example 12.31:**Consider the clauses

*append(c(A,X),Y,c( A,Z))←*

*append(X,Y,Z).*

*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:

askappend(F,c(L,nil),c(l,c(i,c(s,c(t,nil))))).

The following is a derivation:

*yes(F,L)←append(F,c(L,nil),c(l,c(i,c(s,c(t,nil)))))*

*resolve with append(c(A*

_{1},X_{1}),Y_{1},c( A_{1},Z_{1}))←append(X_{1},Y_{1},Z_{1})*substitution: {F/c(l,X*

_{1}), Y_{1}/c(L,nil), A_{1}/l ,Z_{1}/c(i,c(s,c(t,nil)))}*yes(c(l,X*

_{1}),L)←append(X_{1},c(L,nil),c(i,c(s,c(t,nil))))*resolve with append(c(A*

_{2},X_{2}),Y_{2},c( A_{2},Z_{2}))←append(X_{2},Y_{2},Z_{2})*substitution: {X*

_{1}/c(i,X_{2}), Y_{2}/c(L,nil), A_{2}/i ,Z_{2}/c(s,c(t,nil))}*yes(c(l,c(i,X*

_{2})),L)←append(X_{2},c(L,nil),c(s,c(t,nil)))*resolve with append(c(A*

_{3},X_{3}),Y_{3},c( A_{3},Z_{3}))←append(X_{3},Y_{3},Z_{3})*substitution: {X*

_{2}/c(s,X_{3}), Y_{3}/c(L,nil), A_{3}/s ,Z_{3}/c(t,nil)}*yes(c(l,c(i,c(s,X*

_{3}))),L)←append(X_{3},c(L,nil),c(t,nil))At this stage both clauses are applicable. Choosing the first clause gives

*resolve with append(c(A*

_{4},X_{4}),Y_{4},c( A_{4},Z_{4}))←append(X_{4},Y_{4},Z_{4})*substitution: {X*

_{3}/c(t,X_{4}), Y_{4}/c(L,nil), A_{4}/t ,Z_{4}/nil}*yes(c(l,c(i,c(s,X*

_{3}))),L)←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

*resolve with append(nil,Z*

_{5},Z_{5}).*substitution: {Z*

_{5}/c(t,nil),X_{3}/nil,L/t}*yes(c(l,c(i,c(s,nil))),t)←*

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, *nil*, is written as
*[]*. The list with first element *E* and the rest of the list *R*,
which was *cons(E,R)*,
is now written as *[E|R]*. There is one notational simplification:
*[X|[Y]]* is written as *[X,Y]*, where *Y* can be a sequence of
values. For example, *[a|[]]* is written as *[a]*, and *[b|[a|[]]]*
is written as *[b,a]*; *[a|[b|c]]*
is written as *[a,b|c]*.

**Example 12.32:**Using the list notation,

*append*from the previous example can be written as

*append([A|X],Y,[A|Z])←*

*append(X,Y,Z).*

*append( [],Z,Z).*

The query

askappend(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.