880:
44:
297:
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
674:. 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.
669:
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
974:
644:
818:
969:
294:'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.
984:
355:
308:
989:
939:
934:
929:
924:
979:
653:
734:
919:
959:
949:
944:
914:
359:
852:
708:
562:
457:
434:
391:
336:
320:
954:
377:
964:
328:
120:
538:
603:
312:
130:
770:
303:
291:
806:
587:
449:
211:
759:
527:
251:
219:
67:
271:
319:
Fellowship 1990, the
Herbrand Award for Distinguished Contributions to Automatic Reasoning 1996, and the
215:
685:
782:
909:
904:
738:
279:
267:
263:
259:
116:
106:
102:
98:
275:
239:
204:
152:
608:
542:
492:
473:
332:
200:
196:
848:
509:
453:
430:
387:
227:
223:
43:
532:
795:
630:
482:
414:
175:
566:
373:
340:
287:
86:
712:
879:
351:
347:
235:
134:
898:
889:
419:
496:
885:
343:
on 5 August 2016 from a ruptured aneurysm following surgery for pancreatic cancer.
283:
180:
696:
400:
17:
513:
426:
383:
254:, Yorkshire, England in 1930 and left for the United States in 1952 with a
487:
468:
975:
Fellows of the
Association for the Advancement of Artificial Intelligence
404:
255:
231:
195:(9 March 1930 – 5 August 2016) was a philosopher, mathematician, and
159:
270:
where he received his PhD in philosophy in 1956. He then worked at
807:
UP Madrid honorary doctorate for John Alan
Robinson, Oct 1st, 2003
406:
Handbook of Logic in
Artificial Intelligence and Logic Programming
874:
316:
870:
403:.; Hogger, Christopher John; Robinson, J.A., eds. (1993-1998).
290:
in 1961, spending his summers as a visiting researcher at the
469:"A Machine-Oriented Logic Based on the Resolution Principle"
210:
Alan
Robinson's major contribution is to the foundations of
133:
Milestone Award 1985, Humboldt Senior
Scientist Award 1995,
847:(in German) (1 ed.), Göttingen: Cuvillier Verlag,
819:"Profile of John Alan Robinson in the Humboldt network"
315:
Milestone Award in
Automatic Theorem Proving 1985, an
307:, and has received numerous honours. These include a
845:
Reflexionen vor
Reflexen - Memoiren eines Forschers
174:
158:
148:
126:
112:
94:
75:
53:
34:
783:"Honorary doctorates - Uppsala University, Sweden"
418:
327:in 1997. He has received honorary Doctorates from
631:Emeriti Faculty, Engineering and Computer Science
298:programming and the programming language Prolog.
771:KU Leuven honorary doctorates overview 1966–2012
633:, Syracuse University, accessed 2 November 2019.
598:
596:
8:
646:The Coq Reference Manual: Release 8.10+alpha
643:The Coq Development Team (18 October 2018).
421:Natural and Artificial Parallel Computation
878:
42:
31:
486:
354:, which included a six-month stay at the
970:British expatriates in the United States
301:Robinson was the Founding Editor of the
796:UP Madrid honorary doctorates 1973–2013
709:"Herbrand Award 1996: J. Alan Robinson"
554:
234:language. Robinson received the 1996
226:; it also prepared the ground for the
985:Alumni of the University of Cambridge
165:Causation, probability and testimony
7:
990:Mathematicians from New York (state)
940:21st-century American mathematicians
935:20th-century American mathematicians
686:AMS Automatic Theorem Proving Prizes
590:, upm.es, access date 12 August 2016
508:(PhD thesis). Princeton University.
506:Causation, Probability and Testimony
467:Robinson, John Alan (January 1965).
930:21st-century British mathematicians
925:20th-century British mathematicians
410:Vols. 1-5, Oxford University Press.
238:for Distinguished Contributions to
417:; Robinson, J. Alan, eds. (1990).
25:
980:American academic journal editors
337:Universidad Politecnica de Madrid
321:Association for Logic Programming
843:Leonhard Wolfgang Bibel (2017),
360:Technische Universität Darmstadt
230:paradigm, in particular for the
379:Handbook of Automated Reasoning
348:Humboldt Senior Scientist Award
262:. He studied philosophy at the
604:"John Alan Robinson, Obituary"
537:— an alternative to the
356:Department of Computer Science
329:Katholieke Universiteit Leuven
1:
563:"philosophyfamilytree record"
543:Boolean function minimization
313:American Mathematical Society
309:Guggenheim Fellowship in 1967
920:American computer scientists
504:Robinson, John Alan (1957).
325:Founder of Logic Programming
304:Journal of Logic Programming
960:Syracuse University faculty
950:Princeton University alumni
945:University of Oregon alumni
915:British computer scientists
652:. p. 3. Archived from
292:Argonne National Laboratory
27:American computer scientist
1006:
823:www.humboldt-foundation.de
450:Edinburgh University Press
278:analyst, where he learned
539:Quine–McCluskey algorithm
528:Robinson resolvent method
346:In 1994, he received the
218:eliminated one source of
212:automated theorem proving
186:
141:
41:
446:Logic: Form and Function
444:Robinson, J. A. (1979).
955:Rice University faculty
339:2003. Robinson died in
220:combinatorial explosion
68:Halifax, West Yorkshire
965:Formal methods people
735:"CADE Herbrand Award"
588:John Alan Robinson CV
488:10.1145/321250.321253
366:Selected publications
250:Robinson was born in
216:unification algorithm
877:Bibliography Server
741:on 13 September 2014
280:computer programming
268:Princeton University
264:University of Oregon
260:Cambridge University
117:resolution principle
107:Princeton University
103:University of Oregon
99:Cambridge University
372:Robinson, J. Alan;
282:and taught himself
276:operations research
240:Automated Reasoning
205:Syracuse University
153:Syracuse University
871:John Alan Robinson
659:on 19 October 2018
609:The New York Times
569:on 28 October 2014
350:at the request of
333:Uppsala University
224:resolution provers
201:professor emeritus
197:computer scientist
193:John Alan Robinson
36:John Alan Robinson
697:AAAI Fellows List
415:Arbib, Michael A.
266:before moving to
228:logic programming
190:
189:
143:Scientific career
16:(Redirected from
997:
882:
858:
857:
840:
834:
833:
831:
829:
815:
809:
804:
798:
793:
787:
786:
779:
773:
768:
762:
757:
751:
750:
748:
746:
737:. Archived from
731:
725:
724:
722:
720:
711:. Archived from
705:
699:
694:
688:
683:
677:
676:
666:
664:
658:
651:
640:
634:
628:
622:
621:
619:
617:
612:. 17 August 2016
600:
591:
585:
579:
578:
576:
574:
565:. Archived from
559:
536:
517:
500:
490:
463:
440:
424:
397:
374:Voronkov, Andrei
176:Doctoral advisor
170:
82:
63:
61:
48:Robinson in 2012
46:
32:
21:
1005:
1004:
1000:
999:
998:
996:
995:
994:
895:
894:
867:
862:
861:
855:
842:
841:
837:
827:
825:
817:
816:
812:
805:
801:
794:
790:
781:
780:
776:
769:
765:
758:
754:
744:
742:
733:
732:
728:
718:
716:
715:on 7 March 2007
707:
706:
702:
695:
691:
684:
680:
662:
660:
656:
649:
642:
641:
637:
629:
625:
615:
613:
602:
601:
594:
586:
582:
572:
570:
561:
560:
556:
551:
530:
524:
503:
466:
460:
443:
437:
413:
394:
376:, eds. (2001).
371:
368:
341:Portland, Maine
323:honorary title
288:Rice University
248:
168:
105:
101:
95:Alma mater
90:
87:Portland, Maine
84:
80:
71:
65:
59:
57:
49:
37:
28:
23:
22:
15:
12:
11:
5:
1003:
1001:
993:
992:
987:
982:
977:
972:
967:
962:
957:
952:
947:
942:
937:
932:
927:
922:
917:
912:
907:
897:
896:
893:
892:
883:
866:
865:External links
863:
860:
859:
853:
835:
810:
799:
788:
785:. 9 June 2023.
774:
763:
752:
726:
700:
689:
678:
635:
623:
592:
580:
553:
552:
550:
547:
546:
545:
523:
520:
519:
518:
501:
464:
458:
441:
435:
411:
398:
392:
367:
364:
352:Wolfgang Bibel
286:. He moved to
247:
244:
236:Herbrand Award
188:
187:
184:
183:
178:
172:
171:
162:
156:
155:
150:
146:
145:
139:
138:
135:Herbrand Award
128:
124:
123:
114:
113:Known for
110:
109:
96:
92:
91:
85:
83:(aged 86)
77:
73:
72:
66:
55:
51:
50:
47:
39:
38:
35:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1002:
991:
988:
986:
983:
981:
978:
976:
973:
971:
968:
966:
963:
961:
958:
956:
953:
951:
948:
946:
943:
941:
938:
936:
933:
931:
928:
926:
923:
921:
918:
916:
913:
911:
908:
906:
903:
902:
900:
891:
890:The MIT Press
887:
884:
881:
876:
872:
869:
868:
864:
856:
854:9783736995246
850:
846:
839:
836:
824:
820:
814:
811:
808:
803:
800:
797:
792:
789:
784:
778:
775:
772:
767:
764:
761:
756:
753:
740:
736:
730:
727:
714:
710:
704:
701:
698:
693:
690:
687:
682:
679:
675:
673:
655:
648:
647:
639:
636:
632:
627:
624:
611:
610:
605:
599:
597:
593:
589:
584:
581:
568:
564:
558:
555:
548:
544:
540:
534:
529:
526:
525:
521:
515:
511:
507:
502:
498:
494:
489:
484:
480:
476:
475:
470:
465:
461:
459:0-85224-305-7
455:
451:
447:
442:
438:
436:0-262-01120-4
432:
428:
423:
422:
416:
412:
409:
407:
402:
401:Gabbay, Dov M
399:
395:
393:0-444-50813-9
389:
385:
381:
380:
375:
370:
369:
365:
363:
361:
357:
353:
349:
344:
342:
338:
334:
330:
326:
322:
318:
314:
310:
306:
305:
299:
295:
293:
289:
285:
281:
277:
273:
269:
265:
261:
257:
253:
245:
243:
241:
237:
233:
229:
225:
221:
217:
213:
208:
206:
202:
198:
194:
185:
182:
179:
177:
173:
166:
163:
161:
157:
154:
151:
147:
144:
140:
136:
132:
129:
125:
122:
118:
115:
111:
108:
104:
100:
97:
93:
88:
79:5 August 2016
78:
74:
69:
56:
52:
45:
40:
33:
30:
19:
18:J.A. Robinson
844:
838:
826:. Retrieved
822:
813:
802:
791:
777:
766:
755:
745:13 September
743:. Retrieved
739:the original
729:
717:. Retrieved
713:the original
703:
692:
681:
671:
668:
661:. Retrieved
654:the original
645:
638:
626:
614:. Retrieved
607:
583:
573:13 September
571:. Retrieved
567:the original
557:
505:
481:(1): 23–41.
478:
472:
445:
420:
405:
378:
345:
324:
302:
300:
296:
258:degree from
249:
209:
192:
191:
164:
149:Institutions
142:
81:(2016-08-05)
64:9 March 1930
29:
910:2016 deaths
905:1930 births
531: [
284:mathematics
199:. He was a
181:Carl Hempel
121:unification
899:Categories
888:listed by
828:2 November
760:ALP awards
719:13 January
672:resolution
663:19 October
616:2 November
335:1994, and
60:1930-03-09
427:MIT Press
384:MIT Press
522:See also
514:83304635
497:14389185
256:classics
358:of the
252:Halifax
851:
512:
495:
474:J. ACM
456:
433:
390:
331:1988,
311:, the
274:as an
272:DuPont
232:Prolog
214:. His
169:(1957)
167:
160:Thesis
127:Awards
886:Books
657:(PDF)
650:(PDF)
549:Notes
535:]
493:S2CID
875:DBLP
849:ISBN
830:2019
747:2014
721:2007
665:2018
618:2019
575:2014
541:for
510:OCLC
454:ISBN
431:ISBN
388:ISBN
317:AAAI
246:Life
137:1996
89:, US
76:Died
70:, UK
54:Born
873:at
483:doi
222:in
203:at
131:AMS
901::
821:.
667:.
606:.
595:^
533:de
491:.
479:12
477:.
471:.
452:.
448:.
429:.
425:.
386:.
382:.
362:.
242:.
207:.
119:,
832:.
749:.
723:.
620:.
577:.
516:.
499:.
485::
462:.
439:.
408:.
396:.
62:)
58:(
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
