Lógica informática (2013-14)
Este curso ofrece una introducción a los principales conceptos de la lógica proposicional y de la lógica de primer orden. Para ambas, se estudian diversos cálculos y procedimientos de decisión.
Es una asignatura obligatoria de segundo curso del Grado en Ingeniería informática de la Universidad de Sevilla.
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.
Libros con los temas, ejercicios y exámenes
- En Temas de "Lógica informática" (2013-14) se encuentran las transparencias de todo el curso en forma de libro.
- En Ejercicios de "Lógica informática" (2013-14) 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.
- En Ejercicios de deducción natural proposicional se encuentran las soluciones de los ejercicios propuestos de deducción natural proposicional.
- En Ejercicios de deducción natural en lógica de primer orden se encuentran las soluciones de los ejercicios propuestos de deducción natural en lógica de primer orden.
Bibliografía
- J.A. Alonso y J. Borrego Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos) (Ed. Kronos, 2002).
- C. Badesa, I. Jané, R. Jansana. Elementos de lógica formal. Editorial Ariel, 1998).
- 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).
- 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).
Sistemas
- Formalización:
- Tablas de verdad, árboles de formación y formas normales:
- Deducción natural:
- Tableros semánticos:
- Resolución:
- Prolog:
- SWI Prolog
- SldDraw: Herramienta para representar árboles SLD.