A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
From MaRDI portal
Publication:3102734
DOI10.1007/978-3-642-25070-5_3zbMath1350.68233OpenAlexW1523528291MaRDI QIDQ3102734
Publication date: 25 November 2011
Published in: Automated Deduction in Geometry (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-25070-5_3
General theory of linear incidence geometry and projective geometries (51A05) Desarguesian and Pappian geometries (51A30)
Related Items (8)
Pappus's hexagon theorem in real projective plane ⋮ Formalizing geometric algebra in Lean ⋮ Two cryptomorphic formalizations of projective incidence geometry ⋮ Formalization of the arithmetization of Euclidean plane geometry and applications ⋮ Towards an intelligent and dynamic geometry book ⋮ Homography in \(\mathbb{R}\mathbb{P}^2\) ⋮ Implementing geometric algebra products with binary trees ⋮ Formalization of Wu’s Simple Method in Coq
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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.
- Clifford algebra to geometric calculus. A unified language for mathematics and physics
- On the exterior calculus of invariant theory
- Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
- Formalizing Projective Plane Geometry in Coq
- INCIDENCE CONSTRAINTS: A COMBINATORIAL APPROACH
- On the Foundations of Combinatorial Theory: IX Combinatorial Methods in Invariant Theory
- A geometric identity for Pappus' theorem.
- Automated Deduction in Geometry
- Algorithms in invariant theory
This page was built for publication: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry
