Resolution

Resolution is an inference rule which is valid in a number of commonly-used classical logics, including propositional logic and first-order logic.

In particular, resolution applies to clauses of the form

	A_1 \lor \dots \lor A_n

where each A_i is a literal, i.e. either an atomic formula or its negation.

The rule itself is

\frac{
  a_1 \lor \ldots \lor a_n \lor p
  \qquad
  b_1 \lor \ldots \lor b_m \lor \lnot p
}{
  a_1 \lor \ldots \lor a_n \lor b_1 \lor \ldots \lor b_m
}

Refutation-completeness for propositional logic

The resolution rule is refutation-complete for classical propositional logic.

In more detail, let there be a set of clauses

  \phi_i = a_1 \lor \ldots \lor a_{n_i}

where each a_i is a literal. If the formula \bigwedge_i \phi_i is unsatisfiable, then you can prove the empty clause (consisting just of the unit of \lor, namely falsity \bot) starting from the \phi_i's and applying just the resolution rule.

A proof of this theorem may be found in section 1.5 of Schöning, 2008.

Thus, to prove \Gamma \vdash \phi using resolution, you must derive the empty clause from \Gamma \land \lnot \phi (after converting every formula in \Gamma and \phi to resolution-clause form of course).

Relationship to the cut rule

If we use the classical equivalence

  P \to Q \equiv \lnot P \lor Q

we may rewrite the resolution rule as

\frac{
  (\lnot a_1 \land \ldots \land \lnot a_n) \to p
  \qquad
  p \to (b_1 \lor \ldots \lor b_m)
}{
  a_1 \lor \ldots \lor a_n \lor b_1 \lor \ldots \lor b_m
}

which shows that there is a deep relationship between resolution and the cut rule.

References

• A "modern classic" textbook presentation of resolution can be found in the book

BibTeX

@book{schoning_2008,
	address = {Boston, MA},
	title = {Logic for {Computer} {Scientists}},
	publisher = {Birkhäuser Boston},
	author = {Schöning, Uwe},
	year = {2008},
	doi = {10.1007/978-0-8176-4763-6},
}

• The resolution rule appears to be (unsurprisingly) due to Davis and Putnam. It seems to have first appeared in a 1960 JACM paper:

@article{10.1145/321033.321034,
	author = {Davis, Martin and Putnam, Hilary},
	title = {A Computing Procedure for Quantification Theory},
	year = {1960},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {7},
	number = {3},
	url = {https://doi.org/10.1145/321033.321034},
	doi = {10.1145/321033.321034},
	journal = {Journal of the ACM},
	pages = {201–215},
}