Inference in First-Order Logic: Unification and Chaining

unifying two atomic sentences:
   Knows(Anil, x)               Knows(Anil, Meera)               {x/Meera}
   Knows(Anil, x)               Knows(y, Bhavna)                 {x/Bhavna, y/Anil}
   Knows(Anil, x)               Knows(y, Mother(y))              {x/Mother(Anil), y/Anil}
   Knows(Anil, x)               Knows(x, Bhavna)                 DO NOT UNIFY
   Knows(Anil, x)               Teaches(Anil, x)                 DO NOT UNIFY
   x                            Mother(x)                        DO NOT UNIFY

the fourth case fails because one name cannot be two people at once, and
the last fails the OCCUR CHECK: x cannot be a term that contains x.

the substitutions above are printed COMPOSED: the algorithm actually
produces {x/Mother(y), y/Anil} on the third case and the composed form,
{x/Mother(Anil), y/Anil}, is what a paper expects to see.

Read the three failures, because each fails for a different reason and papers ask for exactly these.

Row four fails because the same variable appears in both sentences. x would have to be both Anil and Bhavna. The standard repair is standardising apart: rename the variables of one sentence before unifying, so Knows(Anil, x) meets Knows(x1, Bhavna) and unifies to {x1/Anil, x/Bhavna}. Every real implementation does this before every unification attempt, and forgetting it makes correct rules mysteriously fail.

Row five fails because the predicate symbols differ. Knows is not Teaches, and no substitution changes a predicate symbol.

Row six fails the occur check. x cannot be unified with Mother(x), because the substitution would have to replace x inside its own value, giving Mother(Mother(Mother(...))) forever. The check costs time on every unification, and Prolog omits it by default for speed, which is why a Prolog program can be made to loop by unifying a variable with a term containing it.

Generalised modus ponens

The rule that uses unification. Given a rule p1 and p2 and ... implies q, and facts f1, f2, ..., if a substitution s makes each pi identical to some fi, derive q with s applied.

It is one rule doing the work of infinitely many propositional instances. Without it, the first-order rule would have to be propositionalised: instantiated once for every object in the domain, which is impossible if the domain is infinite and merely wasteful if it is large.

Forward and backward chaining, run over the same rules

# Forward and backward chaining over the SAME first-order rule set, so the two
# directions can be compared. The rules are definite clauses with variables.
def is_var(t):
    return isinstance(t, str) and t[0].islower()

def unify(x, y, sub):
    if sub is None:
        return None
    if x == y:
        return sub
    if is_var(x):
        return bind(x, y, sub)
    if is_var(y):
        return bind(y, x, sub)
    if isinstance(x, tuple) and isinstance(y, tuple) and len(x) == len(y):
        for a, b in zip(x, y):
            sub = unify(a, b, sub)
            if sub is None:
                return None
        return sub
    return None

def bind(v, x, sub):
    if v in sub:
        return unify(sub[v], x, sub)
    out = dict(sub)
    out[v] = x
    return out

def sub_in(t, s):
    if isinstance(t, str):
        return sub_in(s[t], s) if t in s else t
    return tuple([t[0]] + [sub_in(p, s) for p in t[1:]])

def show(t):
    if isinstance(t, tuple):
        return "%s(%s)" % (t[0], ", ".join(show(p) for p in t[1:]))
    return t

# "A student who has attended and passed the internal is eligible."
# "An eligible student who passed the external has passed."
RULES = [([("Attended", "s"), ("PassedInternal", "s")], ("Eligible", "s")),
         ([("Eligible", "s"), ("PassedExternal", "s")], ("Passed", "s"))]
FACTS = [("Attended", "Asha"), ("PassedInternal", "Asha"), ("PassedExternal", "Asha"),
         ("Attended", "Vikram"), ("PassedInternal", "Vikram")]

