Razonamiento automático (2014-15)
El curso "Razonamiento automático (2014-15)" ofrece una introducción al razonamiento formal y la verificación de programas utilizando Isabelle/HOL. A lo largo del curso, se abordan temas fundamentales como la programación funcional en Isabelle, el razonamiento sobre programas (incluyendo casos de estudio como la ordenación por inserción y mezcla), la deducción natural (tanto proposicional como de primer orden), conceptos avanzados como conjuntos inductivos, gramáticas libres de contexto y razonamiento modular, así como aplicaciones prácticas como la resolución de sudokus. Además, el curso incluye una serie de relaciones de ejercicios que permiten profundizar en la formalización, automatización y verificación de propiedades en entornos de demostración asistida.
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: Programación funcional en Isabelle.
- Tema 2a: Razonamiento sobre programas Haskell
- Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL.
- Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL.
- Tema 4: Razonamiento por casos y por inducción.
- Tema 5a: Verificación de la ordenación por inserción.
- Tema 5b: Verificación de la ordenación por mezcla.
- Tema 6: Caso de estudio: Compilación de expresiones.
- Tema 7a: Deducción natural proposicional.
- Tema 7b: Deducción natural proposicional con Isabelle/HOL.
- Tema 8a: Deducción natural en lógica de primer orden.
- Tema 8b: Deducción natural en lógica de primer orden con Isabelle/HOL
- Tema 9: Conjuntos, funciones y relaciones.
- Tema 10: Conjuntos definidos inductivamente.
- Tema 11: Gramáticas libre de contexto.
- Tema 12a: Razonamiento modular (Teoría de grupos).
- Tema 12b: Razonamiento modular.
- Tema 12c: Automatización.
- Tema 12d: Pasos elementales.
- Tema 12e: Sudoku.
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: Cons inverso.
- Relación 5: Cuantificadores sobre listas.
- Relación 6: Sustitución, inversión y eliminación.
- Relación 7: Recorridos de árboles.
- Relación 8: Árboles binarios completos.
- Relación 9: Deducción natural en Isabelle/HOL.
- Relación 10: Formalización y argumentación en Isabelle/HOL.
- Relación 11: Plegados de listas y de árboles.
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.