Un sistema deductivo para la lógica en la práctica.

Ponente(s): Pilar Selene Linares Arevalo, Lourdes del Carmen González Huesca
Con el objetivo de obtener una transición directa entre la lógica matemática tradicional y la lógica aplicada (aquella que se utiliza en la formalización de las matemáticas y en métodos formales para ingeniería de software) hemos diseñado un sistema de deducción para la lógica clásica de primer orden con igualdad. Este sistema de deducción, inspirado en los mecanismos de prueba interactivos que ofrece el asistente de pruebas Coq, es una herramienta que captura el razonamiento matemático cotidiano. En esta ponencia presentaremos las características de nuestro sistema de deducción y daremos un paseo por las diferentes etapas de su desarrollo. También veremos cómo se relaciona con las demostraciones que generamos todos los días en las aulas y sus aplicaciones en la formalización de las matemáticas y métodos formales. Este trabajo se realiza con el apoyo del proyecto UNAM PAPIME PE102117.