Lógica matemática y fundamentos (2012-13)
Este curso proporciona una introducción a los fundamentos de la lógica proposicional y la lógica de primer orden. En ambos sistemas, se exploran distintos cálculos lógicos y procedimientos de decisión, combinando el estudio teórico con aplicaciones prácticas.
El programa incluye:
- Implementaciones en Haskell de los conceptos lógicos
- Demostraciones en Isabelle/HOL de ejercicios de deducción natural
Se trata de una asignatura obligatoria del tercer año del del Grado en Matemáticas de la Universidad de Sevilla, diseñada para dotar al estudiante de herramientas formales esenciales en el razonamiento matemático.
Temas
- Lógica proposicional:
- Lógica de primer orden:
- Tema 7: Sintaxis y semántica de la lógica de primer orden.
- Tema 8: Deducción natural en lógica de primer orden.
- Tema 9: Tableros semánticos en lógica de primer orden.
- Tema 10: Formas normales de Skolem y cláusulas.
- Tema 11: Modelos de Herbrand.
- Tema 12: Resolución en lógica de primer orden.
- Tema 13: Introducción a la programación lógica con Prolog.
- Tema 14: Formalización en Prolog de la lógica proposicional.
- Tema 15: Soluciones lógicas de problemas lógicos.
Prácticas
Relaciones de ejercicios
- Relación 1 : Iniciación a la programación con Haskell.
- Relación 2 : Sintaxis y semántica de la lógica proposicional en Haskell.
- Relación 3 : Deducción natural proposicional con Isabelle/HOL.
- Relación 4 : Argumentación proposicional con Isabelle/HOL.
- Relación 5 : Eliminación de conectivas.
- Relación 6 : Formalización de argumentos en lógica de primer orden.
- Relación 7 : Deducción natural en lógica de primer con Isabelle/HOL.
- Relación 8 : Tableros semánticos proposicionales en Haskell.
- Relación 9 : Formas normales en lógica proposicional en Haskell.
- Relación 10 : Cláusulas proposicionales en Haskell.
- Relación 11 : Resolución proposicional en Haskell.
- Relación 12 : Aplicaciones de la Lógica Proposicional en Haskell.
- Relación 13 : Programación funcional en Isabelle/HOL.
- Relación 14 : Razonamiento sobre programas con Isabelle/HOL.
Teorías Isabelle/HOL
Ejercicios evaluables
- Ejercicio 1: Deducción natural en lógica proposicional con Isabelle/HOL.
- Ejercicio 2: Deducción natural en lógica de primer orden con Isabelle/HOL.
- Ejercicio 3: Argumentación, deducción natural en lógica de primer orden con Isabelle/HOL y tableros semánticos.
- Ejercicio 4: Algoritmos de lógica proposicional en Haskell.
- Ejercicio 5: Formas normales condicionales (Haskell e Isabelle/HOL).
Libros con los temas, ejercicios y exámenes
- En Temas de "Lógica matemática y fundamentos" (2012-13) se encuentran las transparencias de todo el curso en forma de libro.
- En Ejercicios de "Lógica matemática y fundamentos" (2012-13) se encuentran los ejercicios de todo el curso en forma de libro.
- En 50 ejercicios de argumentación se encuentran los enunciados de los ejercicios de formalización de argumentos.
Bibliografía
- M. Ben-Ari. Mathematical logic for computer science. (Springer, 2001).
- I. Bratko. Prolog programming for artificial intelligence (3 ed.). (Addison Wesley, 2001).
- K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers. Reasoned programming. (Imperial College, 1994).
- M. Fitting. First-order logic and automated theorem proving. (Springer, 1996).
- J.H. Gallier. Logic for computer science (Foundations of automatic theorem proving). (Wiley, 1986).
- M.R. Genesereth y N.J. Nilsson. Logical foundations of artificial intelligence. (Morgan Kaufmann, 1987).
- C. Hall y J. O'Donnell Discrete mathematics using a computer. (Springer, 2000).
- M. Huth y M. Ryan. Logic in computer science: Modelling and reasoning about systems (Cambridge University Press, 2000). Incluye el tutor en la Red.
- A. Nerode y R.A. Shore. Logic for applications. (Springer, 1997).
- L. Paulson. Logic and proof (U. Cambridge, 2003).
- S. Reeves y M. Clarke Logic for computer science. (Addison-Wesley 1990 & 2003).
- U. Schöning. Logic for computer scientists. (Birkäuser, 1989).