Diferencia entre revisiones de «Formalizing Desargues' theorem in Coq using ranks»

De WikiGLC
Saltar a: navegación, buscar
 
(No se muestra una edición intermedia del mismo usuario)
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 ranfo y la usa para demostrar el teorema de Desargues.
+
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.
Línea 8: Línea 8:
 
[[User:Jalonso|José A. Alonso]] 10:39, 12 November 2008 (CET)
 
[[User:Jalonso|José A. Alonso]] 10:39, 12 November 2008 (CET)
  
[[Categoría:Lecturas]]
+
[[Category:Lecturas]]

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)