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 razonamiento formalizado son las siguientes:

1. Razonamiento formalizado en geometría. Además, se debería relacionar las demostraciones constructivas en Isar con sistemas de geometría dinámica.
2. Razonamiento formalizado sobre 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.
   • 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.
   • H. Andréka, J.X. Madarász y I. Németi Logic of spacetime and relativity.
   • G. Székely A First Order Logic Investigation of the Twin Paradox and Related Subjects.
3. Razonamiento formalizado sobre la teoría de la programación con conjuntos respuesta (Answer Set Programming, ASP). Para esta tarea los trabajos básicos son:
   • P. Ferraris y V. Lifschitz Mathematical foundations of answer set programming.
   • C. Baral Knowledge representation, reasoning and declarative problem solving with Answer sets.
   • V. Lifschitz Introduction to answer set programming.
   • M. Gelfond Answer sets.
4. Razonamiento formalizados sobre 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.
5. Verificación de sistemas lógicos. Para esta tarea los trabajos básicos son:
   • M. Fitting. First-Order Logic and Automated Theorem Proving.Springer-Verlag, 1996.
   • A.R. Bradley y Z. Manna The Calculus of Computation (Decision Procedures with Applications to Verification). Springer-Verlag, 2007.
6. Formalizar algunos de los teormas de la lista Formalizing 100 Theorems que aún no se ha formalizado. Por ejemplo,
   1. El teorema de Pick. Se puede usar como fuente el trabajo de Tom Davis Pick's Theorem proof.

Aún más interesante sería resolver mediante razonamiento formalizado algún problema abierto de matemáticas. Por ejemplo, alguno de las siguientes listas:

1. Unsolved problems in mathematics.
2. Open Problem Garden.

Proyectos relacionados

1. IsarMathLib:
   • Library of Formalized Mathematics for Isabelle/Isar (ZF Logic).
   • Tiddly Formal Math.
   • Formalized Mathematics
2. Formalized Mathematics.

   Revista de formalización en Mizar.

3. Journal of Formalized Reasoning.

   Revista de razonamiento formalizado que ha comenzado el 2008.

4. The Archive of Formal Proofs

   Biblioteca de formalizaciones en Isabelle.

5. Vdash:

   A formalized math wiki.

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