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
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
