A case study in formalizing projective geometry in Coq: Desargues theorem

DOI10.1016/J.COMGEO.2010.06.004MaRDI QIDQ448975zbMATH OpenOpenAlexFDO

Authors Nicolas Magaud, Julien Narboux, Pascal Schreck

Publication date 11 September 2012

Published in Computational Geometry (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.comgeo.2010.06.004

zbMATH Keywords

rankprojective geometryCoqDesarguesHexamys

Mathematics Subject Classification ID

Desarguesian and Pappian geometries (51A30)

Recommendations

• Formalizing projective plane geometry in Coq
• Two cryptomorphic formalizations of projective incidence geometry
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• On the mechanization of the proof of Hessenberg's theorem in coherent logic

Cites work

• scientific article; zbMATH DE number 4024134 (Why is no real title available?)
• scientific article; zbMATH DE number 1745043 (Why is no real title available?)
• scientific article; zbMATH DE number 743695 (Why is no real title available?)
• DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
• Formalizing Hilbert's Grundlagen in Isabelle/Isar
• Formalizing projective plane geometry in Coq
• INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Machine Proofs in Geometry
• Mechanical Theorem Proving in Tarski’s Geometry
• Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang
• On the mechanization of the proof of Hessenberg's theorem in coherent logic
• Programming Languages and Systems
• Proof certificates for algebra and their application to automatic geometry theorem proving
• Theorem Proving in Higher Order Logics

Cited in

(18)

• An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
• Formalizing constructive projective geometry in Agda
• Some lemmas to hopefully enable search methods to find short and human readable proofs for incidence theorems of projective geometry
• Formalization of the Poincaré disc model of hyperbolic geometry
• Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
• A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
• A synthetic proof of Pappus' theorem in Tarski's geometry
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• The area method. A recapitulation
• Theorem Proving in Higher Order Logics
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
• Two cryptomorphic formalizations of projective incidence geometry
• Duality notions in real projective plane
• Towards an intelligent and dynamic geometry book
• Two new ways to formally prove Dandelin-Gallucci's theorem
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• Formalizing projective plane geometry in Coq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A case study in formalizing projective geometry in Coq: Desargues theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448975)