Formal Proof: Theory and Practice

De WikiGLC
Saltar a: navegación, buscar

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:

  1. 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).