Formal Proof: Theory and Practice
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)).
- ¿Formalización o proceso social?. Comenta que en la historia anterior hay distintas motivaciones: fundamentar la matemática (Russell, Frege, Hilbert, Brouwer) y mejorar su enseñanza (Peano). Respecto a la acualidad comenta la extensión del uso del lenguaje conjuntista en matemática, pero no el de la lógica (as far as the mathematical community is concerned George Boole has lived in vain (Dijkstra)). La certificación de la matemática se hace mediante revisión entre pares y no formalmente. Este proceso de revisión presenta fallos: teoremas grandes (p.e. teorema de los cuatro colores y la conjetura de Kepler). La certificación formal se ve demasiado laboriosa, pero opina que ya se puede facilitar usando ordenadores y sustituirá a la tradicional (the traditional social process is an anachronism to be swept away by formalization, just as empiricism replaced a similar “social process” used by the Greeks to decide scientific questions.).
- Verificación formal. El uso de la matemática en los sistemas informáticos, la importacia crítica de dichos sistemas y sus fallos potencian el uso de métodos formales para verificarlos.
- Aspectos teóricos del razonamiento automático. Comenta la historia de la automatización del razonamiento (Leibniz, Frege). Presenta la lógica de primer orden (sintaxis, semántica, deducción, completitud, teorema de incompletitud, semidecisibilidad).
- Aspectos prácticos del razonamiento automático. Comenta el cálculo simbólico de la lógica mediante lenguajes funcionales que da lugar a demostradores automáticos e interactivos. Comenta algunos de los éxitos de los demostradores: sistemas de decisión (SAT, aritmética de Presburger, SMT (satisfacibilidad módulo teorías), resolución y paramodulación, solución de la conjetura de Robbins, asistentes de prueba (SAM, Automath, LCF, Mizar, Nqthm) y estilos procedural (HOL) y declarativo (Mizar, Isar).
- Conclusiones y prospectivas
- El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor.
- La formalización es un trabajo pesado.
- El uso de asistentes de demostración puede aligerarlo y hacerlo divertido.
- Se progresará mediante la acumulación de bibliotecas de matemáticas formalizadas, la integración en los asistentes de procedimientos de decisión y la mejora de los lenguajes usados para expresar las demostraciones.
Este artículo sirve como lectura para los cursos Lógica informática y Razonamiento automático-
José A. Alonso 10:54, 16 December 2008 (CET)
