The resolution principle
Robinson reduced proof in first-order logic to a single inference rule fit for a machine.
Why it matters
Automatic theorem proving became feasible, and later turned into logic programming.
The key part is the unification algorithm, which finds the most general substitution for two expressions. The method works by refutation: the negation of the goal is added to the set of statements and a contradiction is sought. Prolog in 1972 is built on a restricted form of the same mechanism.