Pages that link to "Item:Q3003232"
From MaRDI portal
The following pages link to Formalizing Projective Plane Geometry in Coq (Q3003232):
Displaying 12 items.
- The area method. A recapitulation (Q437042) (← links)
- A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
- Homography in \(\mathbb{R}\mathbb{P}^2\) (Q520382) (← links)
- A nonexistence certificate for projective planes of order ten with weight 15 codewords (Q780361) (← links)
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL (Q2102946) (← links)
- Duality notions in real projective plane (Q2171520) (← links)
- Formalizing constructive projective geometry in Agda (Q2333313) (← links)
- Automated generation of geometric theorems from images of diagrams (Q2354910) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
- Two cryptomorphic formalizations of projective incidence geometry (Q2631964) (← links)
- A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry (Q3102734) (← links)
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs (Q3102745) (← links)
