« 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édente
Contenu supprimé Contenu ajouté
VisuelWikicode
Python72 (discuter | contributions)
58 928 modifications
m ajout catégories
 
(3 versions intermédiaires par 2 utilisateurs non affichées)
Ligne 10 : Ligne 10 :
== 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}} : {{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>.
C'est à Argonne que Robinson s'intéresse à 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 ==
Ligne 21 : Ligne 21 :
* 1997 : Titre honorifique de ''Founder of Logic Programming'' de Association for Logic Programming<ref>[http://www.cs.nmsu.edu/ALP/the-association-for-logic-programming/alp-awards/ ALP awards].</ref>
* 1997 : Titre honorifique de ''Founder of Logic Programming'' de Association for Logic Programming<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]] en 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]] en 1994<ref>http://www.uu.se/en/about-uu/traditions/prizes/honorary-doctorates/</ref> et de l'[[Université polytechnique de Madrid]] en 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>.
Il a reçu des [[Doctorat honoris causa|doctorats honoris causa]] de la [[KU Leuven|Katholieke Universiteit Leuven]] en 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]] en 1994<ref>{{lien web |langue=en |titre=Honorary Doctorates |url=http://www.uu.se/en/about-uu/traditions/prizes/honorary-doctorates/ |site=uu.se |consulté le=21-06-2023}}.</ref> et de l'[[Université polytechnique de Madrid]] en 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, Robinson a reçu le [[Prix de recherche Humboldt]] sur proposition de {{Lien|Wolfgang Bibel}} ; ce prix qui comprenait un séjour de six mois au Département d'informatique de la [[Université de technologie de Darmstadt]]<ref>{{Lien web |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 }}.</ref>.
En 1994, Robinson a reçu le [[Prix de recherche Humboldt]] sur proposition de {{Lien|Wolfgang Bibel}} ; ce prix qui comprenait un séjour de six mois au Département d'informatique de la [[Université de technologie de Darmstadt]]<ref>{{Lien web |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 }}.</ref>.
Ligne 69 : Ligne 69 :
[[Catégorie:Mathématicien britannique du XXIe siècle]]
[[Catégorie:Mathématicien britannique du XXIe siècle]]
[[Catégorie:Mathématicien britannique du XXe siècle]]
[[Catégorie:Mathématicien britannique du XXe siècle]]
[[Catégorie:Personnalité américaine liée au secteur de l'informatique]]
[[Catégorie:Personnalité américaine de l'informatique]]
[[Catégorie:Personnalité britannique liée au secteur de l'informatique]]
[[Catégorie:Personnalité britannique de l'informatique]]
[[Catégorie:Naissance en mars 1930]]
[[Catégorie:Naissance en mars 1930]]
[[Catégorie:Naissance à Halifax (Royaume-Uni)]]
[[Catégorie:Naissance à Halifax (Royaume-Uni)]]

Dernière version du 19 janvier 2024 à 11:03

Page d’aide sur l’homonymie

Pour les articles homonymes, voir John Robinson.

John Alan Robinson
John Alan Robinson en 2012
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 à Halifax (Royaume-Uni), et mort le à Portland (Maine)) est un philosophe, mathématicien et informaticien. Il termine sa carrière comme 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[modifier | modifier le code]

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[modifier | modifier le code]

C'est à Argonne que Robinson s'intéresse à 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[modifier | modifier le code]

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

Il a reçu des doctorats honoris causa de la Katholieke Universiteit Leuven en 1988[10], de l'Université d'Uppsala en 1994[11] et de l'Université polytechnique de Madrid en 2003[12],[13].

En 1994, Robinson a reçu le Prix de recherche Humboldt sur proposition de Wolfgang Bibel (en) ; ce prix qui comprenait un séjour de six mois au Département d'informatique de la Université de technologie de Darmstadt[14].

Publications (sélection)[modifier | modifier le code]

Articles liés[modifier | modifier le code]

Remarques[modifier | modifier le code]

  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. ↑ (en) « Honorary Doctorates », sur uu.se (consulté le ).
  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[modifier | modifier le code]

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