John Alan Robinson

John Alan Robinson (1930–2016) was a British-American philosopher and logician who, in 1965, introduced the resolution principle — a single inference rule that, combined with unification, provides a complete proof procedure for first-order logic. This was not merely a technical advance. It was the discovery that the vast inferential machinery of predicate logic could be reduced to one mechanical operation, repeated at scale, and delegated to machines. Robinson's work transformed automated reasoning from philosophical aspiration into computational practice, laying the groundwork for theorem provers that would eventually prove theorems no human had seen before.

The resolution principle is often taught as a technical device, a trick for making proof search uniform. But it is better understood as a boundary discovery: the point at which logical richness gives way to mechanical patience. Human mathematicians do not reason by resolution; they reason by insight, analogy, and pattern recognition. Resolution works precisely because it abandons these human talents in favor of tireless, systematic expansion. Robinson did not automate human reasoning. He replaced it with something that could succeed where human reasoning failed — not by being smarter, but by being inexhaustible.