Verificación Formal en Lógica Modal

Ponente(s): Estefanía Prieto Larios

El teorema de la deducción en lógica clásica establece que si existe una derivación de una fórmula B a partir de un conjunto de hipótesis G y una premisa adicional A, entonces es posible construir una derivación de A -> B a partir de G. En el caso particular de la lógica modal proposicional con el operador modal de necesidad el teorema de la deducción, usando sistemas axiomáticos de Hilbert, genera una problemática acerca de su correctud. Mientras que unos autores muestran que es inválido, otros dan una prueba del mismo surgiendo así una aparente contradicción. En esta plática se presentará una solución a tal problema verificando formalmente la correctud del teorema de la deducción en la lógica modal mediante el asistente de pruebas COQ (coq.inria.fr). Adicionalmente se mostrará la equivalencia del sistema axiomático de Hilbert S4 y un sistema de deducción natural, el cual resulta más útil en la práctica. Este trabajo se realiza en el marco del proyecto UNAM PAPIME PE102117.