Skip to main content
Top

2011 | OriginalPaper | Chapter

10. On Geometric Theorem Proving with Null Geometric Algebra

Authors : Hongbo Li, Yuanhao Cao

Published in: Guide to Geometric Algebra in Practice

Publisher: Springer London

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

The bottleneck in symbolic geometric computation is middle expression swell. Another embarrassing problem is geometric explanation of algebraic results, which is often impossible because the results are not invariant under coordinate transformations. In classical invariant-theoretical methods, the two difficulties are more or less alleviated but stay, while new difficulties arise.
In this chapter, we introduce a new framework for symbolic geometric computing based on conformal geometric algebra: the algebra for describing geometric configuration is null Grassmann–Cayley algebra, the algebra for advanced invariant manipulation is null bracket algebra, and the algebra underlying both algebras is null geometric algebra. When used in geometric computing, the new approach not only brings about amazing simplifications in algebraic manipulation, but can be used to extend and generalize existing theorems by removing some geometric constraints from the hypotheses.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
1
Editorial note: This characterization of CGA is more restrictive than elsewhere in this book, where (10.19) is employed.
 
Literature
1.
go back to reference Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994) MATHCrossRef Chou, S.-C., Gao, X.-S., Zhang, J.-Z.: Machine Proofs in Geometry. World Scientific, Singapore (1994) MATHCrossRef
2.
go back to reference Hestenes, D., Sobczyk, G.: Clifford Algebra to Geometric Calculus. Reidel, Dordrecht (1984) MATH Hestenes, D., Sobczyk, G.: Clifford Algebra to Geometric Calculus. Reidel, Dordrecht (1984) MATH
3.
go back to reference Li, H.: Automated theorem proving in the homogeneous model with Clifford bracket algebra. In: Dorst, L., et al. (eds.) Applications of Geometric Algebra in Computer Science and Engineering, pp. 69–78. Birkhäuser, Boston (2002) CrossRef Li, H.: Automated theorem proving in the homogeneous model with Clifford bracket algebra. In: Dorst, L., et al. (eds.) Applications of Geometric Algebra in Computer Science and Engineering, pp. 69–78. Birkhäuser, Boston (2002) CrossRef
4.
go back to reference Li, H.: Algebraic representation and elimination and expansion in automated geometric theorem proving. In: Winkler, F. (ed.) Automated Deduction in Geometry, pp. 106–123. Springer, Heidelberg (2004) CrossRef Li, H.: Algebraic representation and elimination and expansion in automated geometric theorem proving. In: Winkler, F. (ed.) Automated Deduction in Geometry, pp. 106–123. Springer, Heidelberg (2004) CrossRef
5.
go back to reference Li, H.: Automated geometric theorem proving, Clifford bracket algebra and Clifford expansions. In: Qian, T., et al. (eds.) Trends in Mathematics: Advances in Analysis and Geometry, pp. 345–363. Birkhäuser, Basel (2004) CrossRef Li, H.: Automated geometric theorem proving, Clifford bracket algebra and Clifford expansions. In: Qian, T., et al. (eds.) Trends in Mathematics: Advances in Analysis and Geometry, pp. 345–363. Birkhäuser, Basel (2004) CrossRef
6.
go back to reference Li, H.: Clifford algebras and geometric computation. In: Chen, F., Wang, D. (eds.) Geometric Computation, pp. 221–247. World Scientific, Singapore (2004) CrossRef Li, H.: Clifford algebras and geometric computation. In: Chen, F., Wang, D. (eds.) Geometric Computation, pp. 221–247. World Scientific, Singapore (2004) CrossRef
7.
go back to reference Li, H.: Symbolic computation in the homogeneous geometric model with Clifford algebra. In: Gutierrez, J. (ed.) Proceedings of International Symposium on Symbolic and Algebraic Computation 2004, pp. 221–228. ACM Press, New York (2004) CrossRef Li, H.: Symbolic computation in the homogeneous geometric model with Clifford algebra. In: Gutierrez, J. (ed.) Proceedings of International Symposium on Symbolic and Algebraic Computation 2004, pp. 221–228. ACM Press, New York (2004) CrossRef
8.
go back to reference Li, H.: A recipe for symbolic geometric computing: long geometric product, BREEFS and Clifford factorization. In: Brown, C.W. (ed.) Proc. ISSAC 2007, pp. 261–268. ACM Press, New York (2007) CrossRef Li, H.: A recipe for symbolic geometric computing: long geometric product, BREEFS and Clifford factorization. In: Brown, C.W. (ed.) Proc. ISSAC 2007, pp. 261–268. ACM Press, New York (2007) CrossRef
9.
10.
go back to reference Li, H., Huang, L.: Complex brackets balanced complex differences, and applications in symbolic geometric computing. In: Proc. ISSAC 2008, pp. 181–188. ACM Press, New York (2008) CrossRef Li, H., Huang, L.: Complex brackets balanced complex differences, and applications in symbolic geometric computing. In: Proc. ISSAC 2008, pp. 181–188. ACM Press, New York (2008) CrossRef
11.
go back to reference Li, H., Wu, Y.: Automated short proof generation in projective geometry with Cayley and Bracket algebras I. Incidence geometry. J. Symb. Comput. 36(5), 717–762 (2003) MATHCrossRef Li, H., Wu, Y.: Automated short proof generation in projective geometry with Cayley and Bracket algebras I. Incidence geometry. J. Symb. Comput. 36(5), 717–762 (2003) MATHCrossRef
12.
go back to reference Li, H., Wu, Y.: Automated short proof generation in projective geometry with Cayley and Bracket algebras II. Conic geometry. J. Symb. Comput. 36(5), 763–809 (2003) MATHCrossRef Li, H., Wu, Y.: Automated short proof generation in projective geometry with Cayley and Bracket algebras II. Conic geometry. J. Symb. Comput. 36(5), 763–809 (2003) MATHCrossRef
13.
go back to reference Li, H., Hestenes, D., Rockwood, A.: Generalized homogeneous coordinates for computational geometry. In: Sommer, G. (ed.) Geometric Computing with Clifford Algebras, pp. 27–60. Springer, Heidelberg (2001) Li, H., Hestenes, D., Rockwood, A.: Generalized homogeneous coordinates for computational geometry. In: Sommer, G. (ed.) Geometric Computing with Clifford Algebras, pp. 27–60. Springer, Heidelberg (2001)
14.
go back to reference Muir, T.: A Treatise on the Theory of Determinants. Macmillan & Co., London (1882) Muir, T.: A Treatise on the Theory of Determinants. Macmillan & Co., London (1882)
15.
go back to reference Sommer, G. (ed.): Geometric Computing with Clifford Algebras. Springer, Heidelberg (2001) MATH Sommer, G. (ed.): Geometric Computing with Clifford Algebras. Springer, Heidelberg (2001) MATH
16.
go back to reference Sturmfels, B.: Algorithms in Invariant Theory. Springer, Wien (1993) MATH Sturmfels, B.: Algorithms in Invariant Theory. Springer, Wien (1993) MATH
17.
go back to reference Sturmfels, B., White, N. (eds.): Invariant-Theoretic Algorithms in Geometry. Special Issue. J. Symb. Comput. 11 (5/6) (2002) Sturmfels, B., White, N. (eds.): Invariant-Theoretic Algorithms in Geometry. Special Issue. J. Symb. Comput. 11 (5/6) (2002)
18.
go back to reference White, N. (ed.): Invariant Methods in Discrete and Computational Geometry. Kluwer, Dordrecht (1994) White, N. (ed.): Invariant Methods in Discrete and Computational Geometry. Kluwer, Dordrecht (1994)
19.
go back to reference Wu, W.-T.: Mathematics Mechanization. Kluwer and Science Press, Beijing (2000) MATH Wu, W.-T.: Mathematics Mechanization. Kluwer and Science Press, Beijing (2000) MATH
Metadata
Title
On Geometric Theorem Proving with Null Geometric Algebra
Authors
Hongbo Li
Yuanhao Cao
Copyright Year
2011
Publisher
Springer London
DOI
https://doi.org/10.1007/978-0-85729-811-9_10

Premium Partner