FOL-FC-Ask.md

FOL-FC-ASK

AIMA3e

function FOL-FC-ASK(KB, α) returns a substitution or false
 inputs: KB, the knowledge base, a set of first order definite clauses
     α, the query, an atomic sentence
 local variables: new, the new sentences inferred on each iteration

 repeat until new is empty
   new ← { }
   for each rule in KB do
     (p₁ ∧ ... ∧ p_n ⇒ q) ← STANDARDIZE-VARAIBLES(rule)
     for each θ such that SUBST(θ, p₁ ∧ ... ∧ p_n) = SUBST(θ, p'₁ ∧ ... ∧ p'_n)
          for some p'₁ ∧ ... ∧ p'_n in KB
       q' ← SUBST(θ, q)
       if q' does not unify with some sentence already in KB or new then
         add q' to new
         Φ ← UNIFY(q', α)
         if Φ is not fail then return Φ
   add new to KB
 return false

---

Figure ?? A conceptually straightforward, but very inefficient forward-chaining algorithm. On each iteration, it adds to KB all the atomic sentences that can be inferred in one step from the implication sentences and the atomic sentences already in KB. The function STANDARDIZE-VARIABLES replaces all variables in its arguments with new ones that have not been used before.