Formalizing projective plane geometry in Coq

DOI10.1007/978-3-642-21046-4_7MaRDI QIDQ3003232zbMATH OpenOpenAlexFDO

Authors Nicolas Magaud, Julien Narboux, Pascal Schreck

Publication date 26 May 2011

Published in Automated Deduction in Geometry (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-21046-4_7

zbMATH Keywords

dualityprojective geometryCoqformalization

Mathematics Subject Classification ID

Projective analytic geometry (51N15)

Recommendations

• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Two cryptomorphic formalizations of projective incidence geometry
• Formalizing constructive projective geometry in Agda
• Formalization of the arithmetization of Euclidean plane geometry and applications

Cited in

(20)

• scientific article; zbMATH DE number 1745043 (Why is no real title available?)
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Combinatorial analysis of proofs in projective and affine geometry
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• The area method. A recapitulation
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Theorem Proving in Higher Order Logics
• Two cryptomorphic formalizations of projective incidence geometry
• Formalization of the arithmetization of Euclidean plane geometry and applications
• Automated generation of geometric theorems from images of diagrams
• Formalizing complex plane geometry
• Duality notions in real projective plane
• Formalization of gyrovector spaces as models of hyperbolic geometry and special relativity
• A nonexistence certificate for projective planes of order ten with weight 15 codewords
• scientific article; zbMATH DE number 5295702 (Why is no real title available?)
• Formalizing constructive projective geometry in Agda
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
• A coherent logic based geometry theorem prover capable of producing formal and readable proofs
• Homography in \(\mathbb{R}\mathbb{P}^2\)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formalizing projective plane geometry in Coq

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