Resolution Algorithm (Propositional Resolution)

propositional-logic

Definition

Resolution Algorithm

The resolution algorithm decides whether a set of formulas entails a formula by applying the propositional resolution calculus to

By the entailment–unsatisfiability duality, holds exactly when this formula is unsatisfiable.

Procedure

Let be the set obtained from by adding every resolvent of clauses in , 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 . If it returns false, then .