Formal Proof: Theory and Practice
Revisión del 11:21 16 dic 2008 de Jalonso (discusión | contribuciones)
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).
- Lógica formal. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad).
- Los fundamentos de la matemáticas. Presenta una historia de los fundamentos de la matemáticas: su inicio en los Elementos de Euclides, los problemas de los axiomas, la corriente logicista de Frege, la teorái de conjunto de Cantor, la paradoja de Russell y las soluciones mediante tipos o axiomas (de Zermelo-Fraenkel). Termina comentando la relaciones entre tipos y teoría de conjunto, donde se decanta por los tipos:
- Type-based approaches look immediately appealing, because mathematicians generally do make type distinctions: between points and lines, or between numbers and sets of numbers, etc. (p. 1398).
