Martin David Davis (8 de marzo de 1928 - 1 de enero de 2023) fue un matemático y científico informático estadounidense que contribuyó a los campos de la teoría de la computabilidad y la lógica matemática . Su trabajo sobre el décimo problema de Hilbert condujo al teorema MRDP . También desarrolló el modelo Post-Turing y co-desarrolló el algoritmo Davis-Putnam-Logemann-Loveland (DPLL) , que es fundamental para los solucionadores de satisfacibilidad booleana .
Davis ganó el premio Leroy P. Steele , el premio Chauvenet (con Reuben Hersh ) y el premio Lester R. Ford . Fue miembro de la Academia Estadounidense de las Artes y las Ciencias y de la Sociedad Estadounidense de Matemáticas .
Los padres de Davis eran inmigrantes judíos de Łódź , Polonia, que llegaron a los Estados Unidos y se casaron después de reencontrarse en la ciudad de Nueva York. Davis nació en la ciudad de Nueva York el 8 de marzo de 1928. Creció en el Bronx , donde sus padres lo alentaron a obtener una educación completa. [1] [2] Se graduó en la prestigiosa Bronx High School of Science en 1944 y recibió su licenciatura en matemáticas en el City College en 1948 y su doctorado en la Universidad de Princeton en 1950. [3] Su tesis doctoral, titulada On the Theory of Recursive Unsolvability , fue supervisada por el matemático y científico informático estadounidense Alonzo Church . [1] [2] [4]
Durante una pasantía de investigación en la Universidad de Illinois en Urbana-Champaign a principios de la década de 1950, se unió al Laboratorio de Sistemas de Control y se convirtió en uno de los primeros programadores del ORDVAC . [1] Más tarde trabajó en Bell Labs y en la Corporación RAND antes de unirse a la Universidad de Nueva York . [1] Durante su tiempo en la Universidad de Nueva York, ayudó a establecer el departamento de informática de la universidad. Se jubiló de la Universidad de Nueva York en 1996. [3] [1] Más tarde fue miembro del cuerpo docente visitante en la Universidad de California, Berkeley . [5]
Davis trabajó por primera vez en el décimo problema de Hilbert durante su tesis doctoral, en colaboración con Alonzo Church. El teorema, tal como lo planteó el matemático alemán David Hilbert , plantea una pregunta: dada una ecuación diofántica , ¿existe un algoritmo que pueda decidir si la ecuación es solucionable? [1] La tesis de Davis planteó una conjetura de que el problema era irresoluble. En las décadas de 1950 y 1960, Davis, junto con los matemáticos estadounidenses Hilary Putnam y Julia Robinson , avanzaron hacia la solución de esta conjetura. La prueba de la conjetura finalmente se completó en 1970 con el trabajo del matemático ruso Yuri Matiyasevich . Esto dio como resultado el teorema MRDP o DPRM , llamado así por Davis, Putnam, Robinson y Matiyasevich. [1] Al describir el problema, Davis había mencionado anteriormente que lo encontró "irresistiblemente seductor" cuando era estudiante universitario y que luego se había convertido progresivamente en su "obsesión de toda la vida". [6]
Davis colaboró con Putnam, George Logemann y Donald W. Loveland en 1961 para introducir el algoritmo Davis–Putnam–Logemann–Loveland (DPLL) , que era un algoritmo de búsqueda completo basado en retroceso para decidir la satisfacibilidad de fórmulas de lógica proposicional en forma normal conjuntiva , es decir, para resolver el problema CNF-SAT . [7] El algoritmo fue un refinamiento del algoritmo Davis–Putnam anterior , que era un procedimiento basado en resolución desarrollado por Davis y Putnam en 1960. [8] [9] El algoritmo es fundamental en la arquitectura de solucionadores rápidos de satisfacibilidad booleana. [6]
Además de su trabajo sobre la teoría de la computabilidad , Davis también hizo contribuciones significativas en los campos de la complejidad computacional y la lógica matemática . [1] [6] [10] Davis también fue conocido por su modelo de máquinas Post-Turing . [3]
En 1974, Davis ganó el Premio Lester R. Ford por sus escritos expositivos relacionados con su trabajo sobre el décimo problema de Hilbert, [2] [11] y en 1975 ganó el Premio Leroy P. Steele y el Premio Chauvenet (con Reuben Hersh ). [12] Se convirtió en miembro de la Academia Estadounidense de las Artes y las Ciencias en 1982, [2] y en 2013, fue seleccionado como uno de los miembros inaugurales de la Sociedad Matemática Estadounidense . [13]
El libro de Davis de 1958 Computability and Unsolvability se considera un clásico en la informática teórica , mientras que su libro de 2000 The Universal Computer traza la evolución y la historia de la informática comenzando con los trabajos de Gottfried Wilhelm Leibniz y Alan Turing . [1] Su libro The Undecidable , cuya primera edición se publicó en 1965, fue una colección de problemas irresolubles y funciones computables . [6]
Davis se casó con Virginia Whiteford Palmer, una artista textil. La pareja se conoció durante su estancia en el área de Urbana-Champaign y posteriormente se casó en 1951. [14] : 8 Tuvieron dos hijos. [3] La pareja vivió en Berkeley, California , después de su jubilación. [1]
Davis murió el 1 de enero de 2023, a los 94 años. [15] Su esposa murió el mismo día varias horas después. [16]
Libros
Artículos
