John Alan Robinson
Alan Robinson's major contribution is to the foundations of automated theorem proving and logic programming, using the resolution principle and unification (1965). This enabled the efficient implementation of the Prolog logic programming language and theorem provers. Robinson received the 1996 Herbrand Award for Distinguished Contributions to Automated Reasoning (named after the mathematician Jacques Herbrand).
Robinson was born in Yorkshire, England in 1930 and left for the United States in 1952 with a classics degree from Cambridge University. He studied philosophy at the University of Oregon before moving to Princeton University where he received his PhD in philosophy in 1956. He then worked at Du Pont as an operations research analyst, where he learned programming and taught himself mathematics. He moved to Rice University in 1961, spending his summers as a visiting researcher at the Argonne National Laboratory's Applied Mathematics Division. He moved to Syracuse University as Distinguished Professor of Logic and Computer Science in 1967 and became professor emeritus in 1993.
It 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 the Guggenheim Fellowship 1967–1968, American Mathematical Society Milestone Award in Automatic Theorem Proving 1985, AAAI Fellowship 1990, Humboldt Foundation Senior Scientist Award 1995, Herbrand Award for Distinguished Contributions to Automatic Reasoning 1996, and Honorary lifetime Membership of the Association for Logic Programming 1997. He has received Honorary Doctorates from Katholieke Universiteit Leuven 1988, Uppsala University 1994, and Universidad Politecnica de Madrid 2003.
- John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", Journal of the ACM, vol 12, 23–41, 1965.
- Michael A. Arbib and J. Alan Robinson (eds.), Natural and Artificial Parallel Computation, The MIT Press, 1990.
- J. Alan Robinson and Andrei Voronkov (eds.), Handbook of Automated Reasoning, The MIT Press, 2001.
- List of publications from the DBLP Bibliography Server
- Herbrand Award 1996: J. Alan Robinson
- Books listed by The MIT Press