Razonamiento automático (2012-13)
Este curso ofrece una introducción al razonamiento automático 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
- Tema 1: Deducción natural proposicional con Isabelle/HOL.
- Tema 2: Deducción natural en lógica de primer orden en Isabelle/HOL.
- Tema 3: Resumen del lenguaje Isabelle/Isar y las reglas de la lógica.
- Tema 4: Programación funcional en Isabelle.
- Tema 5: Razonamiento sobre programas.
- Tema 6: Razonamiento por casos y por inducción en Isabelle/HOL.
- Tema 7: Caso de estudio: Compilacion de expresiones.
- Tema 8: Conjuntos, funciones y relaciones.
Ejercicios
- Relación 1: Deducción natural en lógica proposicional con Isabelle/HOL.
- Relación 2: Argumentación proposicional con Isabelle/HOL.
- Relación 3: Eliminación de conectivas.
- Relación 4: Deducción natural en lógica de primer con Isabelle/HOL.
- Relación 5: Argumentación en lógica de primer con Isabelle/HOL.
- Relación 6: Argumentación en lógica de primer orden e igualdad con Isabelle/HOL.
- Relación 7: Programación funcional en Isabelle/HOL.
- Relación 8: Razonamiento sobre programas en Isabelle/HOL.
- Relación 9: Cons inverso.
- Relación 10: Cuantificadores sobre listas.
- Relación 11: Sustitución, inversión y eliminación.
- Relación 12: Menor posición válida.
- Relación 13: Número de elementos válidos.
- Relación 14: Contador de occurrencias.
- Relación 15: Suma y aplanamiento de listas.
- Relación 16: Conjuntos mediante listas.
- Relación 17: Ordenación de listas por inserción.
- Relación 18: Ordenación de listas por mezcla.
- Relación 19: Recorridos de árboles.
- Relación 20: Plegados de listas y de árboles.
- Relación 21: Árboles binarios completos.
- Relación 22: Diagramas de decisión binarios.
- Relación 23: Representación de fórmulas proposicionales mediante polinomios.
Bibliografía
Visiones generales de la DAO
- J.A. Alonso. Razonamiento formalizado: Del sueño a la realidad de las pruebas. Vestigium, 26 de diciembre de 2012.
- J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
- M. Davis. The early history of automated deduction.
- J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
- J. Germoni Coq et caractères: Preuve formelle du théorème de Feit et Thompson. Images des Mathématiques, CNRS, 23 de noviembre de 2012.
- H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
- G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
- T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
- J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
- J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
- 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.
- G. Sutcliffe. What is automated theorem proving?.
- F. Wiedijk Formalizing the «top 100» of mathematical theorems.
- F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
- F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.
Referencias sobre Isabelle/HOL
- B. Grechuk Isabelle primer for mathematicians.
- T. Nipkow Programming and proving in Isabelle/HOL.
- T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic.
- Isabelle/HOL — Higher-Order Logic.
- Tutorials and manuals for Isabelle.
Lecturas complementarias
Programación funcional
- J.A. Alonso Temas de "Programación funcional". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
- J.A. Alonso y M.J. Hidalgo Piensa en Haskell (Ejercicios de programación funcional con Haskell). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
- G. Hutton Programming in Haskell. Cambridge University Press, 2007.
- M. Lipovača ¡Aprende Haskell por el bien de todos!.
Lógica computacional
- J.A. Alonso Temas de "Lógica informática" (2012-13). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
- R. Bornat Proof and disproof in formal logic: an introduction for programmers. Oxford University Press, 2005.
- K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
- K. Doets y J. van Eijck The Haskell road to logic, maths and programming.
- M. Huth y M. Ryan Logic in computer science: Modelling and reasoning about systems. Cambridge University Press, 2004. (Incluye el tutor en la Red).
Cursos relacionados
Cursos con Isabelle/HOL
- Clemens Ballarin y Gerwin Klein Introduction to the Isabelle proof assistant. (en el IJCAR-2004).
- A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported modeling and reasoning. (ETH Zurich, 2011).
- Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
- Jacques Fleuriot y Paul Jackson. Automated reasoning. (Univ. de Edimburgo, 2012-13).
- Thomas Genet Software formal analysis and design. (Univ. de Rennes)
- Gerwin Klein. Theorem proving - Principles, techniques, applications. (NICTA, 2004).
- Gerwin Klein. Advanced topics in software verification. (NICTA, 2012).
- Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
- Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
- Tobias Nipkow Theorem proving with Isabelle/HOL: an intensive course.
- Larry Paulson. Interactive formal verification. (Univ. de Cambridge, 2009-10).
- Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
- Christian Sternagel Experiments in verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
- Tjark Weber. Interactive formal verification. (Univ. de Cambridge, 2010-11).
Otros cursos
- José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
- Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi Modelling and verifying algorithms in Coq: an introduction. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
- Pierre Castéran Logic (Master in verification) (Univ. de Burdeos, 2011-12).
- Peter Lucas Knowledge representation and reasoning (Radboud University # egen, 2011-12).
- Larry Paulson Logic and proof (Univ. de Cambridge, 2011-12).
- Riccardo Pucella Logic and computation (Northeastern University, 2009). Curso con ACL2.