Razonamiento automático (2007-08)
Este curso ofrece una introducción completa al razonamiento automático, abarcando dos importantes paradigmas:
- Razonamiento automático Otter (o Prover9) y Mace4.
- Razonamiento asistido con Isabelle/HOL.
La asignatura forma parte del Programa de Doctorado "Lógica, Computación e Inteligencia Artificial" impartido por el Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla.
Temas
- 1ª parte: Introducción
- Tema 0: Introducción al razonamiento automático.
- Tema 1: Lógica de primer orden.
- 2ª parte: Razonamiento automático con Otter y Mace
- 3ª parte: Razonamiento asistido con Isabelle/HOL
- Tema 6: Isabelle como un lenguaje funcional.
- Tema 7: El lenguaje de demostracion Isar.
- Tema 8: Distinción de casos e inducción.
- Tema 9: Patrones de demostración.
- Tema 10: Heurísticas para la inducción y recursión general.
- Tema 11: Caso de estudio: Corrección de un compilador.
Bibliografía
- J.A. Alonso. Introducción a la demostración asistida por ordenador (con Isabelle/Isar). (Universidad de Sevilla, 2008).
- M. Davis. The early history of automated deduction.
- D. MacKenzie Computers and the sociology of mathematical proof.
- G. Kolata. Computer math proof shows reasoning power. (The New York Times, 10 de diciembre de 1996).
- T. Nipkow, L.C. Paulson, M. Wenzel. A proof assistant for Higher-Order Logic.
- G. Sutcliffe. What is automated theorem proving?