John Alan Robinson Explained

John Alan Robinson
Birth Date:1930 3, df=y
Birth Place:Halifax, West Yorkshire, UK
Death Place:Portland, Maine, US
Workplaces:Syracuse University
Alma Mater:Cambridge University
University of Oregon
Princeton University
Thesis Title:Causation, probability and testimony
Thesis1 Url:and
Thesis2 Url:)-->
Thesis Year:1957
Doctoral Advisor:Carl Hempel[1]
Awards:AMS Milestone Award 1985, Humboldt Senior Scientist Award 1995, Herbrand Award 1996
Spouses:)-->
Partners:)-->

John Alan Robinson (9 March 1930 – 5 August 2016) was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

Alan Robinson's major contribution is to the foundations of automated theorem proving. His unification algorithm eliminated one source of combinatorial explosion in resolution provers; it also prepared the ground for the logic programming paradigm, in particular for the Prolog language. Robinson received the 1996 Herbrand Award for Distinguished Contributions to Automated Reasoning.

Life

Robinson was born in Halifax, Yorkshire, England in 1930[2] 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 DuPont as an operations research analyst, where he learned computer 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.[3]

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.[4]

Robinson was the Founding Editor of the Journal of Logic Programming, and has received numerous honours. These include a Guggenheim Fellowship in 1967, the American Mathematical Society Milestone Award in Automatic Theorem Proving 1985,[5] an AAAI Fellowship 1990,[6] the Herbrand Award for Distinguished Contributions to Automatic Reasoning 1996,[7] [8] and the Association for Logic Programming honorary title Founder of Logic Programming in 1997.[9] He has received honorary Doctorates from Katholieke Universiteit Leuven 1988,[10] Uppsala University 1994,[11] and Universidad Politecnica de Madrid 2003.[12] [13] Robinson died in Portland, Maine on 5 August 2016 from a ruptured aneurysm following surgery for pancreatic cancer.[14]

In 1994, he received the Humboldt Senior Scientist Award at the request of Wolfgang Bibel, which included a six-month stay at the Department of Computer Science of the Technische Universität Darmstadt.[15]

Selected publications

See also

External links

Notes and References

  1. Web site: philosophyfamilytree record . 13 September 2014 . 28 October 2014 . https://web.archive.org/web/20141028014837/http://philosophyfamilytree.wikispaces.com/Carl+Hempel . dead .
  2. http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf John Alan Robinson CV
  3. https://eng-cs.syr.edu/directory/?filter=.emeriti-faculty Emeriti Faculty, Engineering and Computer Science
  4. Book: The Coq Development Team. Automated theorem-proving was pioneered in the 1960s by Davis and Putnam in propositional calculus. A complete mechanization (in the sense of a semidecision procedure) of classical first-order logic was proposed in 1965 by J.A. Robinson, with a single uniform inference rule called resolution. Resolution relies on solving equations in free algebras (i.e. term structures), using the unification algorithm. Many refinements of resolution were studied in the 1970s, but few convincing implementations were realized, except of course that PROLOG is in some sense issued from this effort.. 3. The Coq Reference Manual: Release 8.10+alpha. 2018-10-18. 2018-10-19. 19 October 2018. https://web.archive.org/web/20181019075810/https://gitlab.com/coq/coq/-/jobs/109967447/artifacts/file/_install_ci/share/doc/coq/sphinx/latex/CoqRefMan.pdf. dead.
  5. http://www.ams.org/profession/prizes-awards/ams-supported/atp-prizes AMS Automatic Theorem Proving Prizes
  6. http://www.aaai.org/Awards/fellows-list.php AAAI Fellows List
  7. Web site: Herbrand Award 1996: J. Alan Robinson . 13 January 2007 . 7 March 2007 . https://web.archive.org/web/20070307071139/http://www.cadeconference.org/herbrand-award/1996.html . dead .
  8. Web site: CADE Herbrand Award . 13 September 2014 . https://web.archive.org/web/20140913195109/http://www.cs.miami.edu/~geoff/Conferences/CADE/HerbrandAward.html . 13 September 2014 . dead .
  9. http://www.cs.nmsu.edu/ALP/the-association-for-logic-programming/alp-awards/ ALP awards
  10. http://www.kuleuven.be/communicatie/evenementen/evenementen/patroonsfeest/archief.html KU Leuven honorary doctorates overview 1966–2012
  11. Web site: Honorary doctorates - Uppsala University, Sweden. 9 June 2023 .
  12. http://www.upm.es/institucional/UPM/Historia/HonorisCausa UP Madrid honorary doctorates 1973–2013
  13. http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf UP Madrid honorary doctorate for John Alan Robinson, Oct 1st, 2003
  14. Web site: John Alan Robinson, Obituary . . 17 August 2016 . 2 November 2019.
  15. Web site: Profile of John Alan Robinson in the Humboldt network. www.humboldt-foundation.de. 2019-11-02.