Acerca de algunos sistemas de prueba para la Lógica Modal

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

El estudio de diferentes lógicas modales ha permitido desarrollar sistemas de prueba particulares para llevar a cabo razonamientos y demostraciones. Estos sistemas van desde los puramente sintácticos hasta los semánticos y combinaciones de ellos. Algunos sistemas de prueba para lógicas modales, que se ha demostrado son equivalentes, son los axiomáticos o de Hilbert, sistemas de deducción natural y otros basados en el cálculo de secuentes propuesto por Gentzen. Estos sistemas han resultado ineficientes para resolver ciertos problemas haciendo que se propongan diferentes generalizaciones: display calculi, sistemas de hipersecuentes y sistemas con etiquetas (labelled systems). En esta plática revisaremos estos sistemas de prueba haciendo énfasis en sus características distintivas y comparando sus aplicaciones. Lo anterior motivado por la búsqueda de un sistema de prueba que favorezca la mecanización de pruebas mediante un demostrador de teoremas interactivo.