Razonamiento automático (2011-12)
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 Máster Universitario en 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
- 2ª parte: Razonamiento automático con Otter y Mace
- 3ª parte: Razonamiento interactivo con Isabelle/HOL
- Tema 6: Isabelle como un lenguaje funcional y código.
- Tema 7: El lenguaje de demostración Isar y código.
- Tema 8: Distinción de casos e inducción y código.
- Tema 9: Patrones de demostración y código.
- Tema 10: Heurísticas para la inducción y recursión general y código.
- Tema 11: Caso de estudio: Corrección de un compilador y código.
- Tema 12: Conjuntos, funciones y relaciones.
Ejercicios
Ejercicios resueltos
Ejercicios de deducción natural
Razonamiento por inducción sobre listas
Bibliografía
- J.A. Alonso. Introducción a la demostración asistida por ordenador (con Isabelle/HOL). (Universidad de Sevilla, 2010).
- 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?