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
where each is a literal, i.e. either an atomic formula or its negation.
The rule itself is
The resolution rule is refutation-complete for classical propositional logic.
In more detail, let there be a set of clauses
where each is a literal. If the formula is unsatisfiable, then you can prove the empty clause (consisting just of the unit of , namely falsity ) starting from the '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 using resolution, you must derive the empty clause from (after converting every formula in and to resolution-clause form of course).
If we use the classical equivalence
we may rewrite the resolution rule as
which shows that there is a deep relationship between resolution and the cut rule.
Schöning, Uwe. 2008. Logic for Computer Scientists. Boston, MA: Birkhäuser Boston. https://doi.org/10.1007/978-0-8176-4763-6.
@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},
}
Martin Davis and Hilary Putnam. 1960. A Computing Procedure for Quantification Theory. J. ACM 7, 3 (July 1960), 201–215. https://doi.org/10.1145/321033.321034
@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},
}