| 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 because the query and the fact have the same functor ( starred ) and the same number of terms (three), and their terms can unify. Specifically, the atom jamesCagney in the query unifies with its counterpart in the fact because both structures have the same functor ( jamesCagney ) and the same number of terms (zero). The variables in the query unify with their counterparts by binding to them. After the query proves itself, the environment displays the query's variables. If you press Next again, the query unbinds its variables and unifies with the next fact in the program. The results area displays Title = Yankee Doodle Dandy, Year = 1942.0 By pressing the Rest button, you can ask the query to prove itself until no more proofs exist. The results are Title = Ragtime, Year = 1981.0 Title = Yankee Doodle Dandy, Year = 1942.0 no The results area displays no when there is no further proof of a query. | 
