Resolution Algorithm (Propositional Resolution)

propositional-logic

Definition

Resolution Algorithm

The resolution algorithm decides whether a set of formulas $KB=\{Q_1,\dots ,Q_n\}$ entails a formula $P$ by applying the propositional resolution calculus to

$$Q_1\wedge \cdots \wedge Q_n\wedge \neg P.$$

By the entailment–unsatisfiability duality, $KB\models P$ holds exactly when this formula is unsatisfiable.

Procedure

Let $\mathrm{Res}(S)$ be the set obtained from $S$ by adding every resolvent of clauses in $S$, up to factoring.

Bool ResolutionEntails(Set Formula KB, Formula P)
	F = to_cnf(conjunction(KB) ∧ ¬P);
	S = clauses(F);
	Old = ∅;
	while (□ ∉ S && S ≠ Old) {
	    Old = S;
	    S = Res(S);
	}
	return □ ∈ S;

Result

Termination

The algorithm terminates because there are only finitely many clauses over the atoms occurring in the input formula.

If the algorithm returns true, then $KB\models P$. If it returns false, then $KB/\models P$.