JavaScript: proof by resolution refutation
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.
JavaScript
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);