Deducción natural en lógica modal: una implementación en Coq

Ponente: Selene Linares (Maestría en Ciencia e Ingeniería de la Computación, UNAM)

Fecha: 24 de marzo, 12hrs
Lugar: Sala de Investigadores Fernando Salmerón, Instituto de Investigaciones Filosóficas, UNAM

Resumen: Los marcos lógicos (logical framework) son metalenguajes para la formalización de sistemas deductivos, éstos se han utilizado con éxito en la demostración interactiva/automatizada de teoremas.

La Lógica Modal es considerada difícil de implementar de una manera directa en marcos lógicos, pues estos son adecuados para la codificación de los formalismos de Deducción Natural. En la literatura se encuentran diversas propuestas de implementaciones de la Lógica Modal en marcos lógicos pero éstas son en estilo Hilbert y muy ad hoc.

En esta charla, presentaré el sistema de Deducción Natural para la Lógica Modal Intuicionista - propuesto por Frank Pfenning y Rowan Davies - de cual se afirma, no presenta las anomalías encontradas en otras formulaciones. Mostraré la implementación de este sistema de Deducción Natural en el asistente de pruebas Coq, así como la demostración de diversas propriedades del mismo.


Presentación.