Logic Goal Trees: Backward Chaining, DFS, Substitution

1. Rules in two tables

Prolog form	How to read it
dinnerPlan(X) :- restaurant(X), friendLikes(X).	Consequent FIRST, antecedents after. X is a dinner plan if X is a restaurant and the friend likes X. Uppercase = variable (substitutable); lowercase = constant (fixed).
Goal set {A, B, C}	Goals still to prove. Expanding A by a rule replaces it with the rule body; matching a fact deletes it. Empty set = solved.
Backward chaining	Match the goal against rule consequents and fact heads, moving from goal toward facts (the reverse of forward chaining).

DFS rule	What happens
Leftmost goal, leftmost clause, leftmost fact	Always expand the first goal in the set, try rules top to bottom, facts top to bottom. Clause and fact order decides everything.
Unification (substitution)	Binding a variable, e.g. \(X = beach\), rewrites every later goal containing X. One variable, one value at a time.
Backtrack on failure	A goal with no match fails: undo the latest binding and try the next fact, then the next rule. Untried branches right of a success stay untried.
Solution = subtree + substitution	The proof is the successful root-to-facts path (an AND-OR solution subtree); the answer is the final variable binding.

2. The three checks while tracing

Expand leftmost: write the goal set at each step and underline the goal you expand. AND goals fan out below their parent; OR alternatives sit left to right in clause order.
Bind leftmost: the first fact whose head matches binds the variable. Later goals use the bound value, never the variable.
Fail fast, backtrack once: the moment a ground goal (no variables) is absent from the facts, mark FAIL, drop that binding, and resume at the nearest untried alternative. Never reorder goals to dodge a failure.

3. Worked example: evening out (beach, Matrix, Saravana Bhavan)

3a. Knowledge base as tables (solve from this, then check the walkthrough)

Rule	Prolog clause
R0	outingPlan(X,Y,Z) :- eveningPlan(X), moviePlan(Y), dinnerPlan(Z).
R1	eveningPlan(X) :- outing(X), friendLikes(X).
R2	moviePlan(Y) :- movie(Y), friendLikes(Y).
R3	dinnerPlan(Z) :- restaurant(Z), friendLikes(Z).

Facts, top to bottom	Entries in order
outing / movie / restaurant	outing: mall, beach. movie: matrix. restaurant: pizzaHut, saravanaBhavan.
friendLikes	beach, matrix, bhuvanShome, saravanaBhavan. (No mall, no pizzaHut: those branches must fail.)

Query: ?- outingPlan(X,Y,Z). Cover the walkthrough. Expand leftmost, bind leftmost, backtrack on failure.

3b. Walkthrough: goal set plus substitution at every step

Step 0 | filled chip = current goal, struck chip = proved, dashed chip = failed; tracker holds the substitution

Why this step

Tracker (goals + substitution)

3c. The three questions

Knowledge base and query as above. Depth-first, leftmost-first search.

List the expanded nodes in order, marking each FAIL and backtrack.
What is the solution substitution for X, Y, Z?
Give the solution path from the query to the facts.

3d. Answers first, then the working

Expanded: outingPlan, eveningPlan, outing(mall) FAIL, outing(beach), moviePlan, movie(matrix), dinnerPlan, restaurant(pizzaHut) FAIL, restaurant(saravanaBhavan) (friendLikes checks ride along each binding). Substitution: X=beach, Y=matrix, Z=saravanaBhavan. Path: outingPlan - eveningPlan - beach; moviePlan - matrix; dinnerPlan - saravanaBhavan.

X=mall dies at friendLikes(mall). outing(mall) matches, but the rewritten goal friendLikes(mall) is no fact: FAIL, undo X=mall, backtrack to the next outing.
X=beach survives both subgoals (outing(beach), friendLikes(beach)), so the goal set shrinks to moviePlan(Y), dinnerPlan(Z) with \(X = beach\) fixed.
Y=matrix is first-try success (movie(matrix), friendLikes(matrix)). Nothing forces a second movie branch: DFS stops exploring after success.
Z=pizzaHut dies at friendLikes(pizzaHut): FAIL, backtrack to restaurant(saravanaBhavan), both subgoals hold, goal set empties: solved with \(X = beach, Y = matrix, Z = saravanaBhavan\).

4. Second trace: nice toy (backtrack across rules)

Rules: R1: niceToy(X) :- green(X), circle(X). R2: niceToy(X) :- red(X), square(X). Facts: green: A, B. circle: C, E. red: C, D. square: D. Query: ?- niceToy(X). Use the Nice toy tab above, then read the answers.

Expanded: niceToy, green(A), circle(A) FAIL, green(B), circle(B) FAIL, red(C), square(C) FAIL, red(D), square(D). Rule 1 exhausts both greens before rule 2 is ever tried. Substitution: X=D. Path: niceToy - rule 2 - red(D) - square(D). The C failure is the classic trap: C matches red but is a circle, not a square.

5. Practice: two drills

Solve each with a pen before opening the answer. Each drill is self contained.

Drill L1: shared variable must agree

Facts: p(a), p(b), q(b), q(c). Rule: r(X) :- p(X), q(X). Query: ?- r(X). Q1: expansion order? Q2: substitution?

Step 0

Why this step

Tracker

Answer L1

Expanded: r(X), p(a), q(a) FAIL, p(b), q(b). X=a dies because q(a) is no fact; the same X must satisfy both subgoals. Substitution: X=b. Path: r - p(b) - q(b).

Drill L2: second rule saves the proof

Facts: a, c. Rules: g :- a, b. and g :- c. Query: ?- g. Q1: expansion order? Q2: solution path?

Step 0

Why this step

Tracker

Answer L2

Expanded: g, a, b FAIL (no fact b), c. First rule dies on b; backtrack to the second rule, c holds, goal set empties. Path: g - rule 2 - c. No variables, so the solution is the proof itself.

6. Exam checklist (write this on the rough sheet)

Copy facts top to bottom exactly as given. Order decides the trace.
Leftmost goal, leftmost rule, leftmost fact. Write the goal set fresh at every step.
Apply each binding to all later goals before matching them.
Ground goal absent from facts means FAIL: undo one binding, take the next alternative.
A shared variable must take one value across all subgoals (drill L1).
Solution = final substitution; path = successful root-to-facts branches only.