Razonamiento automático (2004-05)
El curso se divide en tres 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 de la deducción natural, empleando el sistema Jape. Finalmente, la tercera parte aborda el estudio del razonamiento automático en lógica de orden superior, utilizando el sistema PVS.
Temas
- Tema 1: Introducción al razonamiento automático.
- Tema 2: Cálculo semántico proposicional con Mace.
- Tema 3: Resolución proposicional en Otter.
- Tema 4: Resolución de primer orden.
- Tema 5: Razonamiento automático con igualdad.
- Tema 6: Deducción natural con Jape.
- Tema 7: Cálculo proposicional en PVS.
- Tema 8: Lógica de primer orden en PVS.
- Tema 9: Teorías de primer orden en PVS.
- Tema 10: Aritmética e inducción en PVS.
- Tema 11: Lógica de orden superior en PVS.
- Tema 12: 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).
- R. Bornat Using ItL Jape with X. (Department of Computer Science, QMW, 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).