Sesión Lógica y ComputabilidadTeoremas de normalización y de eliminación de corte para algunas lógicas de evidencia y verdad
Martín Figallo
Universidad Nacional del Sur, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
En esta charla, analizaremos a las lógicas de evidencia y verdad \(LET_J\) y \(LET_K\) desde el punto de vista de la teoría de la prueba. Estas lógicas extienden, respectivamente, a la lógica de Nelson \(N4\) y a la lógica de first-degree entailment (\(\bf FDE\)), también conocida como lógica cuatro-valuada de Belnap-Dunn, con un operador de clasicalidad \(\circ\) que recupera la lógica clásica para fórmulas en su alcance.
Presentaremos sistemas de deducción natural y de secuentes para \(LET_J\) y \(LET_K\), junto a los respectivos teoremas de normalización y de eliminación de corte. Como aplicación, obtendremos procedimientos de deducción que garantizan la búsquedas de pruebas bottom-up, para ambas lógicas.
Trabajo en conjunto con: Marcelo Coniglio (UNICAMP) y Abilio Rodrigues (Federal University of Minas Gerais).