Fecha: 23 de Septiembre, 12hrs
Lugar: Sala de Investigadores Fernando Salméron, Instituto de Investigaciones Filosóficas, UNAM
Resumen: La lógica minimal constructiva se obtiene al eliminar completamente la
negación de la lógica clásica. El resultado, desde el punto de vista de
la teoría de la demostración, es un sistema deductivo donde las reglas
de inferencia mantienen una dualidad introducción/eliminación que genera
un mecanismo determinista de construcción y verificación de pruebas.
Esta característica permite que las reglas de la lógica sean invertibles
y sirvan como un sistema de tácticas que ayudan al desarrollo, tanto de
teoremas matemáticos como de validaciones de especificaciones de
software mediante los sistemas computacionales llamados asistentes de
prueba. En esta plática daremos un breve panorama de los fundamentos y
aplicaciones de la lógica constructiva sirviendonos del asistente de
prueba Coq (http://coq.inria.fr).
Presentación
Presentación
No hay comentarios.:
Publicar un comentario