Diferencia entre revisiones de «Formalizing Desargues' theorem in Coq using ranks»
(New page: N. Magaud, J Narboux y P. Schreck ''[http://lsiit.u-strasbg.fr/Publications/2009/MNS09/desargues.pdf Formalizing Desargues' theorem in Coq using ranks]''. Proceedings of the ACM Symposium ...) |
|||
| Línea 5: | Línea 5: | ||
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. | ||
| + | |||
| + | [[User:Jalonso|José A. Alonso]] 10:39, 12 November 2008 (CET) | ||
| + | |||
| + | [[Categoría:Lecturas]] | ||
Revisión del 11:39 12 nov 2008
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 ranfo 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)
