John Alan Robinson (9 de marzo de 1930 - 5 de agosto de 2016) fue un filósofo, matemático e informático . Fue profesor emérito de la Universidad de Syracuse .
La principal contribución de Alan Robinson es la de los fundamentos de la demostración automatizada 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 sus contribuciones distinguidas 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 clásicos de la Universidad de Cambridge . Estudió filosofía en la Universidad de Oregón antes de trasladarse 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 aprendió matemáticas por su cuenta . Se mudó a la Universidad Rice en 1961 y pasó los 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 automatizada 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 automatizados de demostración 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. Estos incluyen una beca Guggenheim en 1967 , el premio Milestone de la American Mathematical Society en demostración automática de teoremas 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 la Asociación de Programación Lógica Fundador de Programación Lógica en 1997. [10] Ha recibido doctorados honoris causa de Katholieke Universiteit Leuven 1988, [11] Universidad de Uppsala 1994, [12] y Universidad Politécnica de Madrid 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 Humboldt Senior Scientist Award a petición de Wolfgang Bibel , que incluía una estancia de seis meses en el Departamento de Informática de la Technische Universität Darmstadt . [15] [16]
La demostración automatizada de teoremas fue iniciada en la década de 1960 por Davis y Putnam en el cálculo proposicional. En 1965, JA Robinson propuso una mecanización completa (en el sentido de un procedimiento de semidecisión) de la lógica clásica de primer orden, 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. En la década de 1970 se estudiaron muchos refinamientos de la resolución, pero se realizaron pocas implementaciones convincentes, excepto, por supuesto, que PROLOG en cierto sentido surgió de este esfuerzo.