Diferencia entre revisiones de «Formalizing Desargues' theorem in Coq using ranks»
| Línea 2: | Línea 2: | ||
---- | ---- | ||
| − | El objetivo del trabajo es introducir el concepto de rango para permitir la simplificación de las demostraciones formalizadas en Geometría. Presenta un formalización de la geometría usando | + | El objetivo del trabajo es introducir el concepto de rango para permitir la simplificación de las demostraciones formalizadas en Geometría. Presenta un formalización de la geometría usando rango y la usa para demostrar el teorema de Desargues. |
La formalización se ha hecho en Coq. Sería interesante ver su adaptación a Isabelle/Isar. | La formalización se ha hecho en Coq. Sería interesante ver su adaptación a Isabelle/Isar. | ||
Revisión actual del 20:32 11 nov 2009
N. Magaud, J Narboux y P. Schreck Formalizing Desargues' theorem in Coq using ranks. Proceedings of the ACM Symposium on Applied Computing SAC 2009.
El objetivo del trabajo es introducir el concepto de rango para permitir la simplificación de las demostraciones formalizadas en Geometría. Presenta un formalización de la geometría usando rango y la usa para demostrar el teorema de Desargues.
La formalización se ha hecho en Coq. Sería interesante ver su adaptación a Isabelle/Isar.
José A. Alonso 10:39, 12 November 2008 (CET)
