Formalizing Projective Plane Geometry in Coq
From MaRDI portal
Publication:3003232
DOI10.1007/978-3-642-21046-4_7zbMath1302.68246OpenAlexW1572941424MaRDI QIDQ3003232
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
Related Items (13)
Two cryptomorphic formalizations of projective incidence geometry ⋮ Duality notions in real projective plane ⋮ Formalizing Some “Small” Finite Models of Projective Geometry in Coq ⋮ The area method. A recapitulation ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ Homography in \(\mathbb{R}\mathbb{P}^2\) ⋮ A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords ⋮ Formalizing constructive projective geometry in Agda ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL ⋮ Automated generation of geometric theorems from images of diagrams ⋮ Formalizing complex plane geometry
Uses Software
This page was built for publication: Formalizing Projective Plane Geometry in Coq
