Razonamiento automático (2005-06)
El curso se divide en dos partes. La primera parte se enfoca en el estudio del razonamiento automático en lógica de primer orden, utilizando los sistemas Otter y Mace2. La segunda parte se centra en el estudio del razonamiento automático en lógica de orden superior, utilizando el sistema PVS.
El curso forma parte del Programa de Doctorado "Lógica, Computación e Inteligencia Artificial" del Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla.
Temas
- Tema 0: Introducción al razonamiento automático.
- Tema 1: Lógica de primer orden.
- Tema 2: Razonamiento proposicional con Otter y Mace.
- Tema 3: Razonamiento de primer orden con Otter y Mace.
- Tema 4: Razonamiento ecuacional con Otter.
- Tema 5: Cálculo proposicional en PVS.
- Tema 6: Lógica de primer orden en PVS.
- Tema 7: Teorías de primer orden en PVS.
- Tema 8: Aritmética e inducción en PVS.
- Tema 9: Lógica de orden superior en PVS.
- Tema 10: Tipos abstractos de datos en PVS.
Bibliografía
- J.A. Alonso, A. Fernández y M.J. Pérez. Razonamiento automático (Univ. Sevilla, 1996).
- C. Badesa, I. Jané, R. Jansana. Elementos de lógica formal. Editorial Ariel, 1998).
- A. Bundy. The computer modelling of mathematical reasoning. (Academic Press, 1983).
- C.L. Chang y R.C.T. Lee. Symbolic logic and mechanical theorem proving. (Academic Press, 1973).
- J. Crow, S. Owre, J. Rushby, N. Shankar y M. Srivas. A tutorial introduction to PVS. (SRI International, 1995).
- M. Davis. The early history of automated deduction.
- J.A. Díez. Iniciación a la lógica. (Ed. Ariel, 2002).
- J.L. Fernández, A. Manjarrés y F.J. Díez. Lógica computacional. (UNED, 2003).
- 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.
- G. Kolata. Computer math proof shows reasoning power (The New York Times, 10 de diciembre de 1996).
- D. MacKenzie. Computers and the sociology of mathematical proof.
- W. McCune. Otter 3.3 reference manual.
- N.J. Nilsson. Artificial intelligence: A new synthesis. (McGraw–Hill, 1998).
- E. Paniagua, J.L. Sánchez y F. Martín. Lógica computacional. (Thomson, 2003).
- L. Wos, R. Overbeek, E. Lusk. y J. Boyle. Automated reasoning: Introduction and applications. (McGraw–Hill, 1992).