Unification lets variables bind to values. Unification also lets structures unify if they have the same functor and the same number of terms, and if their terms can unify. When a query structure wants to prove itself, it can do so by unifying with a fact in the program. For example, the query
starred(jamesCagney, Title, Year)
can prove itself by unifying with the facts in the program in Figure 13.1. If you enter the program and query in Figure 13.1 and then click the Next button, the query unifies with the first fact in the program. The results area displays
Title = Mutiny on the Bounty, Year = 1935.0
This shows that the variables in the query have unified with the values in the program's first fact. The unification succeeds ...