was at Argonne that Robinson became interested in automated theorem proving and developed unification and the resolution principle. Resolution and unification have since been incorporated in many automated theorem-proving systems and are the basis for the inference mechanisms used in logic programming and the programming language Prolog.

Robinson was the founding editor of the Journal of Logic Programming, and has received numerous honours. These include a Guggenheim Fellowship in 1967,