Two cryptomorphic formalizations of projective incidence geometry

DOI10.1007/s10472-018-9604-zzbMath1415.51007OpenAlexW2898203788MaRDI QIDQ2631964

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)

Uses Software

• Coq

Cites Work

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

This page was built for publication: Two cryptomorphic formalizations of projective incidence geometry