Formalizing Desargues' theorem in Coq using ranks
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)
