Lógica matemática y fundamentos (2019-20)
Este curso ofrece una introducción completa a la lógica matemática y la programación funcional utilizando Isabelle/HOL, cubriendo desde los fundamentos de la lógica proposicional y de primer orden hasta técnicas avanzadas de razonamiento formal. A lo largo de los temas, se exploran la sintaxis y semántica de la lógica, la deducción natural (tanto en papel como en Isabelle/HOL), la programación funcional, el razonamiento sobre programas, inducción, estructuras como árboles y bosques, definiciones inductivas, y el desarrollo de teorías formalizadas. El material incluye clases grabadas disponibles en YouTube, así como relaciones de ejercicios con soluciones (especialmente en los temas prácticos con Isabelle/HOL), lo que permite un aprendizaje teórico y aplicado.
El curso es una asignatura del tercer año del Grado en Matemáticas de la Universidad de Sevilla.
Temas
- Tema 1: Sintaxis y semántica de la lógica proposicional.
- Tema 2a: Deducción natural proposicional.
- Tema 2b: Deducción natural proposicional en Isabelle/HOL.
- Tema 3: Sintaxis y semántica de la lógica de primer orden.
- Tema 4a: Deducción natural en lógica de primer orden.
- Tema 4b: Deducción natural en lógica de primer orden en Isabelle/HOL.
- Tema 5: Programación funcional en Isabelle/HOL.
- Tema 6a: Razonamiento sobre programas.
- Tema 6b: Razonamiento sobre programas en Isabelle/HOL.
- Tema 7: Razonamiento por casos y por inducción.
- Tema 8: Razonamiento sobre árboles y bosques.
- Tema 9: Definiciones inductivas.
- Tema 10: Conjuntos, funciones y relaciones.
- Tema 11: Desarrollo de teorías formalizadas con Isabelle/HOL.
Nota: Todas las clases están grabadas y disponibles en esta lista de reproducción de YouTube.
Ejercicios, tareas y exámenes
Relaciones de ejercicios
- Relación 1: Sintaxis y semántica de la lógica proposicional.
- Relación 2: Deducción natural proposicional con Isabelle.
- Relación 3: Deducción natural proposicional con Isabelle (II).
- Relación 4: Sintaxis y semántica de la lógica de primer orden.
- Relación 5: Deducción natural en lógica de primer orden.
- Relación 6: Formalización y argumentación con Isabelle/HOL.
- Relación 7: Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.
- Relación 8: Programación funcional en Isabelle/HOL.
- Relación 9: Programación funcional en Isabelle/HOL (II).
- Relación 10: Razonamiento sobre programas en Isabelle/HOL.
- Relación 11: Razonamiento sobre programas en Isabelle/HOL(II).
- Relación 12: Razonamiento sobre programas en Isabelle/HOL(III).
- Relación 13: Recorridos de árboles.
- Relación 14: Una axiomatización de la Geometría.
- Relación 15: Definiciones inductivas: clausuras.
Nota: En las relaciones de ejercicios con Isabelle/HOL (la 2, 3, 6 y de la 7 a la 15) incluye sus soluciones.
Tareas
Exámenes
Libros con los temas, ejercicios y exámenes
- En Temas de "Lógica matemática y fundamentos" (2019-20) se encuentran las transparencias de todo el curso en forma de libro.
- En Ejercicios de "Lógica matemática y fundamentos" (2019-20) se encuentran los ejercicios de todo el curso en forma de libro.
Bibliografía
Libros
- R. Bornat.Proof and disproof in formal logic: an introduction for programmers]] (Oxford University Press, 2005)
- K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers. Reasoned programming. (Imperial College, 1994)
- M. Huth y M. Ryan. Logic in computer science: Modelling and reasoning about systems (Cambridge University Press, 2004) [Incluye el tutor en la Red].
Isabelle/HOL
Cursos relacionados
- J. Fleuriot. Automated reasoning. (Univ. de Edimburgo).
- G. Smolka. Introduction to computational logic (Univ. de Sarre).
- B.C. Peirce et als. Software foundations (Vol. 1: Logical foundations) (Univ. de Pensilvania).
- J. Blanchette y J. Höltz. Logical verification (Vrije Universiteit Amsterdam).
- M. Greenberg. Discrete mathematics and functional programming.