Diferencia entre revisiones de «Razonamiento formalizado»
| Línea 10: | Línea 10: | ||
# [http://www.nongnu.org/isarmathlib/ IsarMathLib]: A library of formalized mathematics for Isabelle/Isar proof assistant. | # [http://www.nongnu.org/isarmathlib/ IsarMathLib]: A library of formalized mathematics for Isabelle/Isar proof assistant. | ||
# [http://slawekk.wordpress.com/ Formalized Mathematics]. | # [http://slawekk.wordpress.com/ Formalized Mathematics]. | ||
| − | # [http://vdash.org/ Vdash]. | + | #: Blog del proyecto IsarMathLib. |
| + | # [http://mizar.org/fm/ Formalized Mathematics]. | ||
| + | #: Revista de formalización en Mizar. | ||
| + | # [http://jfr.cib.unibo.it/ Journal of Formalized Reasoning]. | ||
| + | #: Nueva revista de razonamiento formalizado. El primer número es de 2008. | ||
| + | # [http://afp.sourceforge.net/ The Archive of Formal Proofs] | ||
| + | #: Biblioteca de formalizaciones en Isabelle. | ||
| + | # [http://vdash.org/ Vdash]: A formalized math wiki. | ||
[[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 22:50 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.
- Blog del proyecto IsarMathLib.
- Formalized Mathematics.
- Revista de formalización en Mizar.
- Journal of Formalized Reasoning.
- Nueva revista de razonamiento formalizado. El primer número es de 2008.
- The Archive of Formal Proofs
- Biblioteca de formalizaciones en Isabelle.
- Vdash: A formalized math wiki.
José A. Alonso 10:47, 19 November 2008 (CET)
