Resolution

A Calculus $\mathcal{R}_0$ that operates on Clause sets via a single Inference Rule:

This rule allows to add the lower clause (called resolvent) to a clause set which contains the two clauses above.

The Literals $P^T$ and $P^F$ are called cut literals.

Resolution Refutation

Clause Normal Form CNF