A case study in formalizing projective geometry in Coq: Desargues theorem
From MaRDI portal
(Redirected from Publication:448975)
Recommendations
- Formalizing projective plane geometry in Coq
- Two cryptomorphic formalizations of projective incidence geometry
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
Cites work
- scientific article; zbMATH DE number 4024134 (Why is no real title available?)
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- scientific article; zbMATH DE number 743695 (Why is no real title available?)
- DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Formalizing projective plane geometry in Coq
- INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Machine Proofs in Geometry
- Mechanical Theorem Proving in Tarski’s Geometry
- Non-Desarguian geometries and the foundations of geometry from David Hilbert to Ruth Moufang
- On the mechanization of the proof of Hessenberg's theorem in coherent logic
- Programming Languages and Systems
- Proof certificates for algebra and their application to automatic geometry theorem proving
- Theorem Proving in Higher Order Logics
Cited in
(18)- A synthetic proof of Pappus' theorem in Tarski's geometry
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- Formalization of the Poincaré disc model of hyperbolic geometry
- The area method. A recapitulation
- Theorem Proving in Higher Order Logics
- Two cryptomorphic formalizations of projective incidence geometry
- Formalizing projective plane geometry in Coq
- An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time
- Duality notions in real projective plane
- Formalizing constructive projective geometry in Agda
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
- Two new ways to formally prove Dandelin-Gallucci's theorem
- Towards an intelligent and dynamic geometry book
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Some lemmas to hopefully enable search methods to find short and human readable proofs for incidence theorems of projective geometry
This page was built for publication: A case study in formalizing projective geometry in Coq: Desargues theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q448975)
