Cappuccino Theorem Prover

El último proyecto en el que me veo envuelto trabajando es “Cappuccino”, un probador automático de teoremas de lógica de predicados de primer orden mediante deducción natural. En efecto, estoy desarrollando junto con mi amigo personal Juan José Conti, quien próximamente se recibe de Ingeniero en Sistemas de Información por la Universidad Tecnológica Nacional, un programa informático que posibiliará un tratamiento automatizado de sentencias lógicas permitiendo demostrar la validez o invalidez de un razonamiento.
Existen actualmente una veintena de probadores de teoremas, de los cuales quizá el más importante sea Prover9, desarrollado por un grupo de investigadores del departamento de Computer Science de The University of New Mexico, universidad en la que sin duda me gustaría hacer el PhD. No obstante, hasta donde tenemos conocimiento, ninguno de estos probadores cumple las funciones específicas que cumpliría Cappuccino, de modo que esperamos que sea un programa lo suficientemente completo como para trabajar con razonamientos reconstruidos en el lenguaje de la lógica de primer orden.
El programa actualmente está funcionando, aunque de manera limitada; pero la versión final presentaría una interfaz gráfica en donde pueden introducirse un determinado grupo de premisas y un determinado grupo de conclusiones. Cappuccino se encargaría de:
1. determinar si es posible o no llegar a la conclusión a partir de las premisas dadas utilizando los métodos de deducción natural,
2. en caso de no ser posible, buscaría una asignación en los valores de verdad tal que las premisas resulten verdaderas y la conclusión falsa (demostrando así la invalidez del razonamiento),
3. en caso de ser posible, el programa permitiría determinar el camino más corto para llegar a la conclusión y el conjunto de reglas necesarias para lograr tales fines. Cappuccino también trabajaría con las formas normales prenexas, lo cual permitiría solucionar ciertas falencias del sistema deductivo.
Cappuccino está siendo desarrollado en el lenguaje de programación Python, que si bien trabaja a más alto nivel que C o C++ por ejemplo, su sintaxis simplificada permite un mejor tratamiento a la hora de enfrentar el desafío que supone la construcción de un probador de teoremas. Por lo pronto, habrá que seguir trabajando para que este Cappuccino no se enfríe.