Abstract:
El Santo Grial de las matemáticas es tener un algoritmo que pueda demostrar o refutar automáticamente cualquier enunciado matemático. Aunque sabemos desde hace casi 100 años que un algoritmo tan general no puede existir, sí que es posible obtener métodos de demostración automática en algunos casos particulares. Estos métodos cobran especial relevancia para la verificación formal de programas informáticos. En esta charla presentaré algunos de los objetivos de la investigación en lógica en ciencias de la computación. En particular, explicaré cómo y por qué el estudio de juegos combinatorios puede hacer avanzar estos problemas.