J. A. Robinson

J. A. Robinson introduced the resolution principle in his 1965 paper on machine-oriented logic. His clause-based resolution calculus, using unification, supports a complete refutation procedure for first-order logic: an unsatisfiable clause set has a derivation of the empty clause.^[ref]

For example, resolving $P(x)\vee Q(x)$ with $\neg P(a)$ uses the first-order substitution $x\mapsto a$ and produces $Q(a)$. The rule separates the logical justification of a step from the search for useful clauses. A complete search procedure can still run indefinitely on a satisfiable input; completeness does not supply a decision algorithm for all first-order logic.