Diferencia entre revisiones de «Documentación»
De Demostración asistida por ordenador (2012-13)
(→Visiones generales de la DAO) |
(→Visiones generales de la DAO) |
||
Línea 3: | Línea 3: | ||
== Visiones generales de la DAO == | == Visiones generales de la DAO == | ||
− | # J.A. | + | # J.A. Alonso [http://www.glc.us.es/~jalonso/vestigium Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012. |
# M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction]. | # M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction]. | ||
# J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012. | # J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012. | ||
# J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012. | # J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012. | ||
+ | # H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009. | ||
+ | # G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008. | ||
# T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380. | # T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380. | ||
# J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007. | # J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007. | ||
Línea 13: | Línea 15: | ||
# D. MacKenzie [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof]. | # D. MacKenzie [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof]. | ||
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?]. | # G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?]. | ||
+ | # F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of | ||
+ | mathematical theorems]. | ||
+ | # F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008. | ||
+ | # F. Wiedijk, [http://www.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007. |
Revisión del 12:20 26 dic 2012
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
- J.A. Alonso Razonamiento formalizado: Del sueño a la realidad de las pruebas. Vestigium, 26 de diciembre de 2012.
- M. Davis. The early history of automated deduction.
- J.P. Delahaye Du rêve à la réalité des preuves. Interstices, 8 de julio de 2012.
- 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.
- H. Geuvers Proof assistants: History, ideas and future. Sadhana, Vol. 34-1, pp. 3-25, février 2009.
- G. Gonthier The four-color theorem. Notices of the AMS, Vol. 55, n° 11, pp. 1382-1393, 2008.
- T. Hales. Formal proof. Notices of AMS, Vol. 55, N. 11 (2008) pp. 1370-1380.
- J. Harrison. A short survey of automated reasoning. Lecture Notes in Computer Science, Vol. 4545, pp. 334-349, 2007.
- J. Harrison. Formal proof: Theory and practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
- G. Kolata. Computer math proof shows reasoning power. The New York Times, 10 de diciembre de 1996.
- D. MacKenzie Computers and the sociology of mathematical proof.
- G. Sutcliffe. What is automated theorem proving?.
- F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of
mathematical theorems].
- F. Wiedijk Formal proof - Getting started. Notices of the AMS, Vol. 55, n° 11, pp. 1408-1414, 2008.
- F. Wiedijk, The QED manifesto revisited. Studies in Logic, Grammar and Rhetoric, Vol. 10(23), pp. 121-133, 2007.