Diferencia entre revisiones de «Razonamiento formalizado»
(New page: Este es un megaproyecto. Según [http://www.ams.org/notices/200811/tx081101370p.pdf Thomas Hales] "the formalization of just 100,000 pages of core mathematics" sería "the sequencing of a ...) |
|||
| Línea 3: | Línea 3: | ||
En este proyecto hay dos vías: | 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 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 [http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems] o de .. | + | * De arriba abajo: Elegir un teorema importante (por ejemplo, alguno de la lista [http://www.cs.ru.nl/~freek/100/ Formalizing 100 Theorems], [http://www.cs.ru.nl/~freek/projects/ list of projects in the area of formal mathematics] o de [http://en.wikipedia.org/wiki/Proofs_from_THE_BOOK 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. | 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. | ||
Revisión del 11: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.
José A. Alonso 10:47, 19 November 2008 (CET)
