A case study in formalizing projective geometry in Coq: Desargues theorem

DOI10.1016/j.comgeo.2010.06.004zbMath1248.68449OpenAlexW2054653818MaRDI QIDQ448975

Pascal Schreck, Julien Narboux, Nicolas Magaud

Publication date: 11 September 2012

Published in: Computational Geometry (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.comgeo.2010.06.004

zbMATH Keywords

rankprojective geometryCoqDesarguesHexamys

Mathematics Subject Classification ID

Desarguesian and Pappian geometries (51A30)

Related Items

A synthetic proof of Pappus' theorem in Tarski's geometry ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Duality notions in real projective plane ⋮ Formalizing Some “Small” Finite Models of Projective Geometry in Coq ⋮ Towards an intelligent and dynamic geometry book ⋮ The area method. A recapitulation ⋮ Formalization of the Poincaré disc model of hyperbolic geometry ⋮ A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry ⋮ Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ Formalizing constructive projective geometry in Agda

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• 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
• Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving
• Formalizing Projective Plane Geometry in Coq
• DECOMPOSITION OF GEOMETRIC CONSTRAINT SYSTEMS: A SURVEY
• INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
• Formalizing Hilbert’s Grundlagen in Isabelle/Isar
• Machine Proofs in Geometry
• Programming Languages and Systems
• Mechanical Theorem Proving in Tarski’s Geometry
• Theorem Proving in Higher Order Logics

This page was built for publication: A case study in formalizing projective geometry in Coq: Desargues theorem