function FOL-BC-ASK(KB, query) returns a generator of substitutions
return FOL-BC-OR(KB, query, { })
generator FOL-BC-OR(KB, goal, θ) yields a substitution
for each rule (lhs ⇒ rhs) in FETCH-RULES-FOR-GOAL(KB, goal) do
(lhs, rhs) ← STANDARDIZE-VARIABLES((lhs, rhs))
for each θ' in FOL-BC-AND(KB, lhs, UNIFY(rhs, goal, θ)) do
yield θ'
generator FOL-BC-AND(KB, goals, θ) yields a substitution
if θ = failure then return
else if LENGTH(goals) = 0 then yield θ
else do
first, rest ← FIRST(goals), REST(goals)
for each θ' in FOL-BC-OR(KB, SUBST(θ, first), θ) do
for each θ'' in FOL-BC-AND(KB, rest, θ') do
yield θ''
Figure ?? A simple backward-chaining algorithm for first-order knowledge bases.