Skip to main content
SpringerLink
Log in

A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry

  • Conference paper
Automated Deduction in Geometry (ADG 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6877))

Included in the following conference series:

Abstract

This paper presents a formalization of Grassmann-Cayley algebra [6] that has been done in the COQ [2] proof assistant. The formalization is based on a data structure that represents elements of the algebra as complete binary trees. This allows to define the algebra products recursively. Using this formalization, published proofs of Pappus’ and Desargues’ theorem [7,1] are interactively derived. A method that automatically proves projective geometric theorems [11] is also translated successfully into the proposed formalization.

This work has been supported by the ANR Galapagos.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnabei, M., Brini, A., Rota, G.C.: On the Exterior Calculus of Invariant Theory. Journal of Algebra 96, 120–160 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development, Coq’Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  3. Coq development team: The Coq Proof Assistant Reference Manual, Version 8.2. LogiCal Project (2008), http://coq.inria.fr

  4. Crapo, H., Richter-Gebert, J.: Automatic proving of geometric theorems. In: White [16], pp. 167–196

    Google Scholar 

  5. Dorst, L., Fontijne, D., Mann, S.: Geometric Algebra for Computer Science: An Object Oriented Approach to Geometry. Morgan Kauffmann Publishers (2007)

    Google Scholar 

  6. Doubilet, P., Rota, G.C., Stein, J.: On the foundations of combinatorial theory. IX. Combinatorial methods in invariant theory. Studies in Applied Mathematics 53, 185–216 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  7. Hawrylycz, M.: A geometric identity for Pappus’ theorem. Proceedings of the National Academy of Sciences U.S.A. 91(8), 2909 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  8. Hestenes, D., Sobczyk, G.: Clifford Algebra to Geometric Calculus: A Unified Language for Mathematics and Physics. In: Fundamental Theories of Physics, vol. 5, Kluwer Academic Publishers (1984)

    Google Scholar 

  9. Janicic, P., Narboux, J., Quaresma, P.: The Area Method: a Recapitulation. Journal of Automated Reasoning (2010) (published online)

    Google Scholar 

  10. Li, H.: Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving. In: Winkler, F. (ed.) ADG 2002. LNCS (LNAI), vol. 2930, pp. 106–123. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Li, H., Wu, Y.: Automated short proof generation for projective geometric theorems with Cayley and bracket algebras: I. Incidence geometry. Journal of Symbolic Computation 36(5), 717–762 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  12. Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane Geometry in Coq. In: Sturm, T., Zengler, C. (eds.) ADG 2008. LNCS, vol. 6301, pp. 141–162. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Magaud, N., Narboux, J., Schreck, P.: Formalizing Desargues’ theorem in Coq using ranks. In: Proceedings of the ACM Symposium on Applied Computing SAC 2009, ACM, ACM Press (March 2009), http://lsiit.u-strasbg.fr/Publications/2009/MNS09

  14. Michelucci, D., Schreck, P.: Incidence constraints: A combinatorial approach. International Journal of Computational Geometry & Applications 16(5-6), 443–460 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. Sturmfels, B.: Algorithms in Invariant Theory. Springer, New York (1993)

    Book  MATH  Google Scholar 

  16. White, N.L. (ed.): Invariants Methods in Discrete and Computational Geometry. Kluwer, Dordrecht (1995)

    Google Scholar 

  17. White, N.L.: A tutorial on Grassmann-Cayley algebra. In: Invariants Methods in Discrete and Computational Geometry [16], pp. 93–106

    Google Scholar 

  18. White, N.L.: Geometric applications of the Grassmann-Cayley algebra. In: Handbook of Discrete and Computational Geometry, pp. 881–892. CRC Press, Inc., Boca Raton (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. XLIM-SIC UMR CNRS 6172 - Poitiers University, France

    Laurent Fuchs

  2. INRIA Sophia Antipolis - Méditerranée, France

    Laurent Théry

Authors
  1. Laurent Fuchs
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LSIIT, Pôle API, Boulevard Sébastien Brant, BP 10413, 67412, Illkirch Cédex, France

    Pascal Schreck  & Julien Narboux  & 

  2. Technische Universität München, Zentrum Mathematik (M10), Lehrstuhl für Geometrie und Visualisierung, Boltzmannstraße 3, 85748, Garching, Germany

    Jürgen Richter-Gebert

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fuchs, L., Théry, L. (2011). A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds) Automated Deduction in Geometry. ADG 2010. Lecture Notes in Computer Science(), vol 6877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25070-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-25070-5_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-25069-9

  • Online ISBN: 978-3-642-25070-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation