zbMATH — the first resource for mathematics

Formalization of geometric algebra in HOL Light. (English) Zbl 07100463
Summary: Although the theories of geometric algebra (GA) are widely applied in engineering design and analysis, the studies on their formalization have been scarcely conducted. This paper proposes a relatively complete formalization of GA in HOL Light. Both algebraic and geometric parts of the GA theories are formalized successively. For the algebraic part, a uniform abstract product is proposed to facilitate the formalization of the three basic products based on the formal definition of multivectors with three types of metrics. For the geometric part, the formal formulation is provided for the blades and versors and their relations at first. Then, several commonly used specific spaces are formally represented in the theoretical framework of GA. The novelty of the present paper lies in two aspects: (a) the multivector type, (P,Q,R)geomalg, is defined and the definition provides the most important foundation for the formalization of geometric algebra, and (b) a procedure is developed for automatically proving the properties of GA operations. The present work improves the function of HOL Light and makes the GA-based formal analysis and verification more convenient.
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI
[1] Hestenes, D.: A Unified Language for Mathematics and Physics. Springer, Netherlands (1986) · Zbl 0596.15027
[2] Kleppe, AL; Egeland, O., Inverse kinematics for industrial robots using conformal geometric algebra, Model. Identif. Control, 37, 63-75, (2016)
[3] Stanway, MJ; Kinsey, JC, Rotation identification in geometric algebra: theory and application to the navigation of underwater robots in the field, J. Field Robot., 32, 632-654, (2015)
[4] Bernal-Marin, M.; Bayro-Corrochano, E., Integration of Hough transform of lines and planes in the framework of conformal geometric algebra for 2D and 3D robot vision, Pattern Recognit. Lett., 32, 2213-2223, (2011)
[5] Franchini, S.; Gentile, A.; Sorbello, F.; Vassallo, G.; Vitabile, S., An embedded, FPGA-based computer graphics coprocessor with native geometric algebra support, Integr. VlSI J., 42, 346-355, (2009) · Zbl 1372.68024
[6] Hestenes, D.; Sobczyk, G.; Marsh, JS, Clifford algebra to geometric calculus: a unified language formathematics and physics, Am. J. Phys., 53, 510-511, (1985)
[7] Dorst, L., Doran, C., Lasenby, J.: Applications of Geometric Algebra in Computer Science and Engineering. Birkhauser, Basel (2002) · Zbl 1013.00022
[8] Macdonald, A., A survey of geometric algebra and geometric calculus, Adv. Appl. Clifford Algebras, 27, 1-39, (2016) · Zbl 1046.15036
[9] Abłamowicz, R.; Fauser, B., Clifford and Graßmann Hopf algebras via the BIGEBRA package for Maple, Comput. Phys. Commun., 170, 115-130, (2002) · Zbl 1196.16042
[10] Aragoncamarasa, G., Aragongonzalez, G., Aragon, J.L., Rodriguezandrade, M.A.: Clifford algebra with mathematica. Physics (2008). Preprint. arXiv:0810.2412. October 2008
[11] Mann, S., Dorst, L., Bouma, T.: The Making of GABLE: A Geometric Algebra Learning Environment in Matlab. Birkhüser, Boston (2001)
[12] Gordon, MJC; Melham, TF, Introduction to HOL: a theorem proving environment for higher order logic, FEBS Lett., 89, 317-320, (1993) · Zbl 0779.68007
[13] Harrison, J.: HOL light: a tutorial introduction. In Srivas, M., Camilleri, A., eds.: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96). Volume 1166 of Lecture Notes in Computer Science., Springer, pp. 265-269 (1996)
[14] Paulson, L.C.: Isabelle—A Generic Theorem Prover. LNCS, Heidelberg (1994) · Zbl 0825.68059
[15] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer, Berlin (2004) · Zbl 1069.68095
[16] Dutertre, B., Elements of mathematical analysis in PVS, Lect. Notes Comput. Sci., 1125, 141-156, (1999)
[17] Kaufmann, M., Manolios, P., Moore, J.S., Kaufmann, M., Moore, J.S.: Acl2 Computer Aided Reasoning: An Approach (vol 1). World Scientific Publishing Company 81(957), 1-27 (2002)
[18] Rudnicki, P., An overview of the Mizar project, Univ. Technol. Bastad, 31, 311-332, (1994)
[19] Arthan, R.: Mathematical Case Studies: The Geometric Algebra (2006). http://citeseerx.ist.psu.edu/viewdoc/download?doi= May 2012
[20] Fuchs, L.; Théry, L., Implementing geometric algebra products with binary trees, Adv. Appl. Clifford Algebras, 24, 589-611, (2014) · Zbl 1311.68147
[21] Harrison, J., The HOL Light theory of Euclidean space, J. Autom. Reason., 50, 173-190, (2013) · Zbl 1260.68373
[22] Ma, S.; Shi, Z.; Shao, Z.; Guan, Y.; Li, L.; Li, Y., Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm, Adv. Appl. Clifford Algebras, 26, 1-26, (2016) · Zbl 1367.65032
[23] Harrison, J.: The HOL Light theorem prover. http://www.cl.cam.ac.uk/ jrh13/hol-light/. Accessed 6 Aug 2016
[24] Harrison, J.: HOL Light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009. Volume 5674 of Lecture Notes in Computer Science., Munich, Germany, Springer-Verlag 60-66 (2009) · Zbl 1252.68255
[25] Hales, T.; Adams, M.; Bauer, G.; Dang, DT; Harrison, J.; Hoang, TL; Kaliszyk, C.; Magron, V.; Mclaughlin, S.; Nguyen, TT, A formal proof of the Kepler conjecture, Mathematics, 16, 47-58, (2015) · Zbl 1379.52018
[26] Harrison, J.: Geometric algebra. https://github.com/jrh13/hol-light/blob/master/Multivariate/clifford.ml. Accessed 4 May 2016
[27] Rivera-Rovelo, J., Bayro-Corrochano, E.: Medical image segmentation using a self-organizing neural network and Clifford geometric algebra. In: International Joint Conference on Neural Networks, pp. 3538-3545 (2006)
[28] Hestenes, D., Li, H., Rockwood, A.: New algebraic tools for classical geometry. Geometric Computing with Clifford Algebras, pp. 3-26 (2001) · Zbl 1073.68847
[29] Hestenes, D., New foundations for classical mechanics, Math. Gaz., 71, 703-704, (2002) · Zbl 0932.70001
[30] Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005. Volume 3603 of Lecture Notes in Computer Science., Oxford, UK, Springer-Verlag, pp. 114-129 (2005) · Zbl 1152.68520
[31] Harrison, J.: Definition of finite Cartesian product types. https://github.com/jrh13/hol-light/blob/master/cart.ml. Accessed 16 May 2016
[32] Harrison, J.: Real vectors in Euclidean space, and elementary linear algebra. https://github.com/jrh13/hol-light/blob/master/Multivariate/vectors.ml. Accessed 11 June 2016
[33] Harrison, J.: Determinant and trace of a square matrix. https://github.com/jrh13/hol-light/blob/master/Multivariate/determinants.ml. Accessed 11 Jan 2016
[34] Dorst, L.: The Inner Products of Geometric Algebra. Birkhäuser, Boston (2002) · Zbl 1160.51305
[35] Hartley, D.; Tuckey, P., Gröbner bases in Clifford and Grassmann algebras, J. Symb. Comput., 20, 197-205, (1995) · Zbl 0852.15019
[36] Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Volume 10(23) of Studies in Logic, Grammar and Rhetoric, pp. 151-165. University of Białystok (2007)
[37] Gabrielli, A., Maggesi, M.: In: Formalizing Basic Quaternionic Analysis. Springer, Cham pp. 225-240 (2017) · Zbl 06821854
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.