Demostración asistida por ordenador (2012-13) Demostración asistida por ordenador (2012-13)

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.