= J. A. Robinson
{c}
<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>.<A Machine-Oriented Logic Based on the Resolution Principle by J. A. Robinson>[resolution principle and §§5.3–5.9, unification]{ref}
For example, resolving $P(x)\lor 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 <clause>[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>.
Back to article page
