foundations of computational agents
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.
To see why fairness is important, consider the following clauses:
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 or .
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 does not unify with a term in which occurs and is not 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.
Consider the knowledge base with only one clause:
Suppose the intended interpretation is the domain of integers in which means “less than” and denotes the integer after . The query should fail because it is false in the intended interpretation; there is no number less than itself. However, if and 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 if it selects an equality , where is a variable and is a term that is not , but contains (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.
Consider the clauses
For now, ignore what this may mean. Like the computer, treat this as a problem of symbol manipulation. Consider the following query:
The following is a derivation:
At this stage both clauses are applicable. Choosing the first clause gives
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
At this point, the proof succeeds, with answer , .
For the rest of this chapter, we use the “syntactic sugar” notation of Prolog for representing lists. The empty list, , is written as . The list with first element and the rest of the list , which was in Example 13.29 is now written as . There is one other notational simplification: is written as , where can be a sequence of values. For example, is written as , and is written as . The term is written as .
Using the list notation, from the previous example can be written as
has an answer , . 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.