def forward():
    known = list(FACTS)
    print("FORWARD chaining: start from the facts, derive everything")
    for f in FACTS:
        print("   given  ", show(f))
    added = True
    while added:
        added = False
        for premises, conclusion in RULES:
            for sub in match(premises, {}, known):
                new = sub_in(conclusion, sub)
                if new not in known:
                    known.append(new)
                    print("   derive ", show(new), "  from",
                          ", ".join(show(sub_in(p, sub)) for p in premises))
                    added = True
    return known

def match(premises, sub, known):
    """Every substitution making all the premises true against `known`."""
    if not premises:
        yield sub
        return
    first, rest = premises[0], premises[1:]
    for fact in known:
        s = unify(first, fact, dict(sub))
        if s is not None:
            yield from match(rest, s, known)

def backward(goal, known, depth=0):
    """Ask the goal. Print the question before answering it."""
    print("   %sask %s" % ("  " * depth, show(goal)))
    for fact in known:
        if unify(goal, fact, {}) is not None:
            print("   %s  yes, it is a given fact" % ("  " * depth))
            return True
    for premises, conclusion in RULES:
        s = unify(goal, conclusion, {})
        if s is None:
            continue
        print("   %s  try the rule that concludes %s" % ("  " * depth, show(conclusion)))
        if all(backward(sub_in(p, s), known, depth + 1) for p in premises):
            print("   %s  yes" % ("  " * depth))
            return True
    print("   %s  no" % ("  " * depth))
    return False

known = forward()
print()
print("BACKWARD chaining: start from the question")
backward(("Passed", "Asha"), FACTS)
print()
print("and the same question about the student with no external pass:")
backward(("Passed", "Vikram"), FACTS)

FORWARD chaining: start from the facts, derive everything
   given   Attended(Asha)
   given   PassedInternal(Asha)
   given   PassedExternal(Asha)
   given   Attended(Vikram)
   given   PassedInternal(Vikram)
   derive  Eligible(Asha)   from Attended(Asha), PassedInternal(Asha)
   derive  Eligible(Vikram)   from Attended(Vikram), PassedInternal(Vikram)
   derive  Passed(Asha)   from Eligible(Asha), PassedExternal(Asha)

BACKWARD chaining: start from the question
   ask Passed(Asha)
     try the rule that concludes Passed(s)
     ask Eligible(Asha)
       try the rule that concludes Eligible(s)
       ask Attended(Asha)
         yes, it is a given fact
       ask PassedInternal(Asha)
         yes, it is a given fact
       yes
     ask PassedExternal(Asha)
       yes, it is a given fact
     yes

and the same question about the student with no external pass:
   ask Passed(Vikram)
     try the rule that concludes Passed(s)
     ask Eligible(Vikram)
       try the rule that concludes Eligible(s)
       ask Attended(Vikram)
         yes, it is a given fact
       ask PassedInternal(Vikram)
         yes, it is a given fact
       yes
     ask PassedExternal(Vikram)
       no
     no

The difference is in one line of each output. Forward chaining derived Eligible(Vikram), which is of no use whatever to the question "did Asha pass": it was derived because forward chaining derives everything. Backward chaining asking about Asha never mentions Vikram at all.

And the second backward run shows what failure looks like. It works down to PassedExternal(Vikram), finds no fact and no rule concluding it, and reports no, so Passed(Vikram) is not derived. Note what it did not do: it did not conclude that Vikram failed. The query is unanswered, not answered negatively, which is the unknown of The Knowledge-Based Agent.

Choosing between the two directions

The standard fixes for each weakness are worth naming. Forward chaining's irrelevance is reduced by magic sets, which rewrite the rules to be goal-directed. Backward chaining's repetition is removed by memoisation, storing each subgoal's answers, which is what tabled Prolog does.

And backward chaining needs a loop check. Given Ancestor(x, y) implies Ancestor(x, y) or any left-recursive rule, it will ask the same goal forever. The program above is not loop-safe, and a real one keeps the current goal stack and refuses to re-ask a goal already on it.

Resolution in first-order logic, in one paragraph

Conjunctive Normal Form and Resolution generalises to first-order logic, and unification is the only new ingredient. Two clauses resolve when a literal of one and the negation of a literal of the other unify; the resolvent is the remaining literals with the unifier applied.

