Herbert Gelernter no es un personaje demasiado conocido y fuera del ámbito académico estadounidense y del campo de la investigación en computación su nombre no evoca absolutamente nada en la mayoría de la gente. A pesar de este desconocimiento masivo cabe destacar a Gelernter como el constructor de una máquina increíblemente avanzada para su tiempo capaz de demostrar teoremas matemáticos.
Con el campo de la inteligencia artificial todavía en fase embrionaria buena parte de los esfuerzos invertidos en investigación en el campo de la computación durante los años 60 y 70 se dirigieron a crear máquinas que siguieran un patrón de resolución de problemas similar al de los humanos, que pudieran aprender de sus éxitos y errores y que no tuvieran un comportamiento completamente pautado. Una de las máquinas creadas con esta intención fue la máquina de Gelernter.
Herbert Gelernter construyó hacia 1960 una máquina con capacidad para deducir teoremas dentro del marco de la geometría euclídea elemental. Esta máquina denominada Geometry Theorem Prover (Demostradora de Teoremas de Geometría) seguía una estrategia descendente para la resolución de problemas: a partir del teorema a demostrar iba retrocediendo y construyendo resultados intermedios hasta llegar a axiomas o teoremas conocidos. Para evitar el problema de la explosión de ramas que surgen en cada paso Gelernter añadió un módulo que comprobaba numéricamente algunos casos ayudando así a enfocar mejor el problema y a desechar ramas sin salida con menor esfuerzo.
Lo más sorprendente de esta máquina fue que consiguió encontrar una solución al teorema pons asinorum o teorema del rectángulo isósceles que el propio creador de la máquina desconocía por completo. No queremos decir que la máquina “pensara” pero sí que el programa que la regía tenía la capacidad de explorar otras vías de resolución de problemas en las que su creador no había reparado.
Hoy en día existen varios tipos de herramientas de demostración automática de teoremas con múltiples aplicaciones en el campo de la electrónica digital y su diseño y funcionamiento sigue siendo un tema que enfoca el interés de investigadores en todo el mundo. La máquina de Gelernter fue uno de los primeros demostradores automáticos de teoremas y por tanto precursor de los que a día de hoy demuestran el correcto funcionamiento de nuestros microprocesadores.
Una máquina ingeniosa y sorprendente, ¿la conocías?
