Diferencia entre revisiones de «Formal Proof: Theory and Practice»
(New page: J. Harrison (2008) ''Formal Proof: Theory and Practice'') |
|||
| Línea 1: | Línea 1: | ||
| − | J. Harrison (2008) '' | + | J. Harrison (2008) [http://www.ams.org/notices/200811/tx081101395p.pdf ''Formal Proof: Theory and Practice'']. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406. |
| + | ---- | ||
| + | Este trabajo es el tercer artículo del [http://www.ams.org/notices/200811/ número de Diciembre de 2008 de las ''Notices of the AMS''] dedicado a las demostraciones formales. | ||
| + | |||
| + | El resumen del artículo es el siguiente: | ||
| + | # Introducción. | ||
| + | #: En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos: | ||
| + | #:: ''formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected.'' (p. 1396). | ||
Revisión del 10:10 16 dic 2008
J. Harrison (2008) Formal Proof: Theory and Practice. Notices of the AMS, Vol. 55, N. 11 (2008) p.1395-1406.
Este trabajo es el tercer artículo del número de Diciembre de 2008 de las Notices of the AMS dedicado a las demostraciones formales.
El resumen del artículo es el siguiente:
- Introducción.
- En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:
- formalization of pure mathematics and verification applications are not separate activities, one undertaken for fun and the other for profit, but are intimately connected. (p. 1396).
- En esta sección comenta los conceptos de demostración formal y asistentes de demostración; las razones de crear demostraciones formales (satisfación intelectual, fundamentación de la matemática y mejora de la certidumbre) y aplicaciones (revisión de artículos matemáticos y verificación de sistemas informáticos); los avances en asistentes de prueba (más fácilidad de uso, más potencia y más retos superados) y, la relación entre la formalización en matemáticas y la verificación de sistemas informáticos:
