Razonamiento automático (2018-19)
Este curso introduce los fundamentos del razonamiento formal y la verificación de programas utilizando los asistentes de prueba Isabelle/HOL y Coq. A lo largo del curso, se exploran temas como la programación funcional, el razonamiento automático y estructurado sobre programas, la inducción, la verificación de algoritmos (como la ordenación por inserción y mezcla), la deducción natural en lógica proposicional y de primer orden, así como el manejo de estructuras de datos y definiciones inductivas. Además, se incluyen ejercicios prácticos para aplicar los conceptos teóricos en la resolución de problemas. El objetivo es proporcionar las herramientas necesarias para desarrollar demostraciones formales rigurosas y verificar la corrección de programas de manera sistemática.
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
Razonamiento con Isabelle/HOL
- Tema 1: Programación funcional en Isabelle.
- Tema 2: Razonamiento sobre programas:
- Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL.
- Tema 4: Razonamiento por casos y por inducción.
- Tema 5: Razonamiento sobre árboles y bosques.
- Tema 6: Verificación de algoritmos de ordenación:
- Tema 7: Deducción natural proposicional:
- Tema 8: Deducción natural de primer orden:
- Tema 9: Editores lógicos.
- Tema 10: Caso de estudio: Compilación de expresiones.
- Tema 11: Definiciones inductivas.
- Tema 12: Conjuntos, funciones y relaciones.
Razonamiento con Coq
- Tema 1: Programación funcional y métodos elementales de demostración en Coq.
- Tema 2: Demostraciones por inducción sobre los números naturales en Coq.
- Tema 3: Datos estructurados en Coq.
- Tema 4: Polimorfismo y funciones de orden superior en Coq.
- Tema 5: Tácticas básicas de Coq.
- Tema 6: Lógica en Coq.
- Tema 7: Definiciones inductivas en Coq.
Ejercicios
- Relación 1: Programación funcional en Isabelle/HOL.
- Relación 2: Razonamiento automático sobre programas en Isabelle/HOL.
- Relación 3: Razonamiento estructurado sobre programas en Isabelle/HOL.
- Relación 4: Cuantificadores sobre listas.
- Relación 5: Recorridos de árboles.
- Relación 6: Deducción natural proposicional en Isabelle/HOL.
- Relación 7: Deducción natural LPO en Isabelle/HOL.
- Relación 8: Gramáticas libres de contexto.
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).
Cursos con Coq
- 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).
- Adam Chlipala y Armando Solar Lezama. Foundations of program analysis. (MIT, 2013-14).
- M. Greenberg. Discrete mathematics and functional programming.
- Benjamin C. Pierce et als. Software foundations (Vol. 1: Logical foundations).
- Benjamin C. Pierce. Software foundations. (Univ. de Pensilvania, 2018).
- G. Smolka. Introduction to computational logic. (Univ. de Sarre, 2018).
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.
Sistemas
Asistentes de demostración
Editores de pruebas por deducción natural
Editores de pruebas por secuentes
- Logitext (un demostrador interactivo basado en el cálculo de secuentes).