Resolution is a single inference rule that is complete for propositional logic when used for proof by contradiction. For the restricted but common Horn clause form, forward and backward chaining are simpler and run in linear time.

Converting to CNF

Resolution works on conjunctive normal form (CNF): a conjunction of clauses, each a disjunction of literals. Any sentence can be converted:

Eliminate ⇔
α ⇔ β → (α ⇒ β) ∧ (β ⇒ α)
Eliminate ⇒
α ⇒ β → ¬α ∨ β
Move ¬ inwards
De Morgan and double negation until ¬ applies only to symbols
Distribute ∨ over ∧
α ∨ (β ∧ γ) → (α ∨ β) ∧ (α ∨ γ)

Resolution refutation

To prove α: add ¬α to the KB's clauses and resolve pairs of clauses with complementary literals. Deriving the empty clause (a contradiction) proves KB ⊨ α; if no new clauses can be produced, α is not entailed.

Python

from itertools import combinations

def resolve(a, b):
    out = []
    for lit in sorted(a):
        neg = lit[1:] if lit.startswith("~") else "~" + lit
        if neg in b:
            out.append((a - {lit}) | (b - {neg}))
    return out

def resolution(clauses, query):
    neg = query[1:] if query.startswith("~") else "~" + query
    clauses = set(clauses) | {frozenset([neg])}              # add the negated goal
    derived = []
    while True:
        new = set()
        for a, b in combinations(sorted(clauses, key=sorted), 2):
            for r in resolve(a, b):
                if not r:
                    return True, derived                     # empty clause: contradiction
                if r not in clauses and r not in new:
                    new.add(frozenset(r))
                    derived.append(sorted(r))
        if not new:
            return False, derived                            # nothing new: not entailed
        clauses |= new

# KB:  P ⇒ Q,  Q ⇒ R,  P       as clauses: {¬P, Q}, {¬Q, R}, {P}
kb = [frozenset({"~P", "Q"}), frozenset({"~Q", "R"}), frozenset({"P"})]
proved, derived = resolution(kb, "R")
print(proved, derived)          # True [['Q'], ['R', '~P'], ['~Q'], ['R']]
print(resolution(kb, "~R")[0])  # False ← R is entailed, so ¬R is not

Horn clauses, forward and backward chaining

The textbook KB: P ⇒ Q, L ∧ M ⇒ P, B ∧ L ⇒ M, A ∧ P ⇒ L, A ∧ B ⇒ L, and facts A, B.

Python

RULES = [(["P"], "Q"), (["L", "M"], "P"), (["B", "L"], "M"), (["A", "P"], "L"), (["A", "B"], "L")]
FACTS = ["A", "B"]

def forward_chain(rules, facts, query):
    known, agenda, order = set(), list(facts), []
    count = {i: len(prem) for i, (prem, _) in enumerate(rules)}    # unsatisfied premises per rule
    while agenda:
        p = agenda.pop(0)
        if p in known:
            continue
        known.add(p)
        order.append(p)
        if p == query:
            return True, order
        for i, (prem, concl) in enumerate(rules):
            if p in prem:
                count[i] -= 1
                if count[i] == 0:                                   # all premises known → fire
                    agenda.append(concl)
    return False, order

def backward_chain(rules, facts, goal, seen=()):
    if goal in facts:
        return True
    if goal in seen:                                                # avoid looping on P ⇒ … ⇒ P
        return False
    return any(all(backward_chain(rules, facts, g, seen + (goal,)) for g in prem)
               for prem, concl in rules if concl == goal)

print(forward_chain(RULES, FACTS, "Q"))     # (True, ['A', 'B', 'L', 'M', 'P', 'Q'])
print(backward_chain(RULES, FACTS, "Q"))    # True
print(backward_chain(RULES, FACTS, "Z"))    # False ← no rule concludes Z

	Forward chaining	Backward chaining
Direction	Data-driven: from known facts to all consequences	Goal-driven: from the query back to facts
Fires	Every rule whose premises become true	Only rules relevant to the goal
Good for	Monitoring, reacting to new data, deriving everything	Answering specific questions
Cost	May derive many irrelevant facts	Often much less than linear in KB size
Used in	Production systems, expert-system shells (CLIPS), Datalog	Prolog, diagnostic systems (MYCIN)

Explain resolution refutation.

Forward vs backward chaining — when to use which?

What is a Horn clause and why does it matter?