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.

Jornadas Nacionales de Pensamiento Argentino y Latinoamericano

El 1 y 2 de Noviembre de 2007 se realizaron en la ciudad de Rosario las Jornadas Nacionales de Pensamiento Argentino y Latinoamericano, evento en el que fui convocado y estuve participando como panelista abordando la temática de las relaciones que pueden establecerse entre la Teología de la Liberación y el socialismo. La exposición estuvo basada en un ensayo escrito hace un par de años que se titula Teología de la Liberación: ¿el rostro eclesiástico del socialismo?.
El evento fue organizado y llevado a cabo por un grupo de docentes de la carrera de Filosofía de la Facultad de Humanidades y Artes de la Universidad Nacional de Rosario y contó también con la participación de reconocidos especialistas en el ámbito del pensamiento argentino y latinoamericano.