Exercise 9.16

In this exercise, use the sentences you wrote in Exercise fol-horses-exercise to answer a question by using a backward-chaining algorithm.

1. Draw the proof tree generated by an exhaustive backward-chaining algorithm for the query ${\exists\,h\;\;}{Horse}(h)$, where clauses are matched in the order given.

3. How many solutions for $h$ actually follow from your sentences?