Un teorema demostrado por computador.

Es posible demostrar por computador teoremas matemAticos, generalmente de 
Algebra, a condiciOn que sean fAciles de expresar en sImbolos lOgicos.  
Esta tEcnica se basa en el resultado de la lOgica siguiente: si un 
teorema es cierto, existe una demostracion (una cadena de ecuaciones 
lOgicas, que utilizan solamente axiomas dados y conducen al teorema).  
Intuitivamente, basta entonces con probar por computador todas las 
combinaciones posibles y la demostracion saldra algun dia.

Lastimosamente, en general, ese dia esta lejos!  A diferencia del 
matemAtico, el programa no tiene intuiciOn, el se bloquea en los puntos 
muertos, no descubre los atajos.  Asi, el tiempo de ejecuciOn se vuelve 
disuasivo: crece exponencialmente con el nUmero de axiomas utilizados.  
Es tarea, entonces, del programador cortar las ramificaciones inUtiles, a 
riesgo de perder el buen camino.  Tecnicas como esta han permitido a un 
investigador del laboratorio de Argonne (Estados Unidos) demostrar un 
resultado de Algebra que se resisitIa desde los an~os 30 (W. McCune, J. 
Automated Reasoning, en impresion).

Despues de ocho dIas de cAlculos sobre tres estaciones de trabajo, 
aparecio que un conjunto de tres ecuaciones lOgicas, llamadas de Robbins, 
se reducen a los axiomas del algebra de Boole (definida por los elementos 
0 y 1, y las leyes de la adiciOn, la multiplicaciOn y el complemento a 
1).  La prueba ha sido dada por una mAquina, pero no se puede dudar de su 
validez como se harIa para un cAlculo numErico ya que el software trabaja 
sobre expresiones lOgicas y no sobre nUmeros en coma flotante.  La 
hazan~a no dejarA, sin embargo, sin empleo a los matemAticos, dado que el 
software de Argonne no puede aplicarse sino a una clase muy restringida 
de axiomas.

--------- Fin de texto ------------

Quedan entonces planteadas las dudas respecto a la verdadera 
imposibilidad de darle intuicion a un sistema artificial, de tener un 
sistema que sea capaz de aprender a demostrar (por ejemplo entrenarlo con 
un gran conjunto de demostraciones ya conocidas), aplicar programacion 
genetica, o alguna otra tecnica de aproximacion similar.

Bueno ahi les queda la duda.
_______________________________________________________________________
Carlos Andres Pen~a R.
Institute d'Automatique
Ecole Polytechnique Federale de Lausanne
Suisse
	_________________________________________________
	E-mail  :       c.penha@ieee.org
			penha@dmehpi-f.epfl.ch