Una tesis doctoral automatiza la demostración de teoremas de primer orden
UN-MANIZALES/DICYT El trabajo Formalización en Isar (razonamiento inteligible semi-automático) de la Metodología de Primer Orden, se enfocó en demostrar mediante la asistencia de un software distintos teoremas matemáticos de la lógica de primer orden, la cual permite expresar cierto tipo de fórmulas donde únicamente se cuantifican las variables de un problema o una situación, operaciones con alto grado de complejidad para el hombre.
La mención CumLaude fue otorgada por la Universidad de Sevilla a la tesis doctoral realizada por Fabián Serrano, decano de la Facultad Ciencias Exactas y Naturales de la Sede Manizales.
“La automatización se realizó con sistemas de razonamiento asistido que permiten al computador efectuar operaciones que emulan el ‘pensamiento humano’, para este caso se trabajó con el programa Isabelle”, manifestó Serrano Suárez.
Este sistema contiene los axiomas (reglas) ya definidos en su base de datos a partir de los cuales se demostrará el teorema, o el investigador puede ingresarlos si desea, y a continuación se dan las indicaciones sobre los argumentos que se trabajarán con las reglas de inferencia programadas para que el sistema los resuelva.
Desde el punto de vista teórico de las matemáticas su funcionalidad está dada en la verificación de teoremas cuyas demostraciones son bastantes extensas de 200 o 300 hojas y cuya comprobación puede incluso tardar años y resultar falsa, mientras que con la automatización de este proceso se economizaría bastante tiempo y se aseguraría que la prueba es válida.
Por otro lado el sistema se puede implementar en la verificación de software, es decir que los programas desarrollados para ciertas tareas sean correctos, ya que tradicionalmente se han validado a través de datos, pero aquí se busca hacerlo de forma matemática.
El propósito ahora es trabajar con el programa en semilleros y grupos de formación en investigación en el campo de las matemáticas de manera aplicativa, así como en áreas afines como son los sistemas informáticos.