Backward chaining & DFS inference trees over rules

Backward chaining is and/or DFS over rules

To prove a goal backward, you search an and/or graph:

- or-nodes — choosing among the rules whose *conclusion* matches the goal. Any one succeeding proves the goal. - and-nodes — a chosen rule's *premises*. All must be proved for the rule to fire.

A goal succeeds if it is a known fact, or if some rule concludes it and all that rule's premises succeed (recursively). The search is depth-first: try the first matching rule fully — diving into its premises — before trying the next. Number the rules in the order you *try* them and you get the inference tree the exam asks for.

Worked example — exam Q6

Rules (exactly as on the exam):

- 1: raining ∧ cold → playground_empty - 2: playing_videogame → kids_not_outside - 3: kids_not_outside → kids_videogame_or_school - 4: not_school_day → kids_outside_or_videogame - 5: kids_not_outside → playground_empty

Facts: not_school_day, playing_videogame. Goal: playground_empty.

Depth-first trial (rules tried in number order):

1. Goal playground_empty. Rule 1 concludes it → try rule 1. Premises raining, cold — neither is a fact and no rule concludes them → rule 1 fails, backtrack.
2. Rule 5 also concludes playground_empty → try rule 5. Premise kids_not_outside (a subgoal).
3. Subgoal kids_not_outside. Rule 2 concludes it → try rule 2. Premise playing_videogame — a fact. Rule 2 succeeds → kids_not_outside proved → rule 5 succeeds → playground_empty proved.

The trial order is 1, 5, 2 (rule 1 tried and abandoned), and the proof uses rules 2 then 5. Showing the *failed* branch (rule 1) is the whole point of "draw the DFS tree and number the trial sequence."