Two cryptomorphic formalizations of projective incidence geometry
From MaRDI portal
Publication:2631964
The authors formalize two different projective geometry axiomatic systems in Coq, describing the first in classical terms and the second in terms of rank from matroid theory. They prove the equivalence of these two systems in two and three dimensions. The significance of this result is that it allows for further automation for the proofs of projective geometry theorems.
Recommendations
- Formalizing projective plane geometry in Coq
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A case study in formalizing projective geometry in Coq: Desargues theorem
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- Formalizing constructive projective geometry in Agda
Cites work
- A case study in formalizing projective geometry in Coq: Desargues theorem
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
- Completing Segre's proof of Wedderburn's little theorem
- First-Class Type Classes
- Formalization of Wu's simple method in Coq
- Formalizing Hilbert's Grundlagen in Isabelle/Isar
- Formalizing projective plane geometry in Coq
- scientific article; zbMATH DE number 3151263 (Why is no real title available?)
- scientific article; zbMATH DE number 1061188 (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?)
- scientific article; zbMATH DE number 5047784 (Why is no real title available?)
- 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.
- Mechanical theorem proving in projective geometry
- Mechanical Theorem Proving in Tarski’s Geometry
- The area method. A recapitulation
- The axioms of constructive geometry
- Theorem Proving in Higher Order Logics
Cited in
(12)- Formalizing projective plane geometry in Coq
- A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
- scientific article; zbMATH DE number 1322827 (Why is no real title available?)
- scientific article; zbMATH DE number 1088205 (Why is no real title available?)
- A case study in formalizing projective geometry in Coq: Desargues theorem
- scientific article; zbMATH DE number 1745043 (Why is no real title available?)
- Coordinate-free theorem proving in incidence geometry
- Formalization of formal topology by means of the interactive theorem prover Matita
- Formalizing Some “Small” Finite Models of Projective Geometry in Coq
- A Matroid-Based Automatic Prover and Coq Proof Generator for Projective Incidence Geometry
- Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
- Two new ways to formally prove Dandelin-Gallucci's theorem
This page was built for publication: Two cryptomorphic formalizations of projective incidence geometry
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631964)
