Textbook of AI

1930–2016, Mathematical logician

Also known as: John Alan Robinson, Alan Robinson

John Alan Robinson was an English-American philosopher and logician whose 1965 paper A Machine-Oriented Logic Based on the Resolution Principle introduced the resolution rule, a single inference rule that subsumes modus ponens, syllogism and many others, and is complete for first-order predicate logic. Resolution gave automated theorem proving a uniform, mechanical proof procedure for the first time and remains the basis of every general-purpose first-order theorem prover built since.

Resolution requires that formulas first be converted to clausal normal form (a conjunction of disjunctions of literals); the rule then says that from clauses (A ∨ B) and (¬A ∨ C) one may derive (B ∨ C). Iterated resolution between clauses, with unification to find compatible variable bindings, eventually derives the empty clause from any unsatisfiable set, proving the negation of any theorem.

The resolution principle is also the basis of logic programming: Prolog's execution mechanism is a restricted form of resolution called SLD-resolution. Robinson spent most of his career at Syracuse University and was a co-founder of the Journal of Logic Programming.