A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.comgeo.2010.06.004
+Normal rank
@@ Property / OpenAlex ID @@
+W2054653818
@@ Property / OpenAlex ID: W2054653818 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+On the mechanization of the proof of Hessenberg's theorem in coherent logic
+Normal rank
@@ Property / cites work @@
+Q4763522
@@ Property / cites work: Q4763522 / rank @@
+Normal rank
@@ Property / cites work @@
+Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang
+Normal rank
@@ Property / cites work @@
+Machine Proofs in Geometry
@@ Property / cites work: Machine Proofs in Geometry / rank @@
+Normal rank
@@ Property / cites work @@
+Q3766390
@@ Property / cites work: Q3766390 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4531863
@@ Property / cites work: Q4531863 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
+Normal rank
@@ Property / cites work @@
+DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
+Normal rank
@@ Property / cites work @@
+Formalizing Projective Plane Geometry in Coq
@@ Property / cites work: Formalizing Projective Plane Geometry in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Formalizing Hilbert’s Grundlagen in Isabelle/Isar
+Normal rank
@@ Property / cites work @@
+INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
@@ Property / cites work: INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanical Theorem Proving in Tarski’s Geometry
@@ Property / cites work: Mechanical Theorem Proving in Tarski’s Geometry / rank @@
+Normal rank