Pages that link to "Item:Q448975"
From MaRDI portal
The following pages link to A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975):
Displaying 16 items.
- The area method. A recapitulation (Q437042) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- Towards an intelligent and dynamic geometry book (Q1701659) (← links)
- Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
- Duality notions in real projective plane (Q2171520) (← links)
- Formalizing constructive projective geometry in Agda (Q2333313) (← links)
- A synthetic proof of Pappus' theorem in Tarski's geometry (Q2362204) (← 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)
- Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry (Q3102739) (← links)
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time (Q3102743) (← links)
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs (Q3102745) (← links)
- Theorem Proving in Higher Order Logics (Q5464649) (← links)
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq (Q6108812) (← links)
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach (Q6653961) (← links)
- Two new ways to formally prove Dandelin-Gallucci's theorem (Q6666520) (← links)
