Documentación

En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO).

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. T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
9. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
10. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
11. G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
12. D. MacKenzie Computers and the sociology of mathematical proof.
13. G. Sutcliffe. What is automated theorem proving?.
14. F. Wiedijk Formalizing the «top 100» of mathematical theorems.
15. F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
16. F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.

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. Tutorials and manuals for Isabelle.

Lecturas complementarias

Programación funcional

1. J.A. Alonso Temas de "Programación funcional". Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
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!.

Lógica computacional

1. J.A. Alonso Temas de "Lógica informática" (2012-13). Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
2. R. Bornat Proof and disproof in formal logic: an introduction for programmers. Oxford University Press, 2005.
3. K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers Reasoned programming. Imperial College, 1994.
4. K. Doets y J. van Eijck The Haskell Road to Logic, Maths and Programming.
5. 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

1. Clemens Ballarin. Automatic Deduction. (Univ de Innsbruck, 2008).
2. Clemens Ballarin y Gerwin Klein Introduction to the Isabelle Proof Assistant. (en el IJCAR-2004).
3. Clemens Ballarin y Tjark Weber. Automated Theorem Proving in Isabelle/HOL. (Univ. de Innsbruck, 2006-07).
4. A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. Computer-supported Modeling and Reasoning. (ETH Zurich, 2011).
5. Mads Dam. Advanced formal methods. (KTH Royal Institute of Technology, 2007).
6. Jacques Fleuriot y Paul Jackson. Automated reasoning. (Univ. de Edimburgo, 2012-13).
7. Thomas Genet Software formal analysis and design. (Univ. de Rennes)
8. Gerwin Klein. Theorem Proving - Principles, Techniques, Applications. (NICTA, 2004).
9. Gerwin Klein. Advanced Topics in Software Verification. (NICTA, 2012).
10. Joao Marcos. Lógica computacional: Demonstração assistida e semi-automática de teoremas.(UFRN, 2000).
11. Tobias Nipkow. Semantics of programming languages. (Univ. de Munich, 2012-13).
12. Tobias Nipkow Theorem Proving with Isabelle/HOL An Intensive Course.
13. Larry Paulson. Interactive Formal Verification. (Univ. de Cambridge, 2009-10).
14. Jan-Georg Smaus. Computer-supported modeling and reasoning. (Univ. de Feiburgo, 2009).
15. Christian Sternagel Experiments in Verification – Introduction to Isabelle/HOL. (Univ. de Innsbruck, 2011-12).
16. Tjark Weber. Interactive Formal Verification. (Univ. de Cambridge, 2010-11).

Otros cursos

1. José A. Alonso Lógica informática (Univ. de Sevilla, 2012-13).
2. 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).
3. Pierre Castéran Logic (Master In Verification) (Univ. de Burdeos, 2011-12).
4. Ian Hodkinson Logic (Imperial College, Londres, 2010-11).
5. Peter Lucas Knowledge Representation and Reasoning (Radboud University # egen, 2011-12).
6. Larry Paulson Logic and Proof (Univ. de Cambridge, 2011-12).
7. Riccardo Pucella Logic and Computation (Northeastern University, 2009). Curso con ACL2.

Bibliotecas de ejemplos de verificación

1. Archive of Formal Proofs.
2. Formalizing 100 Theorems.
3. Gallery of verified programs.

Artículos recientes

Están en orden cronológico inverso a la fecha de su reseña en Vestigium:

1. Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel Certified HLints with Isabelle/HOLCF-Prelude.
2. Peter Lammich Automatic data refinement.
3. Assia Mahboubi The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups).
4. Nathan Wetzler, Marijn J. H. Heule y Warren A. Hunt Jr. Mechanical verification of SAT refutations with extended resolution.
5. Johannes Hölzl, Fabian Immler y Brian Huffman Type classes and filters for mathematical analysis in Isabelle/HOL
6. M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler Verifying refutations with extended resolution.
7. C. Lüth y M. Ring A Web interface for Isabelle: The next generation.
8. L. Liu, O. Hasan y S. Tahar On the formalization of continuous-time Markov chains in HOL.
9. A. Asperti y W. Ricciotti Formalizing Turing machines.
10. A. Lochbihler Light-weight containers for Isabelle: efficient, extensible, nestable.
11. L. Noschinski Graph theory.
12. G. Gonthier et als. A machine-checked proof of the odd order theorem.
13. C. Doczkal, J.O. Kaiser y G. Smolka A constructive theory of regular languages in Coq.
14. C. Sternagel A formal proof of Kruskal’s tree theorem in Isabelle/HOL.
15. C. Sternagel y R. Thiemann Formalizing Knuth-Bendix orders and Knuth-Bendix completion.
16. C. Lange, C. Rowat, W. Windsteiger y M. Kerber Developing an auction theory toolbox.
17. M. Spasić y F. Marić Formalization of incremental simplex algorithm by stepwise refinement.
18. J.C. Blanchette, A. Popescu y D. Traytel Coinductive pearl: Modular first-order logic completeness.
19. J. Esparza et als. A fully verified executable LTL model checker.
20. M. Kerber, C. Lange y C. Rowat. ForMaRE - formal mathematical reasoning in economics.
21. J. Urban. AI over large formal knowledge bases: The first decade.
22. S. Boldo, C. Lelay y G. Melquiond. Formalization of real analysis: A survey of proof assistants and libraries.
23. F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow Data refinement in Isabelle/HOL.
24. A.C. Rocha y M. Ayala. Formalizing the confluence of orthogonal rewriting systems.
25. Z. Shi et als. Formalization of the complex number theory in HOL4.
26. F. Loulergue y V. Niculescu Programming and reasonning with PowerLists in Coq.
27. J. Heras, F.J. Martín y V. Pascual. A hierarchy of mathematical structures in ACL2.
28. J. Xu, X. Zhang y C. Urban Mechanising Turing Machines and Computability Theory in Isabelle/HOL