Two cryptomorphic formalizations of projective incidence geometry

DOI10.1007/S10472-018-9604-ZMaRDI QIDQ2631964zbMATH OpenOpenAlexWikidataFDO

Authors Nicolas Magaud, Pascal Schreck, David J. Braun

Publication date 16 May 2019

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-018-9604-z

zbMATH Keywords

ranksmatroidautomationCoqformalizationprojective incidence geometry

Mathematics Subject Classification ID

Combinatorial structures in finite projective spaces (51E20)

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

• 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?)
• 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
• 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 Tarski’s Geometry
• Mechanical theorem proving in projective geometry
• The area method. A recapitulation
• The axioms of constructive geometry
• Theorem Proving in Higher Order Logics

Cited in

(10)

• 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
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Formalizing projective plane geometry in Coq
• 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

Describes a project that uses

Uses Software

• Coq

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)