Razonamiento formalizado

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.

Algunas grandes tareas de formalización son las siguientes:

1. Formalización de la geometría. Además, se debería relacionar las demostraciones constructivas en Isar con sistemas de geometría dinámica.
2. Formalización de la teoría de la relatividad. Para esta tarea, los trabajos básicos son:
   • J.X. Madarasz, I. Nemeti y G. Szekely First-order logic foundation of relativity theories. En New Logics for the XXIst Century II, Mathematical Problems from Applied Logics. International Mathematical Series Vol 5, Springer, 2007. pp.217-252.
   • H. Andréka, J.X. Madarász y I. Németi On the logical structure of relativity theories.
   • H. Andréka, J.X. Madarász, I. Németi y G. Székely Axiomatizing relativistic dynamics without conservation postulates. Studia Logica 89,2 (2008), 163-186.
   • H. Andréka, J.X. Madarász y I. Németi Logic of spacetime and relativity. En Handbook of Spatial Logics. Eds: M. Aiello, I. Pratt-Hartmann y J. van Benthem. Springer Verlag, 2007. pp. 607-711.
   • I. Nemeti Recent work in Logic of Spacetime.
3. Formalización de la teoría de la programación con conjuntos respuesta (Answer Set Programming, ASP). Para esta tarea los trabajos básicos son:
4. P. Ferraris y V. Lifschitz Mathematical foundations of answer set programming.
5. V. Lifschitz Introduction to answer set programming.
6. M. Gelfond Answer sets.
7. Formalización de la teoría de la programación con sistemas de producción. En particular, el algoritmo RETE. Para esta tarea los trabajos básicos son
   • H. Cirstea, C. Kirchner, M. Moossen y P.-E. Moreau. Production Systems and Rete Algorithm Formalisation.
   • H. Cirstea, C. Kirchner, M. Moossen y P.-E. Moreau Production Systems and Rewrite Systems.

Proyectos relacionados

1. IsarMathLib:

   A library of formalized mathematics for Isabelle/Isar proof assistant.

2. Tiddly Formal Math.

   Blog del proyecto IsarMathLib.

3. Formalized Mathematics.

   Revista de formalización en Mizar.

4. Journal of Formalized Reasoning.

   Revista de razonamiento formalizado que ha comenzado el 2008.

5. The Archive of Formal Proofs

   Biblioteca de formalizaciones en Isabelle.

6. Vdash:

   A formalized math wiki.

José A. Alonso 10:47, 19 November 2008 (CET)