Projective geometric theorem proving with Grassmann-Cayley algebra

DOI10.1007/978-3-0346-0405-5_24MaRDI QIDQ2995120zbMATH OpenOpenAlexFDO

Authors Hongbo Li

Publication date 20 April 2011

Published in From Past to Future: Graßmann's Work in Context (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-0346-0405-5_24

zbMATH Keywords

determinantsautomated theorem provingDesargues' theoremGrassmann-Cayley algebraCayley factorizationouter productprojective incidence geometryCayley expansionbracket notationmeet productGrassmann-Plücker syzygies

Mathematics Subject Classification ID

Determinants, permanents, traces, other special matrix functions (15A15) Projective techniques in algebraic geometry (14N05) Exterior algebra, Grassmann algebras (15A75) Incidence structures embeddable into projective geometries (51A45)

Recommendations

• 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.
• Coordinate-free theorem proving in incidence geometry
• scientific article; zbMATH DE number 1182942
• Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. II: Conic geometry.

Cited in

(10)

• Coordinate-free theorem proving in incidence geometry
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• scientific article; zbMATH DE number 1263333 (Why is no real title available?)
• Notes on Plücker's relations in geometric algebra
• scientific article; zbMATH DE number 1182942 (Why is no real title available?)
• Arguesian identities in invariant theory
• Automated short proof generation for projective geometric theorems with Cayley and bracket algebras. I: Incidence geometry.
• Automated Deduction in Geometry
• Grassmann-Cayley algebra and robotics
• Formalizing constructive projective geometry in Agda

This page was built for publication: Projective geometric theorem proving with Grassmann-Cayley algebra

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2995120)