Asistentes de prueba al servicio de la lógica: una lógica modal verificada

Ponente(s): Lourdes Del Carmen González Huesca

En esta plática abordaremos un sistema axiomático para la lógica modal S4 a través de su formalización y verificación utilizando el asistente de pruebas Coq. Este asistente es versátil y ofrece gran dinamismo para formalizar teorías y sobre todo para la construcción, manipulación y verificación de demostraciones alrededor de ellas. Estas cualidades se derivan de una teoría de tipos dependiente así como de un mecanismo para manejar tácticas. Es así que esta plática también tiene por objetivo presentar al asistente mediante un recorrido de algunas de sus características usadas en nuestro ejemplo práctico: un sistema axiomático para S4 con hipótesis locales explícitas que garantiza la validez del teorema de la deducción. Esta investigación se realiza bajo el apoyo de becas posdoctorales UNAM-DGAPA, del proyecto "Lógicas modales en un ambiente de verificación formal".