Formalizing projective plane geometry in Coq
From MaRDI portal
Publication:3003232
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
(19)- Formalizing constructive projective geometry in Agda
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
- 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
- Theorem Proving in Higher Order Logics
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Two cryptomorphic formalizations of projective incidence geometry
- scientific article; zbMATH DE number 5295702 (Why is no real title available?)
- Combinatorial analysis of proofs in projective and affine geometry
- Duality notions in real projective plane
- Formalization of the arithmetization of Euclidean plane geometry and applications
- Automated generation of geometric theorems from images of diagrams
- Formalizing complex plane geometry
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Homography in \(\mathbb{R}\mathbb{P}^2\)
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
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)
