Two cryptomorphic formalizations of projective incidence geometry

DOI10.1007/S10472-018-9604-ZzbMATH Open1415.51007OpenAlexW2898203788WikidataQ129049182 ScholiaQ129049182MaRDI QIDQ2631964FDOQ2631964

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

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

zbMATH Keywords

ranksmatroidautomationCoqformalizationprojective incidence geometry

Mathematics Subject Classification ID

Combinatorial structures in finite projective spaces (51E20)

Cites Work

• The axioms of constructive geometry
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The area method. A recapitulation
• Mechanical Theorem Proving in Tarski’s Geometry
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formalizing Projective Plane Geometry in Coq
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• A case study in formalizing projective geometry in Coq: Desargues theorem
• Theorem Proving in Higher Order Logics
• Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
• INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
• Title not available (Why is that?)
• Mechanical theorem proving in projective geometry
• A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
• Title not available (Why is that?)
• Completing Segre's proof of Wedderburn's little theorem
• Formalization of Wu’s Simple Method in Coq
• First-Class Type Classes

Cited In (4)

• Formalizing Some “Small” Finite Models of Projective Geometry in Coq
• Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach
• Two new ways to formally prove Dandelin-Gallucci's theorem
• Title not available (Why is that?)

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)