Diferencia entre revisiones de «Razonamiento formalizado»
| Línea 10: | Línea 10: | ||
# Formalización de la geometría. Además, se debería relacionar las demostraciones constructivas en Isar con sistemas de geometría dinámica. | # Formalización de la geometría. Además, se debería relacionar las demostraciones constructivas en Isar con sistemas de geometría dinámica. | ||
# Formalización de la teoría de la relatividad. Para esta tarea, los trabajos básicos son: | # 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 [http://www.math-inst.hu/pub/algebraic-logic/springer.2006-04-10.pdf First-order logic foundation of relativity theories] | + | #* J.X. Madarasz, I. Nemeti y G. Szekely [http://www.math-inst.hu/pub/algebraic-logic/springer.2006-04-10.pdf First-order logic foundation of relativity theories]. |
#* H. Andréka, J.X. Madarász y I. Németi [http://www.math-inst.hu/pub/algebraic-logic/olsort.html On the logical structure of relativity theories]. | #* H. Andréka, J.X. Madarász y I. Németi [http://www.math-inst.hu/pub/algebraic-logic/olsort.html On the logical structure of relativity theories]. | ||
| − | #* H. Andréka, J.X. Madarász, I. Németi y G. Székely [http://www.math-inst.hu/pub/algebraic-logic/reldynamics.pdf Axiomatizing relativistic dynamics without conservation postulates] | + | #* H. Andréka, J.X. Madarász, I. Németi y G. Székely [http://www.math-inst.hu/pub/algebraic-logic/reldynamics.pdf Axiomatizing relativistic dynamics without conservation postulates]. |
| − | #* H. Andréka, J.X. Madarász y I. Németi [http://www.math-inst.hu/pub/algebraic-logic/Logicofspacetime.pdf Logic of spacetime and relativity | + | #* H. Andréka, J.X. Madarász y I. Németi [http://www.math-inst.hu/pub/algebraic-logic/Logicofspacetime.pdf Logic of spacetime and relativity]. |
| − | |||
# 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: | # 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: | ||
#* P. Ferraris y V. Lifschitz [http://www.cs.utexas.edu/users/vl/papers/mfasp.ps Mathematical foundations of answer set programming]. | #* P. Ferraris y V. Lifschitz [http://www.cs.utexas.edu/users/vl/papers/mfasp.ps Mathematical foundations of answer set programming]. | ||
Revisión del 10:51 20 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.
Algunas grandes tareas de formalización son las siguientes:
- Formalización de la geometría. Además, se debería relacionar las demostraciones constructivas en Isar con sistemas de geometría dinámica.
- 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.
- 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.
- 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:
- P. Ferraris y V. Lifschitz Mathematical foundations of answer set programming.
- V. Lifschitz Introduction to answer set programming.
- M. Gelfond Answer sets.
- 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
- IsarMathLib:
- A library of formalized mathematics for Isabelle/Isar proof assistant.
- Tiddly Formal Math.
- Blog del proyecto IsarMathLib.
- Formalized Mathematics.
- Revista de formalización en Mizar.
- Journal of Formalized Reasoning.
- Revista de razonamiento formalizado que ha comenzado el 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)
