Lógica informática (2004-05)
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 de la Ingeniería informática de la Universidad de Sevilla.
Temas y ejercicios
- Tema 1: Sintaxis y semántica de la lógica proposicional y ejercicios.
- Tema 2: Deducción natural proposicional y ejercicios.
- Tema 3: Formas normales y ejercicios.
- Tema 4: Tableros semánticos y ejercicios.
- Tema 5: Resolución proposicional y ejercicios.
- Tema 6: Sintaxis y semántica de la lógica de primer orden y ejercicios.
- Tema 7: Deducción natural en lógica de primer orden y ejercicios.
- Tema 8: Formas normales. Cláusulas.
- Tema 9: Resolución en lógica de primer orden y ejercicios.
Exámenes
- Primer parcial (Lógica proposicional):
- Segundo parcial (Lógica de primer orden):
- Examen de Junio
- Examen de Septiembre
Bibliografía
- Ben-Ari, M. Mathematical logic for computer science. (Springer, 2001).
- Chang, C.L. y Lee, R.C.T. Symbolic logic and mechanical theorem proving. (Academic Press, 1973).
- Cuena, J. Lógica informática (Alianza Ed., 1985).
- Doets, K. From logic to logic programming. (MIT Press, 1994).
- Díez, J.A. Iniciación a la lógica. (Ed. Ariel, 2002).
- Fernández, J.L.; Manjarrés, A. y Díez, F.J. Lógica computacional. (UNED, 2003).
- Fitting, M. First-order logic and automated theorem proving. (Springer, 1996).
- Genesereth, M.R. y Nilsson, N.J. Logical foundations of artificial intelligence. (Morgan Kaufmann, 1987).
- Huth, M. y Ryan, M. Logic in computer science: Modelling and reasoning about systems (Cambridge University Press, 2000). Incluye el tutor en la Red.
- Nerode, A. y Shore, R.A. Logic for applications. (Springer, 1997).
- Paniagua, E.; Sánchez, J.L. y Martín, F. Lógica computacional. (Thomson, 2003).
- Paulson, L. Logic and proof (U. Cambridge, 2003).
- Schöning, U. Logic for computer scientists. (Birkäuser, 1989).
Sistemas
- Tablas de verdad: Programa de N.S. Burris.
- Tableros semánticos: Tree proof generator.
- Deducción natural: Jape y cálculo para la asignatura LI.