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

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