Documentación

En esta página se recogen en enlaces que sirven de documentación al seminario 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. T. Nipkow Programming and proving in Isabelle/HOL. 12 de febrero de 2013.
2. T. Nipkow, M. Wenzel y L.C. Paulson A proof assistant for higher-order logic. Springer-Verlag. 12 de febrero de 2013.
3. Isabelle/HOL — Higher-Order Logic. 12 de febrero de 2013.
4. Tutorials and manuals for Isabelle2013.

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.

1. G. Hutton Programming in Haskell. Cambridge University Press, 2007.
2. 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. M. Huth y M. Ryan Logic in computer science: Modelling and reasoning about systems. Cambridge University Press, 2004. (Incluye el tutor en la Red).

Artículos recientes

1. J. Xu, X. Zhang y C. Urban Mechanising Turing Machines and Computability Theory in Isabelle/HOL