One extra step is needed to get to clause form: quantifiers must be removed. Universal quantifiers are dropped, since variables in a clause are read as universally quantified anyway. Existential ones are removed by Skolemisation, replacing the existentially quantified variable by a new function of the enclosing universal variables. And first-order resolution can run forever on a non-entailed query, because first-order entailment is only semi-decidable.

Distinctions

What it does not mean

Unification is not pattern matching on strings. It works on the structure of terms and produces a substitution, and it can fail for three distinct reasons.

The MGU is not "the first unifier found". It is the least committed one, and returning a more specific unifier loses answers.

Failure to unify does not mean the sentences are inconsistent. Knows(Anil, x) and Knows(x, Bhavna) fail only because of a shared variable name, and standardising apart makes them unify.

Forward chaining is not the opposite of backward chaining in correctness. Both are sound and both are complete for definite clauses. They differ in what work they do.

Backward chaining failing does not mean the query is false. It means it does not follow. Concluding otherwise is the closed-world assumption, which is an extra assumption and not a consequence of the logic.

Dropping the occur check is not free. It makes unification faster and allows a program to build an infinite term and hang.

Quick revision

• Substitution: a map from variables to terms, {x/Meera}. Unification finds one making two atomic sentences identical; the most general unifier commits to the fewest variables and is unique up to renaming.
• Unification fails for three reasons: different predicate or function symbols; a shared variable name, repaired by standardising apart; and the occur check, a variable against a term containing it.
• Generalised modus ponens: if a substitution makes a rule's premises match known facts, derive the conclusion with that substitution. One rule replaces infinitely many propositional instances, and works on an infinite domain where propositionalising cannot.
• Forward chaining is data driven and derives everything, including Eligible(Vikram) when the question was about Asha. Backward chaining is goal driven and never mentions Vikram.
• Forward chaining wastes work on irrelevance, fixed by magic sets. Backward chaining repeats subgoals, fixed by memoisation, and needs a loop check on recursive rules.
• Failure of backward chaining means unknown, not false.
• First-order resolution is the propositional rule plus unification, after quantifiers are removed: universals dropped, existentials by Skolemisation. It can run forever on a non-entailed query.

Test yourself

1. Define a substitution, a unifier and the most general unifier. A substitution maps variables to terms. A unifier of two sentences is a substitution that makes them identical. The most general unifier is the unifier that constrains the fewest variables, and it is unique up to the renaming of variables.

2. Give three reasons two atomic sentences may fail to unify. Their predicate or function symbols differ, and no substitution changes a symbol. The same variable name occurs in both sentences and would have to take two values, which is repaired by standardising apart. Or the occur check fails, because a variable would have to be bound to a term containing itself.

3. What is standardising apart and why is it necessary? Renaming the variables of one sentence before attempting to unify, so that a shared variable name does not defeat a legitimate match. Knows(Anil, x) and Knows(x, Bhavna) do not unify as written, and do unify once the second is renamed.

4. State generalised modus ponens and say what it replaces. Given a rule whose premises unify with known facts under a substitution, derive the rule's conclusion with that substitution applied. It replaces propositionalising the rule, that is instantiating it once for every object in the domain, which is impossible on an infinite domain.

5. In this chapter's run, what did forward chaining derive that backward chaining never touched, and why? Eligible(Vikram). Forward chaining derives every consequence of the facts, whether or not it bears on any question. Backward chaining asking whether Asha passed only ever asks about Asha.

6. Backward chaining reported "no" for Passed(Vikram). What exactly does that establish? That Passed(Vikram) does not follow from the knowledge base, because no fact asserts it and no applicable rule succeeds. It does not establish that Vikram failed; that would require the closed-world assumption, which is an extra assumption beyond the logic.

7. What must be done to first-order sentences before resolution can be applied, and what is the extra step called? They must be put in clause form, which requires removing the quantifiers. Universal quantifiers are simply dropped, since variables in a clause are read as universally quantified. Existential quantifiers are removed by Skolemisation, replacing the existentially quantified variable with a new function of the enclosing universally quantified variables.