« John Alan Robinson » : différence entre les versions

Un article de Wikipédia, l'encyclopédie libre.
Navigation interactive dans l’historique
← Modification précédenteModification suivante →
Contenu supprimé Contenu ajouté
VisuelWikicode
Vers75 (discuter | contributions)
16 077 modifications
Vers75 (discuter | contributions)
16 077 modifications
mef
Ligne 6 : Ligne 6 :


== Biographie ==
== Biographie ==
Robinson est né à [[Halifax (Royaume-Uni)|Halifax]], au [[Yorkshire]], en 1930 <ref>[http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf John Alan Robinson CV], upm.es, access date 12 August 2016</ref> et part aux États-Unis en 1952 avec un diplôme en [[humanités classiques]] de [[Université de Cambridge|l']][[Université de Cambridge|Université]] [[Université de Cambridge|de]] [[Université de Cambridge|Cambridge]] . Il étudié la philosophie à l' [[Université de l'Oregon]] puis rejoint [[Université de Princeton|l'Université de Princeton]] où il a obtenu son [[doctorat en philosophie]] en 1956. Il a ensuite travaillé dans l'entreprise [[DuPont]] en tant qu'analyste en [[recherche opérationnelle]], où il a appris la programmation et se forme lui-même en [[mathématiques]] . Il intègre [[Université Rice|l'Université Rice]] en 1961, tout en passant les étés comme chercheur invité à la Division de mathématiques appliquées du [[Laboratoire national d'Argonne]]. Il rejoint l'[[Université de Syracuse]] en tant que professeur distingué de logique et d'informatique en 1967 <ref name="nyt20160817">{{Lien web |titre=John Alan Robinson, Obituary |url=http://www.legacy.com/obituaries/nytimes/obituary.aspx?n=john-robinson&pid=181092820 |série=[[The New York Times]] |date=17 August 2016 |consulté le=2 November 2019}}</ref> et devient professeur émérite en 1993. <ref>[https://eng-cs.syr.edu/directory/?filter=.emeriti-faculty Emeriti Faculty, Engineering and Computer Science], Syracuse University, accessed 2 November 2019.</ref>
Robinson est né à [[Halifax (Royaume-Uni)|Halifax]], au [[Yorkshire]], en 1930<ref>[http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf John Alan Robinson CV], upm.es, access date 12 August 2016.</ref>. Il obtient un diplôme en [[humanités classiques]] de l'[[Université de Cambridge]] et part aux États-Unis en 1952. Il étudié la philosophie à l'[[Université de l'Oregon]] puis rejoint l'[[Université de Princeton]] où il obtient son [[doctorat en philosophie|Ph. D.]] en 1956. Il travaille ensuite dans l'entreprise [[DuPont]] en tant qu'analyste en [[recherche opérationnelle]] ; il y apprend la programmation et se forme lui-même en [[mathématiques]]. Il intègre l'[[Université Rice]] en 1961, tout en passant les étés comme chercheur invité à la Division de mathématiques appliquées du [[Laboratoire national d'Argonne]]. Il rejoint l'[[Université de Syracuse]] en tant que [[Professeur des universités|professeur]] distingué de logique et d'informatique en 1967<ref name="nyt20160817">{{Lien web |titre=John Alan Robinson, Obituary |url=http://www.legacy.com/obituaries/nytimes/obituary.aspx?n=john-robinson&pid=181092820 |série=[[The New York Times]] |date=17 August 2016 |consulté le=2 November 2019}}.</ref>. Il devient professeur émérite en 1993<ref>[https://eng-cs.syr.edu/directory/?filter=.emeriti-faculty Emeriti Faculty, Engineering and Computer Science], Syracuse University, accessed 2 November 2019.</ref>.


== Recherche ==
== Recherche ==


C'est à Argonne que Robinson s'intéressé à la [[démonstration automatique de théorèmes]] ; il y développe l'[[unification]] et le principe de résolution. La résolution et l'unification sont depuis incorporées dans de nombreux systèmes automatiques de démonstration de théorèmes et sont à la base des mécanismes d'inférence utilisés dans la programmation logique et des langages de programmation comme [[Prolog]]. <ref name="coq-refman">{{Ouvrage|nom1=The Coq Development Team|titre=The Coq Reference Manual: Release 8.10+alpha|passage=3|date=2018-10-18|lire en ligne=https://gitlab.com/coq/coq/-/jobs/109967447/artifacts/file/_install_ci/share/doc/coq/sphinx/latex/CoqRefMan.pdf|consulté le=2018-10-19|extrait=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.}}</ref>
C'est à Argonne que Robinson s'intéressé à la [[démonstration automatique de théorèmes]] ; il y développe l'[[unification]] et le principe de résolution. La résolution et l'unification sont depuis incorporées dans de nombreux systèmes automatiques de démonstration de théorèmes et sont à la base des mécanismes d'inférence utilisés dans la programmation logique et des langages de programmation comme [[Prolog]]<ref name="coq-refman">{{Ouvrage|nom1=The Coq Development Team|titre=The Coq Reference Manual: Release 8.10+alpha|passage=3|date=2018-10-18|lire en ligne=https://gitlab.com/coq/coq/-/jobs/109967447/artifacts/file/_install_ci/share/doc/coq/sphinx/latex/CoqRefMan.pdf|consulté le=2018-10-19}} : {{Citation étrangère|langue=en|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}}.</ref>.


== Distinctions ==
== Distinctions ==


Robinson a été le rédacteur en chef fondateur du ''Journal of Logic Programming''. Il a reçu de nombreux honneurs. Ceux-ci incluent :
⚫
Robinson a été le rédacteur en chef fondateur du ''Journal of Logic Programming'' et a reçu de nombreux honneurs. Ceux-ci incluent une bourse Guggenheim en 1967, le ''Milestone Award in Automatic Theorem Proving'' de la [[American Mathematical Society|Société mathématique américaine]] en 1985, <ref>[http://www.ams.org/profession/prizes-awards/ams-supported/atp-prizes AMS Automatic Theorem Proving Prizes]</ref> une bourse [[Association for the Advancement of Artificial Intelligence|AAAI]] 1990, <ref>[http://www.aaai.org/Awards/fellows-list.php AAAI Fellows List]</ref> le [[prix Herbrand]] pour des contributions distingués au raisonnement automatique en 1996, <ref>[http://www.cadeconference.org/herbrand-award/1996.html Herbrand Award 1996: J. Alan Robinson]</ref> <ref>{{Lien web |titre=CADE Herbrand Award |url=http://www.cs.miami.edu/~geoff/Conferences/CADE/HerbrandAward.html |consulté le=13 September 2014 |archive-url=https://web.archive.org/web/20140913195109/http://www.cs.miami.edu/~geoff/Conferences/CADE/HerbrandAward.html |archive-date=13 September 2014}}</ref> et le titre honorifique de ''Founder of Logic Programming'' de Association for Logic Programming en 1997. <ref>[http://www.cs.nmsu.edu/ALP/the-association-for-logic-programming/alp-awards/ ALP awards]</ref> Il a reçu des [[Doctorat honoris causa|doctorats honoris causa]] de la [[KU Leuven|Katholieke Universiteit Leuven]] 1988, <ref>[http://www.kuleuven.be/communicatie/evenementen/evenementen/patroonsfeest/archief.html KU Leuven honorary doctorates overview 1966–2012]</ref>, de l'[[Université d'Uppsala|Uppsala Université]] en 1994, <ref>http://www.uu.se/en/about-uu/traditions/prizes/honorary-doctorates/</ref> et de [[Université polytechnique de Madrid|Universidad Politecnica de Madrid]] 2003. <ref>[http://www.upm.es/institucional/UPM/Historia/HonorisCausa UP Madrid honorary doctorates 1973–2013]</ref> <ref>[http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf UP Madrid honorary doctorate for John Alan Robinson, Oct 1st, 2003]</ref>
* 1967 : Bourse Guggenheim
⚫
* 1985 : ''Milestone Award in Automatic Theorem Proving'' de l'[[American Mathematical Society]] en 1985, <ref>[http://www.ams.org/profession/prizes-awards/ams-supported/atp-prizes AMS Automatic Theorem Proving Prizes]</ref> une bourse [[Association for the Advancement of Artificial Intelligence|AAAI]] 1990, <ref>[http://www.aaai.org/Awards/fellows-list.php AAAI Fellows List]</ref> le [[prix Herbrand]] pour des contributions distingués au raisonnement automatique en 1996, <ref>[http://www.cadeconference.org/herbrand-award/1996.html Herbrand Award 1996: J. Alan Robinson]</ref> <ref>{{Lien web |titre=CADE Herbrand Award |url=http://www.cs.miami.edu/~geoff/Conferences/CADE/HerbrandAward.html |consulté le=13 September 2014 |archive-url=https://web.archive.org/web/20140913195109/http://www.cs.miami.edu/~geoff/Conferences/CADE/HerbrandAward.html |archive-date=13 September 2014}}</ref> et le titre honorifique de ''Founder of Logic Programming'' de Association for Logic Programming en 1997. <ref>[http://www.cs.nmsu.edu/ALP/the-association-for-logic-programming/alp-awards/ ALP awards]</ref> Il a reçu des [[Doctorat honoris causa|doctorats honoris causa]] de la [[KU Leuven|Katholieke Universiteit Leuven]] 1988, <ref>[http://www.kuleuven.be/communicatie/evenementen/evenementen/patroonsfeest/archief.html KU Leuven honorary doctorates overview 1966–2012]</ref>, de l'[[Université d'Uppsala|Uppsala Université]] en 1994, <ref>http://www.uu.se/en/about-uu/traditions/prizes/honorary-doctorates/</ref> et de [[Université polytechnique de Madrid|Universidad Politecnica de Madrid]] 2003. <ref>[http://www.upm.es/institucional/UPM/Historia/HonorisCausa UP Madrid honorary doctorates 1973–2013]</ref> <ref>[http://www.upm.es/sfs/Gabinete%20del%20Rector/Honoris%20Causa/curriculum/john.pdf UP Madrid honorary doctorate for John Alan Robinson, Oct 1st, 2003]</ref>


En 1994, il a reçu le [[Prix de recherche Humboldt|Humboldt Senior Scientist Award]] sur proposition de Wolfgang Bibel, qui comprenait un séjour de six mois au Département d'informatique de la [[Université de technologie de Darmstadt|Technische Universität Darmstadt]] . <ref>{{Lien web |auteur= |prénom= |titre=Profile of John Alan Robinson in the Humboldt network |url=https://www.humboldt-foundation.de/pls/web/pub_hn_query.humboldtianer_details?p_externe_id=7000128710&p_lang=de&p_pattern=John%20Alan%20Robinson |série=www.humboldt-foundation.de |date= |consulté le=2019-11-02 |archive-url= |archive-date=}}</ref>
En 1994, il a reçu le [[Prix de recherche Humboldt|Humboldt Senior Scientist Award]] sur proposition de Wolfgang Bibel, qui comprenait un séjour de six mois au Département d'informatique de la [[Université de technologie de Darmstadt|Technische Universität Darmstadt]] . <ref>{{Lien web |auteur= |prénom= |titre=Profile of John Alan Robinson in the Humboldt network |url=https://www.humboldt-foundation.de/pls/web/pub_hn_query.humboldtianer_details?p_externe_id=7000128710&p_lang=de&p_pattern=John%20Alan%20Robinson |série=www.humboldt-foundation.de |date= |consulté le=2019-11-02 |archive-url= |archive-date=}}</ref>
Ligne 20 : Ligne 22 :
== Publications (sélection) ==
== Publications (sélection) ==


* {{cite book|editor-last1=Robinson|editor-first1=J. Alan|editor-last2=Voronkov|editor-first2=Andrei|editor-link2=Andrei Voronkov|title=Handbook of Automated Reasoning|title-link=Handbook of Automated Reasoning|publisher=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}
* {{ouvrage|auteur1= John Alan Robinson|auteur2=Andrei Voronkov|responsabilité2 = éditeurs|title=Handbook of Automated Reasoning|title-link=Handbook of Automated Reasoning|publisher=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}
* {{ouvrage|auteur1= Dov M. Gabbay|auteur2=Christopher John Hogger|auteur3=John Alan Robinson|responsabilité3 = éditeurs
* [[:en:Dov_Gabbay|Gabbay, Dov M]].; Hogger, Christopher John; Robinson, J.A., eds. (1993-1998). [https://www.worldcat.org/title/handbook-of-logic-in-artificial-intelligence-and-logic-programming/oclc/26300491 ''Handbook of Logic in Artificial Intelligence and Logic Programming''.] Vols. 1-5, Oxford University Press.
| titre = Handbook of Logic in Artificial Intelligence and Logic Programming
⚫
* {{cite book|editor-last1=Arbib|editor-first1=Michael A.|editor-last2=Robinson|editor-first2=J. Alan|title=Natural and Artificial Parallel Computation|publisher=[[MIT Press]]|date=1990|isbn=0-262-01120-4|url-access=registration|url=https://archive.org/details/naturalartificia00arbi}}
| volume =1-5
⚫
* {{cite book|last1=Robinson|first1=J. A.|title=Logic: Form and Function|publisher=[[Edinburgh University Press]]|date=1979|isbn=0-85224-305-7}}
| éditeur = Oxford University Press
⚫
* {{cite journal |first1=John Alan |last1=Robinson |title=A Machine-Oriented Logic Based on the Resolution Principle |journal=[[Journal of the ACM|J. ACM]] |volume=12 |issue=1 |date=January 1965 |doi=10.1145/321250.321253 |pages=23–41 }}
| date = 1993-1998}}
*
* {{ouvrage|auteur1= Michael A. Arbib|auteur2=John Alan Robinson|responsabilité2 = éditeurs

⚫
|title=Natural and Artificial Parallel Computation|publisher=[[MIT Press]]|date=1990|isbn=0-262-01120-4|url-access=registration|url=https://archive.org/details/naturalartificia00arbi}}
*
* {{ouvrage|auteur1=John Alan Robinson
** {{cite book|editor-last1=Robinson|editor-first1=J. Alan|editor-last2=Voronkov|editor-first2=Andrei|editor-link2=Andrei Voronkov|title=Handbook of Automated Reasoning|title-link=Handbook of Automated Reasoning|publisher=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}
⚫
|title=Logic: Form and Function|publisher=[[Edinburgh University Press]]|date=1979|isbn=0-85224-305-7}}
** [[:en:Dov_Gabbay|Gabbay, Dov M]].; Hogger, Christopher John; Robinson, J.A., eds. (1993-1998). [https://www.worldcat.org/title/handbook-of-logic-in-artificial-intelligence-and-logic-programming/oclc/26300491 ''Handbook of Logic in Artificial Intelligence and Logic Programming''.] Vols. 1-5, Oxford University Press.
⚫
* {{cite journal |first1=John Alan |last1=Robinson |title=A Machine-Oriented Logic Based on the Resolution Principle |journal=[[Journal of the ACM]] |volume=12 |issue=1 |date=January 1965 |doi=10.1145/321250.321253 |pages=23–41 }}
** {{cite book|editor-last1=Arbib|editor-first1=Michael A.|editor-last2=Robinson|editor-first2=J. Alan|title=Natural and Artificial Parallel Computation|publisher=[[MIT Press]]|date=1990|isbn=0-262-01120-4|url-access=registration|url=https://archive.org/details/naturalartificia00arbi}}
** {{cite book|last1=Robinson|first1=J. A.|title=Logic: Form and Function|publisher=[[Edinburgh University Press]]|date=1979|isbn=0-85224-305-7}}
** {{cite journal |first1=John Alan |last1=Robinson |title=A Machine-Oriented Logic Based on the Resolution Principle |journal=[[Journal of the ACM|J. ACM]] |volume=12 |issue=1 |date=January 1965 |doi=10.1145/321250.321253 |pages=23–41 }}
**

{{Ouvrage|titre=Handbook of Automated Reasoning|éditeur=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}<bdi>{{Ouvrage|titre=Handbook of Automated Reasoning|éditeur=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}</bdi> {{Ouvrage|titre=Handbook of Automated Reasoning|éditeur=[[MIT Press]]|date=2001|isbn=0-444-50813-9}}


== Articles liés ==
== Articles liés ==


* [[Liste de publications importantes en informatique théorique|Liste des publications importantes en informatique théorique]]
* [[Liste de publications importantes en informatique théorique|Liste des publications importantes en informatique théorique]]
* Robinson resolvent method [ de ] &#x2014; une alternative à l' [[Méthode de Quine-Mc Cluskey|algorithme Quine – McCluskey]] pour la minimisation des fonctions booléennes
* {{Lien|lang=de|trad=Resolventenmethode|fr=méthode de résolution}} de Robinson, une alternative à la [[Méthode de Quine-Mc Cluskey]] pour la minimisation des fonctions booléennes.


== Remarques ==
== Remarques ==

Version du 22 novembre 2020 à 20:29

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.
Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.

Un contributeur travaille en ce moment même sur cet article ou cette section.

Merci de ne pas faire de modifications tant que ce message reste présent. Ce bandeau, destiné à limiter les risques de conflit de versions, ne doit pas être maintenu sur l'article lorsque le contributeur qui l'a apposé n'y travaille plus. Si la page n’a pas été modifiée depuis plusieurs heures, enlevez ce bandeau ou remplacez-le par {{en travaux}}.
La dernière modification de cette page a été faite le 22 novembre 2020 à 20:29.

John Alan Robinson
Biographie
Naissance
Décès
Voir et modifier les données sur Wikidata (à 86 ans)
PortlandVoir et modifier les données sur Wikidata
Nationalités
Formation
Activités
Autres informations
A travaillé pour
Membre de
Directeur de thèse
Distinctions

modifier - modifier le code - modifier WikidataDocumentation du modèle

John Alan Robinson (né le 9 mars 1930 à Halifax (Royaume-Uni), et mort le 5 août 2016 à Portland (Maine)) est un philosophe, mathématicien et informaticien. Il était professeur émérite à l'Université de Syracuse.

La contribution majeure d'Alan Robinson est aux fondements de la démonstration automatique de théorèmes. Son algorithme d'unification a éliminé une source d' explosion combinatoire dans les démonstrateurs de résolution ; il a également préparé le terrain pour le paradigme de programmation logique, en particulier pour le langage Prolog . Robinson a reçu le prix Herbrand 1996 pour ses "contributions remarquables au raisonnement automatisé" .

Biographie

Robinson est né à Halifax, au Yorkshire, en 1930[1]. Il obtient un diplôme en humanités classiques de l'Université de Cambridge et part aux États-Unis en 1952. Il étudié la philosophie à l'Université de l'Oregon puis rejoint l'Université de Princeton où il obtient son Ph. D. en 1956. Il travaille ensuite dans l'entreprise DuPont en tant qu'analyste en recherche opérationnelle ; il y apprend la programmation et se forme lui-même en mathématiques. Il intègre l'Université Rice en 1961, tout en passant les étés comme chercheur invité à la Division de mathématiques appliquées du Laboratoire national d'Argonne. Il rejoint l'Université de Syracuse en tant que professeur distingué de logique et d'informatique en 1967[2]. Il devient professeur émérite en 1993[3].

Recherche

C'est à Argonne que Robinson s'intéressé à la démonstration automatique de théorèmes ; il y développe l'unification et le principe de résolution. La résolution et l'unification sont depuis incorporées dans de nombreux systèmes automatiques de démonstration de théorèmes et sont à la base des mécanismes d'inférence utilisés dans la programmation logique et des langages de programmation comme Prolog[4].

Distinctions

Robinson a été le rédacteur en chef fondateur du Journal of Logic Programming. Il a reçu de nombreux honneurs. Ceux-ci incluent :

En 1994, il a reçu le Humboldt Senior Scientist Award sur proposition de Wolfgang Bibel, qui comprenait un séjour de six mois au Département d'informatique de la Technische Universität Darmstadt . [14]

Publications (sélection)

Articles liés

Remarques

  1. ↑ John Alan Robinson CV, upm.es, access date 12 August 2016.
  2. ↑ « John Alan Robinson, Obituary », The New York Times, (consulté le ).
  3. ↑ Emeriti Faculty, Engineering and Computer Science, Syracuse University, accessed 2 November 2019.
  4. ↑ The Coq Development Team, The Coq Reference Manual: Release 8.10+alpha, (lire en ligne), p. 3 : « 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 ».
  5. ↑ AMS Automatic Theorem Proving Prizes
  6. ↑ AAAI Fellows List
  7. ↑ Herbrand Award 1996: J. Alan Robinson
  8. ↑ « CADE Herbrand Award » [archive du ] (consulté le )
  9. ↑ ALP awards
  10. ↑ KU Leuven honorary doctorates overview 1966–2012
  11. ↑ http://www.uu.se/en/about-uu/traditions/prizes/honorary-doctorates/
  12. ↑ UP Madrid honorary doctorates 1973–2013
  13. ↑ UP Madrid honorary doctorate for John Alan Robinson, Oct 1st, 2003
  14. ↑ « Profile of John Alan Robinson in the Humboldt network », www.humboldt-foundation.de (consulté le )

Liens externes

Ce document provient de « https://fr.wikipedia.org/w/index.php?title=John_Alan_Robinson&oldid=176873074 ».