Diferencia entre revisiones de «Formal Proof: Theory and Practice»
| (No se muestra una edición intermedia del mismo usuario) | |||
| Línea 4: | Línea 4: | ||
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 | + | # '''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)). |
| − | la certidumbre) y aplicaciones (revisión de artículos matemáticos y | + | # '''Lógica formal'''. Presenta la simbolización en la lógica y sus beneficios (brevedad y claridad). |
| − | verificación de sistemas informáticos); los avances en asistentes de prueba | + | # '''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)). |
| − | (más fácilidad de uso, más potencia y más retos superados) y, la relación entre | + | # '''¿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 formalización en matemáticas y la verificación de sistemas informáticos: | + | # '''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. |
| − | (''formalization of pure mathematics and verification applications are not | + | # '''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). |
| − | separate activities, one undertaken for fun and the other for profit, but are | + | # '''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). |
| − | 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 | + | #* El uso de las demostraciones formales en matemáticas es una continuación natural del aumento del rigor. |
| − | natural del aumento del rigor. | + | #* La formalización es un trabajo pesado. |
| − | #* La formalización es un | ||
#* 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 | + | #* 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. |
| − | 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 | + | Este artículo sirve como lectura para los cursos [http://www.cs.us.es/~jalonso/cursos/li Lógica informática] y [http://www.cs.us.es/~jalonso/cursos/d-ra Razonamiento automático]- |
[[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 actual del 12:05 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)).
- 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)
