Documentación

En esta página se recogen en enlaces que sirven de documentación al curso de "Razonamiento automático"

1 Vídeos

• Vídeos de deducción natural con Pandora: ejemplo 1 y ejemplo 2.

2 Visiones generales de la DAO

1. J.A. Alonso. Razonamiento formalizado: Del sueño a la realidad de las pruebas. Vestigium, 26 de diciembre de 2012.
2. J. Avigad. Interactive theorem proving, automated reasoning, and mathematical computation. ICERM, 14 de diciembre de 2012.
3. M. Davis. The early history of automated deduction.
4. J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
5. 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.
6. H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
7. G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
8. J. Gross Machine-checked proof. AMS Notices, 15 de octubre de 2017.
9. T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
10. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
11. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
12. G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
13. D. MacKenzie Computers and the sociology of mathematical proof.
14. G. Sutcliffe. What is automated theorem proving?.
15. F. Wiedijk Formalizing the «top 100» of mathematical theorems.
16. F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
17. F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.

3 Referencias sobre Isabelle/HOL

1. B. Grechuk Isabelle primer for mathematicians.
2. T. Nipkow Programming and proving in Isabelle/HOL.
3. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic.
4. Isabelle/HOL — Higher-Order Logic.
5. M. Wenzel The Isabelle/Isar Reference Manual.
6. M. Wenzel The Isabelle/Isar quick reference.
7. J. Siek Quick Reference for Isabelle/Isar Propositional Logic.
8. J. Siek Quick Reference for Isabelle/Isar More Proof Techniques.
9. J. Siek Quick Reference for Isabelle/Isar First-Order Logic.
10. Tutorials and manuals for Isabelle.

4 Lecturas complementarias

4.1 Programación funcional

1. J.A. Alonso Temas de "Programación funcional". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2016.
2. 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.
3. G. Hutton Programming in Haskell. Cambridge University Press, 2007.
4. M. Lipovača ¡Aprende Haskell por el bien de todos!.

4.2 Lógica computacional

1. J.A. Alonso Temas de "Lógica informática" (2015-16). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2015.
2. K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
3. K. Doets y J. van Eijck The Haskell Road to Logic, Maths and Programming.
4. M. Huth y M. Ryan Logic in computer science: Modelling and reasoning about systems. Cambridge University Press, 2004. (Incluye el tutor en la Red).

5 Cursos relacionados

5.1 Cursos con Isabelle/HOL

1. Jeremy Avigad. Logic and Formal Verification. (Carnegie Mellon, 2009).
2. Clemens Ballarin. Automatic Deduction. (Univ de Innsbruck, 2008).
3. Clemens Ballarin. Introduction to the Isabelle Proof Assistant. (Belgrado, 2008).
4. Clemens Ballarin y Gerwin Klein Introduction to the Isabelle Proof Assistant. (en el IJCAR-2004).
5. Clemens Ballarin y Tjark Weber. Automated Theorem Proving in Isabelle/HOL. (Univ. de Innsbruck, 2006-07).
6. Jasmin Blanchette, Mathias Fleury y Daniel Wand Concrete semantics with Isabelle/HOL. (Univ. del Sarre, 2015-16).
7. A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported Modeling and Reasoning. (ETH Zurich, 2011).
8. Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
9. Jacques Fleuriot. Automated reasoning. (Univ. de Edimburgo, 2016-17).
10. Thomas Genet Software formal analysis and design. (Univ. de Rennes)
11. Gerwin Klein. Theorem Proving - Principles, Techniques, Applications. (NICTA, 2004).
12. Gerwin Klein. Advanced Topics in Software Verification. (NICTA, 2012).
13. Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
14. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
15. Tobias Nipkow. Theorem Proving with Isabelle/HOL An Intensive Course.
16. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
17. Arnd Poetzsch-Heffter. Specification and Verification with Higher-Order Logic.
18. Jeremy G. Siek. Practical Theorem Proving with Isabelle/Isar. (Univ. de Colorado, 2007).
19. Jeremy G. Siek. Theorem proving in Isabelle. (Univ. de Colorado, 2011).
20. Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
21. Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
22. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).

5.2 Cursos con Coq

1. 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).
2. Adam Chlipala Interactive computer theorem proving. (MIT, 2012-13).
3. Adam Chlipala y Armando Solar Lezama Foundations of program analysis. (MIT, 2013-14).
4. Benjamin C. Pierce et als. Software foundations (Vol. 1: Logical foundations).
5. Benjamin C. Pierce Software foundations (Univ. de Pensilvania, 2018).
6. G. Smolka Introduction to computational logic (Univ. de Sarre, 2018).

5.3 Otros cursos

1. José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
2. Thorsten Altenkirch y Peter Morris Introduction to formal reasoning (Univ. de Nottingham, 2010-11).
3. Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
4. Robby Findler Certified programming with dependent types. (Northwestern, 2013-14).
5. Carlos Luna y Gustavo Betarte. Construcción formal de programas en teoría de tipos. (Univ. de la República, Uruguay, 2013-14).
6. Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
7. Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
8. Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).
9. David Pichardie Méthode de vérification (Universidad de Rennes, 2006-07).

6 Bibliotecas de ejemplos de verificación

1. Archive of Formal Proofs.
2. Formalizing 100 Theorems.
3. Gallery of verified programs.
4. Larry Wos' Notebooks.
5. The TPTP Problem Library for Automated Theorem Proving.
6. The 1st Verified Software Competition.
7. The 2nd Verified Software Competition.
8. VerifyThis (A collection of verification benchmarks.

7 Artículos recientes

Hay dos listas de artículos recientes:

• en Twitter que contiene enlaces a los artículos de razonamiento automático y demostración asistida por ordenador que se están publicando y
• en Vestigium que contiene una reseña de los más destacados.

8 Ofertas de trabajo

En GitHub se encuentra una recopilaciónn las ofertas de trabajo de interés para los estudiantes del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla.

Están en orden cronológico inverso por la fecha de su publicación en Twitter.