Diferencia entre revisiones de «Razonamiento formalizado»
| Línea 6: | Línea 6: | ||
En ambos casos, lo importante no es la corrección del teorema final sino que aumente la comprensión del teorema por el autor de la prueba y sus futuros lectores. Por ello, es importante usar demostraciones estructuradas como las de Isabelle/Isar. | En ambos casos, lo importante no es la corrección del teorema final sino que aumente la comprensión del teorema por el autor de la prueba y sus futuros lectores. Por ello, es importante usar demostraciones estructuradas como las de Isabelle/Isar. | ||
| + | |||
| + | === Proyectos relacionados === | ||
| + | # [http://www.nongnu.org/isarmathlib/ IsarMathLib]: A library of formalized mathematics for Isabelle/Isar proof assistant. | ||
| + | # [http://slawekk.wordpress.com/ Formalized Mathematics]. | ||
| + | # [http://vdash.org/ Vdash]. | ||
[[User:Jalonso|José A. Alonso]] 10:47, 19 November 2008 (CET) | [[User:Jalonso|José A. Alonso]] 10:47, 19 November 2008 (CET) | ||
[[Category:Proyectos]] | [[Category:Proyectos]] | ||
Revisión del 13:06 19 nov 2008
Este es un megaproyecto. Según Thomas Hales "the formalization of just 100,000 pages of core mathematics" sería "the sequencing of a mathematical genome".
En este proyecto hay dos vías:
- De abajo arriba: Desarrollar el conocimiento básico común; es decir, el contenido en las licenciaturas e ingenierías. En esta vía, se elegiría algún curso y se procedería a la formalización del conocimiento matemático del mismo. Evidentemente, los cursos fundamentales son los de la Licenciatura en Matemáticas y los de la Ingeniería en Informática.
- De arriba abajo: Elegir un teorema importante (por ejemplo, alguno de la lista Formalizing 100 Theorems, list of projects in the area of formal mathematics o de Proofs from THE BOOK) y desarrollar el contenido matemático necesario para su verificación.
En ambos casos, lo importante no es la corrección del teorema final sino que aumente la comprensión del teorema por el autor de la prueba y sus futuros lectores. Por ello, es importante usar demostraciones estructuradas como las de Isabelle/Isar.
Proyectos relacionados
- IsarMathLib: A library of formalized mathematics for Isabelle/Isar proof assistant.
- Formalized Mathematics.
- Vdash.
José A. Alonso 10:47, 19 November 2008 (CET)
