CSCE 420 Lecture 18

« previous | Tuesday, March 26, 2013 | next »

The Unification Algorithm

function Unify(x,y,θ) returns a substitution to make x and y identical
    inputs: x - a variable, constant, list, or compound
            y - a variable, constant, list, or compound
            θ - the substitution built up so far
    if θ = failure then return failure
    else if x = y then return θ
    else if Variable?(x) then return Unify-Var(x,y,θ)
    else if Variable?(y) then return Unify-Var(y,x,θ)
    else if Compound?(x) and Compound?(y) then
        return Unify(Args[x], Args[y], Unify(Op[x], Op[y], θ))
    else if List?(x) and List?(y) then
        return Unify(Rest[x], Rest[y], Unify(First[x],First[y], θ))
    else return failure
    end if
end function

Forward Chaining

function FOL-FC-Ask(KB, α) returns a substitution or false
    repeat until new is empty
        new := {}
        for each sentence r in KB do
            (p1 ∧ … ∧ pn ⇒ q) := Standardize-Apart(r)
            for each θ such that (p1 ∧ … ∧ pn) θ = (p1' ∧ … ∧ pn') θ for some p1', …, pn' in KB
                q' := Subst(θ, q)
                if q' is not a renaming of a sentence already in KB or new then do
                    add q' to new
                    φ := Unify(q', α)
                    if φ is not fail then return φ
                end if
            end for
        end for
        add new to KB
    end repeat
    return false
end function

only applies to Horn-Clause KB's using Generalized Modus Ponens

Rete algorithm:

• represents facts as a network (directed acyclic graph)
• Hashing for efficiently determining which rules can fire
• Many expert systems use forward chaining (a.k.a. production systems); also include:
  • explanation facilities: explains the "why?" behind results (just show proof tree)
  • uncertainty management: handling cases where data may be incomplete

Resolution Refutation

Same rules apply as in propositional logic:

• Based on Generalized Resolution inference rule.
• Negate query
• Convert KB to CNF
• Choosing clauses to resolve until empty clause is derived; heuristics:
  • Unit clause: pick clauses that can be resolved, where one clause has a single literal to shrink size of other clause
  • Input Resolution: at least one clause must come from original set (reduce irrelevant clauses)

Completeness

Completeness of Resolution Refutation in First-Order Logic is 'semi-decidable:

• If $\alpha \models \beta$, then it can be proved by Resolution refutation
• If $\alpha \not \models \beta$, then no finite proof exists

Ground Resolution Theorem: For a set of unsatisfiable ground/propositional sentences, there always is a finite derivation of the empty clause.

Herbrand's Theorem: For a set of unsatisfiable first-order logic sentences, there is a finite set of ground sentences that is unsatisfiable

Lifting Lemma (not given in class)

Backward Chaining

Restricted to Horn-Clause KB's

Uses goal stack data structure to keep track of what needs to be proved to support query:

KB = { A, B, D, A ∧ B → C, C ∧ D → E }
KB ⊧? E

Goal Stack:
  { E } pop top
  { C, D } push antecedents
  { D } pop top
  { A, B, D } push antecedents
  { B, D } pop top; known fact
  { D } pop top; known fact
  { } pop top; known fact

Potential choice points could be other rules to prove E or C (i.e. multiple rules that imply E or C). May have to backtrack to the most recent choice point if chosen decision method doesn't work.

function FOL-BC-Ask(KB, goals, θ) returns set of substitutions
    inputs: KB    - a knowledge base
            goals - a list of conjuncts forming a query
            θ     - the current substitution, initially the empty substitution {}
    local:  ans   - a set of substitutions, initially empty {}

    if goals is empty then return {θ}
    q' := Subst(θ, First(goals))
    for each r in KB where Standardize-Apart(r) = (p1 ∧ … ∧ pn ⇒ q) and θ' := Unify(q, q') succeeds
        ans := FOL-BC-Ask(KB, [p1, …, pn|Rest(goals)], Compose(θ,θ')) ∪ ans
    end for
    return ans
end function

For example,

KB = { ∀ x dog(x) → barks(x), dog(fido) }
KB ⊧? barks(fido)

Unifier        Goal Stack
-------        ----------
{ }            { barks(fido) }
{ x/fido }     { dog(fido) }
               { }

Backward chaining has particular advantages:

• more efficient than forward chaining
• only derives inference relative to query
• no risk of generating irrelevant consequences

Thus B.C. is he basis of Prolog (a logic programming language; c.f. object-oriented, functional, and procedural)