Diferencia entre revisiones de «Formal Proof: Theory and Practice»
| Línea 1: | Línea 1: | ||
| − | 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. | + | 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. | + | 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: | 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)). | + | # '''Introducción'''. En esta sección comenta los conceptos de demostración |
| − | # '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad). | + | formal y asistentes de demostración; las razones de crear demostraciones |
| − | # '''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)). | + | formales (satisfación intelectual, fundamentación de la matemática y mejora de |
| − | # '''¿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.''). | + | la certidumbre) y aplicaciones (revisión de artículos matemáticos y |
| − | # '''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. | + | verificación de sistemas informáticos); los avances en asistentes de prueba |
| − | # '''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). | + | (más fácilidad de uso, más potencia y más retos superados) y, la relación entre |
| − | # '''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). | + | 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''' | # '''Conclusiones y prospectivas''' | ||
| − | #* El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor. | + | #* El uso de las demostraciones formales en matemáticas es una continuación |
| + | natural del aumento del rigor. | ||
#* La formalización es un tranbajo pesado. | #* La formalización es un tranbajo pesado. | ||
#* El uso de asistentes de demostración puede aligerarlo y hacerlo divertido. | #* 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. | + | #* 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 referencia para los cursos | ||
[[User:Jalonso|José A. Alonso]] 10:54, 16 December 2008 (CET) | [[User:Jalonso|José A. Alonso]] 10:54, 16 December 2008 (CET) | ||
[[Category:Lecturas]] | [[Category:Lecturas]] | ||
Revisión del 11:58 16 dic 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)).
- 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 tranbajo 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 referencia para los cursos
José A. Alonso 10:54, 16 December 2008 (CET)
