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. M. Davis. The early history of automated deduction.
3. J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
4. 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.
5. T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
6. J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
7. J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
8. G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
9. D. MacKenzie Computers and the sociology of mathematical proof.
10. G. Sutcliffe. What is automated theorem proving?.