John Alan Robinson
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 after studying for a classics degree at Corpus Christi College, Cambridge.[3] 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[4] and became professor emeritus in 1993.[5]
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.[6]
كان روبنسون المحرر المؤسس لمجلة البرمجة المنطقية ، وقد حصل على العديد من الجوائز والتكريمات. تشمل هذه الجوائز زمالة غوغنهايم عام 1967 ، وجائزة الجمعية الأمريكية للرياضيات للإنجاز البارز في إثبات النظريات الآلي عام 1985، [ 7 ] وزمالة الجمعية الأمريكية للذكاء الاصطناعي عام 1990، [ 8 ] وجائزة هيربراند للمساهمات المتميزة في الاستدلال الآلي عام 1996، [ 9 ] [ 10 ] ولقب مؤسس البرمجة المنطقية الفخري من جمعية البرمجة المنطقية عام 1997. [ 11 ] وقد حصل على شهادات دكتوراه فخرية من جامعة لوفين الكاثوليكية عام 1988، [ 12 ] وجامعة أوبسالا عام 1994، [ 13 ] وجامعة مدريد التقنية عام 2003. [ 14 ] [ 15 ] توفي روبنسون في بورتلاند، مين، في 5 أغسطس 2016 إثر تمزق تمدد الأوعية الدموية بعد جراحة لعلاج سرطان البنكرياس. [ 4 ]
في عام 1994، حصل على جائزة هومبولت لكبار العلماء بناءً على طلب فولفغانغ بيبل ، والتي تضمنت إقامة لمدة ستة أشهر في قسم علوم الحاسوب بجامعة دارمشتات التقنية . [ 16 ] [ 17 ]
منشورات مختارة
- روبنسون، ج. آلان؛ فورونكوف، أندريه ، محرران. (2001). دليل الاستدلال الآلي . مطبعة معهد ماساتشوستس للتكنولوجيا . ISBN 0-444-50813-9.
- جاباي، دوف م .؛ هوجر، كريستوفر جون؛ روبنسون، جيه إيه، محرران. (1993-1998). دليل المنطق في الذكاء الاصطناعي وبرمجة المنطق . المجلدات 1-5، مطبعة جامعة أكسفورد.
- أربيب، مايكل أ .؛ روبنسون، ج. آلان، محرران. (1990). الحوسبة المتوازية الطبيعية والاصطناعية . مطبعة معهد ماساتشوستس للتكنولوجيا . ISBN 0-262-01120-4.
- روبنسون، جيه إيه (1979). المنطق: الشكل والوظيفة . مطبعة جامعة إدنبرة . رقم ISBN 0-85224-305-7.
- روبنسون، جون آلان (يناير 1965). "منطق موجه نحو الآلة قائم على مبدأ الاستدلال" . مجلة ACM . 12 (1): 23-41 . doi : 10.1145/321250.321253 . S2CID 14389185 .
- Robinson, John Alan (1957). Causation, Probability and Testimony (PhD thesis). Princeton University. OCLC 83304635.
See also
- Robinson resolvent method— an alternative to the Quine–McCluskey algorithm for Boolean function minimization
Notes
- ↑"philosophyfamilytree record". Archived from the original on 28 October 2014. Retrieved 13 September 2014.
- ↑John Alan Robinson CV, upm.es, access date 12 August 2016
- ↑"Tripos Results at Cambridge". The Times Educational Supplement. No. 1938. 20 June 1952. p. 536.
- 12"John Alan Robinson, Obituary". The New York Times. 17 August 2016. Retrieved 2 November 2019.
- ↑"Emeriti Faculty - Office of Academic Affairs – Syracuse University". academicaffairs.syracuse.edu. Retrieved 2 September 2025.
- ↑The Coq Development Team (18 October 2018). The Coq Reference Manual: Release 8.10+alpha(PDF). p. 3. Archived from the original(PDF) on 19 October 2018. Retrieved 19 October 2018.
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.
- ↑AMS Automatic Theorem Proving Prizes
- ↑AAAI Fellows List
- ↑"Herbrand Award 1996: J. Alan Robinson". Archived from the original on 7 March 2007. Retrieved 13 January 2007.
- ↑"CADE Herbrand Award". Archived from the original on 13 September 2014. Retrieved 13 September 2014.
- ↑"ALP awards". Archived from the original on 13 April 2013. Retrieved 13 September 2014.
- ↑KU Leuven honorary doctorates overview 1966–2012
- ↑"Honorary Doctors of the Faculty of Science and Technology – Uppsala University, Sweden". 16 January 2025.
- ↑UP Madrid honorary doctorates 1973–2013
- ↑UP Madrid honorary doctorate for John Alan Robinson, Oct 1st, 2003
- ↑"Profile of John Alan Robinson in the Humboldt network". www.humboldt-foundation.de. Retrieved 2 November 2019.
- ↑Leonhard Wolfgang Bibel (2017), Reflexionen vor Reflexen - Memoiren eines Forschers (in German) (1 ed.), Göttingen: Cuvillier Verlag, ISBN 9783736995246
External links
- John Alan Robinson at DBLP Bibliography Server
- Books listed by The MIT Press
- 1930 births
- 2016 deaths
- British computer scientists
- American computer scientists
- 20th-century British mathematicians
- 21st-century British mathematicians
- 20th-century American mathematicians
- 21st-century American mathematicians
- University of Oregon alumni
- Princeton University alumni
- Rice University faculty
- Syracuse University faculty
- Formal methods people
- British expatriates in the United States
- Fellows of the Association for the Advancement of Artificial Intelligence
- American academic journal editors
- Alumni of Corpus Christi College, Cambridge
- Mathematicians from New York (state)
