Premio Herbrand

Entregado desde 1992 el Premio Herbrand se otorga anualmente a un científico o a un grupo de investigación por sus contribuciones en el área de razonamiento automatizado.

El premio lleva el nombre del matemático y lógico francés Jacques Herbrand (1908-1931) y es considerado el premio de más renombre internacional en esta área.

• 1992 Larry Wos, por sus contribuciones excepcionales en el área razonamiento automatizado.
• 1994 Woody Bledsoe, por sus contribuciones excepcionales en el área razonamiento automatizado.
• 1996 Alan Robinson, por sus contribuciones excepcionales en el área razonamiento automatizado.
• 1997 Wu Wen-Tsun, por sus contribuciones excepcionales en el área razonamiento automatizado.
• 1998 Gerard Huet, por sus contribuciones en sistemas de reescritura y deducción automatizada en lógica de alto nivel, así como muchas otras contribuciones en el área razonamiento automatizado.
• 1999 Robert Boyer y J Strother Moore, por su trabajo en la automatización de la inferencia inductiva y su aplicación a la verificación de hardware y de software.
• 2000 William W. McCune
• 2001 Donald Loveland, por el desarrollo del proceso de eliminación de modelos, por sus contribuciones en verificación de satisfacibilidad proposicional en el proceso Davis-Putnam-Logemann-Loveland, por su trabajo en la familia de cálculos casi-Horn Prolog para programación lógica disyuntiva y muchas otras contribuciones en el área de razonamiento automatizado.
• 2002 Mark Stickel, por sus descubrimientos en unificación asociativa-conmutativa, razonamiento módulo una teoría, indexación de términos, y por su contribución en el desarrollo de los demostradores SNARK y PTTP, así como muchas otras contribuciones en el área de razonamiento automatizado.
• 2003 Peter Andrews, por sus contribuciones, pioneras en el área de teoría de tipos, demostración asistida basada en mating, deducción automatizada en lógica de alto nivel, presentación de pruebas, educación en lógica y sus muchas otras contribuciones en el área de razonamiento automatizado.
• 2004 Harald Ganzinger, por sus trabajos que han servido de base para los sistemas de deducción automatizada; la amplitud de su investigación, la cual cubre prácticamente todas las áreas de deducción, y lo profundo de sus resultados en cada una de ellas; así como sus contribuciones efectivas al desarrollo de sistemas y técnicas de implementación.
• 2005 Martin Davis
• 2006 Wolfgang Bibel
• 2007 Alan Bundy
• 2008 Edmund M. Clarke
• 2009 Deepak Kapur
• 2010 David Plaisted
• 2011 Nachum Dershowitz
• 2012 Melvin Fitting
• 2013 Greg Nelson
• 2014 Robert Lee Constable
• 2015 Andrei Voronkov
• 2016 Zohar Manna y Richard Waldinger

Association for Automated Reasoning