stringtranslate.com

Juan Alan Robinson

John Alan Robinson (9 de marzo de 1930 – 5 de agosto de 2016) fue un filósofo, matemático y científico informático . Fue profesor emérito de la Universidad de Syracuse .

La principal contribución de Alan Robinson es la de sentar las bases de la demostración automática de teoremas . Su algoritmo de unificación eliminó una fuente de explosión combinatoria en los probadores de resolución ; también preparó el terreno para el paradigma de programación lógica , en particular para el lenguaje Prolog . Robinson recibió el Premio Herbrand de 1996 por contribuciones destacadas al razonamiento automatizado .

Vida

Robinson nació en Halifax , Yorkshire, Inglaterra en 1930 [2] y se fue a los Estados Unidos en 1952 con un título en estudios clásicos de la Universidad de Cambridge . Estudió filosofía en la Universidad de Oregon antes de mudarse a la Universidad de Princeton , donde recibió su doctorado en filosofía en 1956. Luego trabajó en DuPont como analista de investigación de operaciones , donde aprendió programación informática y se enseñó matemáticas por su cuenta . Se mudó a la Universidad Rice en 1961, pasando sus veranos como investigador visitante en la División de Matemáticas Aplicadas del Laboratorio Nacional Argonne . Se trasladó a la Universidad de Syracuse como profesor distinguido de lógica y ciencias de la computación en 1967 [3] y se convirtió en profesor emérito en 1993. [4]

Fue en Argonne donde Robinson se interesó en la demostración automática de teoremas y desarrolló la unificación y el principio de resolución. Desde entonces, la resolución y la unificación se han incorporado en muchos sistemas de demostración automática de teoremas y son la base de los mecanismos de inferencia utilizados en la programación lógica y el lenguaje de programación Prolog. [5]

Robinson fue el editor fundador del Journal of Logic Programming y ha recibido numerosos honores, entre ellos una beca Guggenheim en 1967 , el premio Milestone Award in Automatic Theorem Proving de la American Mathematical Society en 1985, [6] una beca AAAI en 1990, [7] el premio Herbrand por contribuciones distinguidas al razonamiento automático en 1996, [8] [9] y el título honorífico de Fundador de la Programación Lógica de la Association for Logic Programming en 1997. [10] Ha recibido doctorados honorarios de la Katholieke Universiteit Leuven en 1988, [11] la Universidad de Uppsala en 1994, [12] y la Universidad Politécnica de Madrid en 2003. [13] [14] Robinson murió en Portland, Maine , el 5 de agosto de 2016 a causa de la rotura de un aneurisma tras una cirugía por cáncer de páncreas. [3]

En 1994 recibió el Premio Científico Senior Humboldt a petición de Wolfgang Bibel , que incluía una estancia de seis meses en el Departamento de Ciencias de la Computación de la Universidad Técnica de Darmstadt . [15] [16]

Publicaciones seleccionadas

Véase también

Notas

  1. ^ "philosophyfamilytree record". Archivado desde el original el 28 de octubre de 2014 . Consultado el 13 de septiembre de 2014 .
  2. ^ CV de John Alan Robinson, upm.es, fecha de acceso 12 de agosto de 2016
  3. ^ ab "John Alan Robinson, Obituary". The New York Times . 17 de agosto de 2016 . Consultado el 2 de noviembre de 2019 .
  4. ^ Profesor Emérito, Ingeniería y Ciencias de la Computación, Universidad de Syracuse, consultado el 2 de noviembre de 2019.
  5. ^ El equipo de desarrollo de Coq (18 de octubre de 2018). Manual de referencia de Coq: versión 8.10+alpha (PDF) . p. 3. Archivado desde el original (PDF) el 19 de octubre de 2018 . Consultado el 19 de octubre de 2018 . La demostración automática de teoremas fue iniciada en la década de 1960 por Davis y Putnam en cálculo proposicional. Una mecanización completa (en el sentido de un procedimiento de semidecisión) de la lógica clásica de primer orden fue propuesta en 1965 por JA Robinson, con una única regla de inferencia uniforme llamada resolución . La resolución se basa en la resolución de ecuaciones en álgebras libres (es decir, estructuras de términos), utilizando el algoritmo de unificación. Se estudiaron muchos refinamientos de la resolución en la década de 1970, pero se realizaron pocas implementaciones convincentes, excepto, por supuesto, que PROLOG es en cierto sentido el resultado de este esfuerzo.
  6. ^ Premios por demostración automática de teoremas de AMS
  7. ^ Lista de becarios de la AAAI
  8. ^ "Premio Herbrand 1996: J. Alan Robinson". Archivado desde el original el 7 de marzo de 2007. Consultado el 13 de enero de 2007 .
  9. ^ "Premio CADE Herbrand". Archivado desde el original el 13 de septiembre de 2014 . Consultado el 13 de septiembre de 2014 .
  10. ^ Premios ALP
  11. ^ Resumen de los doctorados honoris causa de la KU Leuven 1966–2012
  12. ^ "Doctorados honorarios - Universidad de Uppsala, Suecia". 9 de junio de 2023.
  13. ^ Doctorados honoris causa por la UP Madrid 1973-2013
  14. ^ Doctorado honoris causa por la UP Madrid a John Alan Robinson, 1 de octubre de 2003
  15. ^ "Perfil de John Alan Robinson en la red Humboldt". www.humboldt-foundation.de . Consultado el 2 de noviembre de 2019 .[ enlace muerto permanente ]
  16. ^ Leonhard Wolfgang Bibel (2017), Reflexionen vor Reflexen - Memoiren eines Forschers (en alemán) (1 ed.), Göttingen: Cuvillier Verlag, ISBN 9783736995246

Enlaces externos