JavaScript: proof by resolution refutation

Show that a knowledge base entails a query by deriving a contradiction from the knowledge base plus the negated query.

const show = (clause) => (clause.size === 0 ? "empty" : [...clause].sort().join(" v "));

function resolvents(c1, c2) {
  const out = [];
  for (const literal of c1) {
    const negation = literal.startsWith("~") ? literal.slice(1) : "~" + literal;
    if (c2.has(negation)) {
      const merged = new Set([...c1, ...c2]);
      merged.delete(literal);
      merged.delete(negation);
      out.push(merged);
    }
  }
  return out;
}

const clauses = [
  new Set(["A", "B"]),
  new Set(["~A", "C"]),
  new Set(["~B", "C"]),
  new Set(["~C"]),
];
const known = new Set(clauses.map(show));
let proved = false;

for (let i = 0; i < clauses.length && !proved; i++) {
  for (let j = 0; j < i && !proved; j++) {
    for (const r of resolvents(clauses[i], clauses[j])) {
      if (known.has(show(r))) continue;
      known.add(show(r));
      clauses.push(r);
      console.log("derived " + show(r));
      if (r.size === 0) proved = true;
    }
  }
}
console.log("KB entails C: " + proved);

derived B v C
derived A v C
derived ~A
derived ~B
derived C
derived B
derived A
derived empty
KB entails C: true

Explanation

Resolution is an inference rule for clauses, which are disjunctions of literals. From (A or B) and (not A or C) it derives (B or C), because whichever way A is resolved one of the other literals must hold. A knowledge base entails a query if adding the negation of the query makes the clauses contradictory, which means the empty clause can be derived.

The knowledge base says A or B, A implies C (not A or C), and B implies C (not B or C). To prove C, the program adds not-C and resolves pairs of clauses until it finds the empty clause. Each new clause is kept only once. Because the number of possible clauses is finite, the process terminates, with the empty clause if the query is entailed.

—

—

—

derived B v C
derived A v C
derived ~A
derived ~B
derived C
derived B
derived A
derived empty

derived B v C
derived A v C
derived ~A
derived ~B
derived C
derived B
derived A
derived empty
KB entails C: true

Cost and common mistakes

Exponential in the worst case, since the number of possible clauses is 3^n for n symbols.

• Resolution works on clauses, so sentences must first be converted to conjunctive normal form.
• The search can generate many useless clauses. Practical provers use strategies such as unit preference and set of support.
• A resolvent that contains both p and not p is a tautology and should be discarded in a full implementation.

Try it yourself

What happens if the query is A instead of C?

Further reading

• MDN JavaScript guide (external)
• Node.js API documentation (external)
• Artificial Intelligence: A Modern Approach (Russell, Norvig) (external)