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 .
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]
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.