Formalizing Desargues' theorem in Coq using ranks
Revisión del 11:11 12 nov 2008 de Jalonso (discusión | contribuciones) (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 ...)
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.
