Formalizing projective plane geometry in Coq
From MaRDI portal
Publication:3003232
DOI10.1007/978-3-642-21046-4_7zbMATH Open1302.68246OpenAlexW1572941424MaRDI QIDQ3003232FDOQ3003232
Pascal Schreck, Julien Narboux, Nicolas Magaud
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
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 (16)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- 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
- A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
- Automated generation of geometric theorems from images of diagrams
- Formalizing complex plane geometry
- Duality notions in real projective plane
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- Title not available (Why is that?)
- Formalizing constructive projective geometry in Agda
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- Homography in \(\mathbb{R}\mathbb{P}^2\)
- Title not available (Why is that?)
Uses Software
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)
