Maquinas que resuelven y deducen Teoremas

La máquina de Gelernter Herbert Gelernter era un físico que trabajaba en IBM que hacia 1960 creó una máquina con capacidad para deducir teoremas de la geometría euclídea elemental, la Geometry Theorem Prover (GTP), esto es, la Demostradora de Teoremas de Geometría. La GTP funcionaba de atrás a adelante, es decir, a partir del teorema a demostrar el programa iba construyendo diagramas de resultados intermedios hasta llegar a axiomas o a teoremas conocidos. Pero lo más sorprendente no fue eso, sino que la máquina consiguió encontrar una elegante y tremendamente ingeniosa demostración de un teorema, conocido como pons asinorum, de la que el creador no tenía constancia. Mas información : http://gaussianos.com/la-maquina-de-gelernter/