Razonamiento automático (2010-11)
Este curso ofrece una introducción al razonamiento automático usando el sistema 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
- Tema 0: Presentación del razonamiento automático.
- Tema 1: Isabelle como un lenguaje funcional.
- Tema 2: El lenguaje de demostracion Isar.
- Tema 3: Distinción de casos e inducción.
- Tema 4: Patrones de demostración.
- Tema 5: Heurísticas para la inducción y recursión general.
- Tema 6: Caso de estudio: Corrección de un compilador.
- Tema 7: Conjuntos, funciones y relaciones.
Apuntes y códigos
- En Introducción a la demostración asistida por ordenador (con Isabelle/Isar) se encuentra un libro con los apuntes del curso.
- En teorias.tgz se encuentra el código de todas las teorías.
